parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
--- 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)
----------------------------------
--- 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.
--- 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.
--- 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 ..
--- 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)
--- 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
--- 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 *)