author | wenzelm |
Sun, 05 Nov 2017 12:13:27 +0100 | |
changeset 67009 | b68592732783 |
parent 64276 | 622f4e4ac388 |
child 68589 | 9258f16d68b4 |
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, ...}) = |
59054
61b723761dff
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents:
47422
diff
changeset
|
35 |
Multithreading.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 => |
64276 | 40 |
(case Multithreading.sync_wait NONE cond lock of |
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
37906
diff
changeset
|
41 |
Exn.Res _ => wait () |
62505 | 42 |
| Exn.Exn exn => Exn.reraise exn) |
35014
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 = |
59054
61b723761dff
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents:
47422
diff
changeset
|
47 |
Multithreading.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 => |
62923 | 51 |
Thread_Attributes.uninterruptible (fn _ => fn () => |
35014
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; |