added RISC-V strong-acquire/release

18 files changed, 301 insertions, 208 deletions

diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen
index 1839557f..b1968173 100644
--- a/risc-v/hgen/ast.hgen
+++ b/risc-v/hgen/ast.hgen
@@ -5,8 +5,8 @@
 | `RISCVIType of bit12 * reg * reg * riscvIop
 | `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 * bool
+| `RISCVLoad of bit12 * reg * reg * bool * wordWidth * bool * bool
+| `RISCVStore of bit12 * reg * reg * wordWidth * bool * 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 d8806a37..4c51e114 100644
--- a/risc-v/hgen/fold.hgen
+++ b/risc-v/hgen/fold.hgen
@@ -1,16 +1,16 @@
-| `RISCVThreadStart               -> (y_reg, y_sreg)
-| `RISCVUTYPE (_, r0, _)          -> fold_reg r0 (y_reg, y_sreg)
-| `RISCVJAL (_, r0)               -> fold_reg r0 (y_reg, y_sreg)
-| `RISCVJALR (_, r0, r1)          -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
-| `RISCVBType (_, r0, r1, _)      -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
-| `RISCVIType (_, r0, r1, _)      -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
-| `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))
-| `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)))
+| `RISCVThreadStart                      -> (y_reg, y_sreg)
+| `RISCVUTYPE (_, r0, _)                 -> fold_reg r0 (y_reg, y_sreg)
+| `RISCVJAL (_, r0)                      -> fold_reg r0 (y_reg, y_sreg)
+| `RISCVJALR (_, r0, r1)                 -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVBType (_, r0, r1, _)             -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVIType (_, r0, r1, _)             -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `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))
+| `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)))
 | `RISCVLoadRes (_, _, rs1, _, rd)       -> fold_reg rs1 (fold_reg rd (y_reg, y_sreg))
 | `RISCVStoreCon (_, _, rs2, rs1, _, rd) -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (y_reg, y_sreg)))
 | `RISCVAMO (_, _, _, rs2, rs1, _, rd)   -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (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 2e508678..e66608e6 100644
--- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
+++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -30,18 +30,20 @@
       translate_reg "rs1" rs1,
       translate_reg "rd" rd,
       translate_rop op)
-| `RISCVLoad(imm, rs, rd, unsigned, width, aq) -> LOAD(
+| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) -> LOAD(
       translate_imm12 "imm" imm,
       translate_reg "rs" rs,
       translate_reg "rd" rd,
       translate_bool "unsigned" unsigned,
       translate_wordWidth width,
-      translate_bool "aq" aq)
-| `RISCVStore(imm, rs, rd, width, rl) -> STORE (
+      translate_bool "aq" aq,
+      translate_bool "rl" rl)
+| `RISCVStore(imm, rs, rd, width, aq, rl) -> STORE (
       translate_imm12 "imm" imm,
       translate_reg "rs" rs,
       translate_reg "rd" rd,
       translate_wordWidth width,
+      translate_bool "aq" aq,
       translate_bool "rl" rl)
 | `RISCVADDIW(imm, rs, rd) -> ADDIW(
       translate_imm12 "imm" imm,
diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen
index 9d5df538..27df99f4 100644
--- a/risc-v/hgen/lexer.hgen
+++ b/risc-v/hgen/lexer.hgen
@@ -33,31 +33,44 @@
 "or",   RTYPE{op=RISCVOR};
 "and",  RTYPE{op=RISCVAND};
 
-"lb",  LOAD{unsigned=false; width=RISCVBYTE;   aq=false};
-"lbu", LOAD{unsigned=true;  width=RISCVBYTE;   aq=false};
-"lh",  LOAD{unsigned=false; width=RISCVHALF;   aq=false};
-"lhu", LOAD{unsigned=true;  width=RISCVHALF;   aq=false};
-"lw",  LOAD{unsigned=false; width=RISCVWORD;   aq=false};
-"lwu", LOAD{unsigned=true;  width=RISCVWORD;   aq=false};
-"ld",  LOAD{unsigned=false; width=RISCVDOUBLE; aq=false};
-
-"lb.aq",  LOAD{unsigned=false; width=RISCVBYTE;   aq=true};
-"lbu.aq", LOAD{unsigned=true;  width=RISCVBYTE;   aq=true};
-"lh.aq",  LOAD{unsigned=false; width=RISCVHALF;   aq=true};
-"lhu.aq", LOAD{unsigned=true;  width=RISCVHALF;   aq=true};
-"lw.aq",  LOAD{unsigned=false; width=RISCVWORD;   aq=true};
-"lwu.aq", LOAD{unsigned=true;  width=RISCVWORD;   aq=true};
-"ld.aq",  LOAD{unsigned=false; width=RISCVDOUBLE; aq=true};
-
-"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};
+"lb",  LOAD{unsigned=false; width=RISCVBYTE;   aq=false; rl=false};
+"lbu", LOAD{unsigned=true;  width=RISCVBYTE;   aq=false; rl=false};
+"lh",  LOAD{unsigned=false; width=RISCVHALF;   aq=false; rl=false};
+"lhu", LOAD{unsigned=true;  width=RISCVHALF;   aq=false; rl=false};
+"lw",  LOAD{unsigned=false; width=RISCVWORD;   aq=false; rl=false};
+"lwu", LOAD{unsigned=true;  width=RISCVWORD;   aq=false; rl=false};
+"ld",  LOAD{unsigned=false; width=RISCVDOUBLE; aq=false; rl=false};
+
+"lb.aq",  LOAD{unsigned=false; width=RISCVBYTE;   aq=true; rl=false};
+"lbu.aq", LOAD{unsigned=true;  width=RISCVBYTE;   aq=true; rl=false};
+"lh.aq",  LOAD{unsigned=false; width=RISCVHALF;   aq=true; rl=false};
+"lhu.aq", LOAD{unsigned=true;  width=RISCVHALF;   aq=true; rl=false};
+"lw.aq",  LOAD{unsigned=false; width=RISCVWORD;   aq=true; rl=false};
+"lwu.aq", LOAD{unsigned=true;  width=RISCVWORD;   aq=true; rl=false};
+"ld.aq",  LOAD{unsigned=false; width=RISCVDOUBLE; aq=true; rl=false};
+
+"lb.aq.rl",  LOAD{unsigned=false; width=RISCVBYTE;   aq=true; rl=true};
+"lbu.aq.rl", LOAD{unsigned=true;  width=RISCVBYTE;   aq=true; rl=true};
+"lh.aq.rl",  LOAD{unsigned=false; width=RISCVHALF;   aq=true; rl=true};
+"lhu.aq.rl", LOAD{unsigned=true;  width=RISCVHALF;   aq=true; rl=true};
+"lw.aq.rl",  LOAD{unsigned=false; width=RISCVWORD;   aq=true; rl=true};
+"lwu.aq.rl", LOAD{unsigned=true;  width=RISCVWORD;   aq=true; rl=true};
+"ld.aq.rl",  LOAD{unsigned=false; width=RISCVDOUBLE; aq=true; rl=true};
+
+"sb", STORE{width=RISCVBYTE;   aq=false; rl=false};
+"sh", STORE{width=RISCVHALF;   aq=false; rl=false};
+"sw", STORE{width=RISCVWORD;   aq=false; rl=false};
+"sd", STORE{width=RISCVDOUBLE; aq=false; rl=false};
+
+"sb.rl", STORE{width=RISCVBYTE;   aq=false; rl=true};
+"sh.rl", STORE{width=RISCVHALF;   aq=false; rl=true};
+"sw.rl", STORE{width=RISCVWORD;   aq=false; rl=true};
+"sd.rl", STORE{width=RISCVDOUBLE; aq=false; rl=true};
+
+"sb.aq.rl", STORE{width=RISCVBYTE;   aq=true; rl=true};
+"sh.aq.rl", STORE{width=RISCVHALF;   aq=true; rl=true};
+"sw.aq.rl", STORE{width=RISCVWORD;   aq=true; rl=true};
+"sd.aq.rl", STORE{width=RISCVDOUBLE; aq=true; rl=true};
 
 "addiw", ADDIW ();
 
@@ -75,17 +88,22 @@
 "r",  FENCEOPTION Fence_R;
 "w",  FENCEOPTION Fence_W;
 "rw", FENCEOPTION Fence_RW;
-"fence.i", FENCEI ();
 
-"lr.w",    LOADRES {width=RISCVWORD;   aq=false; rl=false};
-"lr.w.aq", LOADRES {width=RISCVWORD;   aq=true;  rl=false};
-"lr.d",    LOADRES {width=RISCVDOUBLE; aq=false; rl=false};
-"lr.d.aq", LOADRES {width=RISCVDOUBLE; aq=true;  rl=false};
+"fence.i", FENCEI ();
 
-"sc.w",    STORECON {width=RISCVWORD;   aq=false; rl=false};
-"sc.w.rl", STORECON {width=RISCVWORD;   aq=false; rl=true};
-"sc.d",    STORECON {width=RISCVDOUBLE; aq=false; rl=false};
-"sc.d.rl", STORECON {width=RISCVDOUBLE; aq=false; rl=true};
+"lr.w",       LOADRES {width=RISCVWORD;   aq=false; rl=false};
+"lr.w.aq",    LOADRES {width=RISCVWORD;   aq=true;  rl=false};
+"lr.w.aq.rl", LOADRES {width=RISCVWORD;   aq=true;  rl=true};
+"lr.d",       LOADRES {width=RISCVDOUBLE; aq=false; rl=false};
+"lr.d.aq",    LOADRES {width=RISCVDOUBLE; aq=true;  rl=false};
+"lr.d.aq.rl", LOADRES {width=RISCVDOUBLE; aq=true;  rl=true};
+
+"sc.w",       STORECON {width=RISCVWORD;   aq=false; rl=false};
+"sc.w.rl",    STORECON {width=RISCVWORD;   aq=false; rl=true};
+"sc.w.aq.rl", STORECON {width=RISCVWORD;   aq=true;  rl=true};
+"sc.d",       STORECON {width=RISCVDOUBLE; aq=false; rl=false};
+"sc.d.rl",    STORECON {width=RISCVDOUBLE; aq=false; rl=true};
+"sc.d.aq.rl", STORECON {width=RISCVDOUBLE; aq=true;  rl=true};
 
 "amoswap.w",  AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOSWAP};
 "amoadd.w",   AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOADD};
diff --git a/risc-v/hgen/map.hgen b/risc-v/hgen/map.hgen
index 91eecc56..bab5ced8 100644
--- a/risc-v/hgen/map.hgen
+++ b/risc-v/hgen/map.hgen
@@ -1,15 +1,15 @@
-| `RISCVUTYPE (x, r0, y)          -> `RISCVUTYPE (x, map_reg r0, y)
-| `RISCVJAL (x, r0)               -> `RISCVJAL (x, map_reg r0)
-| `RISCVJALR (x, r0, r1)          -> `RISCVJALR (x, map_reg r0, map_reg r1)
-| `RISCVBType (x, r0, r1, y)      -> `RISCVBType (x, map_reg r0, map_reg r1, y)
-| `RISCVIType (x, r0, r1, y)      -> `RISCVIType (x, map_reg r0, map_reg r1, y)
-| `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, 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)
+| `RISCVUTYPE (x, r0, y)                   -> `RISCVUTYPE (x, map_reg r0, y)
+| `RISCVJAL (x, r0)                        -> `RISCVJAL (x, map_reg r0)
+| `RISCVJALR (x, r0, r1)                   -> `RISCVJALR (x, map_reg r0, map_reg r1)
+| `RISCVBType (x, r0, r1, y)               -> `RISCVBType (x, map_reg r0, map_reg r1, y)
+| `RISCVIType (x, r0, r1, y)               -> `RISCVIType (x, map_reg r0, map_reg r1, y)
+| `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, b)       -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z, a, b)
+| `RISCVStore (x, r0, r1, y, z, a)         -> `RISCVStore (x, map_reg r0, map_reg r1, y, z, a)
+| `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)
 | `RISCVLoadRes (aq, rl, rs1, w, rd)       -> `RISCVLoadRes (aq, rl, map_reg rs1, w, map_reg rd)
 | `RISCVStoreCon (aq, rl, rs2, rs1, w, rd) -> `RISCVStoreCon (aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd)
 | `RISCVAMO (op, aq, rl, rs2, rs1, w, rd)  -> `RISCVAMO (op, aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd)
diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen
index dc61e566..82bb1d5b 100644
--- a/risc-v/hgen/parser.hgen
+++ b/risc-v/hgen/parser.hgen
@@ -13,9 +13,9 @@
 | RTYPE reg COMMA reg COMMA reg
   { `RISCVRType ($6, $4, $2, $1.op) }
 | LOAD reg COMMA NUM LPAR reg RPAR
-  { `RISCVLoad($4, $6, $2, $1.unsigned, $1.width, $1.aq) }
+  { `RISCVLoad($4, $6, $2, $1.unsigned, $1.width, $1.aq, $1.rl) }
 | STORE reg COMMA NUM LPAR reg RPAR
-  { `RISCVStore($4, $2, $6, $1.width, $1.rl) }
+  { `RISCVStore($4, $2, $6, $1.width, $1.aq, $1.rl) }
 | ADDIW reg COMMA reg COMMA NUM
   { `RISCVADDIW ($6, $4, $2) }
 | SHIFTW reg COMMA reg COMMA NUM
@@ -48,3 +48,6 @@
     `RISCVStoreCon($1.aq, $1.rl, $4, $8, $1.width, $2) }
 | AMO reg COMMA reg COMMA LPAR reg RPAR
   { `RISCVAMO($1.op, $1.aq, $1.rl, $4, $7, $1.width, $2) }
