# HG changeset patch # User wenzelm # Date 1403518820 -7200 # Node ID 4817154180d6978d9acb45dc9cc9b51f82c63664 # Parent a6b1847b6335fb350becd798d95140be1827e47a more on "Futures"; diff -r a6b1847b6335 -r 4817154180d6 src/Doc/Implementation/ML.thy --- a/src/Doc/Implementation/ML.thy Sat Jun 21 21:33:00 2014 +0200 +++ b/src/Doc/Implementation/ML.thy Mon Jun 23 12:20:20 2014 +0200 @@ -2100,12 +2100,12 @@ subsection {* Lazy evaluation *} text {* - Classic lazy evaluation works via two operations: @{text lazy} to wrap an - unevaluated expression, and @{text force} to evaluate it once and store its - result persistently. Later invocations of @{text force} retrieve the stored - result without another evaluation. Isabelle/ML refines this idea to - accommodate the aspects of multi-threading, synchronous program exceptions - and asynchronous interrupts. + Classic lazy evaluation works via the @{text lazy}~/ @{text force} pair of + operations: @{text lazy} to wrap an unevaluated expression, and @{text + force} to evaluate it once and store its result persistently. Later + invocations of @{text force} retrieve the stored result without another + evaluation. Isabelle/ML refines this idea to accommodate the aspects of + multi-threading, synchronous program exceptions and asynchronous interrupts. The first thread that invokes @{text force} on an unfinished lazy value changes its state into a \emph{promise} of the eventual result and starts @@ -2141,8 +2141,8 @@ \item @{ML Lazy.value}~@{text a} wraps the value @{text a} as finished lazy value. When forced, it returns @{text a} without any further evaluation. - The overhead of this pro-forma wrapping of strict values as lazy values is - very low. + There is very low overhead for this proforma wrapping of strict values as + lazy values. \item @{ML Lazy.force}~@{text x} produces the result of the lazy value in a thread-safe manner as explained above. Thus it may cause the current thread @@ -2152,22 +2152,56 @@ *} -subsection {* Future values \label{sec:futures} *} +subsection {* Futures \label{sec:futures} *} text {* - %FIXME - - See also @{file "~~/src/Pure/Concurrent/future.ML"}. + 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). + + 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. + + \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 + future is a new sub-group of the presently running one, but it is also + possible to indicate different group layouts under program control. + + Cancellation of futures actually refers to the corresponding task group and + all its sub-groups. Thus interrupts are propagated down the group hierarchy. + 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. + + \medskip A \emph{passive future} or \emph{promise} is a future with slightly + different evaluation policies: there is only a single-assignment variable + and some expression to evaluate for the \emph{failed} case (e.g.\ to clean + up resources when canceled). A regular result is produced by external means, + using a separate \emph{fulfill} operation. + + Promises are managed in the same task queue, so regular futures may depend + on them. This allows a form of reactive programming, where some promises are + used as minimal elements (or guards) within the future dependency graph: + when these promises are fulfilled the evaluation of subsequent futures + starts spontaneously, according to their own inter-dependencies. *} - text %mlref {* \begin{mldecls} @{index_ML_type "'a future"} \\ @{index_ML Future.fork: "(unit -> 'a) -> 'a future"} \\ @{index_ML Future.forks: "Future.params -> (unit -> 'a) list -> 'a future list"} \\ + @{index_ML Future.join: "'a future -> 'a"} \\ + @{index_ML Future.joins: "'a future list -> 'a list"} \\ @{index_ML Future.value: "'a -> 'a future"} \\ - @{index_ML Future.join: "'a future -> 'a"} \\ @{index_ML Future.map: "('a -> 'b) -> 'a future -> 'b future"} \\ @{index_ML Future.cancel: "'a future -> unit"} \\ @{index_ML Future.cancel_group: "Future.group -> unit"} \\[0.5ex] @@ -2201,8 +2235,7 @@ \item @{text "deps : Future.task list"} (default @{ML "[]"}) specifies dependencies on other future tasks, i.e.\ the adjacency relation in the - global task queue. Dependencies on already finished future tasks are - ignored. + global task queue. Dependencies on already finished tasks are ignored. \item @{text "pri : int"} (default @{ML 0}) specifies a priority within the task queue. @@ -2211,7 +2244,7 @@ As a rule of thumb, @{ML "~1"} means ``low priority" and @{ML 1} means ``high priority''. - Note that the priority only affects the position in the task queue, not a + Note that the task priority only affects the position in the queue, not the thread priority. When a worker thread picks up a task for processing, it runs with the normal thread priority to the end (or until canceled). Higher priority tasks that are queued later need to wait until this (or another) @@ -2219,8 +2252,8 @@ \item @{text "interrupts : bool"} (default @{ML true}) tells whether the worker thread that processes the corresponding task is initially put into - interruptible state. Note that it may change this state later while running, - by modifying the thread attributes. + interruptible state. This state may change again while running, by modifying + the thread attributes. With interrupts disabled, a running future task cannot be canceled. It is the responsibility of the programmer that this special state is retained @@ -2228,13 +2261,6 @@ \end{itemize} - \item @{ML Future.value}~@{text a} wraps the value @{text a} as finished - future value, bypassing the worker-thread farm. When joined, it returns - @{text a} without any further evaluation. - - The overhead of this pro-forma wrapping of strict values as future values is - very low. - \item @{ML Future.join}~@{text x} retrieves the value of an already finished future, which may lead to an exception, according to the result of its previous evaluation. @@ -2243,18 +2269,36 @@ the current thread and the status of the future. A non-worker thread waits passively until the future is eventually evaluated. A worker thread temporarily changes its task context and takes over the responsibility to - evaluate the future expression on the spot; this is done in a thread-safe - manner: other threads that intend to join the same future need to wait until - the ongoing evaluation is finished. - - Excessive use of dynamic dependencies of futures by adhoc joining may lead - to bad utilization of CPU cores, due to threads waiting on other threads to - finish required futures. The future task farm has a limited amount of - replacement threads that continue working on other tasks after some timeout. + evaluate the future expression on the spot. The latter is done in a + thread-safe manner: other threads that intend to join the same future need + to wait until the ongoing evaluation is finished. + + Note that excessive use of dynamic dependencies of futures by adhoc joining + may lead to bad utilization of CPU cores, due to threads waiting on other + threads to finish required futures. The future task farm has a limited + amount of replacement threads that continue working on unrelated tasks after + some timeout. Whenever possible, static dependencies of futures should be specified - explicitly when forked. Thus the evaluation can work from the bottom up, - without join conflicts and wait states. + explicitly when forked (see @{text deps} above). Thus the evaluation can + work from the bottom up, without join conflicts and wait states. + + \item @{ML Future.joins}~@{text xs} joins the given list of futures + simultaneously, which is more efficient than @{ML "map Future.join"}~@{text + xs}. + + Based on the dependency graph of tasks, the current thread takes over the + responsibility to evaluate future expressions that are required for the main + result, working from the bottom up. Waiting on future results that are + presently evaluated on other threads only happens as last resort, when no + other unfinished futures are left over. + + \item @{ML Future.value}~@{text a} wraps the value @{text a} as finished + future value, bypassing the worker-thread farm. When joined, it returns + @{text a} without any further evaluation. + + There is very low overhead for this proforma wrapping of strict values as + future values. \item @{ML Future.map}~@{text "f x"} is a fast-path implementation of @{ML Future.fork}~@{text "(fn () => f ("}@{ML Future.join}~@{text "x))"}, which @@ -2265,9 +2309,10 @@ \item @{ML Future.cancel}~@{text "x"} cancels the task group of the given future, using @{ML Future.cancel_group} below. - \item @{ML Future.cancel_group}~@{text "g"} cancels all tasks of the given - group for all time. Threads that are presently processing a task of the - given group are interrupted. Tasks that are queued but not yet processed are + \item @{ML Future.cancel_group}~@{text "group"} cancels all tasks of the + given task group for all time. Threads that are presently processing a task + of the given group are interrupted: it may take some time until they are + actually terminated. Tasks that are queued but not yet processed are dequeued and forced into interrupted state. Since the task group is itself invalidated, any further attempt to fork a future that belongs to it will yield a canceled result as well.