added RISC-V AMOs

25 files changed, 374 insertions, 68 deletions

diff --git a/etc/regfp.sail b/etc/regfp.sail
index 776e22af..761737db 100644
--- a/etc/regfp.sail
+++ b/etc/regfp.sail
@@ -83,6 +83,7 @@ typedef instruction_kind = const union {
   (barrier_kind) IK_barrier;
   (read_kind) IK_mem_read;
   (write_kind) IK_mem_write;
+  (read_kind, write_kind) IK_mem_rmw;
   IK_cond_branch;
   (trans_kind) IK_trans;
   IK_simple
diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen
index 6fd52b03..1839557f 100644
--- a/risc-v/hgen/ast.hgen
+++ b/risc-v/hgen/ast.hgen
@@ -14,3 +14,4 @@
 | `RISCVFENCEI
 | `RISCVLoadRes of bool * bool * reg * wordWidth * reg
 | `RISCVStoreCon of bool * bool * reg * reg * wordWidth * reg
+| `RISCVAMO of riscvAmoop * bool * bool * reg * reg * wordWidth * reg
diff --git a/risc-v/hgen/fold.hgen b/risc-v/hgen/fold.hgen
index 4cbaf779..d8806a37 100644
--- a/risc-v/hgen/fold.hgen
+++ b/risc-v/hgen/fold.hgen
@@ -13,3 +13,4 @@
 | `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 770f9263..2e508678 100644
--- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
+++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -74,3 +74,11 @@
       translate_reg "rs1" rs1,
       translate_wordWidth width,
       translate_reg "rd" rd)
+| `RISCVAMO (op, aq, rl, rs2, rs1, width, rd) -> AMO(
+      translate_amoop op,
+      translate_bool "aq" aq,
+      translate_bool "rl" rl,
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_wordWidth width,
+      translate_reg "rd" rd)
diff --git a/risc-v/hgen/herdtools_types_to_shallow_types.hgen b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
index 4d8bd87a..a63f9aed 100644
--- a/risc-v/hgen/herdtools_types_to_shallow_types.hgen
+++ b/risc-v/hgen/herdtools_types_to_shallow_types.hgen
@@ -47,6 +47,17 @@ let translate_ropw op = match op with
   | RISCVSRLW -> SRLW 
   | RISCVSRAW -> SRAW 
 
+let translate_amoop op = match op with
+  | RISCVAMOSWAP -> AMOSWAP
+  | RISCVAMOADD  -> AMOADD
+  | RISCVAMOXOR  -> AMOXOR
+  | RISCVAMOAND  -> AMOAND
+  | RISCVAMOOR   -> AMOOR
+  | RISCVAMOMIN  -> AMOMIN
+  | RISCVAMOMAX  -> AMOMAX
+  | RISCVAMOMINU -> AMOMINU
+  | RISCVAMOMAXU -> AMOMAXU
+
 let translate_wordWidth op = match op with
   | RISCVBYTE   -> BYTE  
   | RISCVHALF   -> HALF  
diff --git a/risc-v/hgen/lexer.hgen b/risc-v/hgen/lexer.hgen
index d422e82f..9d5df538 100644
--- a/risc-v/hgen/lexer.hgen
+++ b/risc-v/hgen/lexer.hgen
@@ -86,3 +86,83 @@
 "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};
+
+"amoswap.w",  AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOSWAP};
+"amoadd.w",   AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOADD};
+"amoand.w",   AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOAND};
+"amoor.w",    AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOOR};
+"amoxor.w",   AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOXOR};
+"amomax.w",   AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMAX};
+"amomin.w",   AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMIN};
+"amomaxu.w",  AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMAXU};
+"amominu.w",  AMO {width=RISCVWORD; aq=false; rl=false; op=RISCVAMOMINU};
+
+"amoswap.d",  AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOSWAP};
+"amoadd.d",   AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOADD};
+"amoand.d",   AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOAND};
+"amoor.d",    AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOOR};
+"amoxor.d",   AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOXOR};
+"amomax.d",   AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMAX};
+"amomin.d",   AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMIN};
+"amomaxu.d",  AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMAXU};
+"amominu.d",  AMO {width=RISCVDOUBLE; aq=false; rl=false; op=RISCVAMOMINU};
+
+"amoswap.w.aq",  AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOSWAP};
+"amoadd.w.aq",   AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOADD};
+"amoand.w.aq",   AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOAND};
+"amoor.w.aq",    AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOOR};
+"amoxor.w.aq",   AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOXOR};
+"amomax.w.aq",   AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMAX};
+"amomin.w.aq",   AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMIN};
+"amomaxu.w.aq",  AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMAXU};
+"amominu.w.aq",  AMO {width=RISCVWORD; aq=true; rl=false; op=RISCVAMOMINU};
+
+"amoswap.d.aq",  AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOSWAP};
+"amoadd.d.aq",   AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOADD};
+"amoand.d.aq",   AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOAND};
+"amoor.d.aq",    AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOOR};
+"amoxor.d.aq",   AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOXOR};
+"amomax.d.aq",   AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMAX};
+"amomin.d.aq",   AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMIN};
+"amomaxu.d.aq",  AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMAXU};
+"amominu.d.aq",  AMO {width=RISCVDOUBLE; aq=true; rl=false; op=RISCVAMOMINU};
+
+"amoswap.w.rl",  AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOSWAP};
+"amoadd.w.rl",   AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOADD};
+"amoand.w.rl",   AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOAND};
+"amoor.w.rl",    AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOOR};
+"amoxor.w.rl",   AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOXOR};
+"amomax.w.rl",   AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMAX};
+"amomin.w.rl",   AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMIN};
+"amomaxu.w.rl",  AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMAXU};
+"amominu.w.rl",  AMO {width=RISCVWORD; aq=false; rl=true; op=RISCVAMOMINU};
+
+"amoswap.d.rl",  AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOSWAP};
+"amoadd.d.rl",   AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOADD};
+"amoand.d.rl",   AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOAND};
+"amoor.d.rl",    AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOOR};
+"amoxor.d.rl",   AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOXOR};
+"amomax.d.rl",   AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMAX};
+"amomin.d.rl",   AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMIN};
+"amomaxu.d.rl",  AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMAXU};
+"amominu.d.rl",  AMO {width=RISCVDOUBLE; aq=false; rl=true; op=RISCVAMOMINU};
+
+"amoswap.w.aq.rl",  AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOSWAP};
+"amoadd.w.aq.rl",   AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOADD};
+"amoand.w.aq.rl",   AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOAND};
+"amoor.w.aq.rl",    AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOOR};
+"amoxor.w.aq.rl",   AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOXOR};
+"amomax.w.aq.rl",   AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMAX};
+"amomin.w.aq.rl",   AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMIN};
+"amomaxu.w.aq.rl",  AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMAXU};
+"amominu.w.aq.rl",  AMO {width=RISCVWORD; aq=true; rl=true; op=RISCVAMOMINU};
+
+"amoswap.d.aq.rl",  AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOSWAP};
+"amoadd.d.aq.rl",   AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOADD};
+"amoand.d.aq.rl",   AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOAND};
+"amoor.d.aq.rl",    AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOOR};
+"amoxor.d.aq.rl",   AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOXOR};
+"amomax.d.aq.rl",   AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMAX};
+"amomin.d.aq.rl",   AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMIN};
+"amomaxu.d.aq.rl",  AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMAXU};
+"amominu.d.aq.rl",  AMO {width=RISCVDOUBLE; aq=true; rl=true; op=RISCVAMOMINU};
diff --git a/risc-v/hgen/map.hgen b/risc-v/hgen/map.hgen
index 639a68bd..91eecc56 100644
--- a/risc-v/hgen/map.hgen
+++ b/risc-v/hgen/map.hgen
@@ -12,3 +12,4 @@
 | `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 5b000725..4440ffda 100644
--- a/risc-v/hgen/parser.hgen
+++ b/risc-v/hgen/parser.hgen
@@ -40,3 +40,5 @@
   { `RISCVLoadRes($1.aq, $1.rl, $5, $1.width, $2) }
 | STORECON reg COMMA reg COMMA LPAR reg RPAR
   { `RISCVStoreCon($1.aq, $1.rl, $4, $7, $1.width, $2) }
+| AMO reg COMMA reg COMMA LPAR reg RPAR
+  { `RISCVAMO($1.op, $1.aq, $1.rl, $4, $7, $1.width, $2) }
diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen
index 0b6548ea..b5068c71 100644
--- a/risc-v/hgen/pretty.hgen
+++ b/risc-v/hgen/pretty.hgen
@@ -31,3 +31,10 @@
                                       (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 61477f43..bec35203 100644
--- a/risc-v/hgen/sail_trans_out.hgen
+++ b/risc-v/hgen/sail_trans_out.hgen
@@ -19,3 +19,5 @@
                                   -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
 | ("STORECON", [aq; rl; rs2; rs1; width; rd])
                                   -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
+| ("AMO", [op; aq; rl; rs2; rs1; width; rd])
+                                  -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
index f84ed1fa..662b1044 100644
--- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
+++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -19,3 +19,5 @@
                               -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
 | STORECON( aq, rl, rs2, rs1, width, rd)
                               -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
+| AMO( op, aq, rl, rs2, rs1, width, rd)
+                              -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
diff --git a/risc-v/hgen/shallow_types_to_herdtools_types.hgen b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
index a891d7d0..03b8820c 100644
--- a/risc-v/hgen/shallow_types_to_herdtools_types.hgen
+++ b/risc-v/hgen/shallow_types_to_herdtools_types.hgen
@@ -53,6 +53,17 @@ let translate_out_ropw op = match op with
   | SRLW  -> RISCVSRLW
   | SRAW  -> RISCVSRAW
 
+let translate_out_amoop op = match op with
+  | AMOSWAP -> RISCVAMOSWAP
+  | AMOADD  -> RISCVAMOADD
+  | AMOXOR  -> RISCVAMOXOR
+  | AMOAND  -> RISCVAMOAND
+  | AMOOR   -> RISCVAMOOR
+  | AMOMIN  -> RISCVAMOMIN
+  | AMOMAX  -> RISCVAMOMAX
+  | AMOMINU -> RISCVAMOMINU
+  | AMOMAXU -> RISCVAMOMAXU
+
 let translate_out_wordWidth op = match op with
   | BYTE   -> RISCVBYTE  
   | HALF   -> RISCVHALF  
diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen
index 242a7173..9b469a27 100644
--- a/risc-v/hgen/token_types.hgen
+++ b/risc-v/hgen/token_types.hgen
@@ -14,5 +14,6 @@ type token_FENCE    = unit
 type token_FENCEI   = unit
 type token_LoadRes  = {width : wordWidth; aq: bool; rl: bool }
 type token_StoreCon = {width : wordWidth; aq: bool; rl: bool }
+type token_AMO      = {width : wordWidth; aq: bool; rl: bool; op: riscvAmoop }
 
 type token_FENCEOPTION = Fence_R | Fence_W | Fence_RW
diff --git a/risc-v/hgen/tokens.hgen b/risc-v/hgen/tokens.hgen
index 449be0f0..b0cf1d88 100644
--- a/risc-v/hgen/tokens.hgen
+++ b/risc-v/hgen/tokens.hgen
@@ -15,3 +15,4 @@
 %token <RISCVHGenBase.token_FENCEI>   FENCEI
 %token <RISCVHGenBase.token_LoadRes>  LOADRES
 %token <RISCVHGenBase.token_StoreCon> STORECON
+%token <RISCVHGenBase.token_AMO> AMO
diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen
index 6d10471c..12da62d8 100644
--- a/risc-v/hgen/trans_sail.hgen
+++ b/risc-v/hgen/trans_sail.hgen
@@ -137,3 +137,15 @@
       translate_reg "rd" rd;
     ],
     [])
+| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) ->
+   ("AMO",
+    [
+      translate_amoop "op" op;
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_width "width" width;
+      translate_reg "rd" rd;
+    ],
+    [])
diff --git a/risc-v/hgen/types.hgen b/risc-v/hgen/types.hgen
index 1471812c..83deb4a2 100644
--- a/risc-v/hgen/types.hgen
+++ b/risc-v/hgen/types.hgen
@@ -140,6 +140,38 @@ let pp_riscv_store_conditional_op (aq, rl, width) =
   (if aq then ".aq" else "") ^
   (if rl then ".rl" else "")
 
+type riscvAmoop =
+  | RISCVAMOSWAP
+  | RISCVAMOADD
+  | RISCVAMOXOR
+  | RISCVAMOAND
+  | RISCVAMOOR
+  | RISCVAMOMIN
+  | RISCVAMOMAX
+  | RISCVAMOMINU
+  | RISCVAMOMAXU
+
+let pp_riscv_amo_op (op, aq, rl, width) =
+  "amo" ^
+  begin match op with
+  | RISCVAMOSWAP -> "swap"
+  | RISCVAMOADD  -> "add"
+  | RISCVAMOXOR  -> "xor"
+  | RISCVAMOAND  -> "and"
+  | RISCVAMOOR   -> "or"
+  | RISCVAMOMIN  -> "min"
+  | RISCVAMOMAX  -> "max"
+  | RISCVAMOMINU -> "minu"
+  | RISCVAMOMAXU -> "maxu"
+  end ^
+  begin match width with
+  | RISCVWORD   -> ".w"
+  | RISCVDOUBLE -> ".d"
+  | _ -> assert false
+  end ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
 let pp_riscv_fence_option = function
   | 0b0011 -> "rw"
   | 0b0010 -> "r"
