author | wenzelm |
Thu, 09 Oct 2008 21:06:08 +0200 | |
changeset 28556 | 85d2972fe9e6 |
parent 28543 | 637f2808ab64 |
permissions | -rw-r--r-- |
28121
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Concurrent/schedule.ML |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
28140 | 3 |
Author: Makarius |
28121
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
4 |
|
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
5 |
Scheduling -- multiple threads working on a queue of tasks. |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
6 |
*) |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
7 |
|
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
8 |
signature SCHEDULE = |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
9 |
sig |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
10 |
datatype 'a task = |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
11 |
Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate; |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
12 |
val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
13 |
end; |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
14 |
|
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
15 |
structure Schedule: SCHEDULE = |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
16 |
struct |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
17 |
|
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
18 |
datatype 'a task = |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
19 |
Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate; |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
20 |
|
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
21 |
fun schedule n next_task = uninterruptible (fn restore_attributes => fn tasks => |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
22 |
let |
28148 | 23 |
(*synchronized execution*) |
28121
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
24 |
val lock = Mutex.mutex (); |
28148 | 25 |
fun SYNCHRONIZED e = |
28121
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
26 |
let |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
27 |
val _ = Mutex.lock lock; |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
28 |
val res = Exn.capture e (); |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
29 |
val _ = Mutex.unlock lock; |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
30 |
in Exn.release res end; |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
31 |
|
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
32 |
(*wakeup condition*) |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
33 |
val wakeup = ConditionVar.conditionVar (); |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
34 |
fun wakeup_all () = ConditionVar.broadcast wakeup; |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
35 |
fun wait () = ConditionVar.wait (wakeup, lock); |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
36 |
fun wait_timeout () = |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
37 |
ConditionVar.waitUntil (wakeup, lock, Time.+ (Time.now (), Time.fromSeconds 1)); |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
38 |
|
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
39 |
(*queue of tasks*) |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
40 |
val queue = ref tasks; |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
41 |
val active = ref 0; |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
42 |
fun trace_active () = Multithreading.tracing 1 (fn () => |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
43 |
"SCHEDULE: " ^ string_of_int (! active) ^ " active"); |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
44 |
fun dequeue () = |
28158 | 45 |
(case change_result queue next_task of |
46 |
Wait => |
|
28121
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
47 |
(dec active; trace_active (); |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
48 |
wait (); |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
49 |
inc active; trace_active (); |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
50 |
dequeue ()) |
28158 | 51 |
| next => next); |
28121
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
52 |
|
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
53 |
(*pool of running threads*) |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
54 |
val status = ref ([]: exn list); |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
55 |
val running = ref ([]: Thread.thread list); |
28242 | 56 |
fun start f = (inc active; change running (cons (SimpleThread.fork false f))); |
57 |
fun stop () = (dec active; change running (remove Thread.equal (Thread.self ()))); |
|
28121
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
58 |
|
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
59 |
(*worker thread*) |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
60 |
fun worker () = |
28148 | 61 |
(case SYNCHRONIZED dequeue of |
28121
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
62 |
Task {body, cont, fail} => |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
63 |
(case Exn.capture (restore_attributes body) () of |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
64 |
Exn.Result () => |
28148 | 65 |
(SYNCHRONIZED (fn () => (change queue cont; wakeup_all ())); worker ()) |
28121
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
66 |
| Exn.Exn exn => |
28148 | 67 |
SYNCHRONIZED (fn () => |
28121
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
68 |
(change status (cons exn); change queue fail; stop (); wakeup_all ()))) |
28148 | 69 |
| Terminate => SYNCHRONIZED (fn () => (stop (); wakeup_all ()))); |
28121
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
70 |
|
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
71 |
(*main control: fork and wait*) |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
72 |
fun fork 0 = () |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
73 |
| fork k = (start worker; fork (k - 1)); |
28148 | 74 |
val _ = SYNCHRONIZED (fn () => |
28121
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
75 |
(fork (Int.max (n, 1)); |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
76 |
while not (null (! running)) do |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
77 |
(trace_active (); |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
78 |
if not (null (! status)) |
28543 | 79 |
then (List.app SimpleThread.interrupt (! running)) |
28121
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
80 |
else (); |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
81 |
wait_timeout ()))); |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
82 |
|
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
83 |
in ! status end); |
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
84 |
|
2303b4c53d3a
Scheduling -- multiple threads working on a queue of tasks.
wenzelm
parents:
diff
changeset
|
85 |
end; |