+| AMO reg COMMA reg COMMA NUM LPAR reg RPAR
+  { if $6 <> 0 then failwith "'amo<op>' offset must be 0" else
+    `RISCVAMO($1.op, $1.aq, $1.rl, $4, $8, $1.width, $2) }
diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen
index b5068c71..fc1c0000 100644
--- a/risc-v/hgen/pretty.hgen
+++ b/risc-v/hgen/pretty.hgen
@@ -7,34 +7,24 @@
 | `RISCVIType(imm, rs2, rs1, op)  -> sprintf "%s %s, %s, %d" (pp_riscv_iop op) (pp_reg rs1) (pp_reg rs2) imm
 | `RISCVShiftIop(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm
 | `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, rl)
-                                  -> sprintf "%s %s, %d(%s)" (pp_riscv_store_op (width, rl)) (pp_reg rs2) imm (pp_reg rs1)
+
+| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) ->
+    sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width, aq, rl)) (pp_reg rd) imm (pp_reg rs)
+
+| `RISCVStore(imm, rs2, rs1, width, aq, rl) ->
+    sprintf "%s %s, %d(%s)" (pp_riscv_store_op (width, aq, 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)
 | `RISCVFENCE(pred, succ)         -> sprintf "fence %s, %s" (pp_riscv_fence_option pred) (pp_riscv_fence_option succ)
 | `RISCVFENCEI                    -> sprintf "fence.i"
-| `RISCVLoadRes(aq, rl, rs1, width, rd)
-                                  ->
-                                    assert (rl = false);
-                                    sprintf "%s %s, (%s)"
-                                      (pp_riscv_load_reserved_op (aq, rl, width))
-                                      (pp_reg rd)
-                                      (pp_reg rs1)
-| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd)
-                                  ->
-                                    assert (aq = false);
-                                    sprintf "%s %s, %s, (%s)"
-                                      (pp_riscv_store_conditional_op (aq, rl, width))
-                                      (pp_reg rd)
-                                      (pp_reg rs2)
-                                      (pp_reg rs1)
-| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd)
-                                  ->
-                                    sprintf "%s %s, %s, (%s)"
-                                      (pp_riscv_amo_op (op, aq, rl, width))
-                                      (pp_reg rd)
-                                      (pp_reg rs2)
-                                      (pp_reg rs1)
+
+| `RISCVLoadRes(aq, rl, rs1, width, rd) ->
+    sprintf "%s %s, (%s)" (pp_riscv_load_reserved_op (aq, rl, width)) (pp_reg rd) (pp_reg rs1)
+
+| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) ->
+    sprintf "%s %s, %s, (%s)" (pp_riscv_store_conditional_op (aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1)
+
+| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) ->
+    sprintf "%s %s, %s, (%s)" (pp_riscv_amo_op (op, aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1)
diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen
index bec35203..2f9a80f1 100644
--- a/risc-v/hgen/sail_trans_out.hgen
+++ b/risc-v/hgen/sail_trans_out.hgen
@@ -6,10 +6,10 @@
 | ("ITYPE", [imm; rs1; rd; op])   -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op)
 | ("SHIFTIOP", [imm; rs; rd; op]) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
 | ("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; rl])
-                                  -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool rl)
+| ("LOAD", [imm; rs; rd; unsigned; width; aq; rl])
+                                  -> `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, translate_out_bool rl)
+| ("STORE", [imm; rs; rd; width; aq; rl])
+                                  -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, 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 662b1044..23bcc4cb 100644
--- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
+++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -6,10 +6,10 @@
 | ITYPE( imm, rs1, rd, op)    -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op)
 | SHIFTIOP( imm, rs, rd, op)  -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
 | 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, rl)
