# HG changeset patch # User boehmes # Date 1257432279 -3600 # Node ID 6895b9cadc7cf10b5acb745c2b6bc3271354691e # Parent 153a27370a4214f2be6e9e0098c152327817798f# Parent f5d95787224fe0ca82dd4e00e9e6cbe3f024a188 merged diff -r 153a27370a42 -r 6895b9cadc7c src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Nov 05 15:24:49 2009 +0100 +++ b/src/HOL/IsaMakefile Thu Nov 05 15:44:39 2009 +0100 @@ -28,7 +28,7 @@ HOL-ex \ HOL-Auth \ HOL-Bali \ - HOL-Boogie_Examples \ + HOL-Boogie-Examples \ HOL-Decision_Procs \ HOL-Extraction \ HOL-Hahn_Banach \ @@ -56,7 +56,7 @@ HOL-Probability \ HOL-Prolog \ HOL-SET_Protocol \ - HOL-SMT_Examples \ + HOL-SMT-Examples \ HOL-SizeChange \ HOL-Statespace \ HOL-Subst \ @@ -581,16 +581,15 @@ HOL-Hoare_Parallel: HOL $(LOG)/HOL-Hoare_Parallel.gz $(LOG)/HOL-Hoare_Parallel.gz: $(OUT)/HOL Hoare_Parallel/Gar_Coll.thy \ - Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy \ - Hoare_Parallel/Mul_Gar_Coll.thy \ - Hoare_Parallel/OG_Com.thy Hoare_Parallel/OG_Examples.thy \ - Hoare_Parallel/OG_Hoare.thy Hoare_Parallel/OG_Syntax.thy \ - Hoare_Parallel/OG_Tactics.thy Hoare_Parallel/OG_Tran.thy \ - Hoare_Parallel/Quote_Antiquote.thy Hoare_Parallel/RG_Com.thy \ - Hoare_Parallel/RG_Examples.thy Hoare_Parallel/RG_Hoare.thy \ - Hoare_Parallel/RG_Syntax.thy Hoare_Parallel/RG_Tran.thy \ - Hoare_Parallel/ROOT.ML Hoare_Parallel/document/root.tex \ - Hoare_Parallel/document/root.bib + Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy \ + Hoare_Parallel/Mul_Gar_Coll.thy Hoare_Parallel/OG_Com.thy \ + Hoare_Parallel/OG_Examples.thy Hoare_Parallel/OG_Hoare.thy \ + Hoare_Parallel/OG_Syntax.thy Hoare_Parallel/OG_Tactics.thy \ + Hoare_Parallel/OG_Tran.thy Hoare_Parallel/Quote_Antiquote.thy \ + Hoare_Parallel/RG_Com.thy Hoare_Parallel/RG_Examples.thy \ + Hoare_Parallel/RG_Hoare.thy Hoare_Parallel/RG_Syntax.thy \ + Hoare_Parallel/RG_Tran.thy Hoare_Parallel/ROOT.ML \ + Hoare_Parallel/document/root.tex Hoare_Parallel/document/root.bib @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel @@ -610,20 +609,20 @@ HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz -$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \ - Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \ - Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Manual_Nits.thy \ - Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \ - Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \ - Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \ - Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \ - Nitpick_Examples/Typedef_Nits.thy +$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \ + Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \ + Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Manual_Nits.thy \ + Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \ + Nitpick_Examples/Nitpick_Examples.thy \ + Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \ + Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \ + Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples ## HOL-Algebra -HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz +HOL-Algebra: HOL $(OUT)/HOL-Algebra ALGEBRA_DEPENDENCIES = $(OUT)/HOL \ Algebra/ROOT.ML \ @@ -701,8 +700,8 @@ HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz $(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \ - UNITY/UNITY_Main.thy UNITY/UNITY_Examples.thy UNITY/UNITY_tactics.ML UNITY/Comp.thy \ - UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \ + UNITY/UNITY_Main.thy UNITY/UNITY_Examples.thy UNITY/UNITY_tactics.ML \ + UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \ UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy \ UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy \ UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \ @@ -942,7 +941,7 @@ HOL-ex: HOL $(LOG)/HOL-ex.gz -$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \ +$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \ Number_Theory/Primes.thy \ Tools/Predicate_Compile/predicate_compile_core.ML \ ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \ @@ -950,22 +949,21 @@ ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \ ex/CodegenSML_Test.thy ex/Codegenerator_Candidates.thy \ ex/Codegenerator_Pretty.thy ex/Codegenerator_Pretty_Test.thy \ - ex/Codegenerator_Test.thy ex/Coherent.thy \ - ex/Efficient_Nat_examples.thy \ - ex/Eval_Examples.thy ex/Fundefs.thy ex/Groebner_Examples.thy \ - ex/Guess.thy ex/HarmonicSeries.thy ex/Hebrew.thy \ - ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ + ex/Codegenerator_Test.thy ex/Coherent.thy \ + ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \ + ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ + ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ ex/Hilbert_Classical.thy ex/Induction_Scheme.thy \ ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \ ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \ ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \ ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy \ - ex/Predicate_Compile_ex.thy ex/Predicate_Compile_Quickcheck.thy \ + ex/Predicate_Compile_ex.thy ex/Predicate_Compile_Quickcheck.thy \ ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy \ ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \ ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \ - ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \ + ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \ ex/Unification.thy ex/document/root.bib ex/document/root.tex \ ex/set.thy ex/svc_funcs.ML ex/svc_test.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex @@ -1065,12 +1063,13 @@ HOL-Multivariate_Analysis: HOL $(OUT)/HOL-Multivariate_Analysis -$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL Multivariate_Analysis/ROOT.ML \ - Multivariate_Analysis/Multivariate_Analysis.thy \ - Multivariate_Analysis/Determinants.thy \ - Multivariate_Analysis/Finite_Cartesian_Product.thy \ - Multivariate_Analysis/Euclidean_Space.thy \ - Multivariate_Analysis/Topology_Euclidean_Space.thy \ +$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL \ + Multivariate_Analysis/ROOT.ML \ + Multivariate_Analysis/Multivariate_Analysis.thy \ + Multivariate_Analysis/Determinants.thy \ + Multivariate_Analysis/Finite_Cartesian_Product.thy \ + Multivariate_Analysis/Euclidean_Space.thy \ + Multivariate_Analysis/Topology_Euclidean_Space.thy \ Multivariate_Analysis/Convex_Euclidean_Space.thy @cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis @@ -1224,11 +1223,11 @@ @cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT -## HOL-SMT_Examples +## HOL-SMT-Examples -HOL-SMT_Examples: HOL-SMT $(LOG)/HOL-SMT_Examples.gz +HOL-SMT-Examples: HOL-SMT $(LOG)/HOL-SMT-Examples.gz -$(LOG)/HOL-SMT_Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML \ +$(LOG)/HOL-SMT-Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML \ SMT/Examples/SMT_Examples.thy SMT/Examples/cert/z3_arith_quant_01 \ SMT/Examples/cert/z3_arith_quant_01.proof \ SMT/Examples/cert/z3_arith_quant_02 \ @@ -1395,25 +1394,25 @@ HOL-Boogie: HOL-SMT $(OUT)/HOL-Boogie -$(OUT)/HOL-Boogie: $(OUT)/HOL-SMT Boogie/ROOT.ML Boogie/Boogie.thy \ - Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML \ +$(OUT)/HOL-Boogie: $(OUT)/HOL-SMT Boogie/ROOT.ML Boogie/Boogie.thy \ + Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML \ Boogie/Tools/boogie_commands.ML Boogie/Tools/boogie_split.ML @cd Boogie; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-SMT HOL-Boogie ## HOL-Boogie_Examples -HOL-Boogie_Examples: HOL-Boogie $(LOG)/HOL-Boogie_Examples.gz +HOL-Boogie-Examples: HOL-Boogie $(LOG)/HOL-Boogie-Examples.gz -$(LOG)/HOL-Boogie_Examples.gz: $(OUT)/HOL-SMT Boogie/Examples/ROOT.ML \ - Boogie/Examples/Boogie_Max.thy Boogie/Examples/Boogie_Max.b2i \ - Boogie/Examples/Boogie_Dijkstra.thy Boogie/Examples/VCC_Max.thy \ - Boogie/Examples/Boogie_Dijkstra.b2i Boogie/Examples/VCC_Max.b2i \ - Boogie/Examples/cert/Boogie_max \ - Boogie/Examples/cert/Boogie_max.proof \ - Boogie/Examples/cert/Boogie_Dijkstra \ - Boogie/Examples/cert/Boogie_Dijkstra.proof \ - Boogie/Examples/cert/VCC_maximum \ +$(LOG)/HOL-Boogie-Examples.gz: $(OUT)/HOL-Boogie \ + Boogie/Examples/ROOT.ML Boogie/Examples/Boogie_Max.thy \ + Boogie/Examples/Boogie_Max.b2i Boogie/Examples/Boogie_Dijkstra.thy \ + Boogie/Examples/VCC_Max.thy Boogie/Examples/Boogie_Dijkstra.b2i \ + Boogie/Examples/VCC_Max.b2i Boogie/Examples/cert/Boogie_max \ + Boogie/Examples/cert/Boogie_max.proof \ + Boogie/Examples/cert/Boogie_Dijkstra \ + Boogie/Examples/cert/Boogie_Dijkstra.proof \ + Boogie/Examples/cert/VCC_maximum \ Boogie/Examples/cert/VCC_maximum.proof @cd Boogie; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Boogie Examples @@ -1442,5 +1441,7 @@ $(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA \ $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz \ $(LOG)/HOL-Mirabelle.gz $(OUT)/HOL-SMT \ - $(LOG)/HOL-SMT.gz $(LOG)/HOL-SMT-Examples.gz + $(LOG)/HOL-SMT.gz $(LOG)/HOL-SMT-Examples.gz \ + $(OUT)/HOL-Boogie $(LOG)/HOL-Boogie.gz \ + $(LOG)/HOL-Boogie-Examples.gz diff -r 153a27370a42 -r 6895b9cadc7c src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Thu Nov 05 15:24:49 2009 +0100 +++ b/src/Pure/Concurrent/future.ML Thu Nov 05 15:44:39 2009 +0100 @@ -64,7 +64,7 @@ type group = Task_Queue.group; local - val tag = Universal.tag () : (string * task * group) option Universal.tag; + val tag = Universal.tag () : (task * group) option Universal.tag; in fun thread_data () = the_default NONE (Thread.getLocal tag); fun setmp_thread_data data f x = @@ -72,8 +72,8 @@ end; val is_worker = is_some o thread_data; -val worker_task = Option.map #2 o thread_data; -val worker_group = Option.map #3 o thread_data; +val worker_task = Option.map #1 o thread_data; +val worker_group = Option.map #2 o thread_data; (* datatype future *) @@ -99,17 +99,6 @@ (** scheduling **) -(* global state *) - -val queue = Unsynchronized.ref Task_Queue.empty; -val next = Unsynchronized.ref 0; -val workers = Unsynchronized.ref ([]: (Thread.thread * bool) list); -val scheduler = Unsynchronized.ref (NONE: Thread.thread option); -val excessive = Unsynchronized.ref 0; -val canceled = Unsynchronized.ref ([]: Task_Queue.group list); -val do_shutdown = Unsynchronized.ref false; - - (* synchronization *) val scheduler_event = ConditionVar.conditionVar (); @@ -141,6 +130,24 @@ end; +(* global state *) + +val queue = Unsynchronized.ref Task_Queue.empty; +val next = Unsynchronized.ref 0; +val scheduler = Unsynchronized.ref (NONE: Thread.thread option); +val canceled = Unsynchronized.ref ([]: Task_Queue.group list); +val do_shutdown = Unsynchronized.ref false; +val max_workers = Unsynchronized.ref 0; +val max_active = Unsynchronized.ref 0; +val worker_trend = Unsynchronized.ref 0; + +datatype worker_state = Working | Waiting | Sleeping; +val workers = Unsynchronized.ref ([]: (Thread.thread * worker_state Unsynchronized.ref) list); + +fun count_workers state = (*requires SYNCHRONIZED*) + fold (fn (_, state_ref) => fn i => if ! state_ref = state then i + 1 else i) (! workers) 0; + + (* execute future jobs *) fun future_job group (e: unit -> 'a) = @@ -165,10 +172,10 @@ (Unsynchronized.change canceled (insert Task_Queue.eq_group group); broadcast scheduler_event); -fun execute name (task, group, jobs) = +fun execute (task, group, jobs) = let val valid = not (Task_Queue.is_canceled group); - val ok = setmp_thread_data (name, task, group) (fn () => + val ok = setmp_thread_data (task, group) (fn () => fold (fn job => fn ok => job valid andalso ok) jobs true) (); val _ = SYNCHRONIZED "finish" (fn () => let @@ -178,99 +185,134 @@ else if Task_Queue.cancel (! queue) group then () else do_cancel group; val _ = broadcast work_finished; - val _ = if maximal then () else broadcast work_available; + val _ = if maximal then () else signal work_available; in () end); in () end; -(* worker activity *) - -fun count_active () = (*requires SYNCHRONIZED*) - fold (fn (_, active) => fn i => if active then i + 1 else i) (! workers) 0; - -fun change_active active = (*requires SYNCHRONIZED*) - Unsynchronized.change workers - (AList.update Thread.equal (Thread.self (), active)); - - (* worker threads *) -fun worker_wait cond = (*requires SYNCHRONIZED*) - (change_active false; wait cond; change_active true); +fun worker_wait active cond = (*requires SYNCHRONIZED*) + let + val state = + (case AList.lookup Thread.equal (! workers) (Thread.self ()) of + SOME state => state + | NONE => raise Fail "Unregistered worker thread"); + val _ = state := (if active then Waiting else Sleeping); + val _ = wait cond; + val _ = state := Working; + in () end; fun worker_next () = (*requires SYNCHRONIZED*) - if ! excessive > 0 then - (Unsynchronized.dec excessive; - Unsynchronized.change workers - (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ()))); - broadcast scheduler_event; + if length (! workers) > ! max_workers then + (Unsynchronized.change workers (AList.delete Thread.equal (Thread.self ())); + signal work_available; NONE) - else if count_active () > Multithreading.max_threads_value () then - (worker_wait scheduler_event; worker_next ()) + else if count_workers Working > ! max_active then + (worker_wait false work_available; worker_next ()) else (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ())) of - NONE => (worker_wait work_available; worker_next ()) - | some => some); + NONE => (worker_wait false work_available; worker_next ()) + | some => (signal work_available; some)); fun worker_loop name = (case SYNCHRONIZED name (fn () => worker_next ()) of NONE => () - | SOME work => (execute name work; worker_loop name)); + | SOME work => (execute work; worker_loop name)); fun worker_start name = (*requires SYNCHRONIZED*) - Unsynchronized.change workers (cons (SimpleThread.fork false (fn () => - (broadcast scheduler_event; worker_loop name)), true)); + Unsynchronized.change workers (cons (SimpleThread.fork false (fn () => worker_loop name), + Unsynchronized.ref Working)); (* scheduler *) -val last_status = Unsynchronized.ref Time.zeroTime; -val next_status = Time.fromMilliseconds 500; +val status_ticks = Unsynchronized.ref 0; + +val last_round = Unsynchronized.ref Time.zeroTime; val next_round = Time.fromMilliseconds 50; fun scheduler_next () = (*requires SYNCHRONIZED*) let - (*queue and worker status*) + val now = Time.now (); + val tick = Time.<= (Time.+ (! last_round, next_round), now); + val _ = if tick then last_round := now else (); + + + (* queue and worker status *) + + val _ = + if tick then Unsynchronized.change status_ticks (fn i => (i + 1) mod 10) else (); val _ = - let val now = Time.now () in - if Time.> (Time.+ (! last_status, next_status), now) then () - else - (last_status := now; Multithreading.tracing 1 (fn () => - let - val {ready, pending, running} = Task_Queue.status (! queue); - val total = length (! workers); - val active = count_active (); - in - "SCHEDULE " ^ Time.toString now ^ ": " ^ - string_of_int ready ^ " ready, " ^ - string_of_int pending ^ " pending, " ^ - string_of_int running ^ " running; " ^ - string_of_int total ^ " workers, " ^ - string_of_int active ^ " active" - end)) - end; + if tick andalso ! status_ticks = 0 then + Multithreading.tracing 1 (fn () => + let + val {ready, pending, running} = Task_Queue.status (! queue); + val total = length (! workers); + val active = count_workers Working; + val waiting = count_workers Waiting; + in + "SCHEDULE " ^ Time.toString now ^ ": " ^ + string_of_int ready ^ " ready, " ^ + string_of_int pending ^ " pending, " ^ + string_of_int running ^ " running; " ^ + string_of_int total ^ " workers, " ^ + string_of_int active ^ " active, " ^ + string_of_int waiting ^ " waiting " + end) + else (); - (*worker threads*) val _ = if forall (Thread.isActive o #1) (! workers) then () else - (case List.partition (Thread.isActive o #1) (! workers) of - (_, []) => () - | (alive, dead) => - (workers := alive; Multithreading.tracing 0 (fn () => - "SCHEDULE: disposed " ^ string_of_int (length dead) ^ " dead worker threads"))); + let + val (alive, dead) = List.partition (Thread.isActive o #1) (! workers); + val _ = workers := alive; + in + Multithreading.tracing 0 (fn () => + "SCHEDULE: disposed " ^ string_of_int (length dead) ^ " dead worker threads") + end; + + + (* worker pool adjustments *) + + val max_active0 = ! max_active; + val max_workers0 = ! max_workers; val m = if ! do_shutdown then 0 else Multithreading.max_threads_value (); - val mm = if m = 9999 then 1 else m * 2; - val l = length (! workers); - val _ = excessive := l - mm; + val _ = max_active := m; + + val mm = + if ! do_shutdown then 0 + else if m = 9999 then 1 + else Int.min (Int.max (count_workers Working + 2 * count_workers Waiting, m), 4 * m); val _ = - if mm > l then - funpow (mm - l) (fn () => - worker_start ("worker " ^ string_of_int (Unsynchronized.inc next))) () + if tick andalso mm > ! max_workers then + Unsynchronized.change worker_trend (fn w => if w < 0 then 0 else w + 1) + else if tick andalso mm < ! max_workers then + Unsynchronized.change worker_trend (fn w => if w > 0 then 0 else w - 1) + else (); + val _ = + if mm = 0 orelse ! worker_trend > 50 orelse ! worker_trend < ~50 then + max_workers := mm + else if ! worker_trend > 5 andalso ! max_workers < 2 * m then + max_workers := Int.min (mm, 2 * m) else (); - (*canceled groups*) + val missing = ! max_workers - length (! workers); + val _ = + if missing > 0 then + funpow missing (fn () => + ignore (worker_start ("worker " ^ string_of_int (Unsynchronized.inc next)))) () + else (); + + val _ = + if ! max_active = max_active0 andalso ! max_workers = max_workers0 then () + else signal work_available; + + + (* canceled groups *) + val _ = if null (! canceled) then () else @@ -279,24 +321,30 @@ Unsynchronized.change canceled (filter_out (Task_Queue.cancel (! queue))); broadcast_work ()); - (*delay loop*) + + (* delay loop *) + val _ = Exn.release (wait_timeout next_round scheduler_event); - (*shutdown*) + + (* shutdown *) + val _ = if Task_Queue.is_empty (! queue) then do_shutdown := true else (); val continue = not (! do_shutdown andalso null (! workers)); val _ = if continue then () else scheduler := NONE; + val _ = broadcast scheduler_event; in continue end handle Exn.Interrupt => (Multithreading.tracing 1 (fn () => "Interrupt"); - uninterruptible (fn _ => fn () => List.app do_cancel (Task_Queue.cancel_all (! queue))) (); - scheduler_next ()); + List.app do_cancel (Task_Queue.cancel_all (! queue)); true); fun scheduler_loop () = - Multithreading.with_attributes - (Multithreading.sync_interrupts Multithreading.public_interrupts) - (fn _ => while SYNCHRONIZED "scheduler" (fn () => scheduler_next ()) do ()); + while + Multithreading.with_attributes + (Multithreading.sync_interrupts Multithreading.public_interrupts) + (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ())) + do (); fun scheduler_active () = (*requires SYNCHRONIZED*) (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread); @@ -346,7 +394,7 @@ Exn.Exn (Exn.EXCEPTIONS (Exn.flatten_list (Task_Queue.group_status (group_of x)))) | SOME res => res); -fun join_wait x = +fun passive_wait x = Synchronized.readonly_access (result_of x) (fn NONE => NONE | SOME _ => SOME ()); fun join_next deps = (*requires SYNCHRONIZED*) @@ -354,11 +402,11 @@ else (case Unsynchronized.change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of (NONE, []) => NONE - | (NONE, deps') => (worker_wait work_finished; join_next deps') + | (NONE, deps') => (worker_wait true work_finished; join_next deps') | (SOME work, deps') => SOME (work, deps')); fun execute_work NONE = () - | execute_work (SOME (work, deps')) = (execute "join" work; join_work deps') + | execute_work (SOME (work, deps')) = (execute work; join_work deps') and join_work deps = execute_work (SYNCHRONIZED "join" (fn () => join_next deps)); @@ -375,7 +423,7 @@ else (case worker_task () of SOME task => join_depend task (map task_of xs) - | NONE => List.app join_wait xs; + | NONE => List.app passive_wait xs; map get_result xs); end; diff -r 153a27370a42 -r 6895b9cadc7c src/Pure/proofterm.ML