1.1 --- a/src/Pure/Concurrent/ROOT.ML Tue Dec 16 00:19:47 2008 +0100
1.2 +++ b/src/Pure/Concurrent/ROOT.ML Tue Dec 16 12:13:53 2008 +0100
1.3 @@ -1,15 +1,12 @@
1.4 (* Title: Pure/Concurrent/ROOT.ML
1.5 - ID: $Id$
1.6 + Author: Makarius
1.7
1.8 Concurrency within the ML runtime.
1.9 *)
1.10
1.11 -val future_scheduler = ref true;
1.12 -
1.13 use "simple_thread.ML";
1.14 use "synchronized.ML";
1.15 use "mailbox.ML";
1.16 -use "schedule.ML";
1.17 use "task_queue.ML";
1.18 use "future.ML";
1.19 use "par_list.ML";
2.1 --- a/src/Pure/Concurrent/future.ML Tue Dec 16 00:19:47 2008 +0100
2.2 +++ b/src/Pure/Concurrent/future.ML Tue Dec 16 12:13:53 2008 +0100
2.3 @@ -57,7 +57,7 @@
2.4 (** future values **)
2.5
2.6 fun enabled () =
2.7 - ! future_scheduler andalso Multithreading.enabled () andalso
2.8 + Multithreading.enabled () andalso
2.9 not (Multithreading.self_critical ());
2.10
2.11
3.1 --- a/src/Pure/Concurrent/schedule.ML Tue Dec 16 00:19:47 2008 +0100
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,85 +0,0 @@
3.4 -(* Title: Pure/Concurrent/schedule.ML
3.5 - ID: $Id$
3.6 - Author: Makarius
3.7 -
3.8 -Scheduling -- multiple threads working on a queue of tasks.
3.9 -*)
3.10 -
3.11 -signature SCHEDULE =
3.12 -sig
3.13 - datatype 'a task =
3.14 - Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
3.15 - val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
3.16 -end;
3.17 -
3.18 -structure Schedule: SCHEDULE =
3.19 -struct
3.20 -
3.21 -datatype 'a task =
3.22 - Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
3.23 -
3.24 -fun schedule n next_task = uninterruptible (fn restore_attributes => fn tasks =>
3.25 - let
3.26 - (*synchronized execution*)
3.27 - val lock = Mutex.mutex ();
3.28 - fun SYNCHRONIZED e =
3.29 - let
3.30 - val _ = Mutex.lock lock;
3.31 - val res = Exn.capture e ();
3.32 - val _ = Mutex.unlock lock;
3.33 - in Exn.release res end;
3.34 -
3.35 - (*wakeup condition*)
3.36 - val wakeup = ConditionVar.conditionVar ();
3.37 - fun wakeup_all () = ConditionVar.broadcast wakeup;
3.38 - fun wait () = ConditionVar.wait (wakeup, lock);
3.39 - fun wait_timeout () =
3.40 - ConditionVar.waitUntil (wakeup, lock, Time.+ (Time.now (), Time.fromSeconds 1));
3.41 -
3.42 - (*queue of tasks*)
3.43 - val queue = ref tasks;
3.44 - val active = ref 0;
3.45 - fun trace_active () = Multithreading.tracing 1 (fn () =>
3.46 - "SCHEDULE: " ^ string_of_int (! active) ^ " active");
3.47 - fun dequeue () =
3.48 - (case change_result queue next_task of
3.49 - Wait =>
3.50 - (dec active; trace_active ();
3.51 - wait ();
3.52 - inc active; trace_active ();
3.53 - dequeue ())
3.54 - | next => next);
3.55 -
3.56 - (*pool of running threads*)
3.57 - val status = ref ([]: exn list);
3.58 - val running = ref ([]: Thread.thread list);
3.59 - fun start f = (inc active; change running (cons (SimpleThread.fork false f)));
3.60 - fun stop () = (dec active; change running (remove Thread.equal (Thread.self ())));
3.61 -
3.62 - (*worker thread*)
3.63 - fun worker () =
3.64 - (case SYNCHRONIZED dequeue of
3.65 - Task {body, cont, fail} =>
3.66 - (case Exn.capture (restore_attributes body) () of
3.67 - Exn.Result () =>
3.68 - (SYNCHRONIZED (fn () => (change queue cont; wakeup_all ())); worker ())
3.69 - | Exn.Exn exn =>
3.70 - SYNCHRONIZED (fn () =>
3.71 - (change status (cons exn); change queue fail; stop (); wakeup_all ())))
3.72 - | Terminate => SYNCHRONIZED (fn () => (stop (); wakeup_all ())));
3.73 -
3.74 - (*main control: fork and wait*)
3.75 - fun fork 0 = ()
3.76 - | fork k = (start worker; fork (k - 1));
3.77 - val _ = SYNCHRONIZED (fn () =>
3.78 - (fork (Int.max (n, 1));
3.79 - while not (null (! running)) do
3.80 - (trace_active ();
3.81 - if not (null (! status))
3.82 - then (List.app SimpleThread.interrupt (! running))
3.83 - else ();
3.84 - wait_timeout ())));
3.85 -
3.86 - in ! status end);
3.87 -
3.88 -end;
4.1 --- a/src/Pure/IsaMakefile Tue Dec 16 00:19:47 2008 +0100
4.2 +++ b/src/Pure/IsaMakefile Tue Dec 16 12:13:53 2008 +0100
4.3 @@ -23,26 +23,24 @@
4.4
4.5 $(OUT)/Pure: Concurrent/ROOT.ML Concurrent/future.ML \
4.6 Concurrent/mailbox.ML Concurrent/par_list.ML \
4.7 - Concurrent/par_list_dummy.ML Concurrent/schedule.ML \
4.8 - Concurrent/simple_thread.ML Concurrent/synchronized.ML \
4.9 - Concurrent/task_queue.ML General/ROOT.ML General/alist.ML \
4.10 - General/balanced_tree.ML General/basics.ML General/buffer.ML \
4.11 - General/file.ML General/graph.ML General/heap.ML General/integer.ML \
4.12 - General/lazy.ML General/markup.ML General/name_space.ML \
4.13 - General/ord_list.ML General/output.ML General/path.ML \
4.14 - General/position.ML General/pretty.ML General/print_mode.ML \
4.15 - General/properties.ML General/queue.ML General/scan.ML \
4.16 - General/secure.ML General/seq.ML General/source.ML General/stack.ML \
4.17 - General/symbol.ML General/symbol_pos.ML General/table.ML \
4.18 - General/url.ML General/xml.ML General/yxml.ML Isar/ROOT.ML \
4.19 - Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
4.20 - Isar/calculation.ML Isar/class.ML Isar/code.ML Isar/code_unit.ML \
4.21 - Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \
4.22 - Isar/expression.ML \
4.23 - Isar/find_theorems.ML Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML \
4.24 - Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \
4.25 - Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML \
4.26 - Isar/new_locale.ML \
4.27 + Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML \
4.28 + Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML \
4.29 + General/alist.ML General/balanced_tree.ML General/basics.ML \
4.30 + General/buffer.ML General/file.ML General/graph.ML General/heap.ML \
4.31 + General/integer.ML General/lazy.ML General/markup.ML \
4.32 + General/name_space.ML General/ord_list.ML General/output.ML \
4.33 + General/path.ML General/position.ML General/pretty.ML \
4.34 + General/print_mode.ML General/properties.ML General/queue.ML \
4.35 + General/scan.ML General/secure.ML General/seq.ML General/source.ML \
4.36 + General/stack.ML General/symbol.ML General/symbol_pos.ML \
4.37 + General/table.ML General/url.ML General/xml.ML General/yxml.ML \
4.38 + Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML \
4.39 + Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML Isar/code.ML \
4.40 + Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML \
4.41 + Isar/element.ML Isar/expression.ML Isar/find_theorems.ML \
4.42 + Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML \
4.43 + Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \
4.44 + Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/new_locale.ML \
4.45 Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
4.46 Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
4.47 Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
4.48 @@ -76,17 +74,16 @@
4.49 Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \
4.50 Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML \
4.51 Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \
4.52 - Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML \
4.53 - Tools/isabelle_process.ML Tools/named_thms.ML \
4.54 - Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML \
4.55 - conjunction.ML consts.ML context.ML context_position.ML conv.ML \
4.56 - defs.ML display.ML drule.ML envir.ML facts.ML goal.ML \
4.57 - interpretation.ML library.ML logic.ML meta_simplifier.ML more_thm.ML \
4.58 - morphism.ML name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML \
4.59 - proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML \
4.60 - simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML \
4.61 - term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML \
4.62 - variable.ML ../Tools/quickcheck.ML
4.63 + Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML \
4.64 + Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML \
4.65 + assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \
4.66 + consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \
4.67 + drule.ML envir.ML facts.ML goal.ML interpretation.ML library.ML \
4.68 + logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML \
4.69 + old_goals.ML pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML \
4.70 + pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML \
4.71 + tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML \
4.72 + type_infer.ML unify.ML variable.ML ../Tools/quickcheck.ML
4.73 @./mk
4.74
4.75
5.1 --- a/src/Pure/Thy/thy_info.ML Tue Dec 16 00:19:47 2008 +0100
5.2 +++ b/src/Pure/Thy/thy_info.ML Tue Dec 16 12:13:53 2008 +0100
5.3 @@ -315,7 +315,13 @@
5.4 datatype task = Task of (unit -> unit) | Finished | Running;
5.5 fun task_finished Finished = true | task_finished _ = false;
5.6
5.7 -fun future_schedule task_graph =
5.8 +local
5.9 +
5.10 +fun schedule_seq tasks =
5.11 + Graph.topological_order tasks
5.12 + |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () | _ => ()));
5.13 +
5.14 +fun schedule_futures task_graph =
5.15 let
5.16 val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
5.17 (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
5.18 @@ -339,45 +345,14 @@
5.19 val proof_results = PureThy.join_proofs (map_filter (try get_theory o #1) tasks);
5.20 in ignore (Exn.release_all (thy_results @ proof_results)) end;
5.21
5.22 -local
5.23 -
5.24 -fun max_task (name, (Task body, m)) NONE = SOME (name: string, (body, m))
5.25 - | max_task (name, (Task body, m)) (task' as SOME (name', (_, m'))) =
5.26 - if m > m' orelse m = m' andalso name < name' then SOME (name, (body, m)) else task'
5.27 - | max_task _ task' = task';
5.28 -
5.29 -fun next_task G =
5.30 - let
5.31 - val tasks = Graph.minimals G |> map (fn name =>
5.32 - (name, (Graph.get_node G name, length (Graph.imm_succs G name))));
5.33 - val finished = filter (task_finished o fst o snd) tasks;
5.34 - in
5.35 - if not (null finished) then next_task (Graph.del_nodes (map fst finished) G)
5.36 - else if null tasks then (Schedule.Terminate, G)
5.37 - else
5.38 - (case fold max_task tasks NONE of
5.39 - NONE => (Schedule.Wait, G)
5.40 - | SOME (name, (body, _)) =>
5.41 - (Schedule.Task {body = PrintMode.closure body,
5.42 - cont = Graph.del_nodes [name], fail = K Graph.empty},
5.43 - Graph.map_node name (K Running) G))
5.44 - end;
5.45 -
5.46 -fun schedule_seq tasks =
5.47 - Graph.topological_order tasks
5.48 - |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () | _ => ()));
5.49 -
5.50 in
5.51
5.52 fun schedule_tasks tasks n =
5.53 - let val m = Multithreading.max_threads_value () in
5.54 - if m <= 1 then schedule_seq tasks
5.55 - else if Multithreading.self_critical () then
5.56 + if not (Multithreading.enabled ()) then schedule_seq tasks
5.57 + else if Multithreading.self_critical () then
5.58 (warning (loader_msg "no multithreading within critical section" []);
5.59 schedule_seq tasks)
5.60 - else if Future.enabled () then future_schedule tasks
5.61 - else ignore (Exn.release_all (map Exn.Exn (Schedule.schedule (Int.min (m, n)) next_task tasks)))
5.62 - end;
5.63 + else schedule_futures tasks;
5.64
5.65 end;
5.66