-                              -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool rl)
+| LOAD( imm, rs, rd, unsigned, width, aq, rl)
+                              -> `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, translate_out_bool rl)
+| STORE( imm, rs, rd, width, aq, rl)
+                              -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, 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 9b469a27..d338d865 100644
--- a/risc-v/hgen/token_types.hgen
+++ b/risc-v/hgen/token_types.hgen
@@ -5,8 +5,8 @@ type token_BType    = {op : riscvBop }
 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; rl: bool }
+type token_Load     = {unsigned: bool; width : wordWidth; aq: bool; rl: bool }
+type token_Store    = {width : wordWidth; aq: bool; 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 12da62d8..8b7cbe11 100644
--- a/risc-v/hgen/trans_sail.hgen
+++ b/risc-v/hgen/trans_sail.hgen
@@ -58,7 +58,7 @@
       translate_rop "op" op;
     ],
     [])
-| `RISCVLoad(imm, rs, rd, unsigned, width, aq) ->
+| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) ->
    ("LOAD",
     [
       translate_imm12 "imm" imm;
@@ -67,15 +67,17 @@
       translate_bool "unsigned" unsigned;
       translate_width "width" width;
       translate_bool "aq" aq;
+      translate_bool "rl" rl;
     ],
     [])
-| `RISCVStore(imm, rs2, rs1, width, rl) ->
+| `RISCVStore(imm, rs2, rs1, width, aq, rl) ->
    ("STORE",
     [
       translate_imm12 "imm" imm;
       translate_reg "rs2" rs2;
       translate_reg "rs1" rs1;
       translate_width "width" width;
+      translate_bool "aq" aq;
       translate_bool "rl" rl;
     ],
     [])
diff --git a/risc-v/hgen/types.hgen b/risc-v/hgen/types.hgen
index 83deb4a2..e0caed2d 100644
--- a/risc-v/hgen/types.hgen
+++ b/risc-v/hgen/types.hgen
@@ -99,7 +99,7 @@ type wordWidth =
   | RISCVWORD
   | RISCVDOUBLE
 
-let pp_riscv_load_op (unsigned, width, aq) =
+let pp_riscv_load_op (unsigned, width, aq, rl) =
   begin match (unsigned, width) with
   | (false, RISCVBYTE)    -> "lb"
   | (true,  RISCVBYTE)    -> "lbu"
@@ -108,17 +108,19 @@ let pp_riscv_load_op (unsigned, width, aq) =
   | (false, RISCVWORD)    -> "lw"
   | (true,  RISCVWORD)    -> "lwu"
   | (_, RISCVDOUBLE)      -> "ld"
-  end
-  ^ (if aq then ".aq" else "")
+  end ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
 
-let pp_riscv_store_op (width, rl) =
+let pp_riscv_store_op (width, aq, rl) =
   begin match width with
   | RISCVBYTE -> "sb"
   | RISCVHALF -> "sh"
   | RISCVWORD -> "sw"
   | RISCVDOUBLE -> "sd"
-  end
-  ^ (if rl then ".rl" else "")
+  end ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
 
 let pp_riscv_load_reserved_op (aq, rl, width) =
   "lr" ^
diff --git a/risc-v/hgen/types_trans_sail.hgen b/risc-v/hgen/types_trans_sail.hgen
index 7528a522..238c7e5b 100644
--- a/risc-v/hgen/types_trans_sail.hgen
+++ b/risc-v/hgen/types_trans_sail.hgen
@@ -11,30 +11,47 @@ let translate_enum enum_values name value =
   (name, Range0 (Some size),  IInt.bit_list_of_integer size (Nat_big_num.of_int index))
 
 let translate_uop = translate_enum [RISCVLUI; RISCVAUIPC]
