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