# HG changeset patch # User wenzelm # Date 1296835860 -3600 # Node ID d27950860514a2660e6970c7125a76cf33952c66 # Parent dca4c58c5d578ed4bd6270d611e724b073019e00 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold; diff -r dca4c58c5d57 -r d27950860514 NEWS --- a/NEWS Fri Feb 04 16:33:12 2011 +0100 +++ b/NEWS Fri Feb 04 17:11:00 2011 +0100 @@ -4,12 +4,20 @@ New in this Isabelle version ---------------------------- +*** General *** + +* Parallelization of nested Isar proofs is subject to +Goal.parallel_proofs_threshold (default 100). See also isabelle +usedir option -Q. + + *** Document preparation *** * New term style "isub" as ad-hoc conversion of variables x1, y23 into subscripted form x\<^isub>1, y\<^isub>2\<^isub>3. + New in Isabelle2011 (January 2011) ---------------------------------- diff -r dca4c58c5d57 -r d27950860514 doc-src/System/Thy/Presentation.thy --- a/doc-src/System/Thy/Presentation.thy Fri Feb 04 16:33:12 2011 +0100 +++ b/doc-src/System/Thy/Presentation.thy Fri Feb 04 17:11:00 2011 +0100 @@ -446,6 +446,7 @@ -D PATH dump generated document sources into PATH -M MAX multithreading: maximum number of worker threads (default 1) -P PATH set path for remote theory browsing information + -Q INT set threshold for sub-proof parallelization (default 100) -T LEVEL multithreading: trace level (default 0) -V VERSION declare alternative document VERSION -b build mode (output heap image, using current dir) @@ -565,8 +566,9 @@ \medskip The @{verbatim "-q"} option specifies the level of parallel proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel proofs (default), @{verbatim 2} toplevel and nested Isar proofs. - The resulting speedup may vary, depending on the number of worker - threads, granularity of proofs, and whether proof terms are enabled. + The option @{verbatim "-Q"} specifies a threshold for @{verbatim + "-q2"}: nested proofs are only parallelized when the current number + of forked proofs falls below the given value (default 100). \medskip The @{verbatim "-t"} option produces a more detailed internal timing report of the session. diff -r dca4c58c5d57 -r d27950860514 doc-src/System/Thy/document/Presentation.tex --- a/doc-src/System/Thy/document/Presentation.tex Fri Feb 04 16:33:12 2011 +0100 +++ b/doc-src/System/Thy/document/Presentation.tex Fri Feb 04 17:11:00 2011 +0100 @@ -472,6 +472,7 @@ -D PATH dump generated document sources into PATH -M MAX multithreading: maximum number of worker threads (default 1) -P PATH set path for remote theory browsing information + -Q INT set threshold for sub-proof parallelization (default 100) -T LEVEL multithreading: trace level (default 0) -V VERSION declare alternative document VERSION -b build mode (output heap image, using current dir) @@ -582,8 +583,8 @@ \medskip The \verb|-q| option specifies the level of parallel proof checking: \verb|0| no proofs, \verb|1| toplevel proofs (default), \verb|2| toplevel and nested Isar proofs. - The resulting speedup may vary, depending on the number of worker - threads, granularity of proofs, and whether proof terms are enabled. + The option \verb|-Q| specifies a threshold for \verb|-q2|: nested proofs are only parallelized when the current number + of forked proofs falls below the given value (default 100). \medskip The \verb|-t| option produces a more detailed internal timing report of the session. diff -r dca4c58c5d57 -r d27950860514 lib/Tools/usedir --- a/lib/Tools/usedir Fri Feb 04 16:33:12 2011 +0100 +++ b/lib/Tools/usedir Fri Feb 04 17:11:00 2011 +0100 @@ -19,6 +19,7 @@ echo " -D PATH dump generated document sources into PATH" echo " -M MAX multithreading: maximum number of worker threads (default 1)" echo " -P PATH set path for remote theory browsing information" + echo " -Q INT set threshold for sub-proof parallelization (default 100)" echo " -T LEVEL multithreading: trace level (default 0)" echo " -V VERSION declare alternative document VERSION" echo " -b build mode (output heap image, using current dir)" @@ -84,13 +85,14 @@ SESSION="" PROOFS="0" PARALLEL_PROOFS="1" +PARALLEL_PROOFS_THRESHOLD="100" TIMING=false VERBOSE=false function getoptions() { OPTIND=1 - while getopts "C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT + while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT do case "$OPT" in C) @@ -111,6 +113,10 @@ P) RPATH="$OPTARG" ;; + Q) + check_number "$OPTARG" + PARALLEL_PROOFS_THRESHOLD="$OPTARG" + ;; T) check_number "$OPTARG" TRACETHREADS="$OPTARG" @@ -235,7 +241,7 @@ LOG="$LOGDIR/$ITEM" "$ISABELLE_PROCESS" \ - -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \ + -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \ -q -w $LOGIC $NAME > "$LOG" RC="$?" else @@ -244,7 +250,7 @@ LOG="$LOGDIR/$ITEM" "$ISABELLE_PROCESS" \ - -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \ + -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \ -r -q "$LOGIC" > "$LOG" RC="$?" cd .. diff -r dca4c58c5d57 -r d27950860514 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Fri Feb 04 16:33:12 2011 +0100 +++ b/src/Pure/Isar/toplevel.ML Fri Feb 04 17:11:00 2011 +0100 @@ -663,8 +663,7 @@ val future_proof = Proof.global_future_proof (fn prf => - singleton - (Future.forks {name = "Toplevel.proof_result", group = NONE, deps = [], pri = ~1}) + Goal.fork_name "Toplevel.future_proof" (fn () => let val (states, result_state) = (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev) diff -r dca4c58c5d57 -r d27950860514 src/Pure/System/session.ML --- a/src/Pure/System/session.ML Fri Feb 04 16:33:12 2011 +0100 +++ b/src/Pure/System/session.ML Fri Feb 04 17:11:00 2011 +0100 @@ -11,7 +11,7 @@ val welcome: unit -> string val use_dir: string -> string -> bool -> string list -> bool -> bool -> string -> bool -> string list -> string -> string -> bool * string -> - string -> int -> bool -> bool -> int -> int -> int -> unit + string -> int -> bool -> bool -> int -> int -> int -> int -> unit val finish: unit -> unit end; @@ -93,7 +93,8 @@ | dumping (cp, path) = SOME (cp, Path.explode path); fun use_dir item root build modes reset info doc doc_graph doc_versions parent - name dump rpath level timing verbose max_threads trace_threads parallel_proofs = + name dump rpath level timing verbose max_threads trace_threads + parallel_proofs parallel_proofs_threshold = ((fn () => (init reset parent name; Present.init build info doc doc_graph doc_versions (path ()) name @@ -113,6 +114,7 @@ |> Unsynchronized.setmp Proofterm.proofs level |> Unsynchronized.setmp print_mode (modes @ print_mode_value ()) |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs + |> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold |> Unsynchronized.setmp Multithreading.trace trace_threads |> Unsynchronized.setmp Multithreading.max_threads (if Multithreading.available then max_threads diff -r dca4c58c5d57 -r d27950860514 src/Pure/goal.ML --- a/src/Pure/goal.ML Fri Feb 04 16:33:12 2011 +0100 +++ b/src/Pure/goal.ML Fri Feb 04 17:11:00 2011 +0100 @@ -7,6 +7,7 @@ signature BASIC_GOAL = sig val parallel_proofs: int Unsynchronized.ref + val parallel_proofs_threshold: int Unsynchronized.ref val SELECT_GOAL: tactic -> int -> tactic val CONJUNCTS: tactic -> int -> tactic val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic @@ -105,21 +106,47 @@ #> Drule.zero_var_indexes; -(* parallel proofs *) +(* forked proofs *) + +val forked_proofs = Synchronized.var "forked_proofs" 0; + +fun forked i = + Synchronized.change forked_proofs (fn m => + let + val n = m + i; + val _ = + Multithreading.tracing 1 (fn () => + ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n)); + in n end); fun fork_name name e = - singleton (Future.forks {name = name, group = NONE, deps = [], pri = ~1}) - (fn () => Future.status e); + uninterruptible (fn _ => fn () => + let + val _ = forked 1; + val future = + singleton (Future.forks {name = name, group = NONE, deps = [], pri = ~1}) + (fn () => + (*interruptible*) + Exn.release + (Exn.capture Future.status e before forked ~1 + handle exn => (forked ~1; reraise exn))); + in future end) (); fun fork e = fork_name "Goal.fork" e; +(* scheduling parameters *) + val parallel_proofs = Unsynchronized.ref 1; +val parallel_proofs_threshold = Unsynchronized.ref 100; fun future_enabled () = - Multithreading.enabled () andalso is_some (Future.worker_task ()) andalso ! parallel_proofs >= 1; + Multithreading.enabled () andalso ! parallel_proofs >= 1 andalso + is_some (Future.worker_task ()); -fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2; +fun local_future_enabled () = + future_enabled () andalso ! parallel_proofs >= 2 andalso + Synchronized.value forked_proofs < ! parallel_proofs_threshold; (* future_result *)