src/Pure/Concurrent/future.ML
author wenzelm
Sun, 07 Sep 2008 22:19:42 +0200
changeset 28156 5205f7979b4f
child 28162 55772e4e95e0
permissions -rw-r--r--
Functional threads as future values.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28156
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Concurrent/future.ML
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
     4
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
     5
Functional threads as future values.
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
     6
*)
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
     7
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
     8
signature FUTURE =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
     9
sig
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    10
  type 'a T
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    11
  eqtype id
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    12
  val id_of: 'a T -> id
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    13
  val interrupt: id -> unit
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    14
  val dependent_future: id list -> (unit -> 'a) -> 'a T
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    15
  val future: (unit -> 'a) -> 'a T
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    16
  val await: 'a T -> 'a
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    17
end;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    18
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    19
structure Future: FUTURE =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    20
struct
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    21
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    22
(* synchronized execution *)
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    23
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    24
local
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    25
  val thread = ref (NONE: Thread.thread option);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    26
  val lock = Mutex.mutex ();
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    27
  val cond = ConditionVar.conditionVar ();
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    28
in
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    29
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    30
fun self_synchronized () =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    31
  (case ! thread of
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    32
    NONE => false
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    33
  | SOME t => Thread.equal (t, Thread.self ()));
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    34
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    35
fun SYNCHRONIZED e =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    36
  if self_synchronized () then e ()
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    37
  else
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    38
    uninterruptible (fn restore_attributes => fn () =>
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    39
      let
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    40
        val _ = Mutex.lock lock;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    41
        val _ = thread := SOME (Thread.self ());
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    42
        val result = Exn.capture (restore_attributes e) ();
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    43
        val _ = thread := NONE;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    44
        val _ = Mutex.unlock lock;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    45
      in Exn.release result end) ();
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    46
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    47
fun wait () = ConditionVar.wait (cond, lock);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    48
fun wait_timeout timeout = ConditionVar.waitUntil (cond, lock, Time.+ (Time.now (), timeout));
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    49
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    50
fun notify_all () = ConditionVar.broadcast cond;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    51
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    52
end;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    53
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    54
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    55
(* typed futures, unytped ids *)
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    56
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    57
datatype 'a T = Future of serial * 'a Exn.result option ref;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    58
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    59
datatype id = Id of serial;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    60
fun id_of (Future (id, _)) = Id id;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    61
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    62
local val tag = Universal.tag () : serial Universal.tag in
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    63
  fun get_id () = Thread.getLocal tag;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    64
  fun put_id id = Thread.setLocal (tag, id);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    65
end;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    66
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    67
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    68
(* ordered queue of tasks *)
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    69
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    70
datatype task =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    71
  Task of (unit -> unit) |
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    72
  Running of Thread.thread;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    73
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    74
datatype queue = Queue of task IntGraph.T * (serial * (unit -> unit)) Queue.T;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    75
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    76
val empty_queue = Queue (IntGraph.empty, Queue.empty);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    77
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    78
fun check_cache (queue as Queue (tasks, cache)) =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    79
  if not (Queue.is_empty cache) then queue
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    80
  else
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    81
    let
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    82
      val cache' = fold (fn id =>
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    83
        (case IntGraph.get_node tasks id of
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    84
          Task task => Queue.enqueue (id, task)
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    85
        | Running _ => I)) (IntGraph.minimals tasks) Queue.empty;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    86
    in Queue (tasks, cache') end;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    87
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    88
val next_task = check_cache #> (fn queue as Queue (tasks, cache) =>
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    89
  if Queue.is_empty cache then (NONE, queue)
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    90
  else
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    91
    let val (task, cache') = Queue.dequeue cache
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    92
    in (SOME task, Queue (tasks, cache')) end);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    93
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    94
fun get_task (Queue (tasks, _)) id = IntGraph.get_node tasks id;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    95
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    96
fun new_task deps id task (Queue (tasks, _)) =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    97
  let
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    98
    fun add_dep (Id dep) G = IntGraph.add_edge_acyclic (dep, id) G
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
    99
      handle IntGraph.UNDEF _ => G;  (*dep already finished*)
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   100
    val tasks' = tasks |> IntGraph.new_node (id, Task task) |> fold add_dep deps;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   101
  in Queue (tasks', Queue.empty) end;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   102
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   103
fun running_task id thread (Queue (tasks, cache)) =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   104
  Queue (IntGraph.map_node id (K (Running thread)) tasks, cache);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   105
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   106
fun finished_task id (Queue (tasks, _)) =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   107
  Queue (IntGraph.del_nodes [id] tasks, Queue.empty);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   108
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   109
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   110
(* global state *)
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   111
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   112
local val active = ref 0 in
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   113
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   114
fun change_active b = SYNCHRONIZED (fn () =>
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   115
  let
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   116
    val _ = change active (fn n => if b then n + 1 else n - 1);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   117
    val n = ! active;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   118
    val _ = Multithreading.tracing 1 (fn () => "SCHEDULE: " ^ string_of_int n ^ " active tasks");
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   119
  in () end);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   120
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   121
end;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   122
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   123
val tasks = ref empty_queue;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   124
val scheduler = ref (NONE: Thread.thread option);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   125
val workers = ref ([]: Thread.thread list);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   126
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   127
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   128
fun interrupt (Id id) = SYNCHRONIZED (fn () =>
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   129
  (case try (get_task (! tasks)) id of
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   130
    SOME (Running thread) => Thread.interrupt thread
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   131
  | _ => ()));
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   132
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   133
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   134
(* worker thread *)
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   135
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   136
fun excessive_threads () = false;  (* FIXME *)
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   137
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   138
fun worker_stop () =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   139
  (change_active false; change workers (filter (fn t => not (Thread.equal (t, Thread.self ())))));
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   140
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   141
fun worker_wait () =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   142
  (change_active false; wait (); change_active true);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   143
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   144
fun worker_loop () =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   145
  (case SYNCHRONIZED (fn () => change_result tasks next_task) of
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   146
    SOME (id, task) =>
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   147
      let
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   148
        val _ = SYNCHRONIZED (fn () => change tasks (running_task id (Thread.self ())));
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   149
        val _ = task ();
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   150
        val _ = SYNCHRONIZED (fn () => change tasks (finished_task id));
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   151
        val _ = notify_all ();
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   152
      in if excessive_threads () then worker_stop () else worker_loop () end
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   153
  | NONE => (worker_wait (); worker_loop ()));
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   154
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   155
fun worker_start () =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   156
 (change_active true;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   157
  change workers (cons (Thread.fork (worker_loop, Multithreading.no_interrupts))));
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   158
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   159
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   160
(* scheduler *)
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   161
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   162
fun scheduler_loop () =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   163
  let
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   164
    val m = Multithreading.max_threads_value ();
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   165
    val k = m - length (! workers);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   166
    val _ = if k > 0 then funpow k worker_start () else ();
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   167
  in wait_timeout (Time.fromSeconds 1); scheduler_loop () end;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   168
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   169
fun check_scheduler () = SYNCHRONIZED (fn () =>
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   170
  let
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   171
    val scheduler_active =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   172
      (case ! scheduler of
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   173
        NONE => false
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   174
      | SOME t => Thread.isActive t);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   175
  in
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   176
    if scheduler_active then ()
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   177
    else scheduler := SOME (Thread.fork (SYNCHRONIZED scheduler_loop, Multithreading.no_interrupts))
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   178
  end);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   179
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   180
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   181
(* future values *)
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   182
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   183
fun dependent_future deps (e: unit -> 'a) =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   184
  let
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   185
    val _ = check_scheduler ();
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   186
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   187
    val r = ref (NONE: 'a Exn.result option);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   188
    val task = Multithreading.with_attributes (Thread.getAttributes ())
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   189
      (fn _ => fn () => r := SOME (Exn.capture e ()));
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   190
    val id = serial ();
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   191
    val _ = SYNCHRONIZED (fn () => change tasks (new_task deps id task));
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   192
    val _ = notify_all ();
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   193
  in Future (id, r) end;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   194
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   195
fun future e = dependent_future [] e;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   196
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   197
fun await (Future (_, r)) =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   198
  let
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   199
    val _ = check_scheduler ();
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   200
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   201
    fun loop () =
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   202
      (case SYNCHRONIZED (fn () => ! r) of
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   203
        NONE => (wait (); loop ())
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   204
      | SOME res => Exn.release res);
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   205
  in loop () end;
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   206
5205f7979b4f Functional threads as future values.
wenzelm
parents:
diff changeset
   207
end;