1(*  Title:      Pure/Concurrent/single_assignment.ML
2    Author:     Makarius
3
4Single-assignment variables with locking/signalling.
5*)
6
7signature SINGLE_ASSIGNMENT =
8sig
9  type 'a var
10  val var: string -> 'a var
11  val peek: 'a var -> 'a option
12  val await: 'a var -> 'a
13  val assign: 'a var -> 'a -> unit
14end;
15
16structure Single_Assignment: SINGLE_ASSIGNMENT =
17struct
18
19abstype 'a var = Var of
20 {name: string,
21  lock: Mutex.mutex,
22  cond: ConditionVar.conditionVar,
23  var: 'a SingleAssignment.saref}
24with
25
26fun var name = Var
27 {name = name,
28  lock = Mutex.mutex (),
29  cond = ConditionVar.conditionVar (),
30  var = SingleAssignment.saref ()};
31
32fun peek (Var {var, ...}) = SingleAssignment.savalue var;
33
34fun await (v as Var {name, lock, cond, ...}) =
35  Multithreading.synchronized name lock (fn () =>
36    let
37      fun wait () =
38        (case peek v of
39          NONE =>
40            (case Multithreading.sync_wait NONE cond lock of
41              Exn.Res _ => wait ()
42            | Exn.Exn exn => Exn.reraise exn)
43        | SOME x => x);
44    in wait () end);
45
46fun assign (v as Var {name, lock, cond, var}) x =
47  Multithreading.synchronized name lock (fn () =>
48    (case peek v of
49      SOME _ => raise Fail ("Duplicate assignment to " ^ name)
50    | NONE =>
51        Thread_Attributes.uninterruptible (fn _ => fn () =>
52         (SingleAssignment.saset (var, x); ConditionVar.broadcast cond)) ()));
53
54end;
55
56end;
57