src/Pure/Concurrent/lazy.ML
author wenzelm
Sun, 28 Dec 2014 21:34:45 +0100
changeset 59193 59f1591a11cb
parent 59191 682aa538c5c0
child 59195 f8588372d70e
permissions -rw-r--r--
eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer); clarified Command.run_process etc.: join running eval, bypass running print; eliminated Command.memo in favour of regular Lazy.lazy; more Lazy.lazy status information;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
     1
(*  Title:      Pure/Concurrent/lazy.ML
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
     2
    Author:     Makarius
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
     3
34278
228f27469139 do not memoize interrupts;
wenzelm
parents: 33023
diff changeset
     4
Lazy evaluation with memoing of results and regular exceptions.
40389
511e5263f5c6 tuned comments;
wenzelm
parents: 39232
diff changeset
     5
Parallel version based on (passive) futures, to avoid critical or
511e5263f5c6 tuned comments;
wenzelm
parents: 39232
diff changeset
     6
multiple evaluation (unless interrupted).
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
     7
*)
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
     8
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
     9
signature LAZY =
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    10
sig
28971
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    11
  type 'a lazy
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    12
  val lazy: (unit -> 'a) -> 'a lazy
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    13
  val value: 'a -> 'a lazy
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    14
  val peek: 'a lazy -> 'a Exn.result option
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    15
  val is_running: 'a lazy -> bool
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    16
  val is_finished: 'a lazy -> bool
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    17
  val finished_result: 'a lazy -> 'a Exn.result option
29422
fdf396a24a9f added force_result;
wenzelm
parents: 28971
diff changeset
    18
  val force_result: 'a lazy -> 'a Exn.result
28971
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    19
  val force: 'a lazy -> 'a
44386
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    20
  val map: ('a -> 'b) -> 'a lazy -> 'b lazy
44427
c4a86d72a5cc tuned signature;
wenzelm
parents: 44387
diff changeset
    21
  val future: Future.params -> 'a lazy -> 'a future
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    22
end;
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    23
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    24
structure Lazy: LAZY =
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    25
struct
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    26
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    27
(* datatype *)
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    28
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    29
datatype 'a expr =
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    30
  Expr of unit -> 'a |
37183
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    31
  Result of 'a future;
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    32
37183
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    33
abstype 'a lazy = Lazy of 'a expr Synchronized.var
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    34
with
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    35
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    36
fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    37
fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    38
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    39
fun peek (Lazy var) =
59147
eb3e399f5b9f peek value without synchronization;
wenzelm
parents: 47430
diff changeset
    40
  (case Synchronized.peek var of
37183
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    41
    Expr _ => NONE
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    42
  | Result res => Future.peek res);
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    43
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    44
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    45
(* status *)
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    46
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    47
fun is_future pred (Lazy var) =
59191
682aa538c5c0 more thorough Lazy.is_finished;
wenzelm
parents: 59147
diff changeset
    48
  (case Synchronized.value var of
682aa538c5c0 more thorough Lazy.is_finished;
wenzelm
parents: 59147
diff changeset
    49
    Expr _ => false
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    50
  | Result res => pred res);
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    51
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    52
fun is_running x = is_future (not o Future.is_finished) x;
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    53
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    54
fun is_finished x =
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    55
  is_future (fn res =>
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    56
    Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res))) x;
59191
682aa538c5c0 more thorough Lazy.is_finished;
wenzelm
parents: 59147
diff changeset
    57
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    58
fun finished_result (Lazy var) =
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    59
  (case Synchronized.value var of
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    60
    Expr _ => NONE
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    61
  | Result res =>
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    62
      if Future.is_finished res then
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    63
        let val result = Future.join_result res
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    64
        in if Exn.is_interrupt_exn result then NONE else SOME result end
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    65
      else NONE);
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    66
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    67
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    68
(* force result *)
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    69
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    70
fun force_result (Lazy var) =
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    71
  (case peek (Lazy var) of
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    72
    SOME res => res
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    73
  | NONE =>
41701
430493d65cd2 Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents: 40482
diff changeset
    74
      uninterruptible (fn restore_attributes => fn () =>
37183
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    75
        let
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    76
          val (expr, x) =
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    77
            Synchronized.change_result var
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    78
              (fn Expr e =>
44298
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 44198
diff changeset
    79
                    let val x = Future.promise I
37183
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    80
                    in ((SOME e, x), Result x) end
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    81
                | Result x => ((NONE, x), Result x));
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    82
        in
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    83
          (case expr of
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    84
            SOME e =>
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    85
              let
41701
430493d65cd2 Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents: 40482
diff changeset
    86
                val res0 = Exn.capture (restore_attributes e) ();
47430
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    87
                val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    88
                val res = Future.join_result x;
37183
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    89
                (*semantic race: some other threads might see the same
40389
511e5263f5c6 tuned comments;
wenzelm
parents: 39232
diff changeset
    90
                  interrupt, until there is a fresh start*)
47430
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    91
                val _ =
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    92
                  if Exn.is_interrupt_exn res then
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    93
                    Synchronized.change var (fn _ => Expr e)
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    94
                  else ();
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    95
              in res end
41701
430493d65cd2 Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents: 40482
diff changeset
    96
          | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
37183
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    97
        end) ());
29422
fdf396a24a9f added force_result;
wenzelm
parents: 28971
diff changeset
    98
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    99
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
   100
end;
44386
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
   101
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
   102
fun force r = Exn.release (force_result r);
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
   103
fun map f x = lazy (fn () => f (force x));
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
   104
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
   105
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
   106
(* future evaluation *)
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
   107
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
   108
fun future params x =
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
   109
  if is_finished x then Future.value_result (force_result x)
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
   110
  else (singleton o Future.forks) params (fn () => force x);
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
   111
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
   112
end;
28971
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
   113
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
   114
type 'a lazy = 'a Lazy.lazy;
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
   115