author | wenzelm |
Sat, 20 Aug 2011 15:52:29 +0200 | |
changeset 44330 | b28e091f683a |
parent 44301 | 65f60d9ac4bf |
child 44341 | a93d25fb14fc |
permissions | -rw-r--r-- |
28156 | 1 |
(* Title: Pure/Concurrent/future.ML |
2 |
Author: Makarius |
|
3 |
||
44268 | 4 |
Value-oriented parallelism via futures and promises. See also |
32246 | 5 |
http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf |
37904 | 6 |
http://www4.in.tum.de/~wenzelm/papers/parallel-ml.pdf |
28201 | 7 |
|
8 |
Notes: |
|
9 |
||
10 |
* Futures are similar to delayed evaluation, i.e. delay/force is |
|
44268 | 11 |
generalized to fork/join. The idea is to model parallel |
12 |
value-oriented computations (not communicating processes). |
|
28201 | 13 |
|
14 |
* Forked futures are evaluated spontaneously by a farm of worker |
|
15 |
threads in the background; join resynchronizes the computation and |
|
16 |
delivers results (values or exceptions). |
|
17 |
||
18 |
* The pool of worker threads is limited, usually in correlation with |
|
19 |
the number of physical cores on the machine. Note that allocation |
|
44268 | 20 |
of runtime resources may be distorted either if workers yield CPU |
21 |
time (e.g. via system sleep or wait operations), or if non-worker |
|
28201 | 22 |
threads contend for significant runtime resources independently. |
44268 | 23 |
There is a limited number of replacement worker threads that get |
24 |
activated in certain explicit wait conditions. |
|
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
25 |
|
44268 | 26 |
* Future tasks are organized in groups, which are block-structured. |
27 |
When forking a new new task, the default is to open an individual |
|
28 |
subgroup, unless some common group is specified explicitly. |
|
29 |
Failure of one group member causes the immediate peers to be |
|
30 |
interrupted eventually (i.e. none by default). Interrupted tasks |
|
31 |
that lack regular result information, will pick up parallel |
|
32 |
exceptions from the cumulative group context (as Par_Exn). |
|
33 |
||
44299
061599cb6eb0
refined Future.cancel: explicit future allows to join actual cancellation;
wenzelm
parents:
44298
diff
changeset
|
34 |
* Future task groups may be canceled: present and future group |
061599cb6eb0
refined Future.cancel: explicit future allows to join actual cancellation;
wenzelm
parents:
44298
diff
changeset
|
35 |
members will be interrupted eventually. |
061599cb6eb0
refined Future.cancel: explicit future allows to join actual cancellation;
wenzelm
parents:
44298
diff
changeset
|
36 |
|
44268 | 37 |
* Promised "passive" futures are fulfilled by external means. There |
38 |
is no associated evaluation task, but other futures can depend on |
|
39 |
them via regular join operations. |
|
28156 | 40 |
*) |
41 |
||
42 |
signature FUTURE = |
|
43 |
sig |
|
44300
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
44 |
type task = Task_Queue.task |
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
45 |
type group = Task_Queue.group |
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
46 |
val new_group: group option -> group |
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
47 |
val worker_task: unit -> task option |
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
48 |
val worker_group: unit -> group option |
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
49 |
val worker_subgroup: unit -> group |
28972 | 50 |
type 'a future |
44300
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
51 |
val task_of: 'a future -> task |
28972 | 52 |
val peek: 'a future -> 'a Exn.result option |
53 |
val is_finished: 'a future -> bool |
|
44198 | 54 |
val get_finished: 'a future -> 'a |
44301 | 55 |
val interruptible_task: ('a -> 'b) -> 'a -> 'b |
56 |
val cancel_group: group -> task list |
|
57 |
val cancel: 'a future -> task list |
|
44113 | 58 |
type fork_params = |
44300
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
59 |
{name: string, group: group option, deps: task list, pri: int, interrupts: bool} |
44113 | 60 |
val forks: fork_params -> (unit -> 'a) list -> 'a future list |
29119 | 61 |
val fork_pri: int -> (unit -> 'a) -> 'a future |
32724 | 62 |
val fork: (unit -> 'a) -> 'a future |
28972 | 63 |
val join_results: 'a future list -> 'a Exn.result list |
64 |
val join_result: 'a future -> 'a Exn.result |
|
44330 | 65 |
val joins: 'a future list -> 'a list |
28972 | 66 |
val join: 'a future -> 'a |
44301 | 67 |
val join_tasks: task list -> unit |
44294
a0ddd5760444
clarified Future.cond_forks: more uniform handling of exceptional situations;
wenzelm
parents:
44268
diff
changeset
|
68 |
val value_result: 'a Exn.result -> 'a future |
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
69 |
val value: 'a -> 'a future |
44330 | 70 |
val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list |
28972 | 71 |
val map: ('a -> 'b) -> 'a future -> 'b future |
44300
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
72 |
val promise_group: group -> (unit -> unit) -> 'a future |
44298
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
44295
diff
changeset
|
73 |
val promise: (unit -> unit) -> 'a future |
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
74 |
val fulfill_result: 'a future -> 'a Exn.result -> unit |
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
75 |
val fulfill: 'a future -> 'a -> unit |
28203 | 76 |
val shutdown: unit -> unit |
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
37904
diff
changeset
|
77 |
val status: (unit -> 'a) -> 'a |
28156 | 78 |
end; |
79 |
||
80 |
structure Future: FUTURE = |
|
81 |
struct |
|
82 |
||
28177
8c0335bc9336
inherit group from running thread, or create a new one -- make it harder to re-use canceled groups;
wenzelm
parents:
28170
diff
changeset
|
83 |
(** future values **) |
8c0335bc9336
inherit group from running thread, or create a new one -- make it harder to re-use canceled groups;
wenzelm
parents:
28170
diff
changeset
|
84 |
|
44300
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
85 |
type task = Task_Queue.task; |
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
86 |
type group = Task_Queue.group; |
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
87 |
val new_group = Task_Queue.new_group; |
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
88 |
|
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
89 |
|
28167 | 90 |
(* identifiers *) |
91 |
||
32058 | 92 |
local |
44300
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
93 |
val tag = Universal.tag () : task option Universal.tag; |
32058 | 94 |
in |
41683
73dde8006820
maintain Task_Queue.group within Task_Queue.task;
wenzelm
parents:
41681
diff
changeset
|
95 |
fun worker_task () = the_default NONE (Thread.getLocal tag); |
44110 | 96 |
fun setmp_worker_task task f x = setmp_thread_data tag (worker_task ()) (SOME task) f x; |
28167 | 97 |
end; |
98 |
||
41683
73dde8006820
maintain Task_Queue.group within Task_Queue.task;
wenzelm
parents:
41681
diff
changeset
|
99 |
val worker_group = Option.map Task_Queue.group_of_task o worker_task; |
44300
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
100 |
fun worker_subgroup () = new_group (worker_group ()); |
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
101 |
|
41679 | 102 |
fun worker_joining e = |
103 |
(case worker_task () of |
|
104 |
NONE => e () |
|
105 |
| SOME task => Task_Queue.joining task e); |
|
106 |
||
41680
a4c822915eaa
more informative task timing: some dependency tracking;
wenzelm
parents:
41679
diff
changeset
|
107 |
fun worker_waiting deps e = |
41670 | 108 |
(case worker_task () of |
109 |
NONE => e () |
|
41680
a4c822915eaa
more informative task timing: some dependency tracking;
wenzelm
parents:
41679
diff
changeset
|
110 |
| SOME task => Task_Queue.waiting task deps e); |
41670 | 111 |
|
28167 | 112 |
|
113 |
(* datatype future *) |
|
114 |
||
35016 | 115 |
type 'a result = 'a Exn.result Single_Assignment.var; |
116 |
||
28972 | 117 |
datatype 'a future = Future of |
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
118 |
{promised: bool, |
44300
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
119 |
task: task, |
35016 | 120 |
result: 'a result}; |
28167 | 121 |
|
122 |
fun task_of (Future {task, ...}) = task; |
|
32253 | 123 |
fun result_of (Future {result, ...}) = result; |
28167 | 124 |
|
35016 | 125 |
fun peek x = Single_Assignment.peek (result_of x); |
28558 | 126 |
fun is_finished x = is_some (peek x); |
28320 | 127 |
|
44198 | 128 |
fun get_finished x = |
129 |
(case peek x of |
|
130 |
SOME res => Exn.release res |
|
131 |
| NONE => raise Fail "Unfinished future evaluation"); |
|
132 |
||
28167 | 133 |
|
28177
8c0335bc9336
inherit group from running thread, or create a new one -- make it harder to re-use canceled groups;
wenzelm
parents:
28170
diff
changeset
|
134 |
|
8c0335bc9336
inherit group from running thread, or create a new one -- make it harder to re-use canceled groups;
wenzelm
parents:
28170
diff
changeset
|
135 |
(** scheduling **) |
8c0335bc9336
inherit group from running thread, or create a new one -- make it harder to re-use canceled groups;
wenzelm
parents:
28170
diff
changeset
|
136 |
|
8c0335bc9336
inherit group from running thread, or create a new one -- make it harder to re-use canceled groups;
wenzelm
parents:
28170
diff
changeset
|
137 |
(* synchronization *) |
28156 | 138 |
|
32219
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
139 |
val scheduler_event = ConditionVar.conditionVar (); |
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
140 |
val work_available = ConditionVar.conditionVar (); |
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
141 |
val work_finished = ConditionVar.conditionVar (); |
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
142 |
|
28156 | 143 |
local |
144 |
val lock = Mutex.mutex (); |
|
145 |
in |
|
146 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37182
diff
changeset
|
147 |
fun SYNCHRONIZED name = Simple_Thread.synchronized name lock; |
28156 | 148 |
|
32219
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
149 |
fun wait cond = (*requires SYNCHRONIZED*) |
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32293
diff
changeset
|
150 |
Multithreading.sync_wait NONE NONE cond lock; |
28206
bcd48c6897d4
eliminated requests, use global state variables uniformly;
wenzelm
parents:
28203
diff
changeset
|
151 |
|
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32293
diff
changeset
|
152 |
fun wait_timeout timeout cond = (*requires SYNCHRONIZED*) |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32293
diff
changeset
|
153 |
Multithreading.sync_wait NONE (SOME (Time.+ (Time.now (), timeout))) cond lock; |
28166
43087721a66e
moved task, thread_data, group, queue to task_queue.ML;
wenzelm
parents:
28163
diff
changeset
|
154 |
|
32219
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
155 |
fun signal cond = (*requires SYNCHRONIZED*) |
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
156 |
ConditionVar.signal cond; |
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
157 |
|
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
158 |
fun broadcast cond = (*requires SYNCHRONIZED*) |
28166
43087721a66e
moved task, thread_data, group, queue to task_queue.ML;
wenzelm
parents:
28163
diff
changeset
|
159 |
ConditionVar.broadcast cond; |
28156 | 160 |
|
32248
0241916a5f06
more precise treatment of scheduler_event: continous pulse (50ms) instead of flooding, which was burning many CPU cycles in spare threads;
wenzelm
parents:
32247
diff
changeset
|
161 |
fun broadcast_work () = (*requires SYNCHRONIZED*) |
0241916a5f06
more precise treatment of scheduler_event: continous pulse (50ms) instead of flooding, which was burning many CPU cycles in spare threads;
wenzelm
parents:
32247
diff
changeset
|
162 |
(ConditionVar.broadcast work_available; |
32225
d5d6f47fb018
cancel: improved reactivity due to more careful broadcasting;
wenzelm
parents:
32224
diff
changeset
|
163 |
ConditionVar.broadcast work_finished); |
d5d6f47fb018
cancel: improved reactivity due to more careful broadcasting;
wenzelm
parents:
32224
diff
changeset
|
164 |
|
28156 | 165 |
end; |
166 |
||
167 |
||
33410
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
168 |
(* global state *) |
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
169 |
|
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
170 |
val queue = Unsynchronized.ref Task_Queue.empty; |
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
171 |
val next = Unsynchronized.ref 0; |
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
172 |
val scheduler = Unsynchronized.ref (NONE: Thread.thread option); |
44300
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
173 |
val canceled = Unsynchronized.ref ([]: group list); |
33410
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
174 |
val do_shutdown = Unsynchronized.ref false; |
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
175 |
val max_workers = Unsynchronized.ref 0; |
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
176 |
val max_active = Unsynchronized.ref 0; |
33411
a07558eb5029
worker_next: treat wait for work_available as Sleeping, not Waiting;
wenzelm
parents:
33410
diff
changeset
|
177 |
val worker_trend = Unsynchronized.ref 0; |
33410
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
178 |
|
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
179 |
datatype worker_state = Working | Waiting | Sleeping; |
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
180 |
val workers = Unsynchronized.ref ([]: (Thread.thread * worker_state Unsynchronized.ref) list); |
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
181 |
|
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
182 |
fun count_workers state = (*requires SYNCHRONIZED*) |
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
183 |
fold (fn (_, state_ref) => fn i => if ! state_ref = state then i + 1 else i) (! workers) 0; |
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
184 |
|
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
185 |
|
44110 | 186 |
(* cancellation primitives *) |
32099 | 187 |
|
34279
02936e77a07c
tasks of canceled groups are considered "ready" -- enables to purge the queue from tasks depending on unfinished promises (also improves general reactivity);
wenzelm
parents:
34277
diff
changeset
|
188 |
fun cancel_now group = (*requires SYNCHRONIZED*) |
34280
16bf3e9786a3
eliminated cache, which complicates the code without making a real difference (NB: deque_towards often disrupts caching, and daisy-chaining of workers already reduces queue overhead);
wenzelm
parents:
34279
diff
changeset
|
189 |
Task_Queue.cancel (! queue) group; |
34279
02936e77a07c
tasks of canceled groups are considered "ready" -- enables to purge the queue from tasks depending on unfinished promises (also improves general reactivity);
wenzelm
parents:
34277
diff
changeset
|
190 |
|
02936e77a07c
tasks of canceled groups are considered "ready" -- enables to purge the queue from tasks depending on unfinished promises (also improves general reactivity);
wenzelm
parents:
34277
diff
changeset
|
191 |
fun cancel_later group = (*requires SYNCHRONIZED*) |
32738 | 192 |
(Unsynchronized.change canceled (insert Task_Queue.eq_group group); |
193 |
broadcast scheduler_event); |
|
29341
6bb007a0f9f2
more reactive scheduler: reduced loop timeout, propagate broadcast interrupt via TaskQueue.cancel_all;
wenzelm
parents:
29119
diff
changeset
|
194 |
|
44110 | 195 |
|
44301 | 196 |
fun interruptible_task f x = |
197 |
(if Multithreading.available then |
|
198 |
Multithreading.with_attributes |
|
199 |
(if is_some (worker_task ()) |
|
200 |
then Multithreading.private_interrupts |
|
201 |
else Multithreading.public_interrupts) |
|
202 |
(fn _ => f x) |
|
203 |
else interruptible f x) |
|
204 |
before Multithreading.interrupted (); |
|
205 |
||
206 |
||
44110 | 207 |
(* worker threads *) |
208 |
||
209 |
fun worker_exec (task, jobs) = |
|
28167 | 210 |
let |
41683
73dde8006820
maintain Task_Queue.group within Task_Queue.task;
wenzelm
parents:
41681
diff
changeset
|
211 |
val group = Task_Queue.group_of_task task; |
32102 | 212 |
val valid = not (Task_Queue.is_canceled group); |
41670 | 213 |
val ok = |
214 |
Task_Queue.running task (fn () => |
|
41683
73dde8006820
maintain Task_Queue.group within Task_Queue.task;
wenzelm
parents:
41681
diff
changeset
|
215 |
setmp_worker_task task (fn () => |
41670 | 216 |
fold (fn job => fn ok => job valid andalso ok) jobs true) ()); |
41776 | 217 |
val _ = Multithreading.tracing 2 (fn () => |
41670 | 218 |
let |
43951 | 219 |
val s = Task_Queue.str_of_task_groups task; |
41670 | 220 |
fun micros time = string_of_int (Time.toNanoseconds time div 1000); |
41680
a4c822915eaa
more informative task timing: some dependency tracking;
wenzelm
parents:
41679
diff
changeset
|
221 |
val (run, wait, deps) = Task_Queue.timing_of_task task; |
a4c822915eaa
more informative task timing: some dependency tracking;
wenzelm
parents:
41679
diff
changeset
|
222 |
in "TASK " ^ s ^ " " ^ micros run ^ " " ^ micros wait ^ " (" ^ commas deps ^ ")" end); |
32246 | 223 |
val _ = SYNCHRONIZED "finish" (fn () => |
32219
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
224 |
let |
32738 | 225 |
val maximal = Unsynchronized.change_result queue (Task_Queue.finish task); |
44295
e43f0ea90c9a
more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
wenzelm
parents:
44294
diff
changeset
|
226 |
val test = Exn.capture Multithreading.interrupted (); |
32219
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
227 |
val _ = |
44295
e43f0ea90c9a
more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
wenzelm
parents:
44294
diff
changeset
|
228 |
if ok andalso not (Exn.is_interrupt_exn test) then () |
44299
061599cb6eb0
refined Future.cancel: explicit future allows to join actual cancellation;
wenzelm
parents:
44298
diff
changeset
|
229 |
else if null (cancel_now group) then () |
34279
02936e77a07c
tasks of canceled groups are considered "ready" -- enables to purge the queue from tasks depending on unfinished promises (also improves general reactivity);
wenzelm
parents:
34277
diff
changeset
|
230 |
else cancel_later group; |
32219
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
231 |
val _ = broadcast work_finished; |
33413
cb409680dda8
avoid broadcast work_available, use daisy-chained signal instead;
wenzelm
parents:
33411
diff
changeset
|
232 |
val _ = if maximal then () else signal work_available; |
32219
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
233 |
in () end); |
28167 | 234 |
in () end; |
235 |
||
33410
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
236 |
fun worker_wait active cond = (*requires SYNCHRONIZED*) |
33406
1ddcb8472bd2
slightly leaner and more direct control of worker activity etc.;
wenzelm
parents:
33061
diff
changeset
|
237 |
let |
33410
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
238 |
val state = |
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
239 |
(case AList.lookup Thread.equal (! workers) (Thread.self ()) of |
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
240 |
SOME state => state |
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
241 |
| NONE => raise Fail "Unregistered worker thread"); |
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
242 |
val _ = state := (if active then Waiting else Sleeping); |
33406
1ddcb8472bd2
slightly leaner and more direct control of worker activity etc.;
wenzelm
parents:
33061
diff
changeset
|
243 |
val _ = wait cond; |
33410
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
244 |
val _ = state := Working; |
33406
1ddcb8472bd2
slightly leaner and more direct control of worker activity etc.;
wenzelm
parents:
33061
diff
changeset
|
245 |
in () end; |
28162 | 246 |
|
33415
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
247 |
fun worker_next () = (*requires SYNCHRONIZED*) |
33406
1ddcb8472bd2
slightly leaner and more direct control of worker activity etc.;
wenzelm
parents:
33061
diff
changeset
|
248 |
if length (! workers) > ! max_workers then |
1ddcb8472bd2
slightly leaner and more direct control of worker activity etc.;
wenzelm
parents:
33061
diff
changeset
|
249 |
(Unsynchronized.change workers (AList.delete Thread.equal (Thread.self ())); |
33415
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
250 |
signal work_available; |
28167 | 251 |
NONE) |
33410
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
252 |
else if count_workers Working > ! max_active then |
33415
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
253 |
(worker_wait false work_available; worker_next ()) |
28166
43087721a66e
moved task, thread_data, group, queue to task_queue.ML;
wenzelm
parents:
28163
diff
changeset
|
254 |
else |
32738 | 255 |
(case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ())) of |
33415
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
256 |
NONE => (worker_wait false work_available; worker_next ()) |
33413
cb409680dda8
avoid broadcast work_available, use daisy-chained signal instead;
wenzelm
parents:
33411
diff
changeset
|
257 |
| some => (signal work_available; some)); |
28156 | 258 |
|
28167 | 259 |
fun worker_loop name = |
33415
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
260 |
(case SYNCHRONIZED name (fn () => worker_next ()) of |
29119 | 261 |
NONE => () |
44295
e43f0ea90c9a
more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
wenzelm
parents:
44294
diff
changeset
|
262 |
| SOME work => (worker_exec work; worker_loop name)); |
28156 | 263 |
|
33407
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
264 |
fun worker_start name = (*requires SYNCHRONIZED*) |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37182
diff
changeset
|
265 |
Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name), |
33410
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
266 |
Unsynchronized.ref Working)); |
28156 | 267 |
|
268 |
||
269 |
(* scheduler *) |
|
270 |
||
33407
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
271 |
val status_ticks = Unsynchronized.ref 0; |
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
272 |
|
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
273 |
val last_round = Unsynchronized.ref Time.zeroTime; |
40301 | 274 |
val next_round = seconds 0.05; |
32226 | 275 |
|
28206
bcd48c6897d4
eliminated requests, use global state variables uniformly;
wenzelm
parents:
28203
diff
changeset
|
276 |
fun scheduler_next () = (*requires SYNCHRONIZED*) |
28156 | 277 |
let |
33407
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
278 |
val now = Time.now (); |
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
279 |
val tick = Time.<= (Time.+ (! last_round, next_round), now); |
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
280 |
val _ = if tick then last_round := now else (); |
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
281 |
|
33415
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
282 |
|
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
283 |
(* queue and worker status *) |
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
284 |
|
32226 | 285 |
val _ = |
33407
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
286 |
if tick then Unsynchronized.change status_ticks (fn i => (i + 1) mod 10) else (); |
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
287 |
val _ = |
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
288 |
if tick andalso ! status_ticks = 0 then |
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
289 |
Multithreading.tracing 1 (fn () => |
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
290 |
let |
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
291 |
val {ready, pending, running, passive} = Task_Queue.status (! queue); |
33407
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
292 |
val total = length (! workers); |
33410
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
293 |
val active = count_workers Working; |
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
294 |
val waiting = count_workers Waiting; |
33407
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
295 |
in |
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
296 |
"SCHEDULE " ^ Time.toString now ^ ": " ^ |
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
297 |
string_of_int ready ^ " ready, " ^ |
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
298 |
string_of_int pending ^ " pending, " ^ |
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
299 |
string_of_int running ^ " running, " ^ |
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
300 |
string_of_int passive ^ " passive; " ^ |
33407
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
301 |
string_of_int total ^ " workers, " ^ |
33410
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
302 |
string_of_int active ^ " active, " ^ |
e351f4c1f18c
worker activity: distinguish between waiting (formerly active) and sleeping;
wenzelm
parents:
33409
diff
changeset
|
303 |
string_of_int waiting ^ " waiting " |
33407
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
304 |
end) |
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
305 |
else (); |
32053 | 306 |
|
28191 | 307 |
val _ = |
32219
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
308 |
if forall (Thread.isActive o #1) (! workers) then () |
32095 | 309 |
else |
33409 | 310 |
let |
37682 | 311 |
val (alive, dead) = List.partition (Thread.isActive o #1) (! workers); |
33409 | 312 |
val _ = workers := alive; |
313 |
in |
|
314 |
Multithreading.tracing 0 (fn () => |
|
315 |
"SCHEDULE: disposed " ^ string_of_int (length dead) ^ " dead worker threads") |
|
316 |
end; |
|
28191 | 317 |
|
33415
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
318 |
|
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
319 |
(* worker pool adjustments *) |
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
320 |
|
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
321 |
val max_active0 = ! max_active; |
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
322 |
val max_workers0 = ! max_workers; |
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
323 |
|
28206
bcd48c6897d4
eliminated requests, use global state variables uniformly;
wenzelm
parents:
28203
diff
changeset
|
324 |
val m = if ! do_shutdown then 0 else Multithreading.max_threads_value (); |
33406
1ddcb8472bd2
slightly leaner and more direct control of worker activity etc.;
wenzelm
parents:
33061
diff
changeset
|
325 |
val _ = max_active := m; |
1ddcb8472bd2
slightly leaner and more direct control of worker activity etc.;
wenzelm
parents:
33061
diff
changeset
|
326 |
|
33411
a07558eb5029
worker_next: treat wait for work_available as Sleeping, not Waiting;
wenzelm
parents:
33410
diff
changeset
|
327 |
val mm = |
a07558eb5029
worker_next: treat wait for work_available as Sleeping, not Waiting;
wenzelm
parents:
33410
diff
changeset
|
328 |
if ! do_shutdown then 0 |
a07558eb5029
worker_next: treat wait for work_available as Sleeping, not Waiting;
wenzelm
parents:
33410
diff
changeset
|
329 |
else if m = 9999 then 1 |
33413
cb409680dda8
avoid broadcast work_available, use daisy-chained signal instead;
wenzelm
parents:
33411
diff
changeset
|
330 |
else Int.min (Int.max (count_workers Working + 2 * count_workers Waiting, m), 4 * m); |
33411
a07558eb5029
worker_next: treat wait for work_available as Sleeping, not Waiting;
wenzelm
parents:
33410
diff
changeset
|
331 |
val _ = |
a07558eb5029
worker_next: treat wait for work_available as Sleeping, not Waiting;
wenzelm
parents:
33410
diff
changeset
|
332 |
if tick andalso mm > ! max_workers then |
a07558eb5029
worker_next: treat wait for work_available as Sleeping, not Waiting;
wenzelm
parents:
33410
diff
changeset
|
333 |
Unsynchronized.change worker_trend (fn w => if w < 0 then 0 else w + 1) |
a07558eb5029
worker_next: treat wait for work_available as Sleeping, not Waiting;
wenzelm
parents:
33410
diff
changeset
|
334 |
else if tick andalso mm < ! max_workers then |
a07558eb5029
worker_next: treat wait for work_available as Sleeping, not Waiting;
wenzelm
parents:
33410
diff
changeset
|
335 |
Unsynchronized.change worker_trend (fn w => if w > 0 then 0 else w - 1) |
a07558eb5029
worker_next: treat wait for work_available as Sleeping, not Waiting;
wenzelm
parents:
33410
diff
changeset
|
336 |
else (); |
a07558eb5029
worker_next: treat wait for work_available as Sleeping, not Waiting;
wenzelm
parents:
33410
diff
changeset
|
337 |
val _ = |
33415
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
338 |
if mm = 0 orelse ! worker_trend > 50 orelse ! worker_trend < ~50 then |
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
339 |
max_workers := mm |
44173
aaaa13e297dc
immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029);
wenzelm
parents:
44115
diff
changeset
|
340 |
else if ! worker_trend > 5 andalso ! max_workers < 2 * m orelse ! max_workers = 0 then |
33415
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
341 |
max_workers := Int.min (mm, 2 * m) |
33411
a07558eb5029
worker_next: treat wait for work_available as Sleeping, not Waiting;
wenzelm
parents:
33410
diff
changeset
|
342 |
else (); |
33406
1ddcb8472bd2
slightly leaner and more direct control of worker activity etc.;
wenzelm
parents:
33061
diff
changeset
|
343 |
|
33407
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
344 |
val missing = ! max_workers - length (! workers); |
28203 | 345 |
val _ = |
33407
1427333220bc
worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
wenzelm
parents:
33406
diff
changeset
|
346 |
if missing > 0 then |
33415
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
347 |
funpow missing (fn () => |
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
348 |
ignore (worker_start ("worker " ^ string_of_int (Unsynchronized.inc next)))) () |
28203 | 349 |
else (); |
28206
bcd48c6897d4
eliminated requests, use global state variables uniformly;
wenzelm
parents:
28203
diff
changeset
|
350 |
|
33415
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
351 |
val _ = |
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
352 |
if ! max_active = max_active0 andalso ! max_workers = max_workers0 then () |
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
353 |
else signal work_available; |
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
354 |
|
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
355 |
|
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
356 |
(* canceled groups *) |
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
357 |
|
32225
d5d6f47fb018
cancel: improved reactivity due to more careful broadcasting;
wenzelm
parents:
32224
diff
changeset
|
358 |
val _ = |
d5d6f47fb018
cancel: improved reactivity due to more careful broadcasting;
wenzelm
parents:
32224
diff
changeset
|
359 |
if null (! canceled) then () |
32293 | 360 |
else |
361 |
(Multithreading.tracing 1 (fn () => |
|
362 |
string_of_int (length (! canceled)) ^ " canceled groups"); |
|
44299
061599cb6eb0
refined Future.cancel: explicit future allows to join actual cancellation;
wenzelm
parents:
44298
diff
changeset
|
363 |
Unsynchronized.change canceled (filter_out (null o cancel_now)); |
32293 | 364 |
broadcast_work ()); |
28206
bcd48c6897d4
eliminated requests, use global state variables uniformly;
wenzelm
parents:
28203
diff
changeset
|
365 |
|
33415
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
366 |
|
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
367 |
(* delay loop *) |
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
368 |
|
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32293
diff
changeset
|
369 |
val _ = Exn.release (wait_timeout next_round scheduler_event); |
28167 | 370 |
|
33415
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
371 |
|
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
372 |
(* shutdown *) |
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
373 |
|
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
374 |
val _ = if Task_Queue.all_passive (! queue) then do_shutdown := true else (); |
32219
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
375 |
val continue = not (! do_shutdown andalso null (! workers)); |
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
376 |
val _ = if continue then () else scheduler := NONE; |
33415
352fe8e9162d
worker_next: plain signalling via work_available only, not scheduler_event;
wenzelm
parents:
33413
diff
changeset
|
377 |
|
32219
9a2566d1fdbd
more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
wenzelm
parents:
32186
diff
changeset
|
378 |
val _ = broadcast scheduler_event; |
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32293
diff
changeset
|
379 |
in continue end |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
38236
diff
changeset
|
380 |
handle exn => |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
38236
diff
changeset
|
381 |
if Exn.is_interrupt exn then |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
38236
diff
changeset
|
382 |
(Multithreading.tracing 1 (fn () => "Interrupt"); |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
38236
diff
changeset
|
383 |
List.app cancel_later (Task_Queue.cancel_all (! queue)); |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
38236
diff
changeset
|
384 |
broadcast_work (); true) |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
38236
diff
changeset
|
385 |
else reraise exn; |
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32293
diff
changeset
|
386 |
|
28206
bcd48c6897d4
eliminated requests, use global state variables uniformly;
wenzelm
parents:
28203
diff
changeset
|
387 |
fun scheduler_loop () = |
44173
aaaa13e297dc
immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029);
wenzelm
parents:
44115
diff
changeset
|
388 |
(while |
33416
13d00799fe49
scheduler: clarified interrupt attributes and handling;
wenzelm
parents:
33415
diff
changeset
|
389 |
Multithreading.with_attributes |
13d00799fe49
scheduler: clarified interrupt attributes and handling;
wenzelm
parents:
33415
diff
changeset
|
390 |
(Multithreading.sync_interrupts Multithreading.public_interrupts) |
13d00799fe49
scheduler: clarified interrupt attributes and handling;
wenzelm
parents:
33415
diff
changeset
|
391 |
(fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ())) |
44173
aaaa13e297dc
immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029);
wenzelm
parents:
44115
diff
changeset
|
392 |
do (); last_round := Time.zeroTime); |
28156 | 393 |
|
28203 | 394 |
fun scheduler_active () = (*requires SYNCHRONIZED*) |
395 |
(case ! scheduler of NONE => false | SOME thread => Thread.isActive thread); |
|
396 |
||
32228
7622c03141b0
scheduler: shutdown spontaneously (after some delay) if queue is empty;
wenzelm
parents:
32227
diff
changeset
|
397 |
fun scheduler_check () = (*requires SYNCHRONIZED*) |
7622c03141b0
scheduler: shutdown spontaneously (after some delay) if queue is empty;
wenzelm
parents:
32227
diff
changeset
|
398 |
(do_shutdown := false; |
32248
0241916a5f06
more precise treatment of scheduler_event: continous pulse (50ms) instead of flooding, which was burning many CPU cycles in spare threads;
wenzelm
parents:
32247
diff
changeset
|
399 |
if scheduler_active () then () |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37182
diff
changeset
|
400 |
else scheduler := SOME (Simple_Thread.fork false scheduler_loop)); |
28156 | 401 |
|
44301 | 402 |
|
403 |
||
404 |
(** futures **) |
|
405 |
||
406 |
(* cancel *) |
|
407 |
||
408 |
fun cancel_group group = SYNCHRONIZED "cancel_group" (fn () => |
|
44299
061599cb6eb0
refined Future.cancel: explicit future allows to join actual cancellation;
wenzelm
parents:
44298
diff
changeset
|
409 |
let |
061599cb6eb0
refined Future.cancel: explicit future allows to join actual cancellation;
wenzelm
parents:
44298
diff
changeset
|
410 |
val running = cancel_now group; |
061599cb6eb0
refined Future.cancel: explicit future allows to join actual cancellation;
wenzelm
parents:
44298
diff
changeset
|
411 |
val _ = |
061599cb6eb0
refined Future.cancel: explicit future allows to join actual cancellation;
wenzelm
parents:
44298
diff
changeset
|
412 |
if null running then () |
061599cb6eb0
refined Future.cancel: explicit future allows to join actual cancellation;
wenzelm
parents:
44298
diff
changeset
|
413 |
else (cancel_later group; signal work_available; scheduler_check ()); |
061599cb6eb0
refined Future.cancel: explicit future allows to join actual cancellation;
wenzelm
parents:
44298
diff
changeset
|
414 |
in running end); |
061599cb6eb0
refined Future.cancel: explicit future allows to join actual cancellation;
wenzelm
parents:
44298
diff
changeset
|
415 |
|
44301 | 416 |
fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x)); |
29366 | 417 |
|
28156 | 418 |
|
44110 | 419 |
(* future jobs *) |
420 |
||
44249
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44247
diff
changeset
|
421 |
fun assign_result group result raw_res = |
44110 | 422 |
let |
44249
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44247
diff
changeset
|
423 |
val res = |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44247
diff
changeset
|
424 |
(case raw_res of |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44247
diff
changeset
|
425 |
Exn.Exn exn => Exn.Exn (#2 (Par_Exn.serial exn)) |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
44247
diff
changeset
|
426 |
| _ => raw_res); |
44110 | 427 |
val _ = Single_Assignment.assign result res |
428 |
handle exn as Fail _ => |
|
429 |
(case Single_Assignment.peek result of |
|
430 |
SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn) |
|
431 |
| _ => reraise exn); |
|
432 |
val ok = |
|
433 |
(case the (Single_Assignment.peek result) of |
|
44111
2d16c693d536
synchronized cancel and flushing of Multithreading.interrupted state, to ensure that interrupts stay within task boundaries;
wenzelm
parents:
44110
diff
changeset
|
434 |
Exn.Exn exn => |
2d16c693d536
synchronized cancel and flushing of Multithreading.interrupted state, to ensure that interrupts stay within task boundaries;
wenzelm
parents:
44110
diff
changeset
|
435 |
(SYNCHRONIZED "cancel" (fn () => Task_Queue.cancel_group group exn); false) |
44110 | 436 |
| Exn.Res _ => true); |
437 |
in ok end; |
|
438 |
||
44113 | 439 |
fun future_job group interrupts (e: unit -> 'a) = |
44110 | 440 |
let |
441 |
val result = Single_Assignment.var "future" : 'a result; |
|
442 |
val pos = Position.thread_data (); |
|
443 |
fun job ok = |
|
444 |
let |
|
445 |
val res = |
|
446 |
if ok then |
|
447 |
Exn.capture (fn () => |
|
44113 | 448 |
Multithreading.with_attributes |
449 |
(if interrupts |
|
450 |
then Multithreading.private_interrupts else Multithreading.no_interrupts) |
|
44295
e43f0ea90c9a
more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
wenzelm
parents:
44294
diff
changeset
|
451 |
(fn _ => Position.setmp_thread_data pos e ())) () |
44110 | 452 |
else Exn.interrupt_exn; |
453 |
in assign_result group result res end; |
|
454 |
in (result, job) end; |
|
455 |
||
456 |
||
29366 | 457 |
(* fork *) |
458 |
||
44113 | 459 |
type fork_params = |
44300
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
460 |
{name: string, group: group option, deps: task list, pri: int, interrupts: bool}; |
44113 | 461 |
|
462 |
fun forks ({name, group, deps, pri, interrupts}: fork_params) es = |
|
41674 | 463 |
if null es then [] |
464 |
else |
|
465 |
let |
|
466 |
val grp = |
|
467 |
(case group of |
|
468 |
NONE => worker_subgroup () |
|
469 |
| SOME grp => grp); |
|
41708 | 470 |
fun enqueue e queue = |
41674 | 471 |
let |
44113 | 472 |
val (result, job) = future_job grp interrupts e; |
41708 | 473 |
val (task, queue') = Task_Queue.enqueue name grp deps pri job queue; |
41683
73dde8006820
maintain Task_Queue.group within Task_Queue.task;
wenzelm
parents:
41681
diff
changeset
|
474 |
val future = Future {promised = false, task = task, result = result}; |
41708 | 475 |
in (future, queue') end; |
41674 | 476 |
in |
477 |
SYNCHRONIZED "enqueue" (fn () => |
|
478 |
let |
|
41708 | 479 |
val (futures, queue') = fold_map enqueue es (! queue); |
480 |
val _ = queue := queue'; |
|
481 |
val minimal = forall (not o Task_Queue.known_task queue') deps; |
|
41674 | 482 |
val _ = if minimal then signal work_available else (); |
483 |
val _ = scheduler_check (); |
|
484 |
in futures end) |
|
485 |
end; |
|
28162 | 486 |
|
44113 | 487 |
fun fork_pri pri e = |
44301 | 488 |
(singleton o forks) {name = "fork", group = NONE, deps = [], pri = pri, interrupts = true} e; |
44113 | 489 |
|
41672
2f70b1ddd09f
more direct Future.bulk, which potentially reduces overhead for Par_List;
wenzelm
parents:
41670
diff
changeset
|
490 |
fun fork e = fork_pri 0 e; |
28186 | 491 |
|
492 |
||
29366 | 493 |
(* join *) |
494 |
||
29551
95e469919c3e
join_results: when dependencies are resulved (but not finished yet),
wenzelm
parents:
29431
diff
changeset
|
495 |
local |
95e469919c3e
join_results: when dependencies are resulved (but not finished yet),
wenzelm
parents:
29431
diff
changeset
|
496 |
|
32099 | 497 |
fun get_result x = |
498 |
(case peek x of |
|
37852
a902f158b4fc
eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
wenzelm
parents:
37690
diff
changeset
|
499 |
NONE => Exn.Exn (Fail "Unfinished future") |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
38236
diff
changeset
|
500 |
| SOME res => |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
38236
diff
changeset
|
501 |
if Exn.is_interrupt_exn res then |
44247 | 502 |
(case Task_Queue.group_status (Task_Queue.group_of_task (task_of x)) of |
503 |
NONE => res |
|
504 |
| SOME exn => Exn.Exn exn) |
|
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
38236
diff
changeset
|
505 |
else res); |
28186 | 506 |
|
32095 | 507 |
fun join_next deps = (*requires SYNCHRONIZED*) |
41695
afdbec23b92b
eliminated slightly odd abstract type Task_Queue.deps;
wenzelm
parents:
41683
diff
changeset
|
508 |
if null deps then NONE |
32224 | 509 |
else |
41681
b5d7b15166bf
Future.join_results: discontinued post-hoc recording of dynamic dependencies;
wenzelm
parents:
41680
diff
changeset
|
510 |
(case Unsynchronized.change_result queue (Task_Queue.dequeue_deps (Thread.self ()) deps) of |
41695
afdbec23b92b
eliminated slightly odd abstract type Task_Queue.deps;
wenzelm
parents:
41683
diff
changeset
|
511 |
(NONE, []) => NONE |
afdbec23b92b
eliminated slightly odd abstract type Task_Queue.deps;
wenzelm
parents:
41683
diff
changeset
|
512 |
| (NONE, deps') => |
afdbec23b92b
eliminated slightly odd abstract type Task_Queue.deps;
wenzelm
parents:
41683
diff
changeset
|
513 |
(worker_waiting deps' (fn () => worker_wait true work_finished); join_next deps') |
32224 | 514 |
| (SOME work, deps') => SOME (work, deps')); |
32095 | 515 |
|
32814
81897d30b97f
added Task_Queue.depend (again) -- light-weight version for transitive graph;
wenzelm
parents:
32738
diff
changeset
|
516 |
fun execute_work NONE = () |
44110 | 517 |
| execute_work (SOME (work, deps')) = |
518 |
(worker_joining (fn () => worker_exec work); join_work deps') |
|
32814
81897d30b97f
added Task_Queue.depend (again) -- light-weight version for transitive graph;
wenzelm
parents:
32738
diff
changeset
|
519 |
and join_work deps = |
43538
de5c79682b56
more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!
wenzelm
parents:
42128
diff
changeset
|
520 |
Multithreading.with_attributes Multithreading.no_interrupts |
de5c79682b56
more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!
wenzelm
parents:
42128
diff
changeset
|
521 |
(fn _ => execute_work (SYNCHRONIZED "join" (fn () => join_next deps))); |
32814
81897d30b97f
added Task_Queue.depend (again) -- light-weight version for transitive graph;
wenzelm
parents:
32738
diff
changeset
|
522 |
|
29551
95e469919c3e
join_results: when dependencies are resulved (but not finished yet),
wenzelm
parents:
29431
diff
changeset
|
523 |
in |
95e469919c3e
join_results: when dependencies are resulved (but not finished yet),
wenzelm
parents:
29431
diff
changeset
|
524 |
|
29366 | 525 |
fun join_results xs = |
41679 | 526 |
let |
527 |
val _ = |
|
528 |
if forall is_finished xs then () |
|
529 |
else if Multithreading.self_critical () then |
|
530 |
error "Cannot join future values within critical section" |
|
41695
afdbec23b92b
eliminated slightly odd abstract type Task_Queue.deps;
wenzelm
parents:
41683
diff
changeset
|
531 |
else if is_some (worker_task ()) then join_work (map task_of xs) |
41681
b5d7b15166bf
Future.join_results: discontinued post-hoc recording of dynamic dependencies;
wenzelm
parents:
41680
diff
changeset
|
532 |
else List.app (ignore o Single_Assignment.await o result_of) xs; |
41679 | 533 |
in map get_result xs end; |
28186 | 534 |
|
29551
95e469919c3e
join_results: when dependencies are resulved (but not finished yet),
wenzelm
parents:
29431
diff
changeset
|
535 |
end; |
95e469919c3e
join_results: when dependencies are resulved (but not finished yet),
wenzelm
parents:
29431
diff
changeset
|
536 |
|
28647
8068cdc84e7e
join_results: allow CRITICAL join of finished futures;
wenzelm
parents:
28645
diff
changeset
|
537 |
fun join_result x = singleton join_results x; |
44330 | 538 |
fun joins xs = Par_Exn.release_all (join_results xs); |
28647
8068cdc84e7e
join_results: allow CRITICAL join of finished futures;
wenzelm
parents:
28645
diff
changeset
|
539 |
fun join x = Exn.release (join_result x); |
28156 | 540 |
|
44301 | 541 |
fun join_tasks [] = () |
542 |
| join_tasks tasks = |
|
543 |
(singleton o forks) |
|
544 |
{name = "join_tasks", group = SOME (new_group NONE), |
|
545 |
deps = tasks, pri = 0, interrupts = false} I |
|
546 |
|> join; |
|
547 |
||
29366 | 548 |
|
44110 | 549 |
(* fast-path versions -- bypassing task queue *) |
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
550 |
|
44294
a0ddd5760444
clarified Future.cond_forks: more uniform handling of exceptional situations;
wenzelm
parents:
44268
diff
changeset
|
551 |
fun value_result (res: 'a Exn.result) = |
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
552 |
let |
41683
73dde8006820
maintain Task_Queue.group within Task_Queue.task;
wenzelm
parents:
41681
diff
changeset
|
553 |
val task = Task_Queue.dummy_task (); |
73dde8006820
maintain Task_Queue.group within Task_Queue.task;
wenzelm
parents:
41681
diff
changeset
|
554 |
val group = Task_Queue.group_of_task task; |
35016 | 555 |
val result = Single_Assignment.var "value" : 'a result; |
44294
a0ddd5760444
clarified Future.cond_forks: more uniform handling of exceptional situations;
wenzelm
parents:
44268
diff
changeset
|
556 |
val _ = assign_result group result res; |
41683
73dde8006820
maintain Task_Queue.group within Task_Queue.task;
wenzelm
parents:
41681
diff
changeset
|
557 |
in Future {promised = false, task = task, result = result} end; |
29366 | 558 |
|
44294
a0ddd5760444
clarified Future.cond_forks: more uniform handling of exceptional situations;
wenzelm
parents:
44268
diff
changeset
|
559 |
fun value x = value_result (Exn.Res x); |
a0ddd5760444
clarified Future.cond_forks: more uniform handling of exceptional situations;
wenzelm
parents:
44268
diff
changeset
|
560 |
|
44330 | 561 |
fun cond_forks args es = |
562 |
if Multithreading.enabled () then forks args es |
|
563 |
else map (fn e => value_result (Exn.interruptible_capture e ())) es; |
|
564 |
||
29384
a3c7e9ae9b71
more robust propagation of errors through bulk jobs;
wenzelm
parents:
29366
diff
changeset
|
565 |
fun map_future f x = |
29366 | 566 |
let |
29384
a3c7e9ae9b71
more robust propagation of errors through bulk jobs;
wenzelm
parents:
29366
diff
changeset
|
567 |
val task = task_of x; |
44300
349cc426d929
tuned signature -- treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset
|
568 |
val group = new_group (SOME (Task_Queue.group_of_task task)); |
44113 | 569 |
val (result, job) = future_job group true (fn () => f (join x)); |
29384
a3c7e9ae9b71
more robust propagation of errors through bulk jobs;
wenzelm
parents:
29366
diff
changeset
|
570 |
|
32246 | 571 |
val extended = SYNCHRONIZED "extend" (fn () => |
29366 | 572 |
(case Task_Queue.extend task job (! queue) of |
573 |
SOME queue' => (queue := queue'; true) |
|
574 |
| NONE => false)); |
|
575 |
in |
|
41683
73dde8006820
maintain Task_Queue.group within Task_Queue.task;
wenzelm
parents:
41681
diff
changeset
|
576 |
if extended then Future {promised = false, task = task, result = result} |
41672
2f70b1ddd09f
more direct Future.bulk, which potentially reduces overhead for Par_List;
wenzelm
parents:
41670
diff
changeset
|
577 |
else |
44330 | 578 |
(singleton o cond_forks) |
44301 | 579 |
{name = "map_future", group = SOME group, deps = [task], |
580 |
pri = Task_Queue.pri_of_task task, interrupts = true} |
|
41672
2f70b1ddd09f
more direct Future.bulk, which potentially reduces overhead for Par_List;
wenzelm
parents:
41670
diff
changeset
|
581 |
(fn () => f (join x)) |
29366 | 582 |
end; |
28979
3ce619d8d432
fork/map: no inheritance of group (structure is nested, not parallel);
wenzelm
parents:
28972
diff
changeset
|
583 |
|
28191 | 584 |
|
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
585 |
(* promised futures -- fulfilled by external means *) |
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
586 |
|
44298
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
44295
diff
changeset
|
587 |
fun promise_group group abort : 'a future = |
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
588 |
let |
35016 | 589 |
val result = Single_Assignment.var "promise" : 'a result; |
44298
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
44295
diff
changeset
|
590 |
fun assign () = assign_result group result Exn.interrupt_exn |
39243
307e3d07d19f
Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
wenzelm
parents:
39232
diff
changeset
|
591 |
handle Fail _ => true |
307e3d07d19f
Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
wenzelm
parents:
39232
diff
changeset
|
592 |
| exn => |
44298
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
44295
diff
changeset
|
593 |
if Exn.is_interrupt exn |
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
44295
diff
changeset
|
594 |
then raise Fail "Concurrent attempt to fulfill promise" |
39243
307e3d07d19f
Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
wenzelm
parents:
39232
diff
changeset
|
595 |
else reraise exn; |
44298
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
44295
diff
changeset
|
596 |
fun job () = |
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
44295
diff
changeset
|
597 |
Multithreading.with_attributes Multithreading.no_interrupts |
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
44295
diff
changeset
|
598 |
(fn _ => assign () before abort ()); |
37854
047c96f41455
back to more strict dependencies, even for canceled groups (reverting parts of 02936e77a07c);
wenzelm
parents:
37852
diff
changeset
|
599 |
val task = SYNCHRONIZED "enqueue_passive" (fn () => |
44298
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
44295
diff
changeset
|
600 |
Unsynchronized.change_result queue (Task_Queue.enqueue_passive group job)); |
41683
73dde8006820
maintain Task_Queue.group within Task_Queue.task;
wenzelm
parents:
41681
diff
changeset
|
601 |
in Future {promised = true, task = task, result = result} end; |
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
602 |
|
44298
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
44295
diff
changeset
|
603 |
fun promise abort = promise_group (worker_subgroup ()) abort; |
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
604 |
|
41683
73dde8006820
maintain Task_Queue.group within Task_Queue.task;
wenzelm
parents:
41681
diff
changeset
|
605 |
fun fulfill_result (Future {promised, task, result}) res = |
39243
307e3d07d19f
Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
wenzelm
parents:
39232
diff
changeset
|
606 |
if not promised then raise Fail "Not a promised future" |
307e3d07d19f
Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
wenzelm
parents:
39232
diff
changeset
|
607 |
else |
307e3d07d19f
Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
wenzelm
parents:
39232
diff
changeset
|
608 |
let |
41683
73dde8006820
maintain Task_Queue.group within Task_Queue.task;
wenzelm
parents:
41681
diff
changeset
|
609 |
val group = Task_Queue.group_of_task task; |
39243
307e3d07d19f
Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
wenzelm
parents:
39232
diff
changeset
|
610 |
fun job ok = assign_result group result (if ok then res else Exn.interrupt_exn); |
307e3d07d19f
Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
wenzelm
parents:
39232
diff
changeset
|
611 |
val _ = |
307e3d07d19f
Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
wenzelm
parents:
39232
diff
changeset
|
612 |
Multithreading.with_attributes Multithreading.no_interrupts (fn _ => |
307e3d07d19f
Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
wenzelm
parents:
39232
diff
changeset
|
613 |
let |
307e3d07d19f
Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
wenzelm
parents:
39232
diff
changeset
|
614 |
val still_passive = |
307e3d07d19f
Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
wenzelm
parents:
39232
diff
changeset
|
615 |
SYNCHRONIZED "fulfill_result" (fn () => |
307e3d07d19f
Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
wenzelm
parents:
39232
diff
changeset
|
616 |
Unsynchronized.change_result queue |
307e3d07d19f
Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
wenzelm
parents:
39232
diff
changeset
|
617 |
(Task_Queue.dequeue_passive (Thread.self ()) task)); |
44110 | 618 |
in if still_passive then worker_exec (task, [job]) else () end); |
41681
b5d7b15166bf
Future.join_results: discontinued post-hoc recording of dynamic dependencies;
wenzelm
parents:
41680
diff
changeset
|
619 |
val _ = |
41695
afdbec23b92b
eliminated slightly odd abstract type Task_Queue.deps;
wenzelm
parents:
41683
diff
changeset
|
620 |
if is_some (Single_Assignment.peek result) then () |
afdbec23b92b
eliminated slightly odd abstract type Task_Queue.deps;
wenzelm
parents:
41683
diff
changeset
|
621 |
else worker_waiting [task] (fn () => ignore (Single_Assignment.await result)); |
39243
307e3d07d19f
Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
wenzelm
parents:
39232
diff
changeset
|
622 |
in () end; |
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
623 |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
43665
diff
changeset
|
624 |
fun fulfill x res = fulfill_result x (Exn.Res res); |
34277
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
625 |
|
7325a5e3587f
added Future.promise/fulfill -- promised futures that are fulfilled by external means;
wenzelm
parents:
33416
diff
changeset
|
626 |
|
32228
7622c03141b0
scheduler: shutdown spontaneously (after some delay) if queue is empty;
wenzelm
parents:
32227
diff
changeset
|
627 |
(* shutdown *) |
29366 | 628 |
|
28203 | 629 |
fun shutdown () = |
28276 | 630 |
if Multithreading.available then |
631 |
SYNCHRONIZED "shutdown" (fn () => |
|
32228
7622c03141b0
scheduler: shutdown spontaneously (after some delay) if queue is empty;
wenzelm
parents:
32227
diff
changeset
|
632 |
while scheduler_active () do |
34279
02936e77a07c
tasks of canceled groups are considered "ready" -- enables to purge the queue from tasks depending on unfinished promises (also improves general reactivity);
wenzelm
parents:
34277
diff
changeset
|
633 |
(wait scheduler_event; broadcast_work ())) |
28276 | 634 |
else (); |
28203 | 635 |
|
29366 | 636 |
|
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
37904
diff
changeset
|
637 |
(* status markup *) |
37690
b16231572c61
general Future.report -- also for Toplevel.async_state;
wenzelm
parents:
37682
diff
changeset
|
638 |
|
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
37904
diff
changeset
|
639 |
fun status e = |
37690
b16231572c61
general Future.report -- also for Toplevel.async_state;
wenzelm
parents:
37682
diff
changeset
|
640 |
let |
40448 | 641 |
val task_props = |
642 |
(case worker_task () of |
|
643 |
NONE => I |
|
644 |
| SOME task => Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]); |
|
43665 | 645 |
val _ = Output.status (Markup.markup_only (task_props Markup.forked)); |
37690
b16231572c61
general Future.report -- also for Toplevel.async_state;
wenzelm
parents:
37682
diff
changeset
|
646 |
val x = e (); (*sic -- report "joined" only for success*) |
43665 | 647 |
val _ = Output.status (Markup.markup_only (task_props Markup.joined)); |
37690
b16231572c61
general Future.report -- also for Toplevel.async_state;
wenzelm
parents:
37682
diff
changeset
|
648 |
in x end; |
b16231572c61
general Future.report -- also for Toplevel.async_state;
wenzelm
parents:
37682
diff
changeset
|
649 |
|
b16231572c61
general Future.report -- also for Toplevel.async_state;
wenzelm
parents:
37682
diff
changeset
|
650 |
|
29366 | 651 |
(*final declarations of this structure!*) |
652 |
val map = map_future; |
|
653 |
||
28156 | 654 |
end; |
28972 | 655 |
|
656 |
type 'a future = 'a Future.future; |
|
657 |