author | blanchet |
Wed, 09 Mar 2011 10:25:29 +0100 | |
changeset 41897 | c24e7fd17464 |
parent 41701 | 430493d65cd2 |
child 44198 | a41ea419de68 |
permissions | -rw-r--r-- |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
1 |
(* Title: Pure/Concurrent/lazy.ML |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
2 |
Author: Makarius |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
3 |
|
34278 | 4 |
Lazy evaluation with memoing of results and regular exceptions. |
40389 | 5 |
Parallel version based on (passive) futures, to avoid critical or |
6 |
multiple evaluation (unless interrupted). |
|
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
7 |
*) |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
8 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
9 |
signature LAZY = |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
10 |
sig |
28971 | 11 |
type 'a lazy |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
12 |
val peek: 'a lazy -> 'a Exn.result option |
28971 | 13 |
val lazy: (unit -> 'a) -> 'a lazy |
14 |
val value: 'a -> 'a lazy |
|
29422 | 15 |
val force_result: 'a lazy -> 'a Exn.result |
28971 | 16 |
val force: 'a lazy -> 'a |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
17 |
end; |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
18 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
19 |
structure Lazy: LAZY = |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
20 |
struct |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
21 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
22 |
(* datatype *) |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
23 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
24 |
datatype 'a expr = |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
25 |
Expr of unit -> 'a | |
37183
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
26 |
Result of 'a future; |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
27 |
|
37183
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
28 |
abstype 'a lazy = Lazy of 'a expr Synchronized.var |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
29 |
with |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
30 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
31 |
fun peek (Lazy var) = |
37183
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
32 |
(case Synchronized.value var of |
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
33 |
Expr _ => NONE |
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
34 |
| Result res => Future.peek res); |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
35 |
|
37183
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
36 |
fun lazy e = Lazy (Synchronized.var "lazy" (Expr e)); |
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
37 |
fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a))); |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
38 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
39 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
40 |
(* force result *) |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
41 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
42 |
fun force_result (Lazy var) = |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
43 |
(case peek (Lazy var) of |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
44 |
SOME res => res |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
45 |
| NONE => |
41701
430493d65cd2
Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents:
40482
diff
changeset
|
46 |
uninterruptible (fn restore_attributes => fn () => |
37183
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
47 |
let |
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
48 |
val (expr, x) = |
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
49 |
Synchronized.change_result var |
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
50 |
(fn Expr e => |
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
51 |
let val x = Future.promise () |
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
52 |
in ((SOME e, x), Result x) end |
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
53 |
| Result x => ((NONE, x), Result x)); |
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
54 |
in |
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
55 |
(case expr of |
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
56 |
SOME e => |
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
57 |
let |
41701
430493d65cd2
Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents:
40482
diff
changeset
|
58 |
val res0 = Exn.capture (restore_attributes e) (); |
40482
dc0d4d4a1aa1
Laze.force_result: more robust treatment of interrupts stemming from peer group cancellation;
wenzelm
parents:
40389
diff
changeset
|
59 |
val _ = Future.fulfill_result x res0; |
dc0d4d4a1aa1
Laze.force_result: more robust treatment of interrupts stemming from peer group cancellation;
wenzelm
parents:
40389
diff
changeset
|
60 |
val res = Future.join_result x; |
37183
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
61 |
(*semantic race: some other threads might see the same |
40389 | 62 |
interrupt, until there is a fresh start*) |
37183
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
63 |
val _ = |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
37183
diff
changeset
|
64 |
if Exn.is_interrupt_exn res then |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
37183
diff
changeset
|
65 |
Synchronized.change var (fn _ => Expr e) |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
37183
diff
changeset
|
66 |
else (); |
37183
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
67 |
in res end |
41701
430493d65cd2
Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents:
40482
diff
changeset
|
68 |
| NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ()) |
37183
dae865999db5
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents:
34278
diff
changeset
|
69 |
end) ()); |
29422 | 70 |
|
71 |
fun force r = Exn.release (force_result r); |
|
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
72 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
73 |
end; |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
74 |
end; |
28971 | 75 |
|
76 |
type 'a lazy = 'a Lazy.lazy; |
|
77 |