aboutsummaryrefslogtreecommitdiff
path: root/model/riscv_sys_control.sail
diff options
context:
space:
mode:
Diffstat (limited to 'model/riscv_sys_control.sail')
-rw-r--r--model/riscv_sys_control.sail10
1 files changed, 4 insertions, 6 deletions
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 48a3d90..4155d66 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -114,13 +114,11 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
* where cancellation can be performed.
*/
-val speculate_conditional = {ocaml: "Platform.speculate_conditional", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool effect {exmem}
+val speculate_conditional = {ocaml: "Platform.speculate_conditional", interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool effect {exmem}
-val load_reservation = {ocaml: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit
-
-val match_reservation = {ocaml: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool
-
-val cancel_reservation = {ocaml: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit
+val load_reservation = {ocaml: "Platform.load_reservation", interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit
+val match_reservation = {ocaml: "Platform.match_reservation", interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool
+val cancel_reservation = {ocaml: "Platform.cancel_reservation", interpreter: "Platform.cancel_reservation", c: "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.