clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
authorwenzelm
Wed Mar 13 21:25:08 2013 +0100 (2013-03-13 ago)
changeset 51423e5f9a6d9ca82
parent 51422 821a70e29e0b
child 51424 d2dfd743b58c
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
clarified unknown timing vs. zero timing;
tuned;
etc/options
src/Pure/Isar/toplevel.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/session.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_syntax.ML
src/Pure/Tools/build.ML
src/Pure/goal.ML
src/Tools/jEdit/src/isabelle_options.scala
     1.1 --- a/etc/options	Wed Mar 13 17:15:25 2013 +0100
     1.2 +++ b/etc/options	Wed Mar 13 21:25:08 2013 +0100
     1.3 @@ -51,8 +51,10 @@
     1.4    -- "level of tracing information for multithreading"
     1.5  option parallel_proofs : int = 2
     1.6    -- "level of parallel proof checking: 0, 1, 2"
     1.7 -option parallel_proofs_threshold : int = 100
     1.8 -  -- "threshold for sub-proof parallelization"
     1.9 +option parallel_subproofs_saturation : int = 100
    1.10 +  -- "upper bound for forks of nested proofs (multiplied by worker threads)"
    1.11 +option parallel_subproofs_threshold : real = 0.01
    1.12 +  -- "lower bound of timing estimate for forked nested proofs (seconds)"
    1.13  option parallel_proofs_reuse_timing : bool = true
    1.14    -- "reuse timing information from old log file for parallel proof scheduling"
    1.15  
     2.1 --- a/src/Pure/Isar/toplevel.ML	Wed Mar 13 17:15:25 2013 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Mar 13 21:25:08 2013 +0100
     2.3 @@ -91,8 +91,8 @@
     2.4    val status: transition -> Markup.T -> unit
     2.5    val add_hook: (transition -> state -> state -> unit) -> unit
     2.6    val approximative_id: transition -> {file: string, offset: int, name: string} option
     2.7 -  val get_timing: transition -> Time.time
     2.8 -  val put_timing: Time.time -> transition -> transition
     2.9 +  val get_timing: transition -> Time.time option
    2.10 +  val put_timing: Time.time option -> transition -> transition
    2.11    val transition: bool -> transition -> state -> (state * (exn * string) option) option
    2.12    val command_errors: bool -> transition -> state -> Runtime.error list * state option
    2.13    val command_exception: bool -> transition -> state -> state
    2.14 @@ -346,7 +346,7 @@
    2.15    int_only: bool,            (*interactive-only*)
    2.16    print: bool,               (*print result state*)
    2.17    no_timing: bool,           (*suppress timing*)
    2.18 -  timing: Time.time,         (*prescient timing information*)
    2.19 +  timing: Time.time option,  (*prescient timing information*)
    2.20    trans: trans list};        (*primitive transitions (union)*)
    2.21  
    2.22  fun make_transition (name, pos, int_only, print, no_timing, timing, trans) =
    2.23 @@ -356,7 +356,7 @@
    2.24  fun map_transition f (Transition {name, pos, int_only, print, no_timing, timing, trans}) =
    2.25    make_transition (f (name, pos, int_only, print, no_timing, timing, trans));
    2.26  
    2.27 -val empty = make_transition ("", Position.none, false, false, false, Time.zeroTime, []);
    2.28 +val empty = make_transition ("", Position.none, false, false, false, NONE, []);
    2.29  
    2.30  
    2.31  (* diagnostics *)
    2.32 @@ -638,14 +638,12 @@
    2.33  local
    2.34  
    2.35  fun timing_message tr (t: Timing.timing) =
    2.36 -  if Timing.is_relevant_time (#elapsed t) then
    2.37 -    (case approximative_id tr of
    2.38 -      SOME id =>
    2.39 -        (Output.protocol_message
    2.40 -          (Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) ""
    2.41 -        handle Fail _ => ())
    2.42 -    | NONE => ())
    2.43 -  else ();
    2.44 +  (case approximative_id tr of
    2.45 +    SOME id =>
    2.46 +      (Output.protocol_message
    2.47 +        (Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) ""
    2.48 +      handle Fail _ => ())
    2.49 +  | NONE => ());
    2.50  
    2.51  fun app int (tr as Transition {trans, print, no_timing, ...}) =
    2.52    setmp_thread_position tr (fn state =>
    2.53 @@ -727,29 +725,38 @@
    2.54  val get_result = Result.get o Proof.context_of;
    2.55  val put_result = Proof.map_context o Result.put;
    2.56  
    2.57 -fun proof_future_enabled st =
    2.58 +fun timing_estimate include_head elem =
    2.59 +  let
    2.60 +    val trs = Thy_Syntax.flat_element elem |> not include_head ? tl;
    2.61 +    val timings = map get_timing trs;
    2.62 +  in
    2.63 +    if forall is_some timings then
    2.64 +      SOME (fold (curry Time.+ o the) timings Time.zeroTime)
    2.65 +    else NONE
    2.66 +  end;
    2.67 +
    2.68 +fun priority NONE = ~1
    2.69 +  | priority (SOME estimate) =
    2.70 +      Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
    2.71 +
    2.72 +fun proof_future_enabled estimate st =
    2.73    (case try proof_of st of
    2.74      NONE => false
    2.75    | SOME state =>
    2.76        not (Proof.is_relevant state) andalso
    2.77         (if can (Proof.assert_bottom true) state
    2.78          then Goal.future_enabled ()
    2.79 -        else Goal.future_enabled_nested 2));
    2.80 -
    2.81 -fun priority elem =
    2.82 -  let
    2.83 -    val estimate = Thy_Syntax.fold_element (curry Time.+ o get_timing) elem Time.zeroTime;
    2.84 -  in
    2.85 -    if estimate = Time.zeroTime then ~1
    2.86 -    else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1)
    2.87 -  end;
    2.88 +        else
    2.89 +          (case estimate of
    2.90 +            NONE => Goal.future_enabled_nested 2
    2.91 +          | SOME t => Goal.future_enabled_timing t)));
    2.92  
    2.93  fun atom_result tr st =
    2.94    let
    2.95      val st' =
    2.96        if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
    2.97          setmp_thread_position tr (fn () =>
    2.98 -          (Goal.fork_name "Toplevel.diag" (priority (Thy_Syntax.atom tr))
    2.99 +          (Goal.fork_name "Toplevel.diag" (priority (timing_estimate true (Thy_Syntax.atom tr)))
   2.100              (fn () => command tr st); st)) ()
   2.101        else command tr st;
   2.102    in (Result (tr, st'), st') end;
   2.103 @@ -757,12 +764,13 @@
   2.104  in
   2.105  
   2.106  fun element_result (Thy_Syntax.Element (tr, NONE)) st = atom_result tr st
   2.107 -  | element_result (Thy_Syntax.Element (head_tr, SOME element_rest)) st =
   2.108 +  | element_result (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st =
   2.109        let
   2.110          val (head_result, st') = atom_result head_tr st;
   2.111          val (body_elems, end_tr) = element_rest;
   2.112 +        val estimate = timing_estimate false elem;
   2.113        in
   2.114 -        if not (proof_future_enabled st')
   2.115 +        if not (proof_future_enabled estimate st')
   2.116          then
   2.117            let
   2.118              val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
   2.119 @@ -776,7 +784,7 @@
   2.120                (fn state =>
   2.121                  setmp_thread_position head_tr (fn () =>
   2.122                    Goal.fork_name "Toplevel.future_proof"
   2.123 -                    (priority (Thy_Syntax.Element (empty, SOME element_rest)))
   2.124 +                    (priority estimate)
   2.125                      (fn () =>
   2.126                        let
   2.127                          val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
     3.1 --- a/src/Pure/System/isabelle_process.ML	Wed Mar 13 17:15:25 2013 +0100
     3.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Mar 13 21:25:08 2013 +0100
     3.3 @@ -243,7 +243,8 @@
     3.4          if Multithreading.max_threads_value () < 2
     3.5          then Multithreading.max_threads := 2 else ();
     3.6          Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0);
     3.7 -        Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold";
     3.8 +        Goal.parallel_subproofs_saturation := Options.int options "parallel_subproofs_saturation";
     3.9 +        Goal.parallel_subproofs_threshold := Options.real options "parallel_subproofs_threshold";
    3.10          tracing_messages := Options.int options "editor_tracing_messages"
    3.11        end);
    3.12  
     4.1 --- a/src/Pure/System/session.ML	Wed Mar 13 17:15:25 2013 +0100
     4.2 +++ b/src/Pure/System/session.ML	Wed Mar 13 21:25:08 2013 +0100
     4.3 @@ -94,7 +94,7 @@
     4.4  
     4.5  fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
     4.6      name doc_dump rpath level timing verbose max_threads trace_threads
     4.7 -    parallel_proofs parallel_proofs_threshold =
     4.8 +    parallel_proofs parallel_subproofs_saturation =
     4.9    ((fn () =>
    4.10      let
    4.11        val _ =
    4.12 @@ -116,7 +116,7 @@
    4.13      |> Unsynchronized.setmp Proofterm.proofs level
    4.14      |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
    4.15      |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs
    4.16 -    |> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold
    4.17 +    |> Unsynchronized.setmp Goal.parallel_subproofs_saturation parallel_subproofs_saturation
    4.18      |> Unsynchronized.setmp Multithreading.trace trace_threads
    4.19      |> Unsynchronized.setmp Multithreading.max_threads
    4.20        (if Multithreading.available then max_threads
     5.1 --- a/src/Pure/Thy/thy_info.ML	Wed Mar 13 17:15:25 2013 +0100
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Mar 13 21:25:08 2013 +0100
     5.3 @@ -17,7 +17,7 @@
     5.4    val loaded_files: string -> Path.T list
     5.5    val remove_thy: string -> unit
     5.6    val kill_thy: string -> unit
     5.7 -  val use_theories: {last_timing: Toplevel.transition -> Time.time, master_dir: Path.T} ->
     5.8 +  val use_theories: {last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
     5.9      (string * Position.T) list -> unit
    5.10    val use_thys: (string * Position.T) list -> unit
    5.11    val use_thy: string * Position.T -> unit
    5.12 @@ -174,7 +174,7 @@
    5.13  fun result_commit (Result {commit, ...}) = commit;
    5.14  fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
    5.15  
    5.16 -fun join_proofs (Result {theory, id, present, ...}) =
    5.17 +fun join_proofs (Result {theory, id, ...}) =
    5.18    let
    5.19      val result1 = Exn.capture Thm.join_theory_proofs theory;
    5.20      val results2 = Future.join_results (Goal.peek_futures id);
    5.21 @@ -351,7 +351,7 @@
    5.22  fun use_theories {last_timing, master_dir} imports =
    5.23    schedule_tasks (snd (require_thys last_timing [] master_dir imports String_Graph.empty));
    5.24  
    5.25 -val use_thys = use_theories {last_timing = K Time.zeroTime, master_dir = Path.current};
    5.26 +val use_thys = use_theories {last_timing = K NONE, master_dir = Path.current};
    5.27  val use_thy = use_thys o single;
    5.28  
    5.29  
    5.30 @@ -361,7 +361,7 @@
    5.31    let
    5.32      val {name = (name, _), imports, ...} = header;
    5.33      val _ = kill_thy name;
    5.34 -    val _ = use_theories {last_timing = K Time.zeroTime, master_dir = master_dir} imports;
    5.35 +    val _ = use_theories {last_timing = K NONE, master_dir = master_dir} imports;
    5.36      val _ = Thy_Header.define_keywords header;
    5.37      val parents = map (get_theory o base_name o fst) imports;
    5.38    in Thy_Load.begin_theory master_dir header parents end;
     6.1 --- a/src/Pure/Thy/thy_load.ML	Wed Mar 13 17:15:25 2013 +0100
     6.2 +++ b/src/Pure/Thy/thy_load.ML	Wed Mar 13 21:25:08 2013 +0100
     6.3 @@ -22,7 +22,7 @@
     6.4    val use_ml: Path.T -> unit
     6.5    val exec_ml: Path.T -> generic_theory -> generic_theory
     6.6    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
     6.7 -  val load_thy: (Toplevel.transition -> Time.time) -> int -> Path.T -> Thy_Header.header ->
     6.8 +  val load_thy: (Toplevel.transition -> Time.time option) -> int -> Path.T -> Thy_Header.header ->
     6.9      Position.T -> string -> theory list -> theory * (unit -> unit) * int
    6.10    val set_master_path: Path.T -> unit
    6.11    val get_master_path: unit -> Path.T
     7.1 --- a/src/Pure/Thy/thy_syntax.ML	Wed Mar 13 17:15:25 2013 +0100
     7.2 +++ b/src/Pure/Thy/thy_syntax.ML	Wed Mar 13 21:25:08 2013 +0100
     7.3 @@ -17,7 +17,6 @@
     7.4    val parse_spans: Token.T list -> span list
     7.5    datatype 'a element = Element of 'a * ('a element list * 'a) option
     7.6    val atom: 'a -> 'a element
     7.7 -  val fold_element: ('a -> 'b -> 'b) -> 'a element -> 'b -> 'b
     7.8    val map_element: ('a -> 'b) -> 'a element -> 'b element
     7.9    val flat_element: 'a element -> 'a list
    7.10    val last_element: 'a element -> 'a
    7.11 @@ -144,9 +143,6 @@
    7.12  fun element (a, b) = Element (a, SOME b);
    7.13  fun atom a = Element (a, NONE);
    7.14  
    7.15 -fun fold_element f (Element (a, NONE)) = f a
    7.16 -  | fold_element f (Element (a, SOME (elems, b))) = f a #> (fold o fold_element) f elems #> f b;
    7.17 -
    7.18  fun map_element f (Element (a, NONE)) = Element (f a, NONE)
    7.19    | map_element f (Element (a, SOME (elems, b))) =
    7.20        Element (f a, SOME ((map o map_element) f elems, f b));
     8.1 --- a/src/Pure/Tools/build.ML	Wed Mar 13 17:15:25 2013 +0100
     8.2 +++ b/src/Pure/Tools/build.ML	Wed Mar 13 21:25:08 2013 +0100
     8.3 @@ -50,8 +50,10 @@
     8.4      |> Unsynchronized.setmp print_mode
     8.5          (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
     8.6      |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
     8.7 -    |> Unsynchronized.setmp Goal.parallel_proofs_threshold
     8.8 -        (Options.int options "parallel_proofs_threshold")
     8.9 +    |> Unsynchronized.setmp Goal.parallel_subproofs_saturation
    8.10 +        (Options.int options "parallel_subproofs_saturation")
    8.11 +    |> Unsynchronized.setmp Goal.parallel_subproofs_threshold
    8.12 +        (Options.real options "parallel_subproofs_threshold")
    8.13      |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    8.14      |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    8.15      |> Unsynchronized.setmp Future.ML_statistics true
    8.16 @@ -99,10 +101,10 @@
    8.17        (case Symtab.lookup timings file of
    8.18          SOME offsets =>
    8.19            (case Inttab.lookup offsets offset of
    8.20 -            SOME (name', time) => if name = name' then time else Time.zeroTime
    8.21 -          | NONE => Time.zeroTime)
    8.22 -      | NONE => Time.zeroTime)
    8.23 -  | NONE => Time.zeroTime);
    8.24 +            SOME (name', time) => if name = name' then SOME time else NONE
    8.25 +          | NONE => NONE)
    8.26 +      | NONE => NONE)
    8.27 +  | NONE => NONE);
    8.28  
    8.29  in
    8.30  
     9.1 --- a/src/Pure/goal.ML	Wed Mar 13 17:15:25 2013 +0100
     9.2 +++ b/src/Pure/goal.ML	Wed Mar 13 21:25:08 2013 +0100
     9.3 @@ -7,7 +7,8 @@
     9.4  signature BASIC_GOAL =
     9.5  sig
     9.6    val parallel_proofs: int Unsynchronized.ref
     9.7 -  val parallel_proofs_threshold: int Unsynchronized.ref
     9.8 +  val parallel_subproofs_saturation: int Unsynchronized.ref
     9.9 +  val parallel_subproofs_threshold: real Unsynchronized.ref
    9.10    val SELECT_GOAL: tactic -> int -> tactic
    9.11    val CONJUNCTS: tactic -> int -> tactic
    9.12    val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
    9.13 @@ -32,6 +33,7 @@
    9.14    val future_enabled_level: int -> bool
    9.15    val future_enabled: unit -> bool
    9.16    val future_enabled_nested: int -> bool
    9.17 +  val future_enabled_timing: Time.time -> bool
    9.18    val future_result: Proof.context -> thm future -> term -> thm
    9.19    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
    9.20    val prove_multi: Proof.context -> string list -> term list -> term list ->
    9.21 @@ -191,7 +193,8 @@
    9.22  (* scheduling parameters *)
    9.23  
    9.24  val parallel_proofs = Unsynchronized.ref 1;
    9.25 -val parallel_proofs_threshold = Unsynchronized.ref 100;
    9.26 +val parallel_subproofs_saturation = Unsynchronized.ref 100;
    9.27 +val parallel_subproofs_threshold = Unsynchronized.ref 0.01;
    9.28  
    9.29  fun future_enabled_level n =
    9.30    Multithreading.enabled () andalso ! parallel_proofs >= n andalso
    9.31 @@ -201,7 +204,10 @@
    9.32  
    9.33  fun future_enabled_nested n =
    9.34    future_enabled_level n andalso
    9.35 -  forked_count () < ! parallel_proofs_threshold * Multithreading.max_threads_value ();
    9.36 +  forked_count () < ! parallel_subproofs_saturation * Multithreading.max_threads_value ();
    9.37 +
    9.38 +fun future_enabled_timing t =
    9.39 +  future_enabled () andalso Time.toReal t >= ! parallel_subproofs_threshold;
    9.40  
    9.41  
    9.42  (* future_result *)
    10.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Wed Mar 13 17:15:25 2013 +0100
    10.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Wed Mar 13 21:25:08 2013 +0100
    10.3 @@ -41,10 +41,10 @@
    10.4  {
    10.5    // FIXME avoid hard-wired stuff
    10.6    private val relevant_options =
    10.7 -    Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit",
    10.8 -      "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin",
    10.9 -      "jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs",
   10.10 -      "parallel_proofs_threshold", "editor_load_delay", "editor_input_delay",
   10.11 +    Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit",
   10.12 +      "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_font_scale",
   10.13 +      "jedit_tooltip_margin", "jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs",
   10.14 +      "parallel_subproofs_saturation", "editor_load_delay", "editor_input_delay",
   10.15        "editor_output_delay", "editor_reparse_limit", "editor_tracing_messages",
   10.16        "editor_update_delay", "editor_chart_delay")
   10.17