author | wenzelm |
Thu, 04 Apr 2013 18:25:47 +0200 | |
changeset 51619 | 95b7da3430d4 |
parent 47422 | 5832630f049a |
child 59054 | 61b723761dff |
permissions | -rw-r--r-- |
35014
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Concurrent/single_assignment.ML |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
3 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
4 |
Single-assignment variables with locking/signalling. |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
5 |
*) |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
6 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
7 |
signature SINGLE_ASSIGNMENT = |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
8 |
sig |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
9 |
type 'a var |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
10 |
val var: string -> 'a var |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
11 |
val peek: 'a var -> 'a option |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
12 |
val await: 'a var -> 'a |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
13 |
val assign: 'a var -> 'a -> unit |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
14 |
end; |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
15 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
16 |
structure Single_Assignment: SINGLE_ASSIGNMENT = |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
17 |
struct |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
18 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
19 |
abstype 'a var = Var of |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
20 |
{name: string, |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
21 |
lock: Mutex.mutex, |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
22 |
cond: ConditionVar.conditionVar, |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
23 |
var: 'a SingleAssignment.saref} |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
24 |
with |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
25 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
26 |
fun var name = Var |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
27 |
{name = name, |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
28 |
lock = Mutex.mutex (), |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
29 |
cond = ConditionVar.conditionVar (), |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
30 |
var = SingleAssignment.saref ()}; |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
31 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
32 |
fun peek (Var {var, ...}) = SingleAssignment.savalue var; |
a725ff6ead26
explicit representation of single-assignment 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 single-assignment variables;
wenzelm
parents:
diff
changeset
|
36 |
let |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
37 |
fun wait () = |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
38 |
(case peek v of |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
39 |
NONE => |
a725ff6ead26
explicit representation of single-assignment 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 single-assignment variables;
wenzelm
parents:
diff
changeset
|
42 |
| Exn.Exn exn => reraise exn) |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
43 |
| SOME x => x); |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
44 |
in wait () end); |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
45 |
|
a725ff6ead26
explicit representation of single-assignment 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 single-assignment variables;
wenzelm
parents:
diff
changeset
|
48 |
(case peek v of |
47422 | 49 |
SOME _ => raise Fail ("Duplicate assignment to " ^ name) |
35014
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
50 |
| NONE => |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
51 |
uninterruptible (fn _ => fn () => |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
52 |
(SingleAssignment.saset (var, x); ConditionVar.broadcast cond)) ())); |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
53 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
54 |
end; |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
55 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
56 |
end; |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
57 |