diff options
| author | Alastair Reid | 2018-06-26 15:46:57 +0100 |
|---|---|---|
| committer | Alastair Reid | 2018-06-26 15:50:19 +0100 |
| commit | 68703bf244a10e5281625b0cb1d620d78d6c5cbb (patch) | |
| tree | a55530063bea7fca5ea85e94eeabe55411498c39 /aarch64 | |
| parent | 23f4e803332f4cbbab356f580f09beb4fb8be656 (diff) | |
RTS: implement sleep primitives
Note that an alternative implementation choice is just to implement
them as SAIL functions manipulating a global variable.
Not sure which is better.
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/prelude.sail | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail index 097dc7d9..89a93e11 100644 --- a/aarch64/prelude.sail +++ b/aarch64/prelude.sail @@ -349,3 +349,10 @@ union option ('a : Type) = { Some : 'a } */ + +val __SleepRequest = {ocaml: "sleep_request", lem: "sleep_request", smt: "sleep_request", interpreter: "sleep_request", c: "sleep_request"}: unit -> unit effect {escape, rreg, undef} + +val __WakeupRequest = {ocaml: "wakeup_request", lem: "wakeup_request", smt: "wakeup_request", interpreter: "wakeup_request", c: "wakeup_request"}: unit -> unit effect {escape, rreg, undef} + +val __Sleeping = {ocaml: "sleeping", lem: "sleeping", smt: "sleeping", interpreter: "sleeping", c: "sleeping"}: unit -> bool effect {escape, rreg, undef} + |