# HG changeset patch # User wenzelm # Date 1296836712 -3600 # Node ID a10f0a1cae417e2af1c429e0582c5558288b5628 # Parent a207a858d1f68c44e076a1c6084a85b69011bfe7# Parent d27950860514a2660e6970c7125a76cf33952c66 merged diff -r a207a858d1f6 -r a10f0a1cae41 NEWS --- a/NEWS Fri Feb 04 14:16:55 2011 +0100 +++ b/NEWS Fri Feb 04 17:25:12 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 a207a858d1f6 -r a10f0a1cae41 doc-src/System/Thy/Presentation.thy --- a/doc-src/System/Thy/Presentation.thy Fri Feb 04 14:16:55 2011 +0100 +++ b/doc-src/System/Thy/Presentation.thy Fri Feb 04 17:25:12 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 a207a858d1f6 -r a10f0a1cae41 doc-src/System/Thy/document/Presentation.tex --- a/doc-src/System/Thy/document/Presentation.tex Fri Feb 04 14:16:55 2011 +0100 +++ b/doc-src/System/Thy/document/Presentation.tex Fri Feb 04 17:25:12 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 a207a858d1f6 -r a10f0a1cae41 lib/Tools/usedir --- a/lib/Tools/usedir Fri Feb 04 14:16:55 2011 +0100 +++ b/lib/Tools/usedir Fri Feb 04 17:25:12 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 a207a858d1f6 -r a10f0a1cae41 src/HOL/List.thy --- a/src/HOL/List.thy Fri Feb 04 14:16:55 2011 +0100 +++ b/src/HOL/List.thy Fri Feb 04 17:25:12 2011 +0100 @@ -456,7 +456,9 @@ "xs \ x # xs" by (induct xs) auto -lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric] +lemma not_Cons_self2 [simp]: + "x # xs \ xs" +by (rule not_Cons_self [symmetric]) lemma neq_Nil_conv: "(xs \ []) = (\y ys. xs = y # ys)" by (induct xs) auto diff -r a207a858d1f6 -r a10f0a1cae41 src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Fri Feb 04 14:16:55 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Fri Feb 04 17:25:12 2011 +0100 @@ -214,7 +214,7 @@ end; fun add_dt_realizers config names thy = - if ! Proofterm.proofs < 2 then thy + if not (Proofterm.proofs_enabled ()) then thy else let val _ = Datatype_Aux.message config "Adding realizers for induction and case analysis ..."; diff -r a207a858d1f6 -r a10f0a1cae41 src/Pure/Concurrent/lazy.ML --- a/src/Pure/Concurrent/lazy.ML Fri Feb 04 14:16:55 2011 +0100 +++ b/src/Pure/Concurrent/lazy.ML Fri Feb 04 17:25:12 2011 +0100 @@ -43,7 +43,7 @@ (case peek (Lazy var) of SOME res => res | NONE => - uninterruptible (fn restore_interrupts => fn () => + uninterruptible (fn restore_attributes => fn () => let val (expr, x) = Synchronized.change_result var @@ -55,7 +55,7 @@ (case expr of SOME e => let - val res0 = restore_interrupts (fn () => Exn.capture e ()) (); + val res0 = Exn.capture (restore_attributes e) (); val _ = Future.fulfill_result x res0; val res = Future.join_result x; (*semantic race: some other threads might see the same @@ -65,7 +65,7 @@ Synchronized.change var (fn _ => Expr e) else (); in res end - | NONE => restore_interrupts (fn () => Future.join_result x) ()) + | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ()) end) ()); fun force r = Exn.release (force_result r); diff -r a207a858d1f6 -r a10f0a1cae41 src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Fri Feb 04 14:16:55 2011 +0100 +++ b/src/Pure/Concurrent/task_queue.ML Fri Feb 04 17:25:12 2011 +0100 @@ -120,12 +120,13 @@ fun timing_of_task (Task {timing, ...}) = Synchronized.value timing; fun update_timing update (Task {timing, ...}) e = - let - val start = Time.now (); - val result = Exn.capture e (); - val t = Time.- (Time.now (), start); - val _ = Synchronized.change timing (update t); - in Exn.release result end; + uninterruptible (fn restore_attributes => fn () => + let + val start = Time.now (); + val result = Exn.capture (restore_attributes e) (); + val t = Time.- (Time.now (), start); + val _ = Synchronized.change timing (update t); + in Exn.release result end) (); fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) = prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2)); @@ -147,7 +148,9 @@ fun waiting task deps = update_timing (fn t => fn (a, b, ds) => - (Time.- (a, t), Time.+ (b, t), fold (insert (op =) o name_of_task) deps ds)) task; + (Time.- (a, t), Time.+ (b, t), + if ! Multithreading.trace > 0 + then fold (insert (op =) o name_of_task) deps ds else ds)) task; diff -r a207a858d1f6 -r a10f0a1cae41 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Fri Feb 04 14:16:55 2011 +0100 +++ b/src/Pure/Isar/toplevel.ML Fri Feb 04 17:25:12 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 a207a858d1f6 -r a10f0a1cae41 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Fri Feb 04 14:16:55 2011 +0100 +++ b/src/Pure/ProofGeneral/preferences.ML Fri Feb 04 17:25:12 2011 +0100 @@ -84,7 +84,7 @@ val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () => let - fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2); + fun get () = PgipTypes.bool_to_pgstring (Proofterm.proofs_enabled ()); fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1); in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) (); diff -r a207a858d1f6 -r a10f0a1cae41 src/Pure/System/session.ML --- a/src/Pure/System/session.ML Fri Feb 04 14:16:55 2011 +0100 +++ b/src/Pure/System/session.ML Fri Feb 04 17:25:12 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 a207a858d1f6 -r a10f0a1cae41 src/Pure/goal.ML --- a/src/Pure/goal.ML Fri Feb 04 14:16:55 2011 +0100 +++ b/src/Pure/goal.ML Fri Feb 04 17:25:12 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 *) diff -r a207a858d1f6 -r a10f0a1cae41 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Fri Feb 04 14:16:55 2011 +0100 +++ b/src/Pure/proofterm.ML Fri Feb 04 17:25:12 2011 +0100 @@ -52,6 +52,7 @@ val approximate_proof_body: proof -> proof_body (** primitive operations **) + val proofs_enabled: unit -> bool val proof_combt: proof * term list -> proof val proof_combt': proof * term option list -> proof val proof_combP: proof * proof list -> proof @@ -973,6 +974,7 @@ (***** axioms and theorems *****) val proofs = Unsynchronized.ref 2; +fun proofs_enabled () = ! proofs >= 2; fun vars_of t = map Var (rev (Term.add_vars t [])); fun frees_of t = map Free (rev (Term.add_frees t [])); @@ -1444,7 +1446,7 @@ fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0}; val body0 = - if ! proofs <> 2 then Future.value (make_body0 MinProof) + if not (proofs_enabled ()) then Future.value (make_body0 MinProof) else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ())) else singleton @@ -1453,6 +1455,7 @@ fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0); val (i, body') = + (*non-deterministic, depends on unknown promises*) (case strip_combt (fst (strip_combP prf)) of (PThm (i, ((old_name, prop', NONE), body')), args') => if (old_name = "" orelse old_name = name) andalso prop1 = prop' andalso args = args' diff -r a207a858d1f6 -r a10f0a1cae41 src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Feb 04 14:16:55 2011 +0100 +++ b/src/Pure/thm.ML Fri Feb 04 17:25:12 2011 +0100 @@ -576,6 +576,7 @@ (* closed derivations with official name *) +(*non-deterministic, depends on unknown promises*) fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = Proofterm.get_name shyps hyps prop (Proofterm.proof_of body); @@ -585,7 +586,7 @@ val {thy_ref, shyps, hyps, prop, tpairs, ...} = args; val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]); - val ps = map (apsnd (Future.map proof_body_of)) promises; + val ps = map (apsnd (Future.map fulfill_body)) promises; val thy = Theory.deref thy_ref; val (pthm, proof) = Proofterm.thm_proof thy name shyps hyps prop ps body; val der' = make_deriv [] [] [pthm] proof; @@ -1226,7 +1227,7 @@ val tfrees = rev (Term.add_tfree_names prop []); val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); - val ps = map (apsnd (Future.map proof_body_of)) promises; + val ps = map (apsnd (Future.map fulfill_body)) promises; val thy = Theory.deref thy_ref; val (pthm as (_, (_, prop', _)), proof) = Proofterm.unconstrain_thm_proof thy shyps prop ps body;