# HG changeset patch # User wenzelm # Date 1229426033 -3600 # Node ID 8f2481aa363d886319fb925e35c40dd191f984d1 # Parent 5a79ec2fedfbf29fdee8746df926dc49c6b39895 removed old scheduler; diff -r 5a79ec2fedfb -r 8f2481aa363d src/Pure/Concurrent/ROOT.ML --- 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"; diff -r 5a79ec2fedfb -r 8f2481aa363d src/Pure/Concurrent/future.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 ()); diff -r 5a79ec2fedfb -r 8f2481aa363d src/Pure/Concurrent/schedule.ML --- 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; diff -r 5a79ec2fedfb -r 8f2481aa363d src/Pure/IsaMakefile --- 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 diff -r 5a79ec2fedfb -r 8f2481aa363d src/Pure/Thy/thy_info.ML --- 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;