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);
authorwenzelm
Sun Dec 28 21:34:45 2014 +0100 (2014-12-28)
changeset 5919359f1591a11cb
parent 59192 a1d6d6db781b
child 59194 b51489b75bb9
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;
src/Pure/Concurrent/lazy.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/Concurrent/lazy.ML	Sun Dec 28 12:37:03 2014 +0100
     1.2 +++ b/src/Pure/Concurrent/lazy.ML	Sun Dec 28 21:34:45 2014 +0100
     1.3 @@ -9,10 +9,12 @@
     1.4  signature LAZY =
     1.5  sig
     1.6    type 'a lazy
     1.7 -  val peek: 'a lazy -> 'a Exn.result option
     1.8 -  val is_finished: 'a lazy -> bool
     1.9    val lazy: (unit -> 'a) -> 'a lazy
    1.10    val value: 'a -> 'a lazy
    1.11 +  val peek: 'a lazy -> 'a Exn.result option
    1.12 +  val is_running: 'a lazy -> bool
    1.13 +  val is_finished: 'a lazy -> bool
    1.14 +  val finished_result: 'a lazy -> 'a Exn.result option
    1.15    val force_result: 'a lazy -> 'a Exn.result
    1.16    val force: 'a lazy -> 'a
    1.17    val map: ('a -> 'b) -> 'a lazy -> 'b lazy
    1.18 @@ -31,19 +33,36 @@
    1.19  abstype 'a lazy = Lazy of 'a expr Synchronized.var
    1.20  with
    1.21  
    1.22 +fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
    1.23 +fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
    1.24 +
    1.25  fun peek (Lazy var) =
    1.26    (case Synchronized.peek var of
    1.27      Expr _ => NONE
    1.28    | Result res => Future.peek res);
    1.29  
    1.30 -fun is_finished (Lazy var) =
    1.31 +
    1.32 +(* status *)
    1.33 +
    1.34 +fun is_future pred (Lazy var) =
    1.35    (case Synchronized.value var of
    1.36      Expr _ => false
    1.37 -  | Result res =>
    1.38 -      Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res)));
    1.39 +  | Result res => pred res);
    1.40 +
    1.41 +fun is_running x = is_future (not o Future.is_finished) x;
    1.42 +
    1.43 +fun is_finished x =
    1.44 +  is_future (fn res =>
    1.45 +    Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res))) x;
    1.46  
    1.47 -fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
    1.48 -fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
    1.49 +fun finished_result (Lazy var) =
    1.50 +  (case Synchronized.value var of
    1.51 +    Expr _ => NONE
    1.52 +  | Result res =>
    1.53 +      if Future.is_finished res then
    1.54 +        let val result = Future.join_result res
    1.55 +        in if Exn.is_interrupt_exn result then NONE else SOME result end
    1.56 +      else NONE);
    1.57  
    1.58  
    1.59  (* force result *)
     2.1 --- a/src/Pure/PIDE/command.ML	Sun Dec 28 12:37:03 2014 +0100
     2.2 +++ b/src/Pure/PIDE/command.ML	Sun Dec 28 21:34:45 2014 +0100
     2.3 @@ -36,55 +36,6 @@
     2.4  structure Command: COMMAND =
     2.5  struct
     2.6  
     2.7 -(** memo results **)
     2.8 -
     2.9 -datatype 'a expr =
    2.10 -  Expr of Document_ID.exec * (unit -> 'a) |
    2.11 -  Result of 'a Exn.result;
    2.12 -
    2.13 -abstype 'a memo = Memo of 'a expr Synchronized.var
    2.14 -with
    2.15 -
    2.16 -fun memo exec_id e = Memo (Synchronized.var "Command.memo" (Expr (exec_id, e)));
    2.17 -fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
    2.18 -
    2.19 -fun memo_result (Memo v) =
    2.20 -  (case Synchronized.value v of
    2.21 -    Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
    2.22 -  | Result res => Exn.release res);
    2.23 -
    2.24 -fun memo_finished (Memo v) =
    2.25 -  (case Synchronized.value v of Expr _ => false | Result _ => true);
    2.26 -
    2.27 -fun memo_exec execution_id (Memo v) =
    2.28 -  Synchronized.timed_access v (K (SOME Time.zeroTime))
    2.29 -    (fn expr =>
    2.30 -      (case expr of
    2.31 -        Expr (exec_id, body) =>
    2.32 -          uninterruptible (fn restore_attributes => fn () =>
    2.33 -            let val group = Future.worker_subgroup () in
    2.34 -              if Execution.running execution_id exec_id [group] then
    2.35 -                let
    2.36 -                  val res =
    2.37 -                    (body
    2.38 -                      |> restore_attributes
    2.39 -                      |> Future.task_context "Command.memo_exec" group
    2.40 -                      |> Exn.interruptible_capture) ();
    2.41 -                in SOME ((), Result res) end
    2.42 -              else SOME ((), expr)
    2.43 -            end) ()
    2.44 -      | Result _ => SOME ((), expr)))
    2.45 -  |> (fn NONE => error "Conflicting command execution" | _ => ());
    2.46 -
    2.47 -fun memo_fork params execution_id (Memo v) =
    2.48 -  (case Synchronized.peek v of
    2.49 -    Result _ => ()
    2.50 -  | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec execution_id (Memo v))));
    2.51 -
    2.52 -end;
    2.53 -
    2.54 -
    2.55 -
    2.56  (** main phases of execution **)
    2.57  
    2.58  (* read *)
    2.59 @@ -184,15 +135,19 @@
    2.60  val init_eval_state =
    2.61    {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
    2.62  
    2.63 -datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo};
    2.64 +datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy};
    2.65  
    2.66  fun eval_exec_id (Eval {exec_id, ...}) = exec_id;
    2.67  val eval_eq = op = o apply2 eval_exec_id;
    2.68  
    2.69  val eval_running = Execution.is_running_exec o eval_exec_id;
    2.70 -fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process;
    2.71 +fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process;
    2.72  
    2.73 -fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
    2.74 +fun eval_result (Eval {exec_id, eval_process}) =
    2.75 +  (case Lazy.finished_result eval_process of
    2.76 +    SOME result => Exn.release result
    2.77 +  | NONE => error ("Unfinished execution result: " ^ Document_ID.print exec_id));
    2.78 +
    2.79  val eval_result_state = #state o eval_result;
    2.80  
    2.81  local
    2.82 @@ -279,7 +234,7 @@
    2.83            Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
    2.84              (fn () => read keywords thy master_dir init blobs span |> Toplevel.exec_id exec_id) ();
    2.85        in eval_state keywords span tr eval_state0 end;
    2.86 -  in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
    2.87 +  in Eval {exec_id = exec_id, eval_process = Lazy.lazy process} end;
    2.88  
    2.89  end;
    2.90  
    2.91 @@ -288,7 +243,7 @@
    2.92  
    2.93  datatype print = Print of
    2.94   {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
    2.95 -  exec_id: Document_ID.exec, print_process: unit memo};
    2.96 +  exec_id: Document_ID.exec, print_process: unit lazy};
    2.97  
    2.98  fun print_exec_id (Print {exec_id, ...}) = exec_id;
    2.99  val print_eq = op = o apply2 print_exec_id;
   2.100 @@ -310,7 +265,7 @@
   2.101        if Exn.is_interrupt exn then reraise exn
   2.102        else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
   2.103  
   2.104 -fun print_finished (Print {print_process, ...}) = memo_finished print_process;
   2.105 +fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process;
   2.106  
   2.107  fun print_persistent (Print {persistent, ...}) = persistent;
   2.108  
   2.109 @@ -337,7 +292,7 @@
   2.110        in
   2.111          Print {
   2.112            name = name, args = args, delay = delay, pri = pri, persistent = persistent,
   2.113 -          exec_id = exec_id, print_process = memo exec_id process}
   2.114 +          exec_id = exec_id, print_process = Lazy.lazy process}
   2.115        end;
   2.116  
   2.117      fun bad_print name args exn =
   2.118 @@ -408,32 +363,45 @@
   2.119  
   2.120  type exec = eval * print list;
   2.121  val no_exec: exec =
   2.122 -  (Eval {exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
   2.123 +  (Eval {exec_id = Document_ID.none, eval_process = Lazy.value init_eval_state}, []);
   2.124  
   2.125  fun exec_ids NONE = []
   2.126    | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints;
   2.127  
   2.128  local
   2.129  
   2.130 -fun run_print execution_id (Print {name, delay, pri, print_process, ...}) =
   2.131 -  if pri <= 0 orelse (Multithreading.enabled () andalso Options.default_bool "parallel_print")
   2.132 +fun run_process execution_id exec_id process =
   2.133 +  let val group = Future.worker_subgroup () in
   2.134 +    if Execution.running execution_id exec_id [group] then
   2.135 +      ignore (Future.task_context "Command.run_process" group Lazy.force_result process)
   2.136 +    else ()
   2.137 +  end;
   2.138 +
   2.139 +fun run_eval execution_id (Eval {exec_id, eval_process}) =
   2.140 +  if Lazy.is_finished eval_process then ()
   2.141 +  else run_process execution_id exec_id eval_process;
   2.142 +
   2.143 +fun run_print execution_id (Print {name, delay, pri, exec_id, print_process, ...}) =
   2.144 +  if Lazy.is_running print_process orelse Lazy.is_finished print_process then ()
   2.145 +  else if pri <= 0 orelse (Multithreading.enabled () andalso Options.default_bool "parallel_print")
   2.146    then
   2.147      let
   2.148        val group = Future.worker_subgroup ();
   2.149        fun fork () =
   2.150 -        memo_fork {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
   2.151 -          execution_id print_process;
   2.152 +        ignore ((singleton o Future.forks)
   2.153 +          {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
   2.154 +          (fn () => run_process execution_id exec_id print_process));
   2.155      in
   2.156        (case delay of
   2.157          NONE => fork ()
   2.158        | SOME d => ignore (Event_Timer.request (Time.+ (Time.now (), d)) fork))
   2.159      end
   2.160 -  else memo_exec execution_id print_process;
   2.161 +  else run_process execution_id exec_id print_process;
   2.162  
   2.163  in
   2.164  
   2.165 -fun exec execution_id (Eval {eval_process, ...}, prints) =
   2.166 -  (memo_exec execution_id eval_process; List.app (run_print execution_id) prints);
   2.167 +fun exec execution_id (eval, prints) =
   2.168 +  (run_eval execution_id eval; List.app (run_print execution_id) prints);
   2.169  
   2.170  end;
   2.171  
     3.1 --- a/src/Pure/PIDE/document.ML	Sun Dec 28 12:37:03 2014 +0100
     3.2 +++ b/src/Pure/PIDE/document.ML	Sun Dec 28 21:34:45 2014 +0100
     3.3 @@ -37,9 +37,6 @@
     3.4  
     3.5  
     3.6  
     3.7 -
     3.8 -
     3.9 -
    3.10  (** document structure **)
    3.11  
    3.12  fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
    3.13 @@ -285,16 +282,17 @@
    3.14  type execution =
    3.15   {version_id: Document_ID.version,  (*static version id*)
    3.16    execution_id: Document_ID.execution,  (*dynamic execution id*)
    3.17 -  delay_request: unit future,  (*pending event timer request*)
    3.18 -  frontier: Future.task Symtab.table};  (*node name -> running execution task*)
    3.19 +  delay_request: unit future};  (*pending event timer request*)
    3.20  
    3.21  val no_execution: execution =
    3.22 -  {version_id = Document_ID.none, execution_id = Document_ID.none,
    3.23 -   delay_request = Future.value (), frontier = Symtab.empty};
    3.24 +  {version_id = Document_ID.none,
    3.25 +   execution_id = Document_ID.none,
    3.26 +   delay_request = Future.value ()};
    3.27  
    3.28 -fun new_execution version_id delay_request frontier : execution =
    3.29 -  {version_id = version_id, execution_id = Execution.start (),
    3.30 -   delay_request = delay_request, frontier = frontier};
    3.31 +fun new_execution version_id delay_request : execution =
    3.32 +  {version_id = version_id,
    3.33 +   execution_id = Execution.start (),
    3.34 +   delay_request = delay_request};
    3.35  
    3.36  abstype state = State of
    3.37   {versions: version Inttab.table,  (*version id -> document content*)
    3.38 @@ -318,11 +316,11 @@
    3.39  (* document versions *)
    3.40  
    3.41  fun define_version version_id version =
    3.42 -  map_state (fn (versions, blobs, commands, {delay_request, frontier, ...}) =>
    3.43 +  map_state (fn (versions, blobs, commands, {delay_request, ...}) =>
    3.44      let
    3.45        val versions' = Inttab.update_new (version_id, version) versions
    3.46          handle Inttab.DUP dup => err_dup "document version" dup;
    3.47 -      val execution' = new_execution version_id delay_request frontier;
    3.48 +      val execution' = new_execution version_id delay_request;
    3.49      in (versions', blobs, commands, execution') end);
    3.50  
    3.51  fun the_version (State {versions, ...}) version_id =
    3.52 @@ -408,20 +406,18 @@
    3.53  fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
    3.54    timeit "Document.start_execution" (fn () =>
    3.55      let
    3.56 -      val {version_id, execution_id, delay_request, frontier} = execution;
    3.57 +      val {version_id, execution_id, delay_request} = execution;
    3.58  
    3.59        val delay = seconds (Options.default_real "editor_execution_delay");
    3.60  
    3.61        val _ = Future.cancel delay_request;
    3.62        val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay));
    3.63  
    3.64 -      val new_tasks =
    3.65 +      val _ =
    3.66          nodes_of (the_version state version_id) |> String_Graph.schedule
    3.67            (fn deps => fn (name, node) =>
    3.68              if visible_node node orelse pending_result node then
    3.69                let
    3.70 -                val more_deps =
    3.71 -                  Future.task_of delay_request' :: the_list (Symtab.lookup frontier name);
    3.72                  fun body () =
    3.73                    iterate_entries (fn (_, opt_exec) => fn () =>
    3.74                      (case opt_exec of
    3.75 @@ -433,15 +429,14 @@
    3.76                    handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn;
    3.77                  val future =
    3.78                    (singleton o Future.forks)
    3.79 -                    {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    3.80 -                      deps = more_deps @ map #2 (maps #2 deps),
    3.81 -                      pri = 0, interrupts = false} body;
    3.82 -              in [(name, Future.task_of future)] end
    3.83 +                   {name = "theory:" ^ name,
    3.84 +                    group = SOME (Future.new_group NONE),
    3.85 +                    deps = Future.task_of delay_request' :: maps #2 deps,
    3.86 +                    pri = 0, interrupts = false} body;
    3.87 +              in [Future.task_of future] end
    3.88              else []);
    3.89 -      val frontier' = (fold o fold) Symtab.update new_tasks frontier;
    3.90        val execution' =
    3.91 -        {version_id = version_id, execution_id = execution_id,
    3.92 -         delay_request = delay_request', frontier = frontier'};
    3.93 +        {version_id = version_id, execution_id = execution_id, delay_request = delay_request'};
    3.94      in (versions, blobs, commands, execution') end));
    3.95  
    3.96