+
 let translate_bop = translate_enum [RISCVBEQ; RISCVBNE; RISCVBLT; RISCVBGE; RISCVBLTU; RISCVBGEU] (* branch ops *)
+
 let translate_iop = translate_enum [RISCVADDI; RISCVSLTI; RISCVSLTIU; RISCVXORI; RISCVORI; RISCVANDI] (* immediate ops *)
+
 let translate_sop = translate_enum [RISCVSLLI; RISCVSRLI; RISCVSRAI] (* shift ops *)
+
 let translate_rop = translate_enum [RISCVADD; RISCVSUB; RISCVSLL; RISCVSLT; RISCVSLTU; RISCVXOR; RISCVSRL; RISCVSRA; RISCVOR; RISCVAND] (* reg-reg ops *)
+
 let translate_ropw = translate_enum [RISCVADDW; RISCVSUBW; RISCVSLLW; RISCVSRLW; RISCVSRAW] (* reg-reg 32-bit ops *)
+
 let translate_amoop = translate_enum [RISCVAMOSWAP; RISCVAMOADD; RISCVAMOXOR; RISCVAMOAND; RISCVAMOOR; RISCVAMOMIN; RISCVAMOMAX; RISCVAMOMINU; RISCVAMOMAXU]
+
 let translate_width = translate_enum [RISCVBYTE; RISCVHALF; RISCVWORD; RISCVDOUBLE] 
+
 let translate_reg name value = 
     (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int (reg_to_int value)))
+
 let translate_imm21 name value = 
     (name, Bvector (Some 21), bit_list_of_integer 21 (Nat_big_num.of_int value))
+
 let translate_imm20 name value = 
     (name, Bvector (Some 20), bit_list_of_integer 20 (Nat_big_num.of_int value))
+
 let translate_imm16 name value = 
     (name, Bvector (Some 16), bit_list_of_integer 16 (Nat_big_num.of_int value))
+
 let translate_imm13 name value = 
     (name, Bvector (Some 13), bit_list_of_integer 13 (Nat_big_num.of_int value))
+
 let translate_imm12 name value = 
     (name, Bvector (Some 12), bit_list_of_integer 12 (Nat_big_num.of_int value))
+
 let translate_imm6 name value = 
     (name, Bvector (Some 6), bit_list_of_integer 6 (Nat_big_num.of_int value))
+
 let translate_imm5 name value = 
     (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int value))
+
 let translate_imm4 name value = 
     (name, Bvector (Some 4), bit_list_of_integer 4 (Nat_big_num.of_int value))
+
 let translate_bool name value =
   (name, Bit, [if value then Bitc_one else Bitc_zero])
diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail
index cd0e5bf9..c5b19d26 100644
--- a/risc-v/riscv.sail
+++ b/risc-v/riscv.sail
@@ -62,38 +62,56 @@ function forall 'a. 'a effect { escape } not_implemented((string) message) =
 
 val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
 val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_acquire
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_strong_acquire
 val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved
 val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_acquire
