parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
authorwenzelm
Fri Feb 04 17:11:00 2011 +0100 (2011-02-04 ago)
changeset 41703d27950860514
parent 41702 dca4c58c5d57
child 41707 a10f0a1cae41
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
NEWS
doc-src/System/Thy/Presentation.thy
doc-src/System/Thy/document/Presentation.tex
lib/Tools/usedir
src/Pure/Isar/toplevel.ML
src/Pure/System/session.ML
src/Pure/goal.ML
     1.1 --- a/NEWS	Fri Feb 04 16:33:12 2011 +0100
     1.2 +++ b/NEWS	Fri Feb 04 17:11:00 2011 +0100
     1.3 @@ -4,12 +4,20 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Parallelization of nested Isar proofs is subject to
    1.10 +Goal.parallel_proofs_threshold (default 100).  See also isabelle
    1.11 +usedir option -Q.
    1.12 +
    1.13 +
    1.14  *** Document preparation ***
    1.15  
    1.16  * New term style "isub" as ad-hoc conversion of variables x1, y23 into
    1.17  subscripted form x\<^isub>1, y\<^isub>2\<^isub>3.
    1.18  
    1.19  
    1.20 +
    1.21  New in Isabelle2011 (January 2011)
    1.22  ----------------------------------
    1.23  
     2.1 --- a/doc-src/System/Thy/Presentation.thy	Fri Feb 04 16:33:12 2011 +0100
     2.2 +++ b/doc-src/System/Thy/Presentation.thy	Fri Feb 04 17:11:00 2011 +0100
     2.3 @@ -446,6 +446,7 @@
     2.4      -D PATH      dump generated document sources into PATH
     2.5      -M MAX       multithreading: maximum number of worker threads (default 1)
     2.6      -P PATH      set path for remote theory browsing information
     2.7 +    -Q INT       set threshold for sub-proof parallelization (default 100)
     2.8      -T LEVEL     multithreading: trace level (default 0)
     2.9      -V VERSION   declare alternative document VERSION
    2.10      -b           build mode (output heap image, using current dir)
    2.11 @@ -565,8 +566,9 @@
    2.12    \medskip The @{verbatim "-q"} option specifies the level of parallel
    2.13    proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel
    2.14    proofs (default), @{verbatim 2} toplevel and nested Isar proofs.
    2.15 -  The resulting speedup may vary, depending on the number of worker
    2.16 -  threads, granularity of proofs, and whether proof terms are enabled.
    2.17 +  The option @{verbatim "-Q"} specifies a threshold for @{verbatim
    2.18 +  "-q2"}: nested proofs are only parallelized when the current number
    2.19 +  of forked proofs falls below the given value (default 100).
    2.20  
    2.21    \medskip The @{verbatim "-t"} option produces a more detailed
    2.22    internal timing report of the session.
     3.1 --- a/doc-src/System/Thy/document/Presentation.tex	Fri Feb 04 16:33:12 2011 +0100
     3.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Fri Feb 04 17:11:00 2011 +0100
     3.3 @@ -472,6 +472,7 @@
     3.4      -D PATH      dump generated document sources into PATH
     3.5      -M MAX       multithreading: maximum number of worker threads (default 1)
     3.6      -P PATH      set path for remote theory browsing information
     3.7 +    -Q INT       set threshold for sub-proof parallelization (default 100)
     3.8      -T LEVEL     multithreading: trace level (default 0)
     3.9      -V VERSION   declare alternative document VERSION
    3.10      -b           build mode (output heap image, using current dir)
    3.11 @@ -582,8 +583,8 @@
    3.12    \medskip The \verb|-q| option specifies the level of parallel
    3.13    proof checking: \verb|0| no proofs, \verb|1| toplevel
    3.14    proofs (default), \verb|2| toplevel and nested Isar proofs.
    3.15 -  The resulting speedup may vary, depending on the number of worker
    3.16 -  threads, granularity of proofs, and whether proof terms are enabled.
    3.17 +  The option \verb|-Q| specifies a threshold for \verb|-q2|: nested proofs are only parallelized when the current number
    3.18 +  of forked proofs falls below the given value (default 100).
    3.19  
    3.20    \medskip The \verb|-t| option produces a more detailed
    3.21    internal timing report of the session.
     4.1 --- a/lib/Tools/usedir	Fri Feb 04 16:33:12 2011 +0100
     4.2 +++ b/lib/Tools/usedir	Fri Feb 04 17:11:00 2011 +0100
     4.3 @@ -19,6 +19,7 @@
     4.4    echo "    -D PATH      dump generated document sources into PATH"
     4.5    echo "    -M MAX       multithreading: maximum number of worker threads (default 1)"
     4.6    echo "    -P PATH      set path for remote theory browsing information"
     4.7 +  echo "    -Q INT       set threshold for sub-proof parallelization (default 100)"
     4.8    echo "    -T LEVEL     multithreading: trace level (default 0)"
     4.9    echo "    -V VERSION   declare alternative document VERSION"
    4.10    echo "    -b           build mode (output heap image, using current dir)"
    4.11 @@ -84,13 +85,14 @@
    4.12  SESSION=""
    4.13  PROOFS="0"
    4.14  PARALLEL_PROOFS="1"
    4.15 +PARALLEL_PROOFS_THRESHOLD="100"
    4.16  TIMING=false
    4.17  VERBOSE=false
    4.18  
    4.19  function getoptions()
    4.20  {
    4.21    OPTIND=1
    4.22 -  while getopts "C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
    4.23 +  while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
    4.24    do
    4.25      case "$OPT" in
    4.26        C)
    4.27 @@ -111,6 +113,10 @@
    4.28        P)
    4.29          RPATH="$OPTARG"
    4.30          ;;
    4.31 +      Q)
    4.32 +        check_number "$OPTARG"
    4.33 +        PARALLEL_PROOFS_THRESHOLD="$OPTARG"
    4.34 +        ;;
    4.35        T)
    4.36          check_number "$OPTARG"
    4.37          TRACETHREADS="$OPTARG"
    4.38 @@ -235,7 +241,7 @@
    4.39    LOG="$LOGDIR/$ITEM"
    4.40  
    4.41    "$ISABELLE_PROCESS" \
    4.42 -    -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;" \
    4.43 +    -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;" \
    4.44      -q -w $LOGIC $NAME > "$LOG"
    4.45    RC="$?"
    4.46  else
    4.47 @@ -244,7 +250,7 @@
    4.48    LOG="$LOGDIR/$ITEM"
    4.49  
    4.50    "$ISABELLE_PROCESS" \
    4.51 -    -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();" \
    4.52 +    -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();" \
    4.53      -r -q "$LOGIC" > "$LOG"
    4.54    RC="$?"
    4.55    cd ..
     5.1 --- a/src/Pure/Isar/toplevel.ML	Fri Feb 04 16:33:12 2011 +0100
     5.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Feb 04 17:11:00 2011 +0100
     5.3 @@ -663,8 +663,7 @@
     5.4  
     5.5          val future_proof = Proof.global_future_proof
     5.6            (fn prf =>
     5.7 -            singleton
     5.8 -              (Future.forks {name = "Toplevel.proof_result", group = NONE, deps = [], pri = ~1})
     5.9 +            Goal.fork_name "Toplevel.future_proof"
    5.10                (fn () =>
    5.11                  let val (states, result_state) =
    5.12                    (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
     6.1 --- a/src/Pure/System/session.ML	Fri Feb 04 16:33:12 2011 +0100
     6.2 +++ b/src/Pure/System/session.ML	Fri Feb 04 17:11:00 2011 +0100
     6.3 @@ -11,7 +11,7 @@
     6.4    val welcome: unit -> string
     6.5    val use_dir: string -> string -> bool -> string list -> bool -> bool ->
     6.6      string -> bool -> string list -> string -> string -> bool * string ->
     6.7 -    string -> int -> bool -> bool -> int -> int -> int -> unit
     6.8 +    string -> int -> bool -> bool -> int -> int -> int -> int -> unit
     6.9    val finish: unit -> unit
    6.10  end;
    6.11  
    6.12 @@ -93,7 +93,8 @@
    6.13    | dumping (cp, path) = SOME (cp, Path.explode path);
    6.14  
    6.15  fun use_dir item root build modes reset info doc doc_graph doc_versions parent
    6.16 -    name dump rpath level timing verbose max_threads trace_threads parallel_proofs =
    6.17 +    name dump rpath level timing verbose max_threads trace_threads
    6.18 +    parallel_proofs parallel_proofs_threshold =
    6.19    ((fn () =>
    6.20       (init reset parent name;
    6.21        Present.init build info doc doc_graph doc_versions (path ()) name
    6.22 @@ -113,6 +114,7 @@
    6.23      |> Unsynchronized.setmp Proofterm.proofs level
    6.24      |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
    6.25      |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs
    6.26 +    |> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold
    6.27      |> Unsynchronized.setmp Multithreading.trace trace_threads
    6.28      |> Unsynchronized.setmp Multithreading.max_threads
    6.29        (if Multithreading.available then max_threads
     7.1 --- a/src/Pure/goal.ML	Fri Feb 04 16:33:12 2011 +0100
     7.2 +++ b/src/Pure/goal.ML	Fri Feb 04 17:11:00 2011 +0100
     7.3 @@ -7,6 +7,7 @@
     7.4  signature BASIC_GOAL =
     7.5  sig
     7.6    val parallel_proofs: int Unsynchronized.ref
     7.7 +  val parallel_proofs_threshold: int Unsynchronized.ref
     7.8    val SELECT_GOAL: tactic -> int -> tactic
     7.9    val CONJUNCTS: tactic -> int -> tactic
    7.10    val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
    7.11 @@ -105,21 +106,47 @@
    7.12    #> Drule.zero_var_indexes;
    7.13  
    7.14  
    7.15 -(* parallel proofs *)
    7.16 +(* forked proofs *)
    7.17 +
    7.18 +val forked_proofs = Synchronized.var "forked_proofs" 0;
    7.19 +
    7.20 +fun forked i =
    7.21 +  Synchronized.change forked_proofs (fn m =>
    7.22 +    let
    7.23 +      val n = m + i;
    7.24 +      val _ =
    7.25 +        Multithreading.tracing 1 (fn () =>
    7.26 +          ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
    7.27 +    in n end);
    7.28  
    7.29  fun fork_name name e =
    7.30 -  singleton (Future.forks {name = name, group = NONE, deps = [], pri = ~1})
    7.31 -    (fn () => Future.status e);
    7.32 +  uninterruptible (fn _ => fn () =>
    7.33 +    let
    7.34 +      val _ = forked 1;
    7.35 +      val future =
    7.36 +        singleton (Future.forks {name = name, group = NONE, deps = [], pri = ~1})
    7.37 +          (fn () =>
    7.38 +            (*interruptible*)
    7.39 +            Exn.release
    7.40 +              (Exn.capture Future.status e before forked ~1
    7.41 +                handle exn => (forked ~1; reraise exn)));
    7.42 +    in future end) ();
    7.43  
    7.44  fun fork e = fork_name "Goal.fork" e;
    7.45  
    7.46  
    7.47 +(* scheduling parameters *)
    7.48 +
    7.49  val parallel_proofs = Unsynchronized.ref 1;
    7.50 +val parallel_proofs_threshold = Unsynchronized.ref 100;
    7.51  
    7.52  fun future_enabled () =
    7.53 -  Multithreading.enabled () andalso is_some (Future.worker_task ()) andalso ! parallel_proofs >= 1;
    7.54 +  Multithreading.enabled () andalso ! parallel_proofs >= 1 andalso
    7.55 +  is_some (Future.worker_task ());
    7.56  
    7.57 -fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
    7.58 +fun local_future_enabled () =
    7.59 +  future_enabled () andalso ! parallel_proofs >= 2 andalso
    7.60 +  Synchronized.value forked_proofs < ! parallel_proofs_threshold;
    7.61  
    7.62  
    7.63  (* future_result *)