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