-function forall Nat 'n. (bit[8 * 'n]) effect { rmem } mem_read( (bit[64]) addr, ([|'n|]) width, (bool) aq, (bool) res) =
-  switch (aq, res) {
-    case (false, false) -> MEMr(addr, width)
-    case (true,  false) -> MEMr_acquire(addr, width)
-    case (false, true)  -> MEMr_reserved(addr, width)
-    case (true,  true)  -> MEMr_reserved_acquire(addr, width)
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserved_strong_acquire
+function forall Nat 'n. (bit[8 * 'n]) effect { rmem } mem_read( (bit[64]) addr, ([|'n|]) width, (bool) aq, (bool) rl, (bool) res) =
+  switch (aq, rl, res) {
+    case (false, false, false) -> MEMr(addr, width)
+    case (true,  false, false) -> MEMr_acquire(addr, width)
+    case (false, false, true)  -> MEMr_reserved(addr, width)
+    case (true,  false, true)  -> MEMr_reserved_acquire(addr, width)
+    case (false, true,  false) -> not_implemented("load.rl is not implemented")
+    case (true,  true,  false) -> MEMr_strong_acquire(addr, width)
+    case (false, true,  true)  -> not_implemented("lr.rl is not implemented")
+    case (true,  true,  true)  -> MEMr_reserved_strong_acquire(addr, width)
   }
 
 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
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_strong_release
 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_ea( (bit[64]) addr , ([|'n|]) width, (bool) rl, (bool) con) =
-  switch (rl, con) {
-    case (false, false) -> MEMea(addr, width)
-    case (true,  false) -> MEMea_release(addr, width)
-    case (false, true)  -> MEMea_conditional(addr, width)
-    case (true , true)  -> MEMea_conditional_release(addr, width)
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional_strong_release
+function forall Nat 'n. unit effect { eamem } mem_write_ea( (bit[64]) addr , ([|'n|]) width, (bool) aq, (bool) rl, (bool) con) =
+  switch (aq, rl, con) {
+    case (false, false, false) -> MEMea(addr, width)
+    case (false, true,  false) -> MEMea_release(addr, width)
+    case (false, false, true)  -> MEMea_conditional(addr, width)
+    case (false, true , true)  -> MEMea_conditional_release(addr, width)
+    case (true,  false, false) -> not_implemented("store.aq is not implemented")
+    case (true,  true,  false) -> MEMea_strong_release(addr, width)
+    case (true,  false, true)  -> not_implemented("sc.aq is not implemented")
+    case (true,  true , true)  -> MEMea_conditional_strong_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
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_strong_release
 val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional
 val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_release
-function forall Nat 'n. unit effect { wmv } mem_write_value( (bit[64]) addr , ([|'n|]) width , (bit[8*'n]) value, (bool) rl, (bool) con) =
-  switch (rl, con) {
-    case (false, false) -> MEMval(addr, width, value)
-    case (true,  false) -> MEMval_release(addr, width, value)
-    case (false, true)  -> MEMval_conditional(addr, width, value)
-    case (true,  true)  -> MEMval_conditional_release(addr, width, value)
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval_conditional_strong_release
+function forall Nat 'n. unit effect { wmv } mem_write_value( (bit[64]) addr , ([|'n|]) width , (bit[8*'n]) value, (bool) aq, (bool) rl, (bool) con) =
+  switch (aq, rl, con) {
+    case (false, false, false) -> MEMval(addr, width, value)
+    case (false, true,  false) -> MEMval_release(addr, width, value)
+    case (false, false, true)  -> MEMval_conditional(addr, width, value)
+    case (false, true,  true)  -> MEMval_conditional_release(addr, width, value)
+    case (true,  false, false) -> not_implemented("store.aq is not implemented")
+    case (true,  true,  false) -> MEMval_strong_release(addr, width, value)
+    case (true,  false, true)  -> not_implemented("sc.aq is not implemented")
+    case (true,  true,  true)  -> MEMval_conditional_strong_release(addr, width, value)
   }
 
 val extern unit -> bool effect {exmem} speculate_conditional_success
@@ -245,51 +263,51 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) =
   } in
   wGPR(rd, result)
 
-union ast member ((bit[12]), regno, regno, bool, word_width, bool) LOAD
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE,   false))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF,   false))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD,   false))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, DOUBLE, false))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  BYTE,   false))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  HALF,   false))
-function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  WORD,   false))
-function clause execute(LOAD(imm, rs1, rd, unsigned, width, aq)) =
+union ast member ((bit[12]), regno, regno, bool, word_width, bool, bool) LOAD
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, BYTE,   false, false))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b001 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, HALF,   false, false))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b010 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, WORD,   false, false))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b011 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, false, DOUBLE, false, false))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b100 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  BYTE,   false, false))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b101 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  HALF,   false, false))
+function clause decode ((bit[12]) imm : (regno) rs1 : 0b110 : (regno) rd : 0b0000011) = Some(LOAD(imm, rs1, rd, true,  WORD,   false, false))
+function clause execute(LOAD(imm, rs1, rd, unsigned, width, aq, rl)) =
     let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in
     let (bit[64]) result = if unsigned then 
         switch (width) {
-          case BYTE   -> EXTZ(mem_read(addr, 1, aq, false))
-          case HALF   -> EXTZ(mem_read(addr, 2, aq, false))
-          case WORD   -> EXTZ(mem_read(addr, 4, aq, false))
-          case DOUBLE -> mem_read(addr, 8, aq, false)
+          case BYTE   -> EXTZ(mem_read(addr, 1, aq, rl, false))
+          case HALF   -> EXTZ(mem_read(addr, 2, aq, rl, false))
+          case WORD   -> EXTZ(mem_read(addr, 4, aq, rl, false))
+          case DOUBLE -> mem_read(addr, 8, aq, rl, false)
         }
       else
         switch (width) {
-          case BYTE   -> EXTS(mem_read(addr, 1, aq, false))
-          case HALF   -> EXTS(mem_read(addr, 2, aq, false))
-          case WORD   -> EXTS(mem_read(addr, 4, aq, false))
-          case DOUBLE -> mem_read(addr, 8, aq, false)
+          case BYTE   -> EXTS(mem_read(addr, 1, aq, rl, false))
+          case HALF   -> EXTS(mem_read(addr, 2, aq, rl, false))
+          case WORD   -> EXTS(mem_read(addr, 4, aq, rl, false))
+          case DOUBLE -> mem_read(addr, 8, aq, rl, false)
         } in
     wGPR(rd, result)
 
-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)) =
+union ast member ((bit[12]), regno, regno, word_width, bool, 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, false))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b001 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, HALF, false, false))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b010 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, WORD, false, false))
+function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit[5]) imm5 : 0b0100011) = Some(STORE(imm7 : imm5, rs2, rs1, DOUBLE, false, false))
+function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) =
     let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in {
       switch (width) {
-        case BYTE   -> mem_write_ea(addr, 1, rl, false)
-        case HALF   -> mem_write_ea(addr, 2, rl, false)
-        case WORD   -> mem_write_ea(addr, 4, rl, false)
-        case DOUBLE -> mem_write_ea(addr, 8, rl, false)
+        case BYTE   -> mem_write_ea(addr, 1, aq, rl, false)
+        case HALF   -> mem_write_ea(addr, 2, aq, rl, false)
+        case WORD   -> mem_write_ea(addr, 4, aq, rl, false)
+        case DOUBLE -> mem_write_ea(addr, 8, aq, rl, false)
       };
       let rs2_val = rGPR(rs2) in
       switch (width) {
-        case BYTE   -> mem_write_value(addr, 1, rs2_val[7..0],  rl, false)
-        case HALF   -> mem_write_value(addr, 2, rs2_val[15..0], rl, false)
-        case WORD   -> mem_write_value(addr, 4, rs2_val[31..0], rl, false)
-        case DOUBLE -> mem_write_value(addr, 8, rs2_val,        rl, false)
+        case BYTE   -> mem_write_value(addr, 1, rs2_val[7..0],  aq, rl, false)
+        case HALF   -> mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false)
+        case WORD   -> mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false)
+        case DOUBLE -> mem_write_value(addr, 8, rs2_val,        aq, rl, false)
       }
     }
 
