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