# HG changeset patch # User wenzelm # Date 1403520888 -7200 # Node ID fc4d65afdf136a1d54bbd7419aede9cf70defcff # Parent 4817154180d6978d9acb45dc9cc9b51f82c63664 more on "Futures"; removed obsolete comments; diff -r 4817154180d6 -r fc4d65afdf13 src/Doc/Implementation/ML.thy --- 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 diff -r 4817154180d6 -r fc4d65afdf13 src/Pure/Concurrent/future.ML --- 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 = diff -r 4817154180d6 -r fc4d65afdf13 src/Pure/Concurrent/future.scala --- 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. */