central management of forked goals wrt. transaction id;
authorwenzelm
Sat Sep 01 19:27:28 2012 +0200 (2012-09-01)
changeset 490617449b804073b
parent 49060 fa094e173cb9
child 49062 7e31dfd99ce7
central management of forked goals wrt. transaction id;
clarified stable_exec_id: consider ragular failure as stable;
more robust counting of forked proofs, with global reset after cancellation due to document editing;
src/Pure/Concurrent/par_exn.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/Concurrent/par_exn.ML	Fri Aug 31 22:34:37 2012 +0200
     1.2 +++ b/src/Pure/Concurrent/par_exn.ML	Sat Sep 01 19:27:28 2012 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    val serial: exn -> serial * exn
     1.5    val make: exn list -> exn
     1.6    val dest: exn -> exn list option
     1.7 +  val is_interrupted: 'a Exn.result list -> bool
     1.8    val release_all: 'a Exn.result list -> 'a list
     1.9    val release_first: 'a Exn.result list -> 'a list
    1.10  end;
    1.11 @@ -53,6 +54,10 @@
    1.12  
    1.13  (* parallel results *)
    1.14  
    1.15 +fun is_interrupted results =
    1.16 +  exists (fn Exn.Exn _ => true | _ => false) results andalso
    1.17 +    Exn.is_interrupt (make (map_filter Exn.get_exn results));
    1.18 +
    1.19  fun release_all results =
    1.20    if forall (fn Exn.Res _ => true | _ => false) results
    1.21    then map Exn.release results
     2.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 31 22:34:37 2012 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Sat Sep 01 19:27:28 2012 +0200
     2.3 @@ -359,10 +359,13 @@
     2.4      |> Toplevel.end_theory Position.none
     2.5      |> Thm.join_theory_proofs) ()));
     2.6  
     2.7 -fun stable_command exec =
     2.8 +fun stable_exec_id id =
     2.9 +  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures id)));
    2.10 +
    2.11 +fun stable_exec exec =
    2.12    (case Exn.capture Command.memo_result exec of
    2.13      Exn.Exn exn => not (Exn.is_interrupt exn)
    2.14 -  | Exn.Res ((st, _), _) => is_some (Exn.get_res (Exn.capture Toplevel.join_recent_proofs st)));
    2.15 +  | Exn.Res _ => true);
    2.16  
    2.17  fun make_required nodes =
    2.18    let
    2.19 @@ -423,7 +426,8 @@
    2.20              | SOME (exec_id, exec) =>
    2.21                  (case lookup_entry node0 id of
    2.22                    NONE => false
    2.23 -                | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_command exec));
    2.24 +                | SOME (exec_id0, _) =>
    2.25 +                    exec_id = exec_id0 andalso stable_exec_id exec_id andalso stable_exec exec));
    2.26          in SOME (same', (prev, flags')) end
    2.27        else NONE;
    2.28      val (same, (common, flags)) =
     3.1 --- a/src/Pure/PIDE/protocol.ML	Fri Aug 31 22:34:37 2012 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.ML	Sat Sep 01 19:27:28 2012 +0200
     3.3 @@ -59,6 +59,7 @@
     3.4                in pair int (list (pair int (option int))) end
     3.5                |> YXML.string_of_body);
     3.6  
     3.7 +        val _ = Goal.cancel_futures ();
     3.8          val _ = Document.start_execution state';
     3.9        in state' end));
    3.10  
     4.1 --- a/src/Pure/goal.ML	Fri Aug 31 22:34:37 2012 +0200
     4.2 +++ b/src/Pure/goal.ML	Sat Sep 01 19:27:28 2012 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4  (*  Title:      Pure/goal.ML
     4.5      Author:     Makarius
     4.6  
     4.7 -Goals in tactical theorem proving.
     4.8 +Goals in tactical theorem proving, with support for forked proofs.
     4.9  *)
    4.10  
    4.11  signature BASIC_GOAL =
    4.12 @@ -26,6 +26,8 @@
    4.13    val norm_result: thm -> thm
    4.14    val fork_name: string -> (unit -> 'a) -> 'a future
    4.15    val fork: (unit -> 'a) -> 'a future
    4.16 +  val peek_futures: serial -> unit future list
    4.17 +  val cancel_futures: unit -> unit
    4.18    val future_enabled_level: int -> bool
    4.19    val future_enabled: unit -> bool
    4.20    val future_enabled_nested: int -> bool
    4.21 @@ -109,25 +111,42 @@
    4.22  
    4.23  (* forked proofs *)
    4.24  
    4.25 -val forked_proofs = Synchronized.var "forked_proofs" 0;
    4.26 +local
    4.27  
    4.28 -fun forked i =
    4.29 -  Synchronized.change forked_proofs (fn m =>
    4.30 +val forked_proofs =
    4.31 +  Synchronized.var "forked_proofs"
    4.32 +    (0, []: Future.group list, Inttab.empty: unit future list Inttab.table);
    4.33 +
    4.34 +fun count_forked i =
    4.35 +  Synchronized.change forked_proofs (fn (m, groups, tab) =>
    4.36      let
    4.37        val n = m + i;
    4.38        val _ =
    4.39          Multithreading.tracing 2 (fn () =>
    4.40            ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
    4.41 -    in n end);
    4.42 +    in (n, groups, tab) end);
    4.43 +
    4.44 +fun register_forked id future =
    4.45 +  Synchronized.change forked_proofs (fn (m, groups, tab) =>
    4.46 +    let
    4.47 +      val groups' = Task_Queue.group_of_task (Future.task_of future) :: groups;
    4.48 +      val tab' = Inttab.cons_list (id, Future.map (K ()) future) tab;
    4.49 +    in (m, groups', tab') end);
    4.50  
    4.51  fun status task markups =
    4.52    let val props = Markup.properties [(Isabelle_Markup.taskN, Task_Queue.str_of_task task)]
    4.53    in Output.status (implode (map (Markup.markup_only o props) markups)) end;
    4.54  
    4.55 +in
    4.56 +
    4.57  fun fork_name name e =
    4.58    uninterruptible (fn _ => fn () =>
    4.59      let
    4.60 -      val _ = forked 1;
    4.61 +      val id =
    4.62 +        (case Position.get_id (Position.thread_data ()) of
    4.63 +          NONE => 0
    4.64 +        | SOME id => Markup.parse_int id);
    4.65 +      val _ = count_forked 1;
    4.66        val future =
    4.67          (singleton o Future.forks)
    4.68            {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
    4.69 @@ -144,12 +163,25 @@
    4.70                      (status task [Isabelle_Markup.failed];
    4.71                       Output.report (Markup.markup_only Isabelle_Markup.bad);
    4.72                       Output.error_msg (ML_Compiler.exn_message exn)));
    4.73 +              val _ = count_forked ~1;
    4.74              in Exn.release result end);
    4.75        val _ = status (Future.task_of future) [Isabelle_Markup.forked];
    4.76 +      val _ = register_forked id future;
    4.77      in future end) ();
    4.78  
    4.79  fun fork e = fork_name "Goal.fork" e;
    4.80  
    4.81 +fun forked_count () = #1 (Synchronized.value forked_proofs);
    4.82 +
    4.83 +fun peek_futures id =
    4.84 +  Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
    4.85 +
    4.86 +fun cancel_futures () =
    4.87 +  Synchronized.change forked_proofs (fn (m, groups, tab) =>
    4.88 +    (List.app Future.cancel_group groups; (0, [], Inttab.empty)));
    4.89 +
    4.90 +end;
    4.91 +
    4.92  
    4.93  (* scheduling parameters *)
    4.94  
    4.95 @@ -164,8 +196,7 @@
    4.96  
    4.97  fun future_enabled_nested n =
    4.98    future_enabled_level n andalso
    4.99 -  Synchronized.value forked_proofs <
   4.100 -    ! parallel_proofs_threshold * Multithreading.max_threads_value ();
   4.101 +  forked_count () < ! parallel_proofs_threshold * Multithreading.max_threads_value ();
   4.102  
   4.103  
   4.104  (* future_result *)