1.1 --- a/src/Doc/Implementation/ML.thy	Sat Jun 21 12:19:34 2014 +0200
     1.2 +++ b/src/Doc/Implementation/ML.thy	Sat Jun 21 21:33:00 2014 +0200
     1.3 @@ -2161,4 +2161,127 @@
     1.4  *}
     1.5  
     1.6  
     1.7 +text %mlref {*
     1.8 +  \begin{mldecls}
     1.9 +  @{index_ML_type "'a future"} \\
    1.10 +  @{index_ML Future.fork: "(unit -> 'a) -> 'a future"} \\
    1.11 +  @{index_ML Future.forks: "Future.params -> (unit -> 'a) list -> 'a future list"} \\
    1.12 +  @{index_ML Future.value: "'a -> 'a future"} \\
    1.13 +  @{index_ML Future.join: "'a future -> 'a"} \\
    1.14 +  @{index_ML Future.map: "('a -> 'b) -> 'a future -> 'b future"} \\
    1.15 +  @{index_ML Future.cancel: "'a future -> unit"} \\
    1.16 +  @{index_ML Future.cancel_group: "Future.group -> unit"} \\[0.5ex]
    1.17 +  @{index_ML Future.promise: "(unit -> unit) -> 'a future"} \\
    1.18 +  @{index_ML Future.fulfill: "'a future -> 'a -> unit"} \\
    1.19 +  \end{mldecls}
    1.20 +
    1.21 +  \begin{description}
    1.22 +
    1.23 +  \item Type @{ML_type "'a future"} represents future values over type
    1.24 +  @{verbatim "'a"}.
    1.25 +
    1.26 +  \item @{ML Future.fork}~@{text "(fn () => e)"} registers the unevaluated
    1.27 +  expression @{text e} as unfinished future value, to be evaluated eventually
    1.28 +  on the parallel worker-thread farm. This is a shorthand for @{ML
    1.29 +  Future.forks} below, with default parameters and a single expression.
    1.30 +
    1.31 +  \item @{ML Future.forks}~@{text "params exprs"} is the general interface to
    1.32 +  fork several futures simultaneously. The @{text params} consist of the
    1.33 +  following fields:
    1.34 +
    1.35 +  \begin{itemize}
    1.36 +
    1.37 +  \item @{text "name : string"} (default @{ML "\"\""}) specifies a common name
    1.38 +  for the tasks of the forked futures, which serves diagnostic purposes.
    1.39 +
    1.40 +  \item @{text "group : Future.group option"} (default @{ML NONE}) specifies
    1.41 +  an optional task group for the forked futures. @{ML NONE} means that a new
    1.42 +  sub-group of the current worker-thread task context is created. If this is
    1.43 +  not a worker thread, the group will be a new root in the group hierarchy.
    1.44 +
    1.45 +  \item @{text "deps : Future.task list"} (default @{ML "[]"}) specifies
    1.46 +  dependencies on other future tasks, i.e.\ the adjacency relation in the
    1.47 +  global task queue. Dependencies on already finished future tasks are
    1.48 +  ignored.
    1.49 +
    1.50 +  \item @{text "pri : int"} (default @{ML 0}) specifies a priority within the
    1.51 +  task queue.
    1.52 +
    1.53 +  Typically there is only little deviation from the default priority @{ML 0}.
    1.54 +  As a rule of thumb, @{ML "~1"} means ``low priority" and @{ML 1} means
    1.55 +  ``high priority''.
    1.56 +
    1.57 +  Note that the priority only affects the position in the task queue, not a
    1.58 +  thread priority. When a worker thread picks up a task for processing, it
    1.59 +  runs with the normal thread priority to the end (or until canceled). Higher
    1.60 +  priority tasks that are queued later need to wait until this (or another)
    1.61 +  worker thread becomes free again.
    1.62 +
    1.63 +  \item @{text "interrupts : bool"} (default @{ML true}) tells whether the
    1.64 +  worker thread that processes the corresponding task is initially put into
    1.65 +  interruptible state. Note that it may change this state later while running,
    1.66 +  by modifying the thread attributes.
    1.67 +
    1.68 +  With interrupts disabled, a running future task cannot be canceled.  It is
    1.69 +  the responsibility of the programmer that this special state is retained
    1.70 +  only briefly.
    1.71 +
    1.72 +  \end{itemize}
    1.73 +
    1.74 +  \item @{ML Future.value}~@{text a} wraps the value @{text a} as finished
    1.75 +  future value, bypassing the worker-thread farm. When joined, it returns
    1.76 +  @{text a} without any further evaluation.
    1.77 +
    1.78 +  The overhead of this pro-forma wrapping of strict values as future values is
    1.79 +  very low.
    1.80 +
    1.81 +  \item @{ML Future.join}~@{text x} retrieves the value of an already finished
    1.82 +  future, which may lead to an exception, according to the result of its
    1.83 +  previous evaluation.
    1.84 +
    1.85 +  For an unfinished future there are several cases depending on the role of
    1.86 +  the current thread and the status of the future. A non-worker thread waits
    1.87 +  passively until the future is eventually evaluated. A worker thread
    1.88 +  temporarily changes its task context and takes over the responsibility to
    1.89 +  evaluate the future expression on the spot; this is done in a thread-safe
    1.90 +  manner: other threads that intend to join the same future need to wait until
    1.91 +  the ongoing evaluation is finished.
    1.92 +
    1.93 +  Excessive use of dynamic dependencies of futures by adhoc joining may lead
    1.94 +  to bad utilization of CPU cores, due to threads waiting on other threads to
    1.95 +  finish required futures. The future task farm has a limited amount of
    1.96 +  replacement threads that continue working on other tasks after some timeout.
    1.97 +
    1.98 +  Whenever possible, static dependencies of futures should be specified
    1.99 +  explicitly when forked. Thus the evaluation can work from the bottom up,
   1.100 +  without join conflicts and wait states.
   1.101 +
   1.102 +  \item @{ML Future.map}~@{text "f x"} is a fast-path implementation of @{ML
   1.103 +  Future.fork}~@{text "(fn () => f ("}@{ML Future.join}~@{text "x))"}, which
   1.104 +  avoids the full overhead of the task queue and worker-thread farm as far as
   1.105 +  possible. The function @{text f} is supposed to be some trivial
   1.106 +  post-processing or projection of the future result.
   1.107 +
   1.108 +  \item @{ML Future.cancel}~@{text "x"} cancels the task group of the given
   1.109 +  future, using @{ML Future.cancel_group} below.
   1.110 +
   1.111 +  \item @{ML Future.cancel_group}~@{text "g"} cancels all tasks of the given
   1.112 +  group for all time. Threads that are presently processing a task of the
   1.113 +  given group are interrupted. Tasks that are queued but not yet processed are
   1.114 +  dequeued and forced into interrupted state. Since the task group is itself
   1.115 +  invalidated, any further attempt to fork a future that belongs to it will
   1.116 +  yield a canceled result as well.
   1.117 +
   1.118 +  \item @{ML Future.promise}~@{text abort} registers a passive future with the
   1.119 +  given @{text abort} operation: it is invoked when the future task group is
   1.120 +  canceled.
   1.121 +
   1.122 +  \item @{ML Future.fulfill}~@{text "x a"} finishes the passive future @{text
   1.123 +  x} by the given value @{text a}. If the promise has already been canceled,
   1.124 +  the attempt to fulfill it causes an exception.
   1.125 +
   1.126 +  \end{description}
   1.127 +*}
   1.128 +
   1.129 +
   1.130  end