RISC-V load-reserved and store-conditional

15 files changed, 159 insertions, 3 deletions

diff --git a/risc-v/hgen/ast.hgen b/risc-v/hgen/ast.hgen
index d5e4b45b..a0a59e4a 100644
--- a/risc-v/hgen/ast.hgen
+++ b/risc-v/hgen/ast.hgen
@@ -11,3 +11,5 @@
 | `RISCVSHIFTW of bit5 * reg * reg * riscvSop
 | `RISCVRTYPEW of reg * reg * reg * riscvRopw
 | `RISCVFENCE of bit4 * bit4
+| `RISCVLoadRes of bool * bool * reg * wordWidth * reg
+| `RISCVStoreCon of bool * bool * reg * reg * wordWidth * reg
diff --git a/risc-v/hgen/fold.hgen b/risc-v/hgen/fold.hgen
index 376ab19f..4cbaf779 100644
--- a/risc-v/hgen/fold.hgen
+++ b/risc-v/hgen/fold.hgen
@@ -11,3 +11,5 @@
 | `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)))
diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
index d756d3d0..ffea1575 100644
--- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
+++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -58,5 +58,18 @@
       translate_reg "rd" rd,
       translate_ropw op)
 | `RISCVFENCE(pred, succ) -> FENCE(
-  translate_imm4 "pred" pred,
-  translate_imm4 "succ" succ)
+      translate_imm4 "pred" pred,
+      translate_imm4 "succ" succ)
+| `RISCVLoadRes(aq, rl, rs1, width, rd) -> LOADRES(
+      translate_bool "aq" aq,
+      translate_bool "rl" rl,
+      translate_reg "rs1" rs1,
+      translate_wordWidth width,
+      translate_reg "rd" rd)
+| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> STORECON(
+      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/lexer.hgen b/risc-v/hgen/lexer.hgen
index 40481f75..abc0ff82 100644
--- a/risc-v/hgen/lexer.hgen
+++ b/risc-v/hgen/lexer.hgen
@@ -75,3 +75,13 @@
 "r",  FENCEOPTION Fence_R;
 "w",  FENCEOPTION Fence_W;
 "rw", FENCEOPTION Fence_RW;
+
+"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};
+
+"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};
diff --git a/risc-v/hgen/map.hgen b/risc-v/hgen/map.hgen
index edd376b4..639a68bd 100644
--- a/risc-v/hgen/map.hgen
+++ b/risc-v/hgen/map.hgen
@@ -10,3 +10,5 @@
 | `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)
diff --git a/risc-v/hgen/parser.hgen b/risc-v/hgen/parser.hgen
index cb31f5a9..d077c2df 100644
--- a/risc-v/hgen/parser.hgen
+++ b/risc-v/hgen/parser.hgen
@@ -34,3 +34,7 @@
     | (Fence_W,  Fence_R)  -> failwith "'fence w,r' is not supported"
     | (Fence_W,  Fence_W)  -> failwith "'fence w,w' is not supported"
   }
+| LOADRES reg COMMA LPAR reg RPAR
+  { `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) }
diff --git a/risc-v/hgen/pretty.hgen b/risc-v/hgen/pretty.hgen
index cce77641..b4516b16 100644
--- a/risc-v/hgen/pretty.hgen
+++ b/risc-v/hgen/pretty.hgen
@@ -15,3 +15,18 @@
 | `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)
+| `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)
diff --git a/risc-v/hgen/sail_trans_out.hgen b/risc-v/hgen/sail_trans_out.hgen
index 45445a25..f216180a 100644
--- a/risc-v/hgen/sail_trans_out.hgen
+++ b/risc-v/hgen/sail_trans_out.hgen
@@ -14,3 +14,7 @@
 | ("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)
 | ("FENCE", [pred; succ])         -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
+| ("LOADRES", [aq; rl; rs1; width; rd])
+                                  -> `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)
diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
index abfc0412..01d8dded 100644
--- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
+++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -14,3 +14,7 @@
 | 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)
 | FENCE( pred, succ)          -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
+| LOADRES( aq, rl, rs1, width, rd)
+                              -> `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)
diff --git a/risc-v/hgen/token_types.hgen b/risc-v/hgen/token_types.hgen
index 03dde52b..c0ef8445 100644
--- a/risc-v/hgen/token_types.hgen
+++ b/risc-v/hgen/token_types.hgen
@@ -11,5 +11,7 @@ type token_ADDIW    = unit
 type token_SHIFTW   = {op : riscvSop }
 type token_RTYPEW   = {op : riscvRopw }
 type token_FENCE    = unit