diff --git a/risc-v/hgen/types_sail_trans_out.hgen b/risc-v/hgen/types_sail_trans_out.hgen
index e22110d0..66a2020c 100644
--- a/risc-v/hgen/types_sail_trans_out.hgen
+++ b/risc-v/hgen/types_sail_trans_out.hgen
@@ -84,3 +84,15 @@ let translate_out_ropw op = match translate_out_enum op with
 | 3 -> RISCVSRLW
 | 4 -> RISCVSRAW
 | _ -> failwith "Unknown ropw in sail translate out"
+
+let translate_out_amoop op = match translate_out_enum op with
+| 0 -> RISCVAMOSWAP
+| 1 -> RISCVAMOADD
+| 2 -> RISCVAMOXOR
+| 3 -> RISCVAMOAND
+| 4 -> RISCVAMOOR
+| 5 -> RISCVAMOMIN
+| 6 -> RISCVAMOMAX
+| 7 -> RISCVAMOMINU
+| 8 -> RISCVAMOMAXU
+| _ -> failwith "Unknown amoop in sail translate out"
diff --git a/risc-v/hgen/types_trans_sail.hgen b/risc-v/hgen/types_trans_sail.hgen
index 1bf174fa..7528a522 100644
--- a/risc-v/hgen/types_trans_sail.hgen
+++ b/risc-v/hgen/types_trans_sail.hgen
@@ -16,6 +16,7 @@ let translate_iop = translate_enum [RISCVADDI; RISCVSLTI; RISCVSLTIU; RISCVXORI;
 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)))
diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail
index 1d1867c4..5b749656 100644
--- a/risc-v/riscv.sail
+++ b/risc-v/riscv.sail
@@ -40,7 +40,10 @@ register (bit[64]) PC
 register (bit[64]) nextPC
 
 let (vector <0, 32, inc, (register<(regval)>)>) GPRs =
-  [x0, x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31]
+  [ x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14,
+    x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27,
+    x28, x29, x30, x31
+  ]
 
 function (regval) rGPR ((regno) r) = 
     if (r == 0) then 
@@ -71,35 +74,29 @@ 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|]) -> 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|] , 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|] , 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|]) -> 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 -> bool effect {exmem} speculate_conditional_success
 
 val extern unit -> unit effect { barr } MEM_fence_rw_rw
 val extern unit -> unit effect { barr } MEM_fence_r_rw
@@ -122,6 +119,9 @@ typedef iop = enumerate {ADDI; SLTI; SLTIU; XORI; ORI; ANDI} (* immediate ops *)
 typedef sop = enumerate {SLLI; SRLI; SRAI} (* shift ops *)
 typedef rop = enumerate {ADD; SUB; SLL; SLT; SLTU; XOR; SRL; SRA; OR; AND} (* reg-reg ops *)
 typedef ropw = enumerate {ADDW; SUBW; SLLW; SRLW; SRAW} (* reg-reg 32-bit ops *)
+typedef amoop = enumerate {AMOSWAP; AMOADD; AMOXOR; AMOAND; AMOOR;
+    AMOMIN; AMOMAX; AMOMINU; AMOMAXU} (* AMO ops *)
+
 
 typedef word_width = enumerate {BYTE; HALF; WORD; DOUBLE}
 
@@ -279,17 +279,17 @@ function clause decode ((bit[7]) imm7 : (regno) rs2 : (regno) rs1 : 0b011 : (bit
 function clause execute (STORE(imm, rs2, rs1, width, rl)) =
     let (bit[64]) addr = rGPR(rs1) + EXTS(imm) in {
       switch (width) {
-        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)
+        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)
       };
       let rs2_val = rGPR(rs2) in
       switch (width) {
-        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)
+        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)
       }
     }
 
@@ -376,21 +376,77 @@ function clause decode (0b00011 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b01
 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]));
