author | wenzelm |
Sat, 28 Jul 2018 15:09:37 +0200 | |
changeset 68697 | d81a5da01796 |
parent 68597 | afa7c5a239e6 |
child 68698 | 6ee53660a911 |
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 |
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
12 |
val value: 'a -> 'a lazy |
66167 | 13 |
val lazy_name: string -> (unit -> 'a) -> 'a lazy |
28971 | 14 |
val lazy: (unit -> 'a) -> 'a lazy |
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59191
diff
changeset
|
15 |
val peek: 'a lazy -> 'a Exn.result option |
67661 | 16 |
val is_pending: 'a lazy -> bool |
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59191
diff
changeset
|
17 |
val is_running: 'a lazy -> bool |
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59191
diff
changeset
|
18 |
val is_finished: 'a lazy -> bool |
29422 | 19 |
val force_result: 'a lazy -> 'a Exn.result |
28971 | 20 |
val force: 'a lazy -> 'a |
67661 | 21 |
val force_value: 'a lazy -> 'a lazy |
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
22 |
val map: ('a -> 'b) -> 'a lazy -> 'b lazy |
67661 | 23 |
val map_finished: ('a -> 'b) -> 'a lazy -> 'b lazy |
67668 | 24 |
val consolidate: 'a lazy list -> 'a lazy list |
44427 | 25 |
val future: Future.params -> 'a lazy -> 'a future |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
26 |
end; |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
27 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
28 |
structure Lazy: LAZY = |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
29 |
struct |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
30 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
31 |
(* datatype *) |
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 |
datatype 'a expr = |
66167 | 34 |
Expr of string * (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
|
35 |
Result of 'a future; |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
36 |
|
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
37 |
abstype 'a lazy = Value of 'a | Lazy of 'a expr Synchronized.var |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
38 |
with |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
39 |
|
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
40 |
fun value a = Value a; |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
41 |
|
66167 | 42 |
fun lazy_name name e = Lazy (Synchronized.var "lazy" (Expr (name, e))); |
43 |
fun lazy e = lazy_name "lazy" e; |
|
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59191
diff
changeset
|
44 |
|
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
45 |
fun peek (Value a) = SOME (Exn.Res a) |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
46 |
| peek (Lazy var) = |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
47 |
(case Synchronized.value var of |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
48 |
Expr _ => NONE |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
49 |
| Result res => Future.peek res); |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
50 |
|
67661 | 51 |
|
52 |
(* status *) |
|
66168 | 53 |
|
67657 | 54 |
fun is_value (Value _) = true |
55 |
| is_value (Lazy _) = false; |
|
66168 | 56 |
|
67661 | 57 |
fun is_pending (Value _) = false |
58 |
| is_pending (Lazy var) = |
|
59 |
(case Synchronized.value var of |
|
60 |
Expr _ => true |
|
61 |
| Result _ => false); |
|
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59191
diff
changeset
|
62 |
|
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
63 |
fun is_running (Value _) = false |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
64 |
| is_running (Lazy var) = |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
65 |
(case Synchronized.value var of |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
66 |
Expr _ => false |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
67 |
| Result res => not (Future.is_finished res)); |
59193
59f1591a11cb
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents:
59191
diff
changeset
|
68 |
|
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
69 |
fun is_finished (Value _) = true |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
70 |
| is_finished (Lazy var) = |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
71 |
(case Synchronized.value var of |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
72 |
Expr _ => false |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
73 |
| Result res => |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
74 |
Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res))); |
59191 | 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 |
(* force result *) |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
78 |
|
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
79 |
fun force_result (Value a) = Exn.Res a |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
80 |
| force_result (Lazy var) = |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
81 |
(case peek (Lazy var) of |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
82 |
SOME res => res |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
83 |
| NONE => |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
84 |
Thread_Attributes.uninterruptible (fn restore_attributes => fn () => |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
85 |
let |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
86 |
val (expr, x) = |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
87 |
Synchronized.change_result var |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
88 |
(fn Expr (name, e) => |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
89 |
let val x = Future.promise_name name I |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
90 |
in ((SOME (name, e), x), Result x) end |
68597
afa7c5a239e6
more frugal assignment of lazy value: fewer mutexes, condvars;
wenzelm
parents:
68590
diff
changeset
|
91 |
| Result x => ((NONE, x), Result x)) |
afa7c5a239e6
more frugal assignment of lazy value: fewer mutexes, condvars;
wenzelm
parents:
68590
diff
changeset
|
92 |
handle exn as Fail _ => |
afa7c5a239e6
more frugal assignment of lazy value: fewer mutexes, condvars;
wenzelm
parents:
68590
diff
changeset
|
93 |
(case Synchronized.value var of |
afa7c5a239e6
more frugal assignment of lazy value: fewer mutexes, condvars;
wenzelm
parents:
68590
diff
changeset
|
94 |
Expr _ => Exn.reraise exn |
afa7c5a239e6
more frugal assignment of lazy value: fewer mutexes, condvars;
wenzelm
parents:
68590
diff
changeset
|
95 |
| Result x => (NONE, x)); |
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
96 |
in |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
97 |
(case expr of |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
98 |
SOME (name, e) => |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
99 |
let |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
100 |
val res0 = Exn.capture (restore_attributes e) (); |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
101 |
val _ = Exn.capture (fn () => Future.fulfill_result x res0) (); |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
102 |
val res = Future.join_result x; |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
103 |
(*semantic race: some other threads might see the same |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
104 |
interrupt, until there is a fresh start*) |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
105 |
val _ = |
68590
f3c3c1e6133a
store immutable result: fewer refs, mutexes, condvars;
wenzelm
parents:
68130
diff
changeset
|
106 |
if Exn.is_interrupt_exn res |
f3c3c1e6133a
store immutable result: fewer refs, mutexes, condvars;
wenzelm
parents:
68130
diff
changeset
|
107 |
then Synchronized.change var (fn _ => Expr (name, e)) |
68597
afa7c5a239e6
more frugal assignment of lazy value: fewer mutexes, condvars;
wenzelm
parents:
68590
diff
changeset
|
108 |
else Synchronized.assign var (Result (Future.value_result res)); |
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
109 |
in res end |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
110 |
| NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ()) |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
111 |
end) ()); |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
112 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
113 |
end; |
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
114 |
|
66168 | 115 |
fun force x = Exn.release (force_result x); |
116 |
||
67661 | 117 |
fun force_value x = if is_value x then x else value (force x); |
118 |
||
119 |
||
120 |
(* map *) |
|
67657 | 121 |
|
66167 | 122 |
fun map f x = lazy_name "Lazy.map" (fn () => f (force x)); |
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
123 |
|
67661 | 124 |
fun map_finished f x = if is_finished x then value (f (force x)) else map f x; |
125 |
||
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
126 |
|
67668 | 127 |
(* consolidate in parallel *) |
128 |
||
129 |
fun consolidate xs = |
|
130 |
let |
|
131 |
val pending = |
|
132 |
xs |> map_filter (fn x => if is_pending x then SOME (fn () => force_result x) else NONE); |
|
133 |
val _ = |
|
68130
6fb85346cb79
clarified future scheduling parameters, with support for parallel_limit;
wenzelm
parents:
67669
diff
changeset
|
134 |
if Future.relevant pending then |
67668 | 135 |
ignore (Future.forked_results {name = "Lazy.consolidate", deps = []} pending) |
136 |
else List.app (fn e => ignore (e ())) pending; |
|
137 |
in xs end; |
|
138 |
||
139 |
||
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
140 |
(* future evaluation *) |
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
141 |
|
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
142 |
fun future params x = |
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
143 |
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
|
144 |
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
|
145 |
|
62663 | 146 |
|
147 |
(* toplevel pretty printing *) |
|
148 |
||
149 |
val _ = |
|
62819
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62663
diff
changeset
|
150 |
ML_system_pp (fn depth => fn pretty => fn x => |
62663 | 151 |
(case peek x of |
62823 | 152 |
NONE => PolyML_Pretty.PrettyString "<lazy>" |
153 |
| SOME (Exn.Exn _) => PolyML_Pretty.PrettyString "<failed>" |
|
62663 | 154 |
| SOME (Exn.Res y) => pretty (y, depth))); |
155 |
||
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
156 |
end; |
28971 | 157 |
|
158 |
type 'a lazy = 'a Lazy.lazy; |