1(* Title: Pure/Concurrent/synchronized.ML 2 Author: Fabian Immler and Makarius 3 4Synchronized variables. 5*) 6 7signature SYNCHRONIZED = 8sig 9 type 'a var 10 val var: string -> 'a -> 'a var 11 val value: 'a var -> 'a 12 val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option 13 val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b 14 val change_result: 'a var -> ('a -> 'b * 'a) -> 'b 15 val change: 'a var -> ('a -> 'a) -> unit 16end; 17 18structure Synchronized: SYNCHRONIZED = 19struct 20 21(* state variable *) 22 23abstype 'a var = Var of 24 {name: string, 25 lock: Mutex.mutex, 26 cond: ConditionVar.conditionVar, 27 var: 'a Unsynchronized.ref} 28with 29 30fun var name x = Var 31 {name = name, 32 lock = Mutex.mutex (), 33 cond = ConditionVar.conditionVar (), 34 var = Unsynchronized.ref x}; 35 36fun value (Var {name, lock, var, ...}) = 37 Multithreading.synchronized name lock (fn () => ! var); 38 39 40(* synchronized access *) 41 42fun timed_access (Var {name, lock, cond, var}) time_limit f = 43 Multithreading.synchronized name lock (fn () => 44 let 45 fun try_change () = 46 let val x = ! var in 47 (case f x of 48 NONE => 49 (case Multithreading.sync_wait (time_limit x) cond lock of 50 Exn.Res true => try_change () 51 | Exn.Res false => NONE 52 | Exn.Exn exn => Exn.reraise exn) 53 | SOME (y, x') => 54 Thread_Attributes.uninterruptible (fn _ => fn () => 55 (var := x'; ConditionVar.broadcast cond; SOME y)) ()) 56 end; 57 in try_change () end); 58 59fun guarded_access var f = valOf (timed_access var (fn _ => NONE) f); 60 61 62(* unconditional change *) 63 64fun change_result var f = guarded_access var (SOME o f); 65fun change var f = change_result var (fn x => ((), f x)); 66 67end; 68 69end; 70