# HG changeset patch
# User wenzelm
# Date 1298400255 -3600
# Node ID 2d84831dc1a017d3375beebc59a637f7241d4bb0
# Parent  6d4c3ee8219dde3d9b2d7f2d8a96d7d72d58e0fd
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;

diff -r 6d4c3ee8219d -r 2d84831dc1a0 doc-src/System/Thy/Presentation.thy
--- 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
diff -r 6d4c3ee8219d -r 2d84831dc1a0 doc-src/System/Thy/document/Presentation.tex
--- 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
diff -r 6d4c3ee8219d -r 2d84831dc1a0 src/Pure/goal.ML
--- 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 *)