--- a/src/Pure/Concurrent/ROOT.ML Tue Dec 16 00:19:47 2008 +0100
+++ b/src/Pure/Concurrent/ROOT.ML Tue Dec 16 12:13:53 2008 +0100
@@ -1,15 +1,12 @@
(* Title: Pure/Concurrent/ROOT.ML
- ID: $Id$
+ Author: Makarius
Concurrency within the ML runtime.
*)
-val future_scheduler = ref true;
-
use "simple_thread.ML";
use "synchronized.ML";
use "mailbox.ML";
-use "schedule.ML";
use "task_queue.ML";
use "future.ML";
use "par_list.ML";
--- a/src/Pure/Concurrent/future.ML Tue Dec 16 00:19:47 2008 +0100
+++ b/src/Pure/Concurrent/future.ML Tue Dec 16 12:13:53 2008 +0100
@@ -57,7 +57,7 @@
(** future values **)
fun enabled () =
- ! future_scheduler andalso Multithreading.enabled () andalso
+ Multithreading.enabled () andalso
not (Multithreading.self_critical ());
--- a/src/Pure/Concurrent/schedule.ML Tue Dec 16 00:19:47 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-(* Title: Pure/Concurrent/schedule.ML
- ID: $Id$
- Author: Makarius
-
-Scheduling -- multiple threads working on a queue of tasks.
-*)
-
-signature SCHEDULE =
-sig
- datatype 'a task =
- Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
- val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
-end;
-
-structure Schedule: SCHEDULE =
-struct
-
-datatype 'a task =
- Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
-
-fun schedule n next_task = uninterruptible (fn restore_attributes => fn tasks =>
- let
- (*synchronized execution*)
- val lock = Mutex.mutex ();
- fun SYNCHRONIZED e =
- let
- val _ = Mutex.lock lock;
- val res = Exn.capture e ();
- val _ = Mutex.unlock lock;
- in Exn.release res end;
-
- (*wakeup condition*)
- val wakeup = ConditionVar.conditionVar ();
- fun wakeup_all () = ConditionVar.broadcast wakeup;
- fun wait () = ConditionVar.wait (wakeup, lock);
- fun wait_timeout () =
- ConditionVar.waitUntil (wakeup, lock, Time.+ (Time.now (), Time.fromSeconds 1));
-
- (*queue of tasks*)
- val queue = ref tasks;
- val active = ref 0;
- fun trace_active () = Multithreading.tracing 1 (fn () =>
- "SCHEDULE: " ^ string_of_int (! active) ^ " active");
- fun dequeue () =
- (case change_result queue next_task of
- Wait =>
- (dec active; trace_active ();
- wait ();
- inc active; trace_active ();
- dequeue ())
- | next => next);
-
- (*pool of running threads*)
- val status = ref ([]: exn list);
- val running = ref ([]: Thread.thread list);
- fun start f = (inc active; change running (cons (SimpleThread.fork false f)));
- fun stop () = (dec active; change running (remove Thread.equal (Thread.self ())));
-
- (*worker thread*)
- fun worker () =
- (case SYNCHRONIZED dequeue of
- Task {body, cont, fail} =>
- (case Exn.capture (restore_attributes body) () of
- Exn.Result () =>
- (SYNCHRONIZED (fn () => (change queue cont; wakeup_all ())); worker ())
- | Exn.Exn exn =>
- SYNCHRONIZED (fn () =>
- (change status (cons exn); change queue fail; stop (); wakeup_all ())))
- | Terminate => SYNCHRONIZED (fn () => (stop (); wakeup_all ())));
-
- (*main control: fork and wait*)
- fun fork 0 = ()
- | fork k = (start worker; fork (k - 1));
- val _ = SYNCHRONIZED (fn () =>
- (fork (Int.max (n, 1));
- while not (null (! running)) do
- (trace_active ();
- if not (null (! status))
- then (List.app SimpleThread.interrupt (! running))
- else ();
- wait_timeout ())));
-
- in ! status end);
-
-end;
--- a/src/Pure/IsaMakefile Tue Dec 16 00:19:47 2008 +0100
+++ b/src/Pure/IsaMakefile Tue Dec 16 12:13:53 2008 +0100
@@ -23,26 +23,24 @@
$(OUT)/Pure: Concurrent/ROOT.ML Concurrent/future.ML \
Concurrent/mailbox.ML Concurrent/par_list.ML \
- Concurrent/par_list_dummy.ML Concurrent/schedule.ML \
- Concurrent/simple_thread.ML Concurrent/synchronized.ML \
- Concurrent/task_queue.ML General/ROOT.ML General/alist.ML \
- General/balanced_tree.ML General/basics.ML General/buffer.ML \
- General/file.ML General/graph.ML General/heap.ML General/integer.ML \
- General/lazy.ML General/markup.ML General/name_space.ML \
- General/ord_list.ML General/output.ML General/path.ML \
- General/position.ML General/pretty.ML General/print_mode.ML \
- General/properties.ML General/queue.ML General/scan.ML \
- General/secure.ML General/seq.ML General/source.ML General/stack.ML \
- General/symbol.ML General/symbol_pos.ML General/table.ML \
- General/url.ML General/xml.ML General/yxml.ML Isar/ROOT.ML \
- Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
- Isar/calculation.ML Isar/class.ML Isar/code.ML Isar/code_unit.ML \
- Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \
- Isar/expression.ML \
- Isar/find_theorems.ML Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML \
- Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \
- Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML \
- Isar/new_locale.ML \
+ Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML \
+ Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML \
+ General/alist.ML General/balanced_tree.ML General/basics.ML \
+ General/buffer.ML General/file.ML General/graph.ML General/heap.ML \
+ General/integer.ML General/lazy.ML General/markup.ML \
+ General/name_space.ML General/ord_list.ML General/output.ML \
+ General/path.ML General/position.ML General/pretty.ML \
+ General/print_mode.ML General/properties.ML General/queue.ML \
+ General/scan.ML General/secure.ML General/seq.ML General/source.ML \
+ General/stack.ML General/symbol.ML General/symbol_pos.ML \
+ General/table.ML General/url.ML General/xml.ML General/yxml.ML \
+ Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML \
+ Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML Isar/code.ML \
+ Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML \
+ Isar/element.ML Isar/expression.ML Isar/find_theorems.ML \
+ Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML \
+ Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \
+ Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/new_locale.ML \
Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
@@ -76,17 +74,16 @@
Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \
Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML \
Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \
- Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML \
- Tools/isabelle_process.ML Tools/named_thms.ML \
- Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML \
- conjunction.ML consts.ML context.ML context_position.ML conv.ML \
- defs.ML display.ML drule.ML envir.ML facts.ML goal.ML \
- interpretation.ML library.ML logic.ML meta_simplifier.ML more_thm.ML \
- morphism.ML name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML \
- proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML \
- simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML \
- term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML \
- variable.ML ../Tools/quickcheck.ML
+ Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML \
+ Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML \
+ assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \
+ consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \
+ drule.ML envir.ML facts.ML goal.ML interpretation.ML library.ML \
+ logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML \
+ old_goals.ML pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML \
+ pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML \
+ tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML \
+ type_infer.ML unify.ML variable.ML ../Tools/quickcheck.ML
@./mk
--- a/src/Pure/Thy/thy_info.ML Tue Dec 16 00:19:47 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML Tue Dec 16 12:13:53 2008 +0100
@@ -315,7 +315,13 @@
datatype task = Task of (unit -> unit) | Finished | Running;
fun task_finished Finished = true | task_finished _ = false;
-fun future_schedule task_graph =
+local
+
+fun schedule_seq tasks =
+ Graph.topological_order tasks
+ |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () | _ => ()));
+
+fun schedule_futures task_graph =
let
val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
(case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
@@ -339,45 +345,14 @@
val proof_results = PureThy.join_proofs (map_filter (try get_theory o #1) tasks);
in ignore (Exn.release_all (thy_results @ proof_results)) end;
-local
-
-fun max_task (name, (Task body, m)) NONE = SOME (name: string, (body, m))
- | max_task (name, (Task body, m)) (task' as SOME (name', (_, m'))) =
- if m > m' orelse m = m' andalso name < name' then SOME (name, (body, m)) else task'
- | max_task _ task' = task';
-
-fun next_task G =
- let
- val tasks = Graph.minimals G |> map (fn name =>
- (name, (Graph.get_node G name, length (Graph.imm_succs G name))));
- val finished = filter (task_finished o fst o snd) tasks;
- in
- if not (null finished) then next_task (Graph.del_nodes (map fst finished) G)
- else if null tasks then (Schedule.Terminate, G)
- else
- (case fold max_task tasks NONE of
- NONE => (Schedule.Wait, G)
- | SOME (name, (body, _)) =>
- (Schedule.Task {body = PrintMode.closure body,
- cont = Graph.del_nodes [name], fail = K Graph.empty},
- Graph.map_node name (K Running) G))
- end;
-
-fun schedule_seq tasks =
- Graph.topological_order tasks
- |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () | _ => ()));
-
in
fun schedule_tasks tasks n =
- let val m = Multithreading.max_threads_value () in
- if m <= 1 then schedule_seq tasks
- else if Multithreading.self_critical () then
+ if not (Multithreading.enabled ()) then schedule_seq tasks
+ else if Multithreading.self_critical () then
(warning (loader_msg "no multithreading within critical section" []);
schedule_seq tasks)
- else if Future.enabled () then future_schedule tasks
- else ignore (Exn.release_all (map Exn.Exn (Schedule.schedule (Int.min (m, n)) next_task tasks)))
- end;
+ else schedule_futures tasks;
end;