clarified future scheduling parameters, with support for parallel_limit;
authorwenzelm
Wed May 09 20:45:57 2018 +0200 (13 months ago ago)
changeset 681326fb85346cb79
parent 68131 b73678836f8e
child 68133 62a3294edda3
clarified future scheduling parameters, with support for parallel_limit;
etc/options
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/lazy.ML
src/Pure/Concurrent/multithreading.ML
src/Pure/Concurrent/par_list.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML/ml_compiler.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/execution.ML
src/Pure/Thy/thy_info.ML
src/Pure/goal.ML
src/Pure/par_tactical.ML
     1.1 --- a/etc/options	Wed May 09 19:53:37 2018 +0200
     1.2 +++ b/etc/options	Wed May 09 20:45:57 2018 +0200
     1.3 @@ -71,6 +71,8 @@
     1.4  option threads_stack_limit : real = 0.25
     1.5    -- "maximum stack size for worker threads (in giga words, 0 = unlimited)"
     1.6  
     1.7 +public option parallel_limit : int = 0
     1.8 +  -- "approximative limit for parallel tasks (0 = unlimited)"
     1.9  public option parallel_print : bool = true
    1.10    -- "parallel and asynchronous printing of results"
    1.11  public option parallel_proofs : int = 1
     2.1 --- a/src/Pure/Concurrent/future.ML	Wed May 09 19:53:37 2018 +0200
     2.2 +++ b/src/Pure/Concurrent/future.ML	Wed May 09 20:45:57 2018 +0200
     2.3 @@ -34,6 +34,10 @@
     2.4    val forked_results: {name: string, deps: Task_Queue.task list} ->
     2.5      (unit -> 'a) list -> 'a Exn.result list
     2.6    val task_context: string -> group -> ('a -> 'b) -> 'a -> 'b
     2.7 +  val enabled: unit -> bool
     2.8 +  val relevant: 'a list -> bool
     2.9 +  val proofs_enabled: int -> bool
    2.10 +  val proofs_enabled_timing: Time.time -> bool
    2.11    val value_result: 'a Exn.result -> 'a future
    2.12    val value: 'a -> 'a future
    2.13    val cond_forks: params -> (unit -> 'a) list -> 'a future list
    2.14 @@ -577,6 +581,22 @@
    2.15      end);
    2.16  
    2.17  
    2.18 +(* scheduling parameters *)
    2.19 +
    2.20 +fun enabled () =
    2.21 +  Multithreading.max_threads () > 1 andalso
    2.22 +    let val lim = Options.default_int "parallel_limit"
    2.23 +    in lim <= 0 orelse SYNCHRONIZED "enabled" (fn () => Task_Queue.total_jobs (! queue) < lim) end;
    2.24 +
    2.25 +val relevant = (fn [] => false | [_] => false | _ => enabled ());
    2.26 +
    2.27 +fun proofs_enabled n =
    2.28 +  ! Multithreading.parallel_proofs >= n andalso is_some (worker_task ()) andalso enabled ();
    2.29 +
    2.30 +fun proofs_enabled_timing t =
    2.31 +  proofs_enabled 1 andalso Time.toReal t >= Options.default_real "parallel_subproofs_threshold";
    2.32 +
    2.33 +
    2.34  (* fast-path operations -- bypass task queue if possible *)
    2.35  
    2.36  fun value_result (res: 'a Exn.result) =
    2.37 @@ -590,7 +610,7 @@
    2.38  fun value x = value_result (Exn.Res x);
    2.39  
    2.40  fun cond_forks args es =
    2.41 -  if Multithreading.enabled () then forks args es
    2.42 +  if enabled () then forks args es
    2.43    else map (fn e => value_result (Exn.interruptible_capture e ())) es;
    2.44  
    2.45  fun map_future f x =
     3.1 --- a/src/Pure/Concurrent/lazy.ML	Wed May 09 19:53:37 2018 +0200
     3.2 +++ b/src/Pure/Concurrent/lazy.ML	Wed May 09 20:45:57 2018 +0200
     3.3 @@ -129,7 +129,7 @@
     3.4      val pending =
     3.5        xs |> map_filter (fn x => if is_pending x then SOME (fn () => force_result x) else NONE);
     3.6      val _ =
     3.7 -      if Multithreading.relevant pending then
     3.8 +      if Future.relevant pending then
     3.9          ignore (Future.forked_results {name = "Lazy.consolidate", deps = []} pending)
    3.10        else List.app (fn e => ignore (e ())) pending;
    3.11    in xs end;
     4.1 --- a/src/Pure/Concurrent/multithreading.ML	Wed May 09 19:53:37 2018 +0200
     4.2 +++ b/src/Pure/Concurrent/multithreading.ML	Wed May 09 20:45:57 2018 +0200
     4.3 @@ -8,10 +8,7 @@
     4.4  sig
     4.5    val max_threads: unit -> int
     4.6    val max_threads_update: int -> unit
     4.7 -  val enabled: unit -> bool
     4.8 -  val relevant: 'a list -> bool
     4.9    val parallel_proofs: int ref
    4.10 -  val parallel_proofs_enabled: int -> bool
    4.11    val sync_wait: Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
    4.12    val trace: int ref
    4.13    val tracing: int -> (unit -> string) -> unit
    4.14 @@ -42,9 +39,6 @@
    4.15  
    4.16  fun max_threads () = ! max_threads_state;
    4.17  fun max_threads_update m = max_threads_state := max_threads_result m;
    4.18 -fun enabled () = max_threads () > 1;
    4.19 -
    4.20 -val relevant = (fn [] => false | [_] => false | _ => enabled ());
    4.21  
    4.22  end;
    4.23  
    4.24 @@ -53,9 +47,6 @@
    4.25  
    4.26  val parallel_proofs = ref 1;
    4.27  
    4.28 -fun parallel_proofs_enabled n =
    4.29 -  enabled () andalso ! parallel_proofs >= n;
    4.30 -
    4.31  
    4.32  (* synchronous wait *)
    4.33  
     5.1 --- a/src/Pure/Concurrent/par_list.ML	Wed May 09 19:53:37 2018 +0200
     5.2 +++ b/src/Pure/Concurrent/par_list.ML	Wed May 09 20:45:57 2018 +0200
     5.3 @@ -29,7 +29,7 @@
     5.4  struct
     5.5  
     5.6  fun forked_results name f xs =
     5.7 -  if Multithreading.relevant xs
     5.8 +  if Future.relevant xs
     5.9    then Future.forked_results {name = name, deps = []} (map (fn x => fn () => f x) xs)
    5.10    else map (Exn.capture f) xs;
    5.11  
     6.1 --- a/src/Pure/Isar/proof.ML	Wed May 09 19:53:37 2018 +0200
     6.2 +++ b/src/Pure/Isar/proof.ML	Wed May 09 20:45:57 2018 +0200
     6.3 @@ -1301,7 +1301,7 @@
     6.4  local
     6.5  
     6.6  fun future_terminal_proof proof1 proof2 done state =
     6.7 -  if Goal.future_enabled 3 andalso not (is_relevant state) then
     6.8 +  if Future.proofs_enabled 3 andalso not (is_relevant state) then
     6.9      state |> future_proof (fn state' =>
    6.10        let val pos = Position.thread_data () in
    6.11          Execution.fork {name = "Proof.future_terminal_proof", pos = pos, pri = ~1}
     7.1 --- a/src/Pure/Isar/toplevel.ML	Wed May 09 19:53:37 2018 +0200
     7.2 +++ b/src/Pure/Isar/toplevel.ML	Wed May 09 20:45:57 2018 +0200
     7.3 @@ -668,19 +668,19 @@
     7.4    let val trs = tl (Thy_Syntax.flat_element elem)
     7.5    in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
     7.6  
     7.7 -fun proof_future_enabled estimate st =
     7.8 +fun future_proofs_enabled estimate st =
     7.9    (case try proof_of st of
    7.10      NONE => false
    7.11    | SOME state =>
    7.12        not (Proof.is_relevant state) andalso
    7.13         (if can (Proof.assert_bottom true) state
    7.14 -        then Goal.future_enabled 1
    7.15 -        else Goal.future_enabled 2 orelse Goal.future_enabled_timing estimate));
    7.16 +        then Future.proofs_enabled 1
    7.17 +        else Future.proofs_enabled 2 orelse Future.proofs_enabled_timing estimate));
    7.18  
    7.19  fun atom_result keywords tr st =
    7.20    let
    7.21      val st' =
    7.22 -      if Goal.future_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
    7.23 +      if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
    7.24          (Execution.fork
    7.25            {name = "Toplevel.diag", pos = pos_of tr, pri = ~1}
    7.26            (fn () => command tr st); st)
    7.27 @@ -696,7 +696,7 @@
    7.28          val (body_elems, end_tr) = element_rest;
    7.29          val estimate = timing_estimate elem;
    7.30        in
    7.31 -        if not (proof_future_enabled estimate st')
    7.32 +        if not (future_proofs_enabled estimate st')
    7.33          then
    7.34            let
    7.35              val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
     8.1 --- a/src/Pure/ML/ml_compiler.ML	Wed May 09 19:53:37 2018 +0200
     8.2 +++ b/src/Pure/ML/ml_compiler.ML	Wed May 09 20:45:57 2018 +0200
     8.3 @@ -120,7 +120,7 @@
     8.4        |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
     8.5        |> Output.report;
     8.6      val _ =
     8.7 -      if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
     8.8 +      if not (null persistent_reports) andalso redirect andalso Future.enabled ()
     8.9        then
    8.10          Execution.print
    8.11            {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
     9.1 --- a/src/Pure/PIDE/command.ML	Wed May 09 19:53:37 2018 +0200
     9.2 +++ b/src/Pure/PIDE/command.ML	Wed May 09 20:45:57 2018 +0200
     9.3 @@ -190,7 +190,7 @@
     9.4    end) ();
     9.5  
     9.6  fun run keywords int tr st =
     9.7 -  if Goal.future_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then
     9.8 +  if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then
     9.9      (Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
    9.10        (fn () => Toplevel.command_exception int tr st); ([], SOME st))
    9.11    else Toplevel.command_errors int tr st;
    9.12 @@ -429,7 +429,7 @@
    9.13  
    9.14  fun run_print execution_id (Print {name, delay, pri, exec_id, print_process, ...}) =
    9.15    if ignore_process print_process then ()
    9.16 -  else if pri <= 0 orelse (Multithreading.enabled () andalso Options.default_bool "parallel_print")
    9.17 +  else if pri <= 0 orelse (Future.enabled () andalso Options.default_bool "parallel_print")
    9.18    then
    9.19      let
    9.20        val group = Future.worker_subgroup ();
    10.1 --- a/src/Pure/PIDE/execution.ML	Wed May 09 19:53:37 2018 +0200
    10.2 +++ b/src/Pure/PIDE/execution.ML	Wed May 09 20:45:57 2018 +0200
    10.3 @@ -162,7 +162,7 @@
    10.4  fun fork_prints exec_id =
    10.5    (case Inttab.lookup (#2 (get_state ())) exec_id of
    10.6      SOME (_, prints) =>
    10.7 -      if Multithreading.relevant prints then
    10.8 +      if Future.relevant prints then
    10.9          let val pos = Position.thread_data () in
   10.10            List.app (fn {name, pri, body} =>
   10.11              ignore (fork {name = name, pos = pos, pri = pri} body)) (rev prints)
    11.1 --- a/src/Pure/Thy/thy_info.ML	Wed May 09 19:53:37 2018 +0200
    11.2 +++ b/src/Pure/Thy/thy_info.ML	Wed May 09 20:45:57 2018 +0200
    11.3 @@ -388,7 +388,7 @@
    11.4        {document = document, symbols = symbols, bibtex_entries = bibtex_entries,
    11.5          last_timing = last_timing};
    11.6      val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty;
    11.7 -  in if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks end;
    11.8 +  in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end;
    11.9  
   11.10  fun use_thy name =
   11.11    use_theories
    12.1 --- a/src/Pure/goal.ML	Wed May 09 19:53:37 2018 +0200
    12.2 +++ b/src/Pure/goal.ML	Wed May 09 20:45:57 2018 +0200
    12.3 @@ -23,8 +23,6 @@
    12.4    val finish: Proof.context -> thm -> thm
    12.5    val norm_result: Proof.context -> thm -> thm
    12.6    val skip_proofs_enabled: unit -> bool
    12.7 -  val future_enabled: int -> bool
    12.8 -  val future_enabled_timing: Time.time -> bool
    12.9    val future_result: Proof.context -> thm future -> term -> thm
   12.10    val prove_internal: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm
   12.11    val is_schematic: term -> bool
   12.12 @@ -111,14 +109,6 @@
   12.13      else skip
   12.14    end;
   12.15  
   12.16 -fun future_enabled n =
   12.17 -  Multithreading.parallel_proofs_enabled n andalso
   12.18 -  is_some (Future.worker_task ());
   12.19 -
   12.20 -fun future_enabled_timing t =
   12.21 -  future_enabled 1 andalso
   12.22 -    Time.toReal t >= Options.default_real "parallel_subproofs_threshold";
   12.23 -
   12.24  
   12.25  (* future_result *)
   12.26  
   12.27 @@ -176,7 +166,7 @@
   12.28  
   12.29      val schematic = exists is_schematic props;
   12.30      val immediate = is_none fork_pri;
   12.31 -    val future = future_enabled 1;
   12.32 +    val future = Future.proofs_enabled 1;
   12.33      val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
   12.34  
   12.35      val pos = Position.thread_data ();
   12.36 @@ -258,7 +248,7 @@
   12.37  fun prove_sorry ctxt xs asms prop tac =
   12.38    if Config.get ctxt quick_and_dirty then
   12.39      prove ctxt xs asms prop (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt))
   12.40 -  else (if future_enabled 1 then prove_future_pri ctxt ~2 else prove ctxt) xs asms prop tac;
   12.41 +  else (if Future.proofs_enabled 1 then prove_future_pri ctxt ~2 else prove ctxt) xs asms prop tac;
   12.42  
   12.43  fun prove_sorry_global thy xs asms prop tac =
   12.44    Drule.export_without_context
    13.1 --- a/src/Pure/par_tactical.ML	Wed May 09 19:53:37 2018 +0200
    13.2 +++ b/src/Pure/par_tactical.ML	Wed May 09 20:45:57 2018 +0200
    13.3 @@ -46,7 +46,7 @@
    13.4        Drule.strip_imp_prems (Thm.cprop_of st)
    13.5        |> map (Thm.adjust_maxidx_cterm ~1);
    13.6    in
    13.7 -    if Multithreading.relevant goals andalso forall (fn g => Thm.maxidx_of_cterm g = ~1) goals then
    13.8 +    if Future.relevant goals andalso forall (fn g => Thm.maxidx_of_cterm g = ~1) goals then
    13.9        let
   13.10          fun try_goal g =
   13.11            (case SINGLE tac (Goal.init g) of