RISC-V store-release

19 files changed, 147 insertions, 66 deletions

diff --git a/etc/regfp.sail b/etc/regfp.sail
index c98e3fa4..71f53547 100644
--- a/etc/regfp.sail
+++ b/etc/regfp.sail
@@ -50,6 +50,9 @@ typedef write_kind = enumerate {
   Write_release;
   Write_exclusive;
   Write_exclusive_release;
+  Write_RISCV_release;
+  Write_RISCV_conditional;
+  Write_RISCV_conditional_release;
 }
 
 typedef barrier_kind = enumerate {
diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen
index 6e323e85..d5e4b45b 100644
--- a/risc-v/hgen/ast.hgen
+++ b/risc-v/hgen/ast.hgen
@@ -6,7 +6,7 @@
 | `RISCVShiftIop of bit6 * reg * reg * riscvSop
 | `RISCVRType of reg * reg * reg * riscvRop
 | `RISCVLoad of bit12 * reg * reg * bool * wordWidth * bool
-| `RISCVStore of bit12 * reg * reg * wordWidth
+| `RISCVStore of bit12 * reg * reg * wordWidth * bool
 | `RISCVADDIW of bit12 * reg * reg
 | `RISCVSHIFTW of bit5 * reg * reg * riscvSop
 | `RISCVRTYPEW of reg * reg * reg * riscvRopw
diff --git a/risc-v/hgen/fold.hgen b/risc-v/hgen/fold.hgen
index be91659b..376ab19f 100644
--- a/risc-v/hgen/fold.hgen
+++ b/risc-v/hgen/fold.hgen
@@ -7,7 +7,7 @@
 | `RISCVShiftIop (_, r0, r1, _)   -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
 | `RISCVRType (r0, r1, r2, _)     -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg)))
 | `RISCVLoad (_, r0, r1, _, _, _) -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
-| `RISCVStore (_, r0, r1, _)      -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVStore (_, r0, r1, _, _)   -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
 | `RISCVADDIW (_, r0, r1)         -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
 | `RISCVSHIFTW (_, r0, r1, _)     -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
 | `RISCVRTYPEW (r0, r1, r2, _)    -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg)))
diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
index 0e8bfdc2..d756d3d0 100644
--- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
+++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -37,11 +37,12 @@
       translate_bool "unsigned" unsigned,
       translate_wordWidth width,
       translate_bool "aq" aq)
-| `RISCVStore(imm, rs, rd, width) -> STORE (
+| `RISCVStore(imm, rs, rd, width, rl) -> STORE (
       translate_imm12 "imm" imm,
       translate_reg "rs" rs,
       translate_reg "rd" rd,
-      translate_wordWidth width)
+      translate_wordWidth width,
+      translate_bool "rl" rl)
 | `RISCVADDIW(imm, rs, rd) -> ADDIW(
       translate_imm12 "imm" imm,
       translate_reg "rs" rs,
diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen
index c4408139..40481f75 100644
--- a/risc-v/hgen/lexer.hgen
+++ b/risc-v/hgen/lexer.hgen
@@ -49,10 +49,15 @@
 "lwu.aq", LOAD{unsigned=true;  width=RISCVWORD;   aq=true};
 "ld.aq",  LOAD{unsigned=false; width=RISCVDOUBLE; aq=true};
 
-"sb", STORE{width=RISCVBYTE};
-"sh", STORE{width=RISCVHALF};
-"sw", STORE{width=RISCVWORD};
-"sd", STORE{width=RISCVDOUBLE};
+"sb", STORE{width=RISCVBYTE;   rl=false};
+"sh", STORE{width=RISCVHALF;   rl=false};
+"sw", STORE{width=RISCVWORD;   rl=false};
+"sd", STORE{width=RISCVDOUBLE; rl=false};
+
+"sb.rl", STORE{width=RISCVBYTE;   rl=true};
+"sh.rl", STORE{width=RISCVHALF;   rl=true};
+"sw.rl", STORE{width=RISCVWORD;   rl=true};
+"sd.rl", STORE{width=RISCVDOUBLE; rl=true};
 
 "addiw", ADDIW ();
 
diff --git a/risc-v/hgen/map.hgen b/risc-v/hgen/map.hgen
index 1deacc06..edd376b4 100644
--- a/risc-v/hgen/map.hgen
+++ b/risc-v/hgen/map.hgen
@@ -6,7 +6,7 @@
 | `RISCVShiftIop (x, r0, r1, y)   -> `RISCVShiftIop (x, map_reg r0, map_reg r1, y)
 | `RISCVRType (r0, r1, r2, y)     -> `RISCVRType (r0, map_reg r1, map_reg r2, y)
 | `RISCVLoad (x, r0, r1, y, z, a) -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z, a)
-| `RISCVStore (x, r0, r1, y)      -> `RISCVStore (x, map_reg r0, map_reg r1, y)
+| `RISCVStore (x, r0, r1, y, z)   -> `RISCVStore (x, map_reg r0, map_reg r1, y, z)
 | `RISCVADDIW (x, r0, r1)         -> `RISCVADDIW (x, map_reg r0, map_reg r1)
 | `RISCVSHIFTW (x, r0, r1, y)     -> `RISCVSHIFTW (x, map_reg r0, map_reg r1, y)
 | `RISCVRTYPEW (r0, r1, r2, x)    -> `RISCVRTYPEW (r0, map_reg r1, map_reg r2, x)
diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen
index 10257ecd..cb31f5a9 100644
--- a/risc-v/hgen/parser.hgen
+++ b/risc-v/hgen/parser.hgen
@@ -15,7 +15,7 @@
 | LOAD reg COMMA NUM LPAR reg RPAR
   { `RISCVLoad($4, $6, $2, $1.unsigned, $1.width, $1.aq) }
 | STORE reg COMMA NUM LPAR reg RPAR
-  { `RISCVStore($4, $2, $6, $1.width) }
+  { `RISCVStore($4, $2, $6, $1.width, $1.rl) }
 | ADDIW reg COMMA reg COMMA NUM
   { `RISCVADDIW ($6, $4, $2) }
 | SHIFTW reg COMMA reg COMMA NUM
diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen
index 6c4f3e53..cce77641 100644
--- a/risc-v/hgen/pretty.hgen
+++ b/risc-v/hgen/pretty.hgen
@@ -9,7 +9,8 @@
 | `RISCVRType (rs2, rs1, rd, op)  -> sprintf "%s %s, %s, %s" (pp_riscv_rop op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2)
 | `RISCVLoad(imm, rs, rd, unsigned, width, aq)
                                   -> sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width, aq)) (pp_reg rd) imm (pp_reg rs)
-| `RISCVStore(imm, rs2, rs1, width) -> sprintf "%s %s, %d(%s)" (pp_riscv_store_op width) (pp_reg rs2) imm (pp_reg rs1)
+| `RISCVStore(imm, rs2, rs1, width, rl)
+                                  -> sprintf "%s %s, %d(%s)" (pp_riscv_store_op (width, rl)) (pp_reg rs2) imm (pp_reg rs1)
 | `RISCVADDIW(imm, rs, rd)        -> sprintf "addiw %s, %s, %d" (pp_reg rd) (pp_reg rs) imm
 | `RISCVSHIFTW(imm, rs, rd, op)   -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm
 | `RISCVRTYPEW(rs2, rs1, rd, op)  -> sprintf "%s %s, %s, %s" (pp_riscv_ropw op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2)
diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen
index 2a161bda..45445a25 100644
--- a/risc-v/hgen/sail_trans_out.hgen
+++ b/risc-v/hgen/sail_trans_out.hgen
@@ -8,7 +8,8 @@
 | ("RTYPE", [rs2; rs1; rd; op])   -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op)
 | ("LOAD", [imm; rs; rd; unsigned; width; aq])
                                   -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq)
