diff options
| -rw-r--r-- | riscv/platform.ml | 17 | ||||
| -rw-r--r-- | riscv/riscv.sail | 117 | ||||
| -rw-r--r-- | riscv/riscv_extras.lem | 7 | ||||
| -rw-r--r-- | riscv/riscv_extras_sequential.lem | 7 | ||||
| -rw-r--r-- | riscv/riscv_mem.sail | 3 | ||||
| -rw-r--r-- | riscv/riscv_sys.sail | 24 |
6 files changed, 133 insertions, 42 deletions
diff --git a/riscv/platform.ml b/riscv/platform.ml index 0366e601..ddae4840 100644 --- a/riscv/platform.ml +++ b/riscv/platform.ml @@ -97,7 +97,24 @@ let clint_size () = bits_of_int64 P.clint_size let insns_per_tick () = Big_int.of_int P.insns_per_tick +(* load reservation *) + +let reservation = ref "none" (* shouldn't match any valid address *) + +let load_reservation addr = + Printf.eprintf "reservation <- %s\n" (!reservation); + reservation := string_of_bits addr + +let match_reservation addr = + Printf.eprintf "reservation: %s, key=%s\n" (!reservation) (string_of_bits addr); + string_of_bits addr = !reservation + +let cancel_reservation () = + Printf.eprintf "reservation <- none\n"; + reservation := "none" + (* terminal I/O *) + let term_write char_bits = let big_char = Big_int.bitwise_and (uint char_bits) (Big_int.of_int 255) in P.term_write (char_of_int (Big_int.to_int big_char)) diff --git a/riscv/riscv.sail b/riscv/riscv.sail index 35f3c625..687531c1 100644 --- a/riscv/riscv.sail +++ b/riscv/riscv.sail @@ -328,7 +328,7 @@ function extend_value(is_unsigned, value) = match (value) { val process_load : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg} function process_load(rd, addr, value, is_unsigned) = - match (extend_value(is_unsigned, value)) { + match extend_value(is_unsigned, value) { MemValue(result) => { X(rd) = result; true }, MemException(e) => { handle_mem_exception(addr, e); false } } @@ -913,20 +913,43 @@ union clause ast = LOADRES : (bool, bool, regbits, word_width, regbits) mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 -val process_loadres : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> unit +/* We could set load-reservations on physical or virtual addresses. + * For now we set them on virtual addresses, since it makes the + * sequential model of SC a bit simpler, at the cost of an explicit + * call to load_reservation in LR and cancel_reservation in SC. + */ -function clause execute(LOADRES(aq, rl, rs1, width, rd)) = - let vaddr : xlenbits = X(rs1) in - match translateAddr(vaddr, Read, Data) { - TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, - TR_Address(addr) => - match width { - WORD => process_load(rd, addr, mem_read(addr, 4, aq, rl, true), false), - DOUBLE => process_load(rd, addr, mem_read(addr, 8, aq, rl, true), false), - _ => internal_error("LOADRES expected WORD or DOUBLE") - } +val process_loadres : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg} +function process_loadres(rd, addr, value, is_unsigned) = + match extend_value(is_unsigned, value) { + MemValue(result) => { X(rd) = result; load_reservation(addr); true }, + MemException(e) => { handle_mem_exception(addr, e); false } } +function clause execute(LOADRES(aq, rl, rs1, width, rd)) = + let vaddr : xlenbits = X(rs1) in + let aligned : bool = + /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt + * to treat them as valid here; otherwise we'd need to throw an internal_error. + * May need to revisit for latex output. + */ + match width { + BYTE => true, + HALF => vaddr[0] == 0b0, + WORD => vaddr[1..0] == 0b00, + DOUBLE => vaddr[2..0] == 0b000 + } in + if (~ (aligned)) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false } + else match translateAddr(vaddr, Read, Data) { + TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, + TR_Address(addr) => + match width { + WORD => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false), + DOUBLE => process_loadres(rd, vaddr, mem_read(addr, 8, aq, rl, true), false), + _ => internal_error("LOADRES expected WORD or DOUBLE") + } + } function clause print_insn (LOADRES(aq, rl, rs1, width, rd)) = "lr" ^ lrsc_width_str(width) ^ aqrl_str(aq, rl) ^ " " ^ rd ^ ", " ^ rs1 @@ -941,31 +964,51 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) <-> 0b00011 @ bool_ /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { - status : bits(1) = if speculate_conditional_success() then 0b0 else 0b1; - X(rd) = EXTZ(status); - - if status == 0b1 then true else { - vaddr : xlenbits = X(rs1); - match translateAddr(vaddr, Write, Data) { - TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, - TR_Address(addr) => { - let eares : MemoryOpResult(unit) = match width { - WORD => mem_write_ea(addr, 4, aq, rl, true), - DOUBLE => mem_write_ea(addr, 8, aq, rl, true), - _ => internal_error("STORECON expected word or double") - }; - match (eares) { - MemException(e) => { handle_mem_exception(addr, e); false }, - MemValue(_) => { - rs2_val = X(rs2); - let res : MemoryOpResult(unit) = match width { - WORD => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true), - DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, true), - _ => internal_error("STORECON expected word or double") - } in - match (res) { - MemValue(_) => true, - MemException(e) => { handle_mem_exception(addr, e); false } + /* RMEM FIXME: This definition differs from the Sail1 version: + * rs1 is read *before* speculate_conditional_success + * (called via match_reservation), partly due to the current api of + * match_reservation. Reverting back to the weaker Sail1 version + * will require changes to the API for the ghost reservation state. + */ + vaddr : xlenbits = X(rs1); + let aligned : bool = + /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt + * to treat them as valid here; otherwise we'd need to throw an internal_error. + * May need to revisit for latex output. + */ + match width { + BYTE => true, + HALF => vaddr[0] == 0b0, + WORD => vaddr[1..0] == 0b00, + DOUBLE => vaddr[2..0] == 0b000 + } in + if (~ (aligned)) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false } + else { + if match_reservation(vaddr) == false + then { X(rd) = EXTZ(0b1); true } + else { + match translateAddr(vaddr, Write, Data) { + TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, + TR_Address(addr) => { + let eares : MemoryOpResult(unit) = match width { + WORD => mem_write_ea(addr, 4, aq, rl, true), + DOUBLE => mem_write_ea(addr, 8, aq, rl, true), + _ => internal_error("STORECON expected word or double") + }; + match (eares) { + MemException(e) => { handle_mem_exception(addr, e); false }, + MemValue(_) => { + rs2_val = X(rs2); + let res : MemoryOpResult(unit) = match width { + WORD => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true), + DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, true), + _ => internal_error("STORECON expected word or double") + }; + match (res) { + MemValue(_) => { X(rd) = EXTZ(0b0); cancel_reservation(); true }, + MemException(e) => { handle_mem_exception(addr, e); false } + } } } } diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem index b3d84df6..88ac3e6f 100644 --- a/riscv/riscv_extras.lem +++ b/riscv/riscv_extras.lem @@ -45,7 +45,12 @@ val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => let read_ram addrsize size hexRAM address = read_mem Read_plain address size -let speculate_conditional_success () = excl_result () +val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit +let load_reservation addr = () + +let speculate_conditional_success _ = excl_result () + +let cancel_reservation () = () val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_ram_base () = wordFromInteger 0 diff --git a/riscv/riscv_extras_sequential.lem b/riscv/riscv_extras_sequential.lem index b3d84df6..88ac3e6f 100644 --- a/riscv/riscv_extras_sequential.lem +++ b/riscv/riscv_extras_sequential.lem @@ -45,7 +45,12 @@ val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => let read_ram addrsize size hexRAM address = read_mem Read_plain address size -let speculate_conditional_success () = excl_result () +val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit +let load_reservation addr = () + +let speculate_conditional_success _ = excl_result () + +let cancel_reservation () = () val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_ram_base () = wordFromInteger 0 diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail index 9ead3aeb..008c1642 100644 --- a/riscv/riscv_mem.sail +++ b/riscv/riscv_mem.sail @@ -92,6 +92,7 @@ function phys_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) - else MemException(E_SAMO_Access_Fault) } +// dispatches to MMIO regions or physical memory regions depending on physical memory map function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(unit) = if within_mmio_writable(addr, width) then mmio_write(addr, width, data) @@ -133,8 +134,6 @@ function mem_write_value (addr, width, value, aq, rl, con) = { } } -val "speculate_conditional_success" : unit -> bool effect {exmem} - val MEM_fence_rw_rw = {ocaml: "skip", lem: "MEM_fence_rw_rw"} : unit -> unit effect {barr} val MEM_fence_r_rw = {ocaml: "skip", lem: "MEM_fence_r_rw"} : unit -> unit effect {barr} val MEM_fence_r_r = {ocaml: "skip", lem: "MEM_fence_r_r"} : unit -> unit effect {barr} diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail index bb3d13db..e8128edf 100644 --- a/riscv/riscv_sys.sail +++ b/riscv/riscv_sys.sail @@ -363,7 +363,6 @@ function legalize_sedeleg(s : Sedeleg, v : xlenbits) -> Sedeleg = { Mk_Sedeleg(EXTZ(v[8..0])) } -/* TODO: handle views for interrupt delegation */ bitfield Sinterrupts : bits(64) = { SEI : 9, /* external interrupts */ UEI : 8, @@ -670,6 +669,24 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool = & check_TVM_SATP(csr, p) & check_Counteren(csr, p) +/* Reservation handling for LR/SC. + * + * The reservation state is maintained external to the model since the + * reservation behavior is platform-specific anyway and maintaining + * this state outside the model simplifies the concurrency analysis. + * + * These are externs are defined here in the system module since + * we currently perform reservation cancellation on privilege level + * transition. Ideally, the platform should get more visibility into + * where cancellation can be performed. + */ + +val load_reservation = {ocaml: "Platform.load_reservation", lem: "load_reservation"} : xlenbits -> unit + +val match_reservation = {ocaml: "Platform.match_reservation", lem: "speculate_conditional_success"} : xlenbits -> bool effect {exmem} + +val cancel_reservation = {ocaml: "Platform.cancel_reservation", lem: "cancel_reservation"} : unit -> unit + /* Exception delegation: given an exception and the privilege at which * it occured, returns the privilege at which it should be handled. */ @@ -776,6 +793,7 @@ union ctl_result = { function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits)) -> xlenbits = { print("handling " ^ (if intr then "int#" else "exc#") ^ BitStr(c) ^ " at priv " ^ del_priv ^ " with tval " ^ BitStr(tval(info))); + cancel_reservation(); match (del_priv) { Machine => { mcause->IsInterrupt() = intr; @@ -840,6 +858,8 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result, cur_privilege = privLevel_of_bits(mstatus.MPP()); mstatus->MPP() = privLevel_to_bits(User); + cancel_reservation(); + print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log print("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege); mepc @@ -851,6 +871,8 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result, cur_privilege = if mstatus.SPP() == true then Supervisor else User; mstatus->SPP() = false; + cancel_reservation(); + print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log print("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege); sepc |