scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
--- a/doc-src/System/Thy/Presentation.thy Tue Feb 22 17:06:14 2011 +0100
+++ b/doc-src/System/Thy/Presentation.thy Tue Feb 22 19:44:15 2011 +0100
@@ -446,7 +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)
+ -Q INT set threshold for sub-proof parallelization (default 50)
-T LEVEL multithreading: trace level (default 0)
-V VERSION declare alternative document VERSION
-b build mode (output heap image, using current dir)
@@ -568,7 +568,9 @@
proofs (default), @{verbatim 2} toplevel and nested Isar proofs.
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).
+ of forked proofs falls below the given value (default 50),
+ multiplied by the number of worker threads (see option @{verbatim
+ "-M"}).
\medskip The @{verbatim "-t"} option produces a more detailed
internal timing report of the session.
@@ -578,16 +580,16 @@
prepared documents.
\medskip The @{verbatim "-M"} option specifies the maximum number of
- parallel threads used for processing independent tasks when checking
- theory sources (multithreading only works on suitable ML platforms).
- The special value of @{verbatim 0} or @{verbatim max} refers to the
- number of actual CPU cores of the underlying machine, which is a
- good starting point for optimal performance tuning. The @{verbatim
- "-T"} option determines the level of detail in tracing output
- concerning the internal locking and scheduling in multithreaded
- operation. This may be helpful in isolating performance
- bottle-necks, e.g.\ due to excessive wait states when locking
- critical code sections.
+ parallel worker threads used for processing independent tasks when
+ checking theory sources (multithreading only works on suitable ML
+ platforms). The special value of @{verbatim 0} or @{verbatim max}
+ refers to the number of actual CPU cores of the underlying machine,
+ which is a good starting point for optimal performance tuning. The
+ @{verbatim "-T"} option determines the level of detail in tracing
+ output concerning the internal locking and scheduling in
+ multithreaded operation. This may be helpful in isolating
+ performance bottle-necks, e.g.\ due to excessive wait states when
+ locking critical code sections.
\medskip Any @{tool usedir} session is named by some \emph{session
identifier}. These accumulate, documenting the way sessions depend
--- a/doc-src/System/Thy/document/Presentation.tex Tue Feb 22 17:06:14 2011 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex Tue Feb 22 19:44:15 2011 +0100
@@ -472,7 +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)
+ -Q INT set threshold for sub-proof parallelization (default 50)
-T LEVEL multithreading: trace level (default 0)
-V VERSION declare alternative document VERSION
-b build mode (output heap image, using current dir)
@@ -584,7 +584,8 @@
proof checking: \verb|0| no proofs, \verb|1| toplevel
proofs (default), \verb|2| toplevel and nested Isar proofs.
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).
+ of forked proofs falls below the given value (default 50),
+ multiplied by the number of worker threads (see option \verb|-M|).
\medskip The \verb|-t| option produces a more detailed
internal timing report of the session.
@@ -594,15 +595,16 @@
prepared documents.
\medskip The \verb|-M| option specifies the maximum number of
- parallel threads used for processing independent tasks when checking
- theory sources (multithreading only works on suitable ML platforms).
- The special value of \verb|0| or \verb|max| refers to the
- number of actual CPU cores of the underlying machine, which is a
- good starting point for optimal performance tuning. The \verb|-T| option determines the level of detail in tracing output
- concerning the internal locking and scheduling in multithreaded
- operation. This may be helpful in isolating performance
- bottle-necks, e.g.\ due to excessive wait states when locking
- critical code sections.
+ parallel worker threads used for processing independent tasks when
+ checking theory sources (multithreading only works on suitable ML
+ platforms). The special value of \verb|0| or \verb|max|
+ refers to the number of actual CPU cores of the underlying machine,
+ which is a good starting point for optimal performance tuning. The
+ \verb|-T| option determines the level of detail in tracing
+ output concerning the internal locking and scheduling in
+ multithreaded operation. This may be helpful in isolating
+ performance bottle-necks, e.g.\ due to excessive wait states when
+ locking critical code sections.
\medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session
identifier}. These accumulate, documenting the way sessions depend
--- a/src/Pure/goal.ML Tue Feb 22 17:06:14 2011 +0100
+++ b/src/Pure/goal.ML Tue Feb 22 19:44:15 2011 +0100
@@ -138,7 +138,7 @@
(* scheduling parameters *)
val parallel_proofs = Unsynchronized.ref 1;
-val parallel_proofs_threshold = Unsynchronized.ref 100;
+val parallel_proofs_threshold = Unsynchronized.ref 50;
fun future_enabled () =
Multithreading.enabled () andalso ! parallel_proofs >= 1 andalso
@@ -146,7 +146,8 @@
fun local_future_enabled () =
future_enabled () andalso ! parallel_proofs >= 2 andalso
- Synchronized.value forked_proofs < ! parallel_proofs_threshold;
+ Synchronized.value forked_proofs <
+ ! parallel_proofs_threshold * Multithreading.max_threads_value ();
(* future_result *)