+type token_LoadRes  = {width : wordWidth; aq: bool; rl: bool }
+type token_StoreCon = {width : wordWidth; aq: bool; rl: bool }
 
 type token_FENCEOPTION = Fence_R | Fence_W | Fence_RW
diff --git a/risc-v/hgen/tokens.hgen b/risc-v/hgen/tokens.hgen
index f952cf77..1276fd68 100644
--- a/risc-v/hgen/tokens.hgen
+++ b/risc-v/hgen/tokens.hgen
@@ -12,3 +12,5 @@
 %token <RISCVHGenBase.token_RTYPEW>   RTYPEW  
 %token <RISCVHGenBase.token_FENCE>    FENCE
 %token <RISCVHGenBase.token_FENCEOPTION> FENCEOPTION
+%token <RISCVHGenBase.token_LoadRes>  LOADRES
+%token <RISCVHGenBase.token_StoreCon> STORECON
diff --git a/risc-v/hgen/trans_sail.hgen b/risc-v/hgen/trans_sail.hgen
index 9fb3b546..4d568fe8 100644
--- a/risc-v/hgen/trans_sail.hgen
+++ b/risc-v/hgen/trans_sail.hgen
@@ -112,3 +112,24 @@
      translate_imm4 "succ" succ;
   ], 
   [])
+| `RISCVLoadRes(aq, rl, rs1, width, rd) ->
+   ("LOADRES",
+    [
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
+      translate_reg "rs1" rs1;
+      translate_width "width" width;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) ->
+   ("STORECON",
+    [
+      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 180e0b37..1471812c 100644
--- a/risc-v/hgen/types.hgen
+++ b/risc-v/hgen/types.hgen
@@ -120,6 +120,26 @@ let pp_riscv_store_op (width, rl) =
   end
   ^ (if rl then ".rl" else "")
 
+let pp_riscv_load_reserved_op (aq, rl, width) =
+  "lr" ^
+  begin match width with
+  | RISCVWORD   -> ".w"
+  | RISCVDOUBLE -> ".d"
+  | _ -> assert false
+  end ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
+let pp_riscv_store_conditional_op (aq, rl, width) =
+  "sc" ^
+  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/riscv.sail b/risc-v/riscv.sail
index 3b42b94c..b5a25578 100644
--- a/risc-v/riscv.sail
+++ b/risc-v/riscv.sail
@@ -353,6 +353,41 @@ union ast member unit EBREAK
 function clause decode (0b000000000001 : 0b00000 : 0b000 : 0b00000 : 0b1110011) = Some(EBREAK ())
 function clause execute EBREAK = { exit () }
 
+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)
+  }
+
+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[64]) addr := rGPR(rs1);
+  switch width {
+    case WORD   -> mem_write_conditional_ea(addr, 4, rl)
+    case DOUBLE -> mem_write_conditional_ea(addr, 8, rl)
+  };
+  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);
+}
+
 
 function clause decode _ = None
 
diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail
index 2c94012e..1cfc68d7 100644
--- a/risc-v/riscv_regfp.sail
+++ b/risc-v/riscv_regfp.sail
@@ -82,7 +82,27 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
               case (0b0011, 0b0011) -> IK_barrier (Barrier_RISCV_rw_rw)
               case (0b0010, 0b0011) -> IK_barrier (Barrier_RISCV_r_rw)
               case (0b0011, 0b0001) -> IK_barrier (Barrier_RISCV_rw_w)
-              case _ -> exit "unsupported fence"
+              case _ -> exit "not implemented"
+            };
+     }
+     case (LOADRES ( aq, rl, rs1, width, rd)) -> {
+            if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR;
+            if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR;
+            aR := iR;
+            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 (STORECON( 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;
+            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"
             };
      }
   };