author  wenzelm 
Wed, 11 Apr 2012 13:37:46 +0200  
changeset 47422  5832630f049a 
parent 43761  e72ba84ae58f 
child 59054  61b723761dff 
permissions  rwrr 
35014
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/Concurrent/single_assignment.ML 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

3 

a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

4 
Singleassignment variables with locking/signalling. 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

5 
*) 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

6 

a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

7 
signature SINGLE_ASSIGNMENT = 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

8 
sig 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

9 
type 'a var 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

10 
val var: string > 'a var 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

11 
val peek: 'a var > 'a option 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

12 
val await: 'a var > 'a 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

13 
val assign: 'a var > 'a > unit 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

14 
end; 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

15 

a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

16 
structure Single_Assignment: SINGLE_ASSIGNMENT = 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

17 
struct 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

18 

a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

19 
abstype 'a var = Var of 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

20 
{name: string, 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

21 
lock: Mutex.mutex, 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

22 
cond: ConditionVar.conditionVar, 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

23 
var: 'a SingleAssignment.saref} 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

24 
with 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

25 

a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

26 
fun var name = Var 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

27 
{name = name, 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

28 
lock = Mutex.mutex (), 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

29 
cond = ConditionVar.conditionVar (), 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

30 
var = SingleAssignment.saref ()}; 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

31 

a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

32 
fun peek (Var {var, ...}) = SingleAssignment.savalue var; 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

33 

37906  34 
fun await (v as Var {name, lock, cond, ...}) = 
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
35014
diff
changeset

35 
Simple_Thread.synchronized name lock (fn () => 
35014
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

36 
let 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

37 
fun wait () = 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

38 
(case peek v of 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

39 
NONE => 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

40 
(case Multithreading.sync_wait NONE NONE cond lock of 
43761
e72ba84ae58f
tuned signature  corresponding to Scala version;
wenzelm
parents:
37906
diff
changeset

41 
Exn.Res _ => wait () 
35014
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

42 
 Exn.Exn exn => reraise exn) 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

43 
 SOME x => x); 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

44 
in wait () end); 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

45 

a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

46 
fun assign (v as Var {name, lock, cond, var}) x = 
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
35014
diff
changeset

47 
Simple_Thread.synchronized name lock (fn () => 
35014
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

48 
(case peek v of 
47422  49 
SOME _ => raise Fail ("Duplicate assignment to " ^ name) 
35014
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

50 
 NONE => 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

51 
uninterruptible (fn _ => fn () => 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

52 
(SingleAssignment.saset (var, x); ConditionVar.broadcast cond)) ())); 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

53 

a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

54 
end; 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

55 

a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

56 
end; 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
diff
changeset

57 