@@ -360,36 +378,31 @@ union ast member (bool, bool, regno, word_width, regno) LOADRES
 function clause decode (0b00010 : [aq] : [rl] : 0b00000 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(LOADRES(aq, rl, rs1, WORD, rd))
 function clause decode (0b00010 : [aq] : [rl] : 0b00000 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(LOADRES(aq, rl, rs1, DOUBLE, rd))
 function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
-  if rl then not_implemented("load-reserved-release is not implemented")
-  else {
-    let (bit[64]) addr = rGPR(rs1) in
-    let (bit[64]) result =
-        switch width {
-          case WORD   -> EXTS(mem_read(addr, 4, aq, true))
-          case DOUBLE -> mem_read(addr, 8, aq, true)
-        } in
-    wGPR(rd, result)
-  }
+  let (bit[64]) addr = rGPR(rs1) in
+  let (bit[64]) result =
+      switch width {
+        case WORD   -> EXTS(mem_read(addr, 4, aq, rl, true))
+        case DOUBLE -> mem_read(addr, 8, aq, rl, true)
+      } in
+  wGPR(rd, result)
 
 union ast member (bool, bool, regno, regno, word_width, regno) STORECON
 function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(STORECON(aq, rl, rs2, rs1, WORD, rd))
 function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(STORECON(aq, rl, rs2, rs1, DOUBLE, rd))
 function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
-  if aq then not_implemented("store-conditional-acquire is not implemented");
-
   (*(bit)*) status := if speculate_conditional_success() then 0 else 1;
   wGPR(rd) := (bit[64]) (EXTZ([status]));
 
   if status == 1 then () else {
     (bit[64]) addr := rGPR(rs1);
     switch width {
-      case WORD   -> mem_write_ea(addr, 4, rl, true)
-      case DOUBLE -> mem_write_ea(addr, 8, rl, true)
+      case WORD   -> mem_write_ea(addr, 4, aq, rl, true)
+      case DOUBLE -> mem_write_ea(addr, 8, aq, rl, true)
     };
     rs2_val := rGPR(rs2);
     switch width {
-      case WORD   -> mem_write_value(addr, 4, rs2_val[31..0], rl, true)
-      case DOUBLE -> mem_write_value(addr, 8, rs2_val,        rl, true)
+      case WORD   -> mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true)
+      case DOUBLE -> mem_write_value(addr, 8, rs2_val,        aq, rl, true)
     };
   };
 }
@@ -418,14 +431,14 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
   (bit[64]) addr := rGPR(rs1);
 
   switch (width) {
-    case WORD   -> mem_write_ea(addr, 4, rl, true)
-    case DOUBLE -> mem_write_ea(addr, 8, rl, true)
+    case WORD   -> mem_write_ea(addr, 4, aq, rl, true)
+    case DOUBLE -> mem_write_ea(addr, 8, aq, rl, true)
   };
 
   (bit[64]) loaded :=
     switch (width) {
-      case WORD   -> EXTS(mem_read(addr, 4, aq, true))
-      case DOUBLE -> mem_read(addr, 8, aq, true)
+      case WORD   -> EXTS(mem_read(addr, 4, aq, rl, true))
+      case DOUBLE -> mem_read(addr, 8, aq, rl, true)
     };
   wGPR(rd, loaded);
 
@@ -445,8 +458,8 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
     };
 
   switch (width) {
-    case WORD   -> mem_write_value(addr, 4, result[31..0], rl, true)
-    case DOUBLE -> mem_write_value(addr, 8, result,        rl, true)
+    case WORD   -> mem_write_value(addr, 4, result[31..0], aq, rl, true)
+    case DOUBLE -> mem_write_value(addr, 8, result,        aq, rl, true)
   };
 }
 
diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem
index 62a7bb91..280095e5 100644
--- a/risc-v/riscv_extras.lem
+++ b/risc-v/riscv_extras.lem
@@ -34,8 +34,11 @@ let memory_parameter_transformer_option_address _mode v =
 let read_memory_functions : memory_reads =
   [ ("MEMr",                  (MR Read_plain                  memory_parameter_transformer));
     ("MEMr_acquire",          (MR Read_RISCV_acquire          memory_parameter_transformer));
+    ("MEMr_strong_acquire",   (MR Read_RISCV_strong_acquire   memory_parameter_transformer));
     ("MEMr_reserved",         (MR Read_RISCV_reserved         memory_parameter_transformer));
     ("MEMr_reserved_acquire", (MR Read_RISCV_reserved_acquire memory_parameter_transformer));
+    ("MEMr_reserved_strong_acquire",
+                              (MR Read_RISCV_reserved_acquire memory_parameter_transformer));
   ]
 
 let memory_writes : memory_writes =