-| ("STORE", [imm; rs; rd; width]) -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width)
+| ("STORE", [imm; rs; rd; width; rl])
+                                  -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool rl)
 | ("ADDIW", [imm; rs; rd])        -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
 | ("SHIFTW", [imm; rs; rd; op])   -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
 | ("RTYPEW", [rs2; rs1; rd; op])  -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op)
diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
index c24ecd8f..abfc0412 100644
--- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
+++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -8,7 +8,8 @@
 | RTYPE( rs2, rs1, rd, op)    -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op)
 | LOAD( imm, rs, rd, unsigned, width, aq)
                               -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq)
-| STORE( imm, rs, rd, width)  -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width)
+| STORE( imm, rs, rd, width, rl)
+                              -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool rl)
 | ADDIW( imm, rs, rd)         -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
 | SHIFTW( imm, rs, rd, op)    -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
 | RTYPEW( rs2, rs1, rd, op)   -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op)
diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen
index ca19c6eb..03dde52b 100644
--- a/risc-v/hgen/token_types.hgen
+++ b/risc-v/hgen/token_types.hgen
@@ -6,7 +6,7 @@ type token_IType    = {op : riscvIop }
 type token_ShiftIop = {op : riscvSop }
 type token_RTYPE    = {op : riscvRop }
 type token_Load     = {unsigned: bool; width : wordWidth; aq: bool }