+
   (bit[64]) addr := rGPR(rs1);
   switch width {
-    case WORD   -> mem_write_conditional_ea(addr, 4, rl)
-    case DOUBLE -> mem_write_conditional_ea(addr, 8, rl)
+    case WORD   -> mem_write_ea(addr, 4, rl, true)
+    case DOUBLE -> mem_write_ea(addr, 8, rl, true)
   };
   rs2_val := rGPR(rs2);
-  (bool) success :=
-    switch width {
-      case WORD   -> mem_write_conditional_value(addr, 4, rs2_val[31..0], rl)
-      case DOUBLE -> mem_write_conditional_value(addr, 8, rs2_val, rl)
-    };
-  if success then wGPR(rd, 0)
-  else wGPR(rd, 1);
+  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)
+  };
 }
 
+union ast member (amoop, bool, bool, regno, regno, word_width, regno) AMO
+
+function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b00001 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOSWAP, aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOADD , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b00000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOADD , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOXOR , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b00100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOXOR , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOAND , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b01100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOAND , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOOR  , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b01000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOOR  , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMIN , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b10000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMIN , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMAX , aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b10100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMAX , aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMINU, aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b11000 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMINU, aq, rl, rs2, rs1, DOUBLE, rd))
+function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b010 : (regno) rd : 0b0101111) = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, WORD,   rd))
+function clause decode (0b11100 : [aq] : [rl] : (regno) rs2 : (regno) rs1 : 0b011 : (regno) rd : 0b0101111) = Some(AMO(AMOMAXU, aq, rl, rs2, rs1, DOUBLE, rd))
+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)
+  };
+
+  (bit[64]) loaded :=
+    switch (width) {
+      case WORD   -> EXTS(mem_read(addr, 4, aq, true))
+      case DOUBLE -> mem_read(addr, 8, aq, true)
+    };
+  wGPR(rd, loaded);
+
+  (bit[64]) rs2_val := rGPR(rs2);
+  (bit[64]) result :=
+    switch(op) {
+      case AMOSWAP -> rs2_val
+      case AMOADD  -> rs2_val + loaded
+      case AMOXOR  -> rs2_val ^ loaded
+      case AMOAND  -> rs2_val & loaded
+      case AMOOR   -> rs2_val | loaded
+
+      case AMOMIN  -> (bit[64]) (min(signed(rs2_val),   signed(loaded)))
+      case AMOMAX  -> (bit[64]) (max(signed(rs2_val),   signed(loaded)))
+      case AMOMINU -> (bit[64]) (min(unsigned(rs2_val), unsigned(loaded)))
+      case AMOMAXU -> (bit[64]) (max(unsigned(rs2_val), unsigned(loaded)))
+    };
+
+  switch (width) {
+    case WORD   -> mem_write_value(addr, 4, result[31..0], rl, true)
+    case DOUBLE -> mem_write_value(addr, 8, result,        rl, true)
+  };
+}
 
 function clause decode _ = None
 
diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem
index 59e3cd4a..62a7bb91 100644
--- a/risc-v/riscv_extras.lem
+++ b/risc-v/riscv_extras.lem
@@ -51,20 +51,27 @@ let memory_eas : memory_write_eas =
 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
+    ("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
+                            (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)))));
+                             (IState (Interp.add_answer_to_stack interp bit) context))))); *)
   ]
 
+let speculate_conditional_success : excl_res =
+  let f = fun (IState interp context) b ->
+    let bool_res = 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 bool_res) context
+  in
+  Just ("speculate_conditional_success", (ER (Just f)))
+
 let barrier_functions =
   [ ("MEM_fence_rw_rw", Barrier_RISCV_rw_rw);
     ("MEM_fence_r_rw",  Barrier_RISCV_r_rw);
diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem
index 6bfc2490..3f04f9a2 100644
--- a/risc-v/riscv_extras_embed.lem
+++ b/risc-v/riscv_extras_embed.lem
@@ -26,13 +26,15 @@ let MEMea_conditional_release (addr,size) = write_mem_ea Write_RISCV_conditional
 
 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
+val MEMval_conditional         : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_conditional_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 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)
+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 speculate_conditional_success () = excl_result () >>= 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 0fca7709..dabd4d12 100644
--- a/risc-v/riscv_extras_embed_sequential.lem
+++ b/risc-v/riscv_extras_embed_sequential.lem
@@ -26,13 +26,15 @@ let MEMea_conditional_release (addr,size) = write_mem_ea Write_RISCV_conditional
 
 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