@@ -44,25 +47,23 @@ let memory_writes : memory_writes =
 let memory_eas : memory_write_eas =
   [ ("MEMea",                     (MEA Write_plain                     memory_parameter_transformer));
     ("MEMea_release",             (MEA Write_RISCV_release             memory_parameter_transformer));
+    ("MEMea_strong_release",      (MEA Write_RISCV_strong_release      memory_parameter_transformer));
     ("MEMea_conditional",         (MEA Write_RISCV_conditional         memory_parameter_transformer));
     ("MEMea_conditional_release", (MEA Write_RISCV_conditional_release memory_parameter_transformer));
+    ("MEMea_conditional_strong_release",
+                                  (MEA Write_RISCV_conditional_strong_release
+                                                                       memory_parameter_transformer));
   ]
 
 let memory_vals : memory_write_vals =
-  [ ("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 Nothing));
-                        (* (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 Nothing));
-                        (* (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",                    (MV memory_parameter_transformer_option_address Nothing));
+    ("MEMval_release",            (MV memory_parameter_transformer_option_address Nothing));
+    ("MEMval_strong_release",     (MV memory_parameter_transformer_option_address Nothing));
+    ("MEMval_conditional",        (MV memory_parameter_transformer_option_address Nothing));
+    ("MEMval_conditional_release",(MV memory_parameter_transformer_option_address Nothing));
+    ("MEMval_conditional_strong_release",
+                                  (MV memory_parameter_transformer_option_address Nothing));
+
   ]
 
 let speculate_conditional_success : excl_res =
diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem
index 3f04f9a2..d89dc44c 100644
--- a/risc-v/riscv_extras_embed.lem
+++ b/risc-v/riscv_extras_embed.lem
@@ -6,33 +6,48 @@ open import Prompt
 
 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)
 
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)
 
diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail
index e6813c37..602f0bec 100644
--- a/risc-v/riscv_regfp.sail
+++ b/risc-v/riscv_regfp.sail
@@ -51,17 +51,29 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
             if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR;
             if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
      }
-     case (LOAD ( imm, rs, rd, unsign, width, aq)) -> { (* XXX "unsigned" causes name conflict in lem shallow embedding... *)
+     case (LOAD ( imm, rs, rd, unsign, width, aq, rl)) -> { (* XXX "unsigned" causes name conflict in lem shallow embedding... *)
             if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR;
             if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
             aR := iR;
-            ik := if aq then IK_mem_read (Read_RISCV_acquire) else IK_mem_read (Read_plain);
+            ik :=
+              switch (aq, rl) {
+                case (false, false) -> IK_mem_read (Read_plain)
+                case (true,  false) -> IK_mem_read (Read_RISCV_acquire)
+                case (false, true)  -> exit "not implemented"
+                case (true,  true)  -> IK_mem_read (Read_RISCV_strong_acquire)
+              };
      }
-     case (STORE( imm, rs2, rs1, width, rl)) -> {
+     case (STORE( imm, rs2, rs1, width, aq, 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 := if rl then IK_mem_write (Write_RISCV_release) else IK_mem_write (Write_plain);
+            ik :=
+              switch (aq, rl) {
+                case (false, false) -> IK_mem_write (Write_plain)
+                case (true,  false) -> exit "not implemented"
+                case (false, true)  -> IK_mem_write (Write_RISCV_release)
+                case (true,  true)  -> IK_mem_write (Write_RISCV_strong_release)
+              };
      }
      case (ADDIW ( imm, rs, rd)) -> {
             if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR;
@@ -96,7 +108,8 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
             ik := switch (aq, rl) {
               case (false, false) -> IK_mem_read (Read_RISCV_reserved)
               case (true,  false) -> IK_mem_read (Read_RISCV_reserved_acquire)
-              case (_,     true)  -> exit "not implemented"
+              case (false, true)  -> exit "not implemented"
+              case (true,  true)  -> IK_mem_read (Read_RISCV_reserved_strong_acquire)
             };
      }
      case (STORECON( aq, rl, rs2, rs1, width, rd)) -> {
@@ -118,10 +131,12 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
             if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
 
             ik := switch (aq, rl) {
-              case (false, false) -> IK_mem_rmw (Read_RISCV_reserved,         Write_RISCV_conditional)
-              case (false, true)  -> IK_mem_rmw (Read_RISCV_reserved,         Write_RISCV_conditional_release)
-              case (true,  false) -> IK_mem_rmw (Read_RISCV_reserved_acquire, Write_RISCV_conditional)
-              case (true,  true)  -> IK_mem_rmw (Read_RISCV_reserved_acquire, Write_RISCV_conditional_release)
+              case (false, false) -> IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional)
+              case (false, true)  -> IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional_release)
+              case (true,  false) -> IK_mem_rmw (Read_RISCV_reserved_acquire,
+                                                                      Write_RISCV_conditional)
+              case (true,  true)  -> IK_mem_rmw (Read_RISCV_reserved_strong_acquire,
+                                                                      Write_RISCV_conditional_strong_release)
             };
      }
   };