# HG changeset patch # User wenzelm # Date 1221133422 -7200 # Node ID 7ae5cdb7b122d26cb04b01be7468e9e6b67bd2f1 # Parent 5ef2c4bde4e5b90d5c930f02bb6cf7877d9a1cb0 some general notes on future values; diff -r 5ef2c4bde4e5 -r 7ae5cdb7b122 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Thu Sep 11 13:24:19 2008 +0200 +++ b/src/Pure/Concurrent/future.ML Thu Sep 11 13:43:42 2008 +0200 @@ -2,7 +2,27 @@ ID: $Id$ Author: Makarius -Functional threads as future values. +Future values. + +Notes: + + * Futures are similar to delayed evaluation, i.e. delay/force is + generalized to fork/join (and variants). The idea is to model + parallel value-oriented computations, but *not* communicating + processes. + + * Futures are grouped; failure of one group member causes the whole + group to be interrupted eventually. + + * 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 is 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. *) signature FUTURE =