author | wenzelm |
Thu, 14 Aug 2014 16:20:14 +0200 | |
changeset 57942 | e5bec882fdd0 |
parent 47430 | b254fdaf1973 |
child 59147 | eb3e399f5b9f |
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 |
28971 | 14 |
val lazy: (unit -> 'a) -> 'a lazy |
15 |
val value: 'a -> 'a lazy |
|
29422 | 16 |
val force_result: 'a lazy -> 'a Exn.result |
28971 | 17 |
val force: 'a lazy -> 'a |
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
18 |
val map: ('a -> 'b) -> 'a lazy -> 'b lazy |
44427 | 19 |
val future: Future.params -> 'a lazy -> 'a future |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
20 |
end; |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
21 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
22 |
structure Lazy: LAZY = |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
23 |
struct |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
24 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
25 |
(* datatype *) |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
26 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
27 |
datatype 'a expr = |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
28 |
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
|
29 |
Result of 'a future; |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
30 |
|
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
|
31 |
abstype 'a lazy = Lazy of 'a expr Synchronized.var |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
32 |
with |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
33 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
34 |
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
|
35 |
(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
|
36 |
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
|
37 |
| Result res => Future.peek res); |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
38 |
|
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
|
39 |
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
|
40 |
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
|
41 |
|
44198 | 42 |
fun is_finished x = is_some (peek x); |
43 |
||
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
44 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
45 |
(* force result *) |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
46 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
47 |
fun force_result (Lazy var) = |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
48 |
(case peek (Lazy var) of |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
49 |
SOME res => res |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
50 |
| NONE => |
41701
430493d65cd2
Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents:
40482
diff
changeset
|
51 |
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
|
52 |
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
|
53 |
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
|
54 |
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
|
55 |
(fn Expr e => |
44298
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
44198
diff
changeset
|
56 |
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
|
57 |
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
|
58 |
| 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
|
59 |
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
|
60 |
(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
|
61 |
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
|
62 |
let |
41701
430493d65cd2
Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents:
40482
diff
changeset
|
63 |
val res0 = Exn.capture (restore_attributes e) (); |
47430
b254fdaf1973
partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents:
47423
diff
changeset
|
64 |
val _ = Exn.capture (fn () => Future.fulfill_result x res0) (); |
b254fdaf1973
partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents:
47423
diff
changeset
|
65 |
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
|
66 |
(*semantic race: some other threads might see the same |
40389 | 67 |
interrupt, until there is a fresh start*) |
47430
b254fdaf1973
partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents:
47423
diff
changeset
|
68 |
val _ = |
b254fdaf1973
partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents:
47423
diff
changeset
|
69 |
if Exn.is_interrupt_exn res then |
b254fdaf1973
partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents:
47423
diff
changeset
|
70 |
Synchronized.change var (fn _ => Expr e) |
b254fdaf1973
partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents:
47423
diff
changeset
|
71 |
else (); |
b254fdaf1973
partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents:
47423
diff
changeset
|
72 |
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
|
73 |
| 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
|
74 |
end) ()); |
29422 | 75 |
|
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
76 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
77 |
end; |
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
78 |
|
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
79 |
fun force r = Exn.release (force_result r); |
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
80 |
fun map f x = lazy (fn () => f (force x)); |
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
81 |
|
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
82 |
|
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
83 |
(* future evaluation *) |
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
84 |
|
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
85 |
fun future params x = |
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
86 |
if is_finished x then Future.value_result (force_result x) |
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
87 |
else (singleton o Future.forks) params (fn () => force x); |
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
88 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
89 |
end; |
28971 | 90 |
|
91 |
type 'a lazy = 'a Lazy.lazy; |
|
92 |