src/Pure/Concurrent/synchronized.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/synchronized.ML	Mon Oct 13 15:48:40 2008 +0200
@@ -0,0 +1,53 @@
+(*  Title:      Pure/Concurrent/synchronized.ML
+    ID:         $Id$
+    Author:     Fabian Immler and Makarius
+
+State variables with synchronized access.
+*)
+
+signature SYNCHRONIZED =
+sig
+  type 'a var
+  val var: string -> 'a -> 'a var
+  val guarded_change: ('a -> bool) -> ('a -> Time.time option) ->
+    'a var -> (bool -> 'a -> 'b * 'a) -> 'b
+  val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
+  val change: 'a var -> ('a -> 'a) -> unit
+end;
+
+structure Synchronized: SYNCHRONIZED =
+struct
+
+(* state variables *)
+
+datatype 'a var = Var of
+ {name: string,
+  lock: Mutex.mutex,
+  cond: ConditionVar.conditionVar,
+  var: 'a ref};
+
+fun var name x = Var
+ {name = name,
+  lock = Mutex.mutex (),
+  cond = ConditionVar.conditionVar (),
+  var = ref x};
+
+
+(* synchronized access *)
+
+fun guarded_change guard time_limit (Var {name, lock, cond, var}) f =
+  SimpleThread.synchronized name lock (fn () =>
+    let
+      fun check () = guard (! var) orelse
+        (case time_limit (! var) of
+          NONE => (ConditionVar.wait (cond, lock); check ())
+        | SOME t => ConditionVar.waitUntil (cond, lock, t) andalso check ());
+      val ok = check ();
+      val res = change_result var (f ok);
+      val _ = ConditionVar.broadcast cond;
+    in res end);
+
+fun change_result var f = guarded_change (K true) (K NONE) var (K f);
+fun change var f = change_result var (fn x => ((), f x));
+
+end;