added RISC-V strong-acquire/release

1 files changed, 17 insertions, 2 deletions

diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem
index dabd4d12..1f2a0e47 100644
--- a/risc-v/riscv_extras_embed_sequential.lem
+++ b/risc-v/riscv_extras_embed_sequential.lem
@@ -6,33 +6,48 @@ open import State
 
 val MEMr                  : (vector bitU * integer) -> M (vector bitU)
 val MEMr_acquire          : (vector bitU * integer) -> M (vector bitU)
+val MEMr_strong_acquire   : (vector bitU * integer) -> M (vector bitU)
 val MEMr_reserved         : (vector bitU * integer) -> M (vector bitU)
 val MEMr_reserved_acquire : (vector bitU * integer) -> M (vector bitU)
+val MEMr_reserved_strong_acquire : (vector bitU * integer) -> M (vector bitU)
 
 let MEMr (addr,size)                  = read_mem false Read_plain addr size
 let MEMr_acquire (addr,size)          = read_mem false Read_RISCV_acquire addr size
+let MEMr_strong_acquire (addr,size)   = read_mem false Read_RISCV_strong_acquire addr size
 let MEMr_reserved (addr,size)         = read_mem false Read_RISCV_reserved addr size
 let MEMr_reserved_acquire (addr,size) = read_mem false Read_RISCV_reserved_acquire addr size
+let MEMr_reserved_strong_acquire (addr,size)
+                                      = read_mem false Read_RISCV_reserved_strong_acquire addr size
 
 val MEMea                     : (vector bitU * integer) -> M unit
 val MEMea_release             : (vector bitU * integer) -> M unit
+val MEMea_strong_release             : (vector bitU * integer) -> M unit
 val MEMea_conditional         : (vector bitU * integer) -> M unit
 val MEMea_conditional_release : (vector bitU * integer) -> M unit
+val MEMea_conditional_strong_release : (vector bitU * integer) -> M unit
 
 let MEMea (addr,size)                     = write_mem_ea Write_plain addr size
 let MEMea_release (addr,size)             = write_mem_ea Write_RISCV_release addr size
+let MEMea_strong_release (addr,size)      = write_mem_ea Write_RISCV_strong_release addr size
 let MEMea_conditional (addr,size)         = write_mem_ea Write_RISCV_conditional addr size
 let MEMea_conditional_release (addr,size) = write_mem_ea Write_RISCV_conditional_release addr size
+let MEMea_conditional_strong_release (addr,size)
+                                          = write_mem_ea Write_RISCV_conditional_strong_release addr size
 
 val MEMval                     : (vector bitU * integer * vector bitU) -> M unit
 val MEMval_release             : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_strong_release      : (vector bitU * integer * vector bitU) -> M unit
 val MEMval_conditional         : (vector bitU * integer * vector bitU) -> M unit
 val MEMval_conditional_release : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_conditional_strong_release : (vector bitU * integer * vector bitU) -> M unit
 
 let MEMval (_,_,v)                     = write_mem_val v >>= fun _ -> return ()
 let MEMval_release (_,_,v)             = write_mem_val v >>= fun _ -> return ()
-let MEMval_conditional (_,_,v)         = write_mem_val v >>= fun _ -> return () (* (if b then B1 else B0) *)
-let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun _ -> return () (* (if b then B1 else B0) *)
+let MEMval_strong_release (_,_,v)      = write_mem_val v >>= fun _ -> return ()
+let MEMval_conditional (_,_,v)         = write_mem_val v >>= fun _ -> return ()
+let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun _ -> return ()
+let MEMval_conditional_strong_release (_,_,v)
+                                       = write_mem_val v >>= fun _ -> return ()
 
 let speculate_conditional_success () = excl_result () >>= fun b -> return (if b then B1 else B0)