--- a/src/Doc/Implementation/ML.thy Mon Jun 23 12:20:20 2014 +0200
+++ b/src/Doc/Implementation/ML.thy Mon Jun 23 12:54:48 2014 +0200
@@ -2157,17 +2157,27 @@
text {*
Futures help to organize parallel execution in a value-oriented manner, with
@{text fork}~/ @{text join} as the main pair of operations, and some further
- variants. Unlike lazy values, futures are evaluated strictly and
- spontaneously on separate worker threads. Futures may be canceled, which
- leads to interrupts on running evaluation attempts, and forces structurally
- related futures to fail for all time. Exceptions between related futures are
- propagated as well, and turned into parallel exceptions (see above).
+ variants; see also \cite{Wenzel:2009,Wenzel:2013:ITP}. Unlike lazy values,
+ futures are evaluated strictly and spontaneously on separate worker threads.
+ Futures may be canceled, which leads to interrupts on running evaluation
+ attempts, and forces structurally related futures to fail for all time;
+ already finished futures remain unchanged. Exceptions between related
+ futures are propagated as well, and turned into parallel exceptions (see
+ above).
Technically, a future is a single-assignment variable together with a
\emph{task} that serves administrative purposes, notably within the
\emph{task queue} where new futures are registered for eventual evaluation
and the worker threads retrieve their work.
+ The pool of worker threads is limited, in correlation with the number of
+ physical cores on the machine. Note that allocation of runtime resources may
+ be distorted either if workers yield CPU time (e.g.\ via system sleep or
+ wait operations), or if non-worker threads contend for significant runtime
+ resources independently. There is a limited number of replacement worker
+ threads that get activated in certain explicit wait conditions, after a
+ timeout.
+
\medskip Each future task belongs to some \emph{task group}, which
represents the hierarchic structure of related tasks, together with the
exception status a that point. By default, the task group of a newly created
@@ -2179,7 +2189,9 @@
Regular program exceptions are treated likewise: failure of the evaluation
of some future task affects its own group and all sub-groups. Given a
particular task group, its \emph{group status} cumulates all relevant
- exceptions according to its position within the group hierarchy.
+ exceptions according to its position within the group hierarchy. Interrupted
+ tasks that lack regular result information, will pick up parallel exceptions
+ from the cumulative group status.
\medskip A \emph{passive future} or \emph{promise} is a future with slightly
different evaluation policies: there is only a single-assignment variable
--- a/src/Pure/Concurrent/future.ML Mon Jun 23 12:20:20 2014 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Jun 23 12:54:48 2014 +0200
@@ -1,42 +1,7 @@
(* Title: Pure/Concurrent/future.ML
Author: Makarius
-Value-oriented parallelism via futures and promises. See also
-http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf
-http://www4.in.tum.de/~wenzelm/papers/parallel-ml.pdf
-
-Notes:
-
- * Futures are similar to delayed evaluation, i.e. delay/force is
- generalized to fork/join. The idea is to model parallel
- value-oriented computations (not communicating processes).
-
- * Forked futures are evaluated spontaneously by a farm of worker
- threads in the background; join resynchronizes the computation and
- delivers results (values or exceptions).
-
- * The pool of worker threads is limited, usually in correlation with
- the number of physical cores on the machine. Note that allocation
- of runtime resources may be distorted either if workers yield CPU
- time (e.g. via system sleep or wait operations), or if non-worker
- threads contend for significant runtime resources independently.
- There is a limited number of replacement worker threads that get
- activated in certain explicit wait conditions.
-
- * Future tasks are organized in groups, which are block-structured.
- When forking a new new task, the default is to open an individual
- subgroup, unless some common group is specified explicitly.
- Failure of one group member causes peer and subgroup members to be
- interrupted eventually. Interrupted tasks that lack regular
- result information, will pick up parallel exceptions from the
- cumulative group context (as Par_Exn).
-
- * Future task groups may be canceled: present and future group
- members will be interrupted eventually.
-
- * Promised "passive" futures are fulfilled by external means. There
- is no associated evaluation task, but other futures can depend on
- them via regular join operations.
+Value-oriented parallel execution via futures and promises.
*)
signature FUTURE =
--- a/src/Pure/Concurrent/future.scala Mon Jun 23 12:20:20 2014 +0200
+++ b/src/Pure/Concurrent/future.scala Mon Jun 23 12:54:48 2014 +0200
@@ -2,7 +2,7 @@
Module: PIDE
Author: Makarius
-Value-oriented parallelism via futures and promises in Scala -- with
+Value-oriented parallel execution via futures and promises in Scala -- with
signatures as in Isabelle/ML.
*/