1.1 --- a/src/Pure/Concurrent/future.ML	Thu Aug 18 15:51:34 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Thu Aug 18 16:07:58 2011 +0200
     1.3 @@ -1,19 +1,15 @@
     1.4  (*  Title:      Pure/Concurrent/future.ML
     1.5      Author:     Makarius
     1.6  
     1.7 -Future values, see also
     1.8 +Value-oriented parallelism via futures and promises.  See also
     1.9  http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf
    1.10  http://www4.in.tum.de/~wenzelm/papers/parallel-ml.pdf
    1.11  
    1.12  Notes:
    1.13  
    1.14    * Futures are similar to delayed evaluation, i.e. delay/force is
    1.15 -    generalized to fork/join (and variants).  The idea is to model
    1.16 -    parallel value-oriented computations, but *not* communicating
    1.17 -    processes.
    1.18 -
    1.19 -  * Futures are grouped; failure of one group member causes the whole
    1.20 -    group to be interrupted eventually.  Groups are block-structured.
    1.21 +    generalized to fork/join.  The idea is to model parallel
    1.22 +    value-oriented computations (not communicating processes).
    1.23  
    1.24    * Forked futures are evaluated spontaneously by a farm of worker
    1.25      threads in the background; join resynchronizes the computation and
    1.26 @@ -21,13 +17,23 @@
    1.27  
    1.28    * The pool of worker threads is limited, usually in correlation with
    1.29      the number of physical cores on the machine.  Note that allocation
    1.30 -    of runtime resources is distorted either if workers yield CPU time
    1.31 -    (e.g. via system sleep or wait operations), or if non-worker
    1.32 +    of runtime resources may be distorted either if workers yield CPU
    1.33 +    time (e.g. via system sleep or wait operations), or if non-worker
    1.34      threads contend for significant runtime resources independently.
    1.35 +    There is a limited number of replacement worker threads that get
    1.36 +    activated in certain explicit wait conditions.
    1.37  
    1.38 -  * Promised futures are fulfilled by external means.  There is no
    1.39 -    associated evaluation task, but other futures can depend on them
    1.40 -    as usual.
    1.41 +  * Future tasks are organized in groups, which are block-structured.
    1.42 +    When forking a new new task, the default is to open an individual
    1.43 +    subgroup, unless some common group is specified explicitly.
    1.44 +    Failure of one group member causes the immediate peers to be
    1.45 +    interrupted eventually (i.e. none by default).  Interrupted tasks
    1.46 +    that lack regular result information, will pick up parallel
    1.47 +    exceptions from the cumulative group context (as Par_Exn).
    1.48 +
    1.49 +  * Promised "passive" futures are fulfilled by external means.  There
    1.50 +    is no associated evaluation task, but other futures can depend on
    1.51 +    them via regular join operations.
    1.52  *)
    1.53  
    1.54  signature FUTURE =