author | wenzelm |
Fri, 19 Aug 2011 14:01:20 +0200 | |
changeset 44298 | b8f8488704e2 |
parent 44198 | a41ea419de68 |
child 44386 | 4048ca2658b7 |
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 |
44198 | 13 |
val is_finished: 'a lazy -> bool |
14 |
val get_finished: 'a lazy -> 'a |
|
28971 | 15 |
val lazy: (unit -> 'a) -> 'a lazy |
16 |
val value: 'a -> 'a lazy |
|
29422 | 17 |
val force_result: 'a lazy -> 'a Exn.result |
28971 | 18 |
val force: 'a lazy -> 'a |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
19 |
end; |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
20 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
21 |
structure Lazy: LAZY = |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
22 |
struct |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
23 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
24 |
(* datatype *) |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
25 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
26 |
datatype 'a expr = |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
27 |
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
|
28 |
Result of 'a future; |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
29 |
|
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
|
30 |
abstype 'a lazy = Lazy of 'a expr Synchronized.var |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
31 |
with |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
32 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
33 |
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
|
34 |
(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
|
35 |
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
|
36 |
| Result res => Future.peek res); |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
37 |
|
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
|
38 |
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
|
39 |
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
|
40 |
|
44198 | 41 |
fun is_finished x = is_some (peek x); |
42 |
||
43 |
fun get_finished x = |
|
44 |
(case peek x of |
|
45 |
SOME res => Exn.release res |
|
46 |
| NONE => raise Fail "Unfinished lazy evaluation"); |
|
47 |
||
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
48 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
49 |
(* force result *) |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
50 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
51 |
fun force_result (Lazy var) = |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
52 |
(case peek (Lazy var) of |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
53 |
SOME res => res |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
54 |
| NONE => |
41701
430493d65cd2
Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents:
40482
diff
changeset
|
55 |
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
|
56 |
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
|
57 |
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
|
58 |
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
|
59 |
(fn Expr e => |
44298
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
44198
diff
changeset
|
60 |
let val x = Future.promise I |
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 |
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
|
62 |
| 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
|
63 |
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
|
64 |
(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
|
65 |
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
|
66 |
let |
41701
430493d65cd2
Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents:
40482
diff
changeset
|
67 |
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
|
68 |
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
|
69 |
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
|
70 |
(*semantic race: some other threads might see the same |
40389 | 71 |
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
|
72 |
val _ = |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
37183
diff
changeset
|
73 |
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
|
74 |
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
|
75 |
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
|
76 |
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
|
77 |
| 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
|
78 |
end) ()); |
29422 | 79 |
|
80 |
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
|
81 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
82 |
end; |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
83 |
end; |
28971 | 84 |
|
85 |
type 'a lazy = 'a Lazy.lazy; |
|
86 |