1 (* Title: Pure/Concurrent/future.ML |
1 (* Title: Pure/Concurrent/future.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Value-oriented parallelism via futures and promises. See also |
4 Value-oriented parallel execution via futures and promises. |
5 http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf |
|
6 http://www4.in.tum.de/~wenzelm/papers/parallel-ml.pdf |
|
7 |
|
8 Notes: |
|
9 |
|
10 * Futures are similar to delayed evaluation, i.e. delay/force is |
|
11 generalized to fork/join. The idea is to model parallel |
|
12 value-oriented computations (not communicating processes). |
|
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 |
|
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 |
|
22 threads contend for significant runtime resources independently. |
|
23 There is a limited number of replacement worker threads that get |
|
24 activated in certain explicit wait conditions. |
|
25 |
|
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 peer and subgroup members to be |
|
30 interrupted eventually. Interrupted tasks that lack regular |
|
31 result information, will pick up parallel exceptions from the |
|
32 cumulative group context (as Par_Exn). |
|
33 |
|
34 * Future task groups may be canceled: present and future group |
|
35 members will be interrupted eventually. |
|
36 |
|
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. |
|
40 *) |
5 *) |
41 |
6 |
42 signature FUTURE = |
7 signature FUTURE = |
43 sig |
8 sig |
44 type task = Task_Queue.task |
9 type task = Task_Queue.task |