-type token_Store    = {width : wordWidth }
+type token_Store    = {width : wordWidth; rl: bool }
 type token_ADDIW    = unit
 type token_SHIFTW   = {op : riscvSop }
 type token_RTYPEW   = {op : riscvRopw }
diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen
index 7fdfd516..9fb3b546 100644
--- a/risc-v/hgen/trans_sail.hgen
+++ b/risc-v/hgen/trans_sail.hgen
@@ -69,13 +69,14 @@
       translate_bool "aq" aq;
     ],
     [])
-| `RISCVStore(imm, rs2, rs1, width) -> 
+| `RISCVStore(imm, rs2, rs1, width, rl) ->
    ("STORE",
     [
       translate_imm12 "imm" imm;
       translate_reg "rs2" rs2;
       translate_reg "rs1" rs1;
       translate_width "width" width;
+      translate_bool "rl" rl;
     ],
     [])
 | `RISCVADDIW(imm, rs, rd)        -> 
diff --git a/risc-v/hgen/types.hgen b/risc-v/hgen/types.hgen
index 11d0921e..180e0b37 100644
--- a/risc-v/hgen/types.hgen
+++ b/risc-v/hgen/types.hgen
@@ -111,11 +111,14 @@ let pp_riscv_load_op (unsigned, width, aq) =
   end
   ^ (if aq then ".aq" else "")
 
-let pp_riscv_store_op width = match width with
-| RISCVBYTE -> "sb"
-| RISCVHALF -> "sh"
-| RISCVWORD -> "sw"
-| RISCVDOUBLE -> "sd"
+let pp_riscv_store_op (width, rl) =
+  begin match width with
+  | RISCVBYTE -> "sb"
+  | RISCVHALF -> "sh"
+  | RISCVWORD -> "sw"
+  | RISCVDOUBLE -> "sd"
+  end
+  ^ (if rl then ".rl" else "")
 
 let pp_riscv_fence_option = function
   | 0b0011 -> "rw"
diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail
index c9ba5256..3b42b94c 100644
--- a/risc-v/riscv.sail
+++ b/risc-v/riscv.sail
@@ -70,7 +70,37 @@ function forall Nat 'n. (bit[8 * 'n]) effect { rmem } mem_read( (bit[64]) addr,
   }
 
 val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_release
+function forall Nat 'n. unit effect { eamem } mem_write_ea( (bit[64]) addr , ([|'n|]) width, (bool) rl) =
+  switch rl {
+    case false -> MEMea(addr, width)
+    case true  -> MEMea_release(addr, width)
+  }
+
 val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_release
+function forall Nat 'n. unit effect { wmv } mem_write_value( (bit[64]) addr , ([|'n|]) width , (bit[8*'n]) value, (bool) rl) =
+  switch rl {
+    case false -> MEMval(addr, width, value)
+    case true  -> MEMval_release(addr, width, value)
+  }
+
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional_release
+function forall Nat 'n. unit effect { eamem } mem_write_conditional_ea( (bit[64]) addr , ([|'n|]) width, (bool) rl) =
+  switch rl {
+    case false -> MEMea_conditional(addr, width)
+    case true  -> MEMea_conditional_release(addr, width)
+  }
+
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> bool effect { wmv } MEMval_conditional
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> bool effect { wmv } MEMval_conditional_release
+function forall Nat 'n. bool effect { wmv } mem_write_conditional_value( (bit[64]) addr , ([|'n|]) width , (bit[8*'n]) value, (bool) rl) =
+  switch rl {
+    case false -> MEMval_conditional(addr, width, value)
+    case true  -> MEMval_conditional_release(addr, width, value)
+  }
+
 val extern unit -> unit effect { barr } MEM_fence_rw_rw
 val extern unit -> unit effect { barr } MEM_fence_r_rw
 val extern unit -> unit effect { barr } MEM_fence_rw_w
@@ -239,25 +269,25 @@ function clause execute(LOAD(imm, rs1, rd, unsigned, width, aq)) =
         } in
     wGPR(rd, result)
 
-union ast member ((bit[12]), regno, regno, word_width) STORE
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, BYTE))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, HALF))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, WORD))
-function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, DOUBLE))
-function clause execute (STORE(imm, rs2, rs1, width)) =
+union ast member ((bit[12]), regno, regno, word_width, bool) STORE
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b000 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, BYTE, false))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, HALF, false))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, WORD, false))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, DOUBLE, false))
+function clause execute (STORE(imm, rs2, rs1, width, rl)) =
     let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in {
       switch (width) {
-        case BYTE   -> MEMea(addr, 1)
-        case HALF   -> MEMea(addr, 2)
-        case WORD   -> MEMea(addr, 4)
-        case DOUBLE -> MEMea(addr, 8)
+        case BYTE   -> mem_write_ea(addr, 1, rl)
+        case HALF   -> mem_write_ea(addr, 2, rl)
+        case WORD   -> mem_write_ea(addr, 4, rl)
+        case DOUBLE -> mem_write_ea(addr, 8, rl)
       };
       let rs2_val = rGPR(rs2) in
       switch (width) {
-        case BYTE   -> MEMval(addr, 1, rs2_val[7..0])
-        case HALF   -> MEMval(addr, 2, rs2_val[15..0])
-        case WORD   -> MEMval(addr, 4, rs2_val[31..0])
-        case DOUBLE -> MEMval(addr, 8, rs2_val)
+        case BYTE   -> mem_write_value(addr, 1, rs2_val[7..0], rl)
+        case HALF   -> mem_write_value(addr, 2, rs2_val[15..0], rl)
+        case WORD   -> mem_write_value(addr, 4, rs2_val[31..0], rl)
+        case DOUBLE -> mem_write_value(addr, 8, rs2_val, rl)
       }
     }
 
diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem
index 80f8bcc9..3803839d 100644
--- a/risc-v/riscv_extras.lem
+++ b/risc-v/riscv_extras.lem
@@ -42,15 +42,25 @@ let memory_writes : memory_writes =
   []
 
 let memory_eas : memory_write_eas =
-  [ ("MEMea",                 (MEA Write_plain           memory_parameter_transformer));
-    ("MEMea_conditional",     (MEA Write_conditional     memory_parameter_transformer));
+  [ ("MEMea",                     (MEA Write_plain                     memory_parameter_transformer));
+    ("MEMea_release",             (MEA Write_RISCV_release             memory_parameter_transformer));
+    ("MEMea_conditional",         (MEA Write_RISCV_conditional         memory_parameter_transformer));
+    ("MEMea_conditional_release", (MEA Write_RISCV_conditional_release memory_parameter_transformer));
   ]
 
 let memory_vals : memory_write_vals =
-  [ ("MEMval",      (MV memory_parameter_transformer_option_address Nothing));
-    ("MEMval_conditional", (MV memory_parameter_transformer_option_address
-                           (Just 
-                           (fun (IState interp context) b -> 
+  [ ("MEMval",          (MV memory_parameter_transformer_option_address Nothing));
+    ("MEMval_release",  (MV memory_parameter_transformer_option_address Nothing));
+    ("MEMval_conditional",
+                        (MV memory_parameter_transformer_option_address
+                            (Just
+                            (fun (IState interp context) b ->
+                              let bit = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in
+                            (IState (Interp.add_answer_to_stack interp bit) context)))));
+    ("MEMval_conditional_release",
+                        (MV memory_parameter_transformer_option_address
+                           (Just
+                           (fun (IState interp context) b ->
                              let bit = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in
                              (IState (Interp.add_answer_to_stack interp bit) context)))));
   ]
diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem
index 440ad378..35d217ff 100644
--- a/risc-v/riscv_extras_embed.lem
+++ b/risc-v/riscv_extras_embed.lem
@@ -14,18 +14,25 @@ let MEMr_acquire (addr,size)          = read_mem false Read_RISCV_acquire addr s
 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
 
-
-val MEMea                 : (vector bitU * integer) -> M unit
-val MEMea_conditional     : (vector bitU * integer) -> M unit
-
-let MEMea (addr,size)                 = write_mem_ea Write_plain addr size
-let MEMea_conditional (addr,size)     = write_mem_ea Write_conditional addr size
-
-val MEMval                 : (vector bitU * integer * vector bitU) -> M unit
-val MEMval_conditional     : (vector bitU * integer * vector bitU) -> M bitU
-
-let MEMval (_,_,v)                 = write_mem_val v >>= fun _ -> return ()
-let MEMval_conditional (_,_,v)     = write_mem_val v >>= fun b -> return (if b then B1 else B0)
+val MEMea                     : (vector bitU * integer) -> M unit
+val MEMea_release             : (vector bitU * integer) -> M unit
+val MEMea_conditional         : (vector bitU * integer) -> M unit
+val MEMea_conditional_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_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
+
+val MEMval                     : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_release             : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_conditional         : (vector bitU * integer * vector bitU) -> M bitU
+val MEMval_conditional_release : (vector bitU * integer * vector bitU) -> M bitU
+
+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 b -> return (if b then B1 else B0)
+let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0)
 
 val MEM_fence_rw_rw : unit -> M unit
 val MEM_fence_r_rw  : unit -> M unit
diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem
index 518a5a15..93b5dfec 100644
--- a/risc-v/riscv_extras_embed_sequential.lem
+++ b/risc-v/riscv_extras_embed_sequential.lem
@@ -14,18 +14,25 @@ let MEMr_acquire (addr,size)          = read_mem false Read_RISCV_acquire addr s
 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
 
-val MEMea                 : (vector bitU * integer) -> M unit
-val MEMea_conditional     : (vector bitU * integer) -> M unit
-
-let MEMea (addr,size)                 = write_mem_ea Write_plain addr size
-let MEMea_conditional (addr,size)     = write_mem_ea Write_conditional addr size
-
-
-val MEMval                 : (vector bitU * integer * vector bitU) -> M unit
-val MEMval_conditional     : (vector bitU * integer * vector bitU) -> M bitU
-
-let MEMval (_,_,v)                   = write_mem_val v >>= fun _ -> return ()
-let MEMval_conditional (_,_,v)       = write_mem_val v >>= fun b -> return (if b then B1 else B0)
+val MEMea                     : (vector bitU * integer) -> M unit
+val MEMea_release             : (vector bitU * integer) -> M unit
+val MEMea_conditional         : (vector bitU * integer) -> M unit
+val MEMea_conditional_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_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
+
+val MEMval                     : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_release             : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_conditional         : (vector bitU * integer * vector bitU) -> M bitU
+val MEMval_conditional_release : (vector bitU * integer * vector bitU) -> M bitU
+
+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 b -> return (if b then B1 else B0)
+let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0)
 
 val MEM_fence_rw_rw : unit -> M unit
 val MEM_fence_r_rw  : unit -> M unit
diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail
index fe0efa43..2c94012e 100644
--- a/risc-v/riscv_regfp.sail
+++ b/risc-v/riscv_regfp.sail
@@ -57,11 +57,11 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
             aR := iR;
             ik := if aq then IK_mem_read (Read_RISCV_acquire) else IK_mem_read (Read_plain);
      }
-     case (STORE( imm, rs2, rs1, width)) -> {
+     case (STORE( imm, rs2, rs1, width, rl)) -> {
             if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR;
             if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR;
             if (rs1 == 0) then () else aR := RFull(GPRstr[rs1]) :: aR;
-            ik := IK_mem_write (Write_plain);
+            ik := if rl then IK_mem_write (Write_RISCV_release) else IK_mem_write (Write_plain);
      }
      case (ADDIW ( imm, rs, rd)) -> {
             if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR;
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 1642bc81..caec3838 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -437,6 +437,9 @@ instance (Show read_kind)
     | Read_exclusive -> "Read_exclusive"
     | Read_exclusive_acquire -> "Read_exclusive_acquire"
     | Read_stream -> "Read_stream"
+    | Read_RISCV_acquire -> "Read_RISCV_acquire"
+    | Read_RISCV_reserved -> "Read_RISCV_reserved"
+    | Read_RISCV_reserved_acquire -> "Read_RISCV_reserved_acquire"
   end
 end
 
@@ -447,6 +450,8 @@ type write_kind =
   | Write_conditional
   (* AArch64 writes *)
   | Write_release | Write_exclusive | Write_exclusive_release
+  (* RISC-V *)
+  | Write_RISCV_release | Write_RISCV_conditional | Write_RISCV_conditional_release
 
 instance (Show write_kind)
   let show = function
@@ -455,6 +460,9 @@ instance (Show write_kind)
     | Write_release -> "Write_release"
     | Write_exclusive -> "Write_exclusive"
     | Write_exclusive_release -> "Write_exclusive_release"
+    | Write_RISCV_release -> "Write_RISCV_release"
+    | Write_RISCV_conditional -> "Write_RISCV_conditional"
+    | Write_RISCV_conditional_release -> "Write_RISCV_conditional_release"
   end
 end
 
@@ -488,6 +496,9 @@ instance (Show barrier_kind)
     | Barrier_ISB -> "Barrier_ISB"
     | Barrier_TM_COMMIT -> "Barrier_TM_COMMIT"
     | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC"
+    | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw"
+    | Barrier_RISCV_r_rw  -> "Barrier_RISCV_r_rw"
+    | Barrier_RISCV_rw_w  -> "Barrier_RISCV_rw_w"
   end
 end