keep memo_exec execution running, which is important to cancel goal forks eventually;
authorwenzelm
Mon Jul 29 18:59:58 2013 +0200 (2013-07-29)
changeset 52775e0169f13bd37
parent 52774 627fb639a2d9
child 52776 fd81d51460b7
keep memo_exec execution running, which is important to cancel goal forks eventually;
run as nested worker task to keep main group valid, even after cancelation of removed subgroups;
do not memoize interrupt, but absorb it silently in main execution;
Goal.purge_futures: rough sanity check of group status;
src/Pure/Concurrent/future.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/execution.ML
src/Pure/PIDE/protocol.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Mon Jul 29 16:52:04 2013 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Mon Jul 29 18:59:58 2013 +0200
     1.3 @@ -48,6 +48,7 @@
     1.4    val worker_group: unit -> group option
     1.5    val the_worker_group: unit -> group
     1.6    val worker_subgroup: unit -> group
     1.7 +  val worker_nest: string -> ('a -> 'b) -> 'a -> 'b
     1.8    val worker_guest: string -> group -> ('a -> 'b) -> 'a -> 'b
     1.9    type 'a future
    1.10    val task_of: 'a future -> task
    1.11 @@ -108,6 +109,9 @@
    1.12  
    1.13  fun worker_subgroup () = new_group (worker_group ());
    1.14  
    1.15 +fun worker_nest name f x =
    1.16 +  setmp_worker_task (Task_Queue.new_task (the_worker_group ()) name NONE) f x;
    1.17 +
    1.18  fun worker_guest name group f x =
    1.19    if is_some (worker_task ()) then
    1.20      raise Fail "Already running as worker thread"
     2.1 --- a/src/Pure/PIDE/command.ML	Mon Jul 29 16:52:04 2013 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Mon Jul 29 18:59:58 2013 +0200
     2.3 @@ -28,7 +28,7 @@
     2.4  structure Command: COMMAND =
     2.5  struct
     2.6  
     2.7 -(** memo results -- including physical interrupts **)
     2.8 +(** memo results **)
     2.9  
    2.10  datatype 'a expr =
    2.11    Expr of Document_ID.exec * (unit -> 'a) |
    2.12 @@ -48,24 +48,25 @@
    2.13  fun memo_finished (Memo v) =
    2.14    (case Synchronized.value v of
    2.15     Expr _ => false
    2.16 - | Result res => not (Exn.is_interrupt_exn res));
    2.17 + | Result _ => true);
    2.18  
    2.19  fun memo_exec execution_id (Memo v) =
    2.20    Synchronized.timed_access v (K (SOME Time.zeroTime))
    2.21      (fn expr =>
    2.22        (case expr of
    2.23 -        Expr (exec_id, e) =>
    2.24 +        Expr (exec_id, body) =>
    2.25            uninterruptible (fn restore_attributes => fn () =>
    2.26              if Execution.running execution_id exec_id then
    2.27                let
    2.28 -                val res = Exn.capture (restore_attributes e) ();
    2.29 -                val _ = Execution.finished exec_id;
    2.30 -              in SOME (Exn.is_interrupt_exn res, Result res) end
    2.31 -            else SOME (true, expr)) ()
    2.32 -      | Result _ => SOME (false, expr)))
    2.33 -  |> (fn SOME false => ()
    2.34 -       | SOME true => Exn.interrupt ()
    2.35 -       | NONE => error "Conflicting command execution");
    2.36 +                val res =
    2.37 +                  (body
    2.38 +                    |> restore_attributes
    2.39 +                    |> Future.worker_nest "Command.memo_exec"
    2.40 +                    |> Exn.interruptible_capture) ();
    2.41 +              in SOME ((), Result res) end
    2.42 +            else SOME ((), expr)) ()
    2.43 +      | Result _ => SOME ((), expr)))
    2.44 +  |> (fn NONE => error "Conflicting command execution" | _ => ());
    2.45  
    2.46  fun memo_fork params execution_id (Memo v) =
    2.47    (case Synchronized.value v of
    2.48 @@ -216,7 +217,7 @@
    2.49  
    2.50  fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
    2.51  
    2.52 -fun print_finished (Print {exec_id, print_process, ...}) = memo_finished print_process;
    2.53 +fun print_finished (Print {print_process, ...}) = memo_finished print_process;
    2.54  
    2.55  fun print_persistent (Print {persistent, ...}) = persistent;
    2.56  
     3.1 --- a/src/Pure/PIDE/document.ML	Mon Jul 29 16:52:04 2013 +0200
     3.2 +++ b/src/Pure/PIDE/document.ML	Mon Jul 29 18:59:58 2013 +0200
     3.3 @@ -303,19 +303,20 @@
     3.4              if visible_node node orelse pending_result node then
     3.5                let
     3.6                  val former_task = Symtab.lookup frontier name;
     3.7 +                fun body () =
     3.8 +                  iterate_entries (fn (_, opt_exec) => fn () =>
     3.9 +                    (case opt_exec of
    3.10 +                      SOME exec =>
    3.11 +                        if Execution.is_running execution_id
    3.12 +                        then SOME (Command.exec execution_id exec)
    3.13 +                        else NONE
    3.14 +                    | NONE => NONE)) node ()
    3.15 +                  handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn;
    3.16                  val future =
    3.17                    (singleton o Future.forks)
    3.18                      {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    3.19                        deps = the_list former_task @ map #2 (maps #2 deps),
    3.20 -                      pri = pri, interrupts = false}
    3.21 -                    (fn () =>
    3.22 -                      iterate_entries (fn (_, opt_exec) => fn () =>
    3.23 -                        (case opt_exec of
    3.24 -                          SOME exec =>
    3.25 -                            if Execution.is_running execution_id
    3.26 -                            then SOME (Command.exec execution_id exec)
    3.27 -                            else NONE
    3.28 -                        | NONE => NONE)) node ());
    3.29 +                      pri = pri, interrupts = false} body;
    3.30                in [(name, Future.task_of future)] end
    3.31              else [])
    3.32        else [];
     4.1 --- a/src/Pure/PIDE/execution.ML	Mon Jul 29 16:52:04 2013 +0200
     4.2 +++ b/src/Pure/PIDE/execution.ML	Mon Jul 29 18:59:58 2013 +0200
     4.3 @@ -11,7 +11,6 @@
     4.4    val discontinue: unit -> unit
     4.5    val is_running: Document_ID.execution -> bool
     4.6    val running: Document_ID.execution -> Document_ID.exec -> bool
     4.7 -  val finished: Document_ID.exec -> unit
     4.8    val cancel: Document_ID.exec -> unit
     4.9    val terminate: Document_ID.exec -> unit
    4.10  end;
    4.11 @@ -52,12 +51,6 @@
    4.12            else execs;
    4.13        in SOME (continue, (execution_id', execs')) end);
    4.14  
    4.15 -fun finished exec_id =
    4.16 -  Synchronized.change state
    4.17 -    (apsnd (fn execs =>
    4.18 -      Inttab.delete exec_id execs handle Inttab.UNDEF bad =>
    4.19 -        error ("Attempt to finish unknown execution " ^ Document_ID.print bad)));
    4.20 -
    4.21  fun peek_list exec_id =
    4.22    the_list (Inttab.lookup (snd (Synchronized.value state)) exec_id);
    4.23  
     5.1 --- a/src/Pure/PIDE/protocol.ML	Mon Jul 29 16:52:04 2013 +0200
     5.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Jul 29 18:59:58 2013 +0200
     5.3 @@ -75,7 +75,7 @@
     5.4    Isabelle_Process.protocol_command "Document.dialog_result"
     5.5      (fn [serial, result] =>
     5.6        Active.dialog_result (Markup.parse_int serial) result
     5.7 -        handle exn => if Exn.is_interrupt exn then () else reraise exn);
     5.8 +        handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn);
     5.9  
    5.10  end;
    5.11  
     6.1 --- a/src/Pure/goal.ML	Mon Jul 29 16:52:04 2013 +0200
     6.2 +++ b/src/Pure/goal.ML	Mon Jul 29 18:59:58 2013 +0200
     6.3 @@ -181,11 +181,18 @@
     6.4  fun peek_futures id =
     6.5    map #2 (Inttab.lookup_list (#2 (Synchronized.value forked_proofs)) id);
     6.6  
     6.7 +fun check_canceled id group =
     6.8 +  if Task_Queue.is_canceled group then ()
     6.9 +  else raise Fail ("Attempt to purge valid execution " ^ string_of_int id);
    6.10 +
    6.11  fun purge_futures ids =
    6.12    Synchronized.change forked_proofs (fn (_, tab) =>
    6.13      let
    6.14        val tab' = fold Inttab.delete_safe ids tab;
    6.15 -      val n' = Inttab.fold (Integer.add o length o #2) tab' 0;
    6.16 +      val n' =
    6.17 +        Inttab.fold (fn (id, futures) => fn m =>
    6.18 +          if Inttab.defined tab' id then m + length futures
    6.19 +          else (List.app (check_canceled id o #1) futures; m)) tab 0;
    6.20        val _ = Future.forked_proofs := n';
    6.21      in (n', tab') end);
    6.22