--- 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
--- 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;