1(*  Title:      Pure/Concurrent/unsynchronized.ML
2    Author:     Makarius
3
4Raw ML references as unsynchronized state variables.
5*)
6
7signature UNSYNCHRONIZED =
8sig
9  datatype ref = datatype ref
10  val := : 'a ref * 'a -> unit
11  val ! : 'a ref -> 'a
12  val change: 'a ref -> ('a -> 'a) -> unit
13  val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b
14  val inc: int ref -> int
15  val dec: int ref -> int
16  val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
17end;
18
19structure Unsynchronized: UNSYNCHRONIZED =
20struct
21
22datatype ref = datatype ref;
23
24val op := = op :=;
25val ! = !;
26
27fun change r f = r := f (! r);
28fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
29
30fun inc i = (i := ! i + (1: int); ! i);
31fun dec i = (i := ! i - (1: int); ! i);
32
33fun setmp flag value f x =
34  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
35    let
36      val orig_value = ! flag;
37      val _ = flag := value;
38      val result = Exn.capture (restore_attributes f) x;
39      val _ = flag := orig_value;
40    in Exn.release result end) ();
41
42end;
43