discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
authorwenzelm
Sun Aug 25 16:03:12 2013 +0200 (2013-08-25)
changeset 53189ee8b8dafef0e
parent 53188 bb5433b13ff2
child 53190 5d92649a310e
discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
simplified Goal.future_enabled;
etc/options
src/Pure/Concurrent/future.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
src/Pure/Tools/ml_statistics.scala
src/Pure/goal.ML
     1.1 --- a/etc/options	Sun Aug 25 14:35:25 2013 +0200
     1.2 +++ b/etc/options	Sun Aug 25 16:03:12 2013 +0200
     1.3 @@ -71,8 +71,6 @@
     1.4    -- "level of tracing information for multithreading"
     1.5  public option parallel_proofs : int = 2
     1.6    -- "level of parallel proof checking: 0, 1, 2"
     1.7 -option parallel_subproofs_saturation : int = 100
     1.8 -  -- "upper bound for forks of nested proofs (multiplied by worker threads)"
     1.9  option parallel_subproofs_threshold : real = 0.01
    1.10    -- "lower bound of timing estimate for forked nested proofs (seconds)"
    1.11  
     2.1 --- a/src/Pure/Concurrent/future.ML	Sun Aug 25 14:35:25 2013 +0200
     2.2 +++ b/src/Pure/Concurrent/future.ML	Sun Aug 25 16:03:12 2013 +0200
     2.3 @@ -55,7 +55,6 @@
     2.4    val peek: 'a future -> 'a Exn.result option
     2.5    val is_finished: 'a future -> bool
     2.6    val ML_statistics: bool Unsynchronized.ref
     2.7 -  val forked_proofs: int Unsynchronized.ref
     2.8    val interruptible_task: ('a -> 'b) -> 'a -> 'b
     2.9    val cancel_group: group -> unit
    2.10    val cancel: 'a future -> unit
    2.11 @@ -200,7 +199,6 @@
    2.12  (* status *)
    2.13  
    2.14  val ML_statistics = Unsynchronized.ref false;
    2.15 -val forked_proofs = Unsynchronized.ref 0;
    2.16  
    2.17  fun report_status () = (*requires SYNCHRONIZED*)
    2.18    if ! ML_statistics then
    2.19 @@ -211,7 +209,6 @@
    2.20        val waiting = count_workers Waiting;
    2.21        val stats =
    2.22         [("now", Markup.print_real (Time.toReal (Time.now ()))),
    2.23 -        ("tasks_proof", Markup.print_int (! forked_proofs)),
    2.24          ("tasks_ready", Markup.print_int ready),
    2.25          ("tasks_pending", Markup.print_int pending),
    2.26          ("tasks_running", Markup.print_int running),
     3.1 --- a/src/Pure/Isar/proof.ML	Sun Aug 25 14:35:25 2013 +0200
     3.2 +++ b/src/Pure/Isar/proof.ML	Sun Aug 25 16:03:12 2013 +0200
     3.3 @@ -1164,7 +1164,7 @@
     3.4  local
     3.5  
     3.6  fun future_terminal_proof proof1 proof2 done int state =
     3.7 -  if Goal.future_enabled_level 3 andalso not (is_relevant state) then
     3.8 +  if Goal.future_enabled 3 andalso not (is_relevant state) then
     3.9      state |> future_proof (fn state' =>
    3.10        let
    3.11          val pos = Position.thread_data ();
     4.1 --- a/src/Pure/Isar/toplevel.ML	Sun Aug 25 14:35:25 2013 +0200
     4.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Aug 25 16:03:12 2013 +0200
     4.3 @@ -698,16 +698,16 @@
     4.4    | SOME state =>
     4.5        not (Proof.is_relevant state) andalso
     4.6         (if can (Proof.assert_bottom true) state
     4.7 -        then Goal.future_enabled ()
     4.8 +        then Goal.future_enabled 1
     4.9          else
    4.10            (case estimate of
    4.11 -            NONE => Goal.future_enabled_nested 2
    4.12 +            NONE => Goal.future_enabled 2
    4.13            | SOME t => Goal.future_enabled_timing t)));
    4.14  
    4.15  fun atom_result tr st =
    4.16    let
    4.17      val st' =
    4.18 -      if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
    4.19 +      if Goal.future_enabled 1 andalso Keyword.is_diag (name_of tr) then
    4.20          (Goal.fork_params
    4.21            {name = "Toplevel.diag", pos = pos_of tr,
    4.22              pri = priority (timing_estimate true (Thy_Syntax.atom tr))}
     5.1 --- a/src/Pure/PIDE/command.ML	Sun Aug 25 14:35:25 2013 +0200
     5.2 +++ b/src/Pure/PIDE/command.ML	Sun Aug 25 16:03:12 2013 +0200
     5.3 @@ -130,7 +130,7 @@
     5.4  local
     5.5  
     5.6  fun run int tr st =
     5.7 -  if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
     5.8 +  if Goal.future_enabled 1 andalso Keyword.is_diag (Toplevel.name_of tr) then
     5.9      (Goal.fork_params {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
    5.10        (fn () => Toplevel.command_exception int tr st); ([], SOME st))
    5.11    else Toplevel.command_errors int tr st;
     6.1 --- a/src/Pure/Tools/ml_statistics.scala	Sun Aug 25 14:35:25 2013 +0200
     6.2 +++ b/src/Pure/Tools/ml_statistics.scala	Sun Aug 25 16:03:12 2013 +0200
     6.3 @@ -48,8 +48,7 @@
     6.4    val speed_fields = ("Speed", List("speed_CPU", "speed_GC"))
     6.5  
     6.6    val tasks_fields =
     6.7 -    ("Future tasks",
     6.8 -      List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
     6.9 +    ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
    6.10  
    6.11    val workers_fields =
    6.12      ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
     7.1 --- a/src/Pure/goal.ML	Sun Aug 25 14:35:25 2013 +0200
     7.2 +++ b/src/Pure/goal.ML	Sun Aug 25 16:03:12 2013 +0200
     7.3 @@ -31,9 +31,7 @@
     7.4    val reset_futures: unit -> Future.group list
     7.5    val shutdown_futures: unit -> unit
     7.6    val skip_proofs_enabled: unit -> bool
     7.7 -  val future_enabled_level: int -> bool
     7.8 -  val future_enabled: unit -> bool
     7.9 -  val future_enabled_nested: int -> bool
    7.10 +  val future_enabled: int -> bool
    7.11    val future_enabled_timing: Time.time -> bool
    7.12    val future_result: Proof.context -> thm future -> term -> thm
    7.13    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
    7.14 @@ -119,21 +117,12 @@
    7.15  
    7.16  val forked_proofs =
    7.17    Synchronized.var "forked_proofs"
    7.18 -    (0, Inttab.empty: (Future.group * unit future) list Inttab.table);
    7.19 -
    7.20 -fun count_forked i =
    7.21 -  Synchronized.change forked_proofs (fn (m, tab) =>
    7.22 -    let
    7.23 -      val n = m + i;
    7.24 -      val _ = Future.forked_proofs := n;
    7.25 -    in (n, tab) end);
    7.26 +    (Inttab.empty: (Future.group * unit future) list Inttab.table);
    7.27  
    7.28  fun register_forked id future =
    7.29 -  Synchronized.change forked_proofs (fn (m, tab) =>
    7.30 -    let
    7.31 -      val group = Task_Queue.group_of_task (Future.task_of future);
    7.32 -      val tab' = Inttab.cons_list (id, (group, Future.map (K ()) future)) tab;
    7.33 -    in (m, tab') end);
    7.34 +  Synchronized.change forked_proofs (fn tab =>
    7.35 +    let val group = Task_Queue.group_of_task (Future.task_of future)
    7.36 +    in Inttab.cons_list (id, (group, Future.map (K ()) future)) tab end);
    7.37  
    7.38  fun status task markups =
    7.39    let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
    7.40 @@ -145,7 +134,6 @@
    7.41    uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
    7.42      let
    7.43        val id = the_default 0 (Position.parse_id pos);
    7.44 -      val _ = count_forked 1;
    7.45  
    7.46        val future =
    7.47          (singleton o Future.forks)
    7.48 @@ -167,7 +155,6 @@
    7.49                        (status task [Markup.failed];
    7.50                         Output.report (Markup.markup_only Markup.bad);
    7.51                         List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)));
    7.52 -              val _ = count_forked ~1;
    7.53              in Exn.release result end);
    7.54        val _ = status (Future.task_of future) [Markup.forked];
    7.55        val _ = register_forked id future;
    7.56 @@ -176,32 +163,27 @@
    7.57  fun fork pri e =
    7.58    fork_params {name = "Goal.fork", pos = Position.thread_data (), pri = pri} e;
    7.59  
    7.60 -fun forked_count () = #1 (Synchronized.value forked_proofs);
    7.61 -
    7.62  fun peek_futures id =
    7.63 -  map #2 (Inttab.lookup_list (#2 (Synchronized.value forked_proofs)) id);
    7.64 +  map #2 (Inttab.lookup_list (Synchronized.value forked_proofs) id);
    7.65  
    7.66  fun check_canceled id group =
    7.67    if Task_Queue.is_canceled group then ()
    7.68    else raise Fail ("Attempt to purge valid execution " ^ string_of_int id);
    7.69  
    7.70  fun purge_futures ids =
    7.71 -  Synchronized.change forked_proofs (fn (_, tab) =>
    7.72 +  Synchronized.change forked_proofs (fn tab =>
    7.73      let
    7.74        val tab' = fold Inttab.delete_safe ids tab;
    7.75 -      val n' =
    7.76 -        Inttab.fold (fn (id, futures) => fn m =>
    7.77 -          if Inttab.defined tab' id then m + length futures
    7.78 -          else (List.app (check_canceled id o #1) futures; m)) tab 0;
    7.79 -      val _ = Future.forked_proofs := n';
    7.80 -    in (n', tab') end);
    7.81 +      val () =
    7.82 +        Inttab.fold (fn (id, futures) => fn () =>
    7.83 +          if Inttab.defined tab' id then ()
    7.84 +          else List.app (check_canceled id o #1) futures) tab ();
    7.85 +    in tab' end);
    7.86  
    7.87  fun reset_futures () =
    7.88 -  Synchronized.change_result forked_proofs (fn (_, tab) =>
    7.89 -    let
    7.90 -      val groups = Inttab.fold (fold (cons o #1) o #2) tab [];
    7.91 -      val _ = Future.forked_proofs := 0;
    7.92 -    in (groups, (0, Inttab.empty)) end);
    7.93 +  Synchronized.change_result forked_proofs (fn tab =>
    7.94 +    let val groups = Inttab.fold (fold (cons o #1) o #2) tab []
    7.95 +    in (groups, Inttab.empty) end);
    7.96  
    7.97  fun shutdown_futures () =
    7.98    (Future.shutdown ();
    7.99 @@ -223,19 +205,12 @@
   7.100  
   7.101  val parallel_proofs = Unsynchronized.ref 1;
   7.102  
   7.103 -fun future_enabled_level n =
   7.104 +fun future_enabled n =
   7.105    Multithreading.enabled () andalso ! parallel_proofs >= n andalso
   7.106    is_some (Future.worker_task ());
   7.107  
   7.108 -fun future_enabled () = future_enabled_level 1;
   7.109 -
   7.110 -fun future_enabled_nested n =
   7.111 -  future_enabled_level n andalso
   7.112 -  forked_count () <
   7.113 -    Options.default_int "parallel_subproofs_saturation" * Multithreading.max_threads_value ();
   7.114 -
   7.115  fun future_enabled_timing t =
   7.116 -  future_enabled () andalso
   7.117 +  future_enabled 1 andalso
   7.118      Time.toReal t >= Options.default_real "parallel_subproofs_threshold";
   7.119  
   7.120  
   7.121 @@ -299,7 +274,7 @@
   7.122      val string_of_term = Syntax.string_of_term ctxt;
   7.123  
   7.124      val schematic = exists is_schematic props;
   7.125 -    val future = future_enabled ();
   7.126 +    val future = future_enabled 1;
   7.127      val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
   7.128  
   7.129      val pos = Position.thread_data ();
   7.130 @@ -363,7 +338,7 @@
   7.131  fun prove_sorry ctxt xs asms prop tac =
   7.132    if Config.get ctxt quick_and_dirty then
   7.133      prove ctxt xs asms prop (fn _ => ALLGOALS Skip_Proof.cheat_tac)
   7.134 -  else (if future_enabled () then prove_future_pri ~2 else prove) ctxt xs asms prop tac;
   7.135 +  else (if future_enabled 1 then prove_future_pri ~2 else prove) ctxt xs asms prop tac;
   7.136  
   7.137  fun prove_sorry_global thy xs asms prop tac =
   7.138    Drule.export_without_context