+val MEMval_conditional         : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_conditional_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 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)
+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 speculate_conditional_success () = excl_result () >>= 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 20da3da3..e6813c37 100644
--- a/risc-v/riscv_regfp.sail
+++ b/risc-v/riscv_regfp.sail
@@ -103,12 +103,27 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
             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;
+            if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
+
             ik := switch (aq, rl) {
               case (false, false) -> IK_mem_write (Write_RISCV_conditional)
               case (false, true)  -> IK_mem_write (Write_RISCV_conditional_release)
               case (true,  _)     -> exit "not implemented"
             };
      }
+     case (AMO( op, aq, rl, rs2, rs1, width, rd)) -> {
+            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;
+            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)
+            };
+     }
   };
   (iR,oR,aR,Nias,Dia,ik)
 }
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 6a9a77a1..411ad3fc 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -1416,6 +1416,41 @@ let interp_instruction_analysis
 
           if forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind then
             inst_kind
+
+          else if
+            (forall (inst_kind' MEM (inst_kind :: inst_kinds)).
+                match inst_kind' with
+                | IK_mem_read _  -> true
+                | IK_mem_write _ -> true
+                | IK_mem_rmw _   -> false
+                | IK_barrier _   -> false
+                | IK_cond_branch -> false
+                | IK_trans _     -> false
+                | IK_simple      -> false
+                end) &&
+            (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
+                match inst_kind' with
+                | IK_mem_read _  -> true
+                | _              -> false
+                end) &&
+            (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
+                match inst_kind' with
+                | IK_mem_write _ -> true
+                | _              -> false
+                end)
+          then
+            match
+              List.partition
+                (function IK_mem_read _ -> true | _ -> false end)
+                (inst_kind :: inst_kinds)
+            with
+            | ((IK_mem_read r) :: rs, (IK_mem_write w) :: ws) ->
+                let () = ensure (forall (r' MEM rs). r' = IK_mem_read r) "more than one kind of read" in
+                let () = ensure (forall (w' MEM ws). w' = IK_mem_write w) "more than one kind of write" in
+                IK_mem_rmw (r, w)
+            | _ -> fail
+            end
+
           (* the TSTART instruction can also be aborted so it will have two kinds of events *)
           else if (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
                         inst_kind' = IK_trans Transaction_start) &&
@@ -1424,7 +1459,9 @@ let interp_instruction_analysis
                         || inst_kind' = IK_trans Transaction_abort)
           then
             IK_trans Transaction_start
-          else failwith "multiple instruction kinds"
+
+          else
+            failwith "multiple instruction kinds"
     end in
 
   (regs_in, regs_out, regs_feeding_address, nias, dia, inst_kind)
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 3886f919..721c0226 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -552,26 +552,27 @@ instance (Show trans_kind)
 end
 
 type instruction_kind = 
-  | IK_barrier of barrier_kind 
-  | IK_mem_read of read_kind 
+  | IK_barrier   of barrier_kind
+  | IK_mem_read  of read_kind
   | IK_mem_write of write_kind
-(* SS reinstating cond_branches
-at present branches are not distinguished in the instruction_kind;
-they just have particular nias (and will be IK_simple *)
-  | IK_cond_branch 
-(*  | IK_uncond_branch *)
-  | IK_trans of trans_kind
+  | IK_mem_rmw   of (read_kind * write_kind)
+  | IK_cond_branch
+  (* unconditional branches are not distinguished in the instruction_kind;
+  they just have particular nias (and will be IK_simple *)
+  (* | IK_uncond_branch *)
+  | IK_trans     of trans_kind
   | IK_simple
 
 
 instance (Show instruction_kind)
   let show = function
     | IK_barrier barrier_kind -> "IK_barrier " ^ (show barrier_kind)
-    | IK_mem_read read_kind -> "IK_mem_read " ^ (show read_kind)
+    | IK_mem_read read_kind   -> "IK_mem_read " ^ (show read_kind)
     | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind)
-    | IK_cond_branch -> "IK_cond_branch"
-    | IK_trans trans_kind -> "IK_trans " ^ (show trans_kind)
-    | IK_simple -> "IK_simple"
+    | IK_mem_rmw (r, w)       -> "IK_mem_rmw " ^ (show r) ^ " " ^ (show w)
+    | IK_cond_branch          -> "IK_cond_branch"
+    | IK_trans trans_kind     -> "IK_trans " ^ (show trans_kind)
+    | IK_simple               -> "IK_simple"
   end
 end