From 68703bf244a10e5281625b0cb1d620d78d6c5cbb Mon Sep 17 00:00:00 2001
From: Alastair Reid
Date: Tue, 26 Jun 2018 15:46:57 +0100
Subject: 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.
---
 aarch64/prelude.sail | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'aarch64')

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}
+
-- 
cgit v1.2.3