author | wenzelm |
Sat, 25 Jul 2009 00:39:05 +0200 | |
changeset 32185 | 57ecfab3bcfe |
parent 32184 | cfa0ef0c0c5f |
child 32186 | 8026b73cd357 |
permissions | -rw-r--r-- |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/multithreading.ML |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
3 |
|
28149 | 4 |
Dummy implementation of multithreading setup. |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
5 |
*) |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
6 |
|
25704 | 7 |
signature BASIC_MULTITHREADING = |
8 |
sig |
|
9 |
val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a |
|
10 |
val CRITICAL: (unit -> 'a) -> 'a |
|
11 |
end; |
|
12 |
||
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
13 |
signature MULTITHREADING = |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
14 |
sig |
25704 | 15 |
include BASIC_MULTITHREADING |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
16 |
val trace: int ref |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
17 |
val tracing: int -> (unit -> string) -> unit |
32184 | 18 |
val tracing_time: Time.time -> (unit -> string) -> unit |
32185 | 19 |
val real_time: ('a -> unit) -> 'a -> Time.time |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
20 |
val available: bool |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
21 |
val max_threads: int ref |
25775
90525e67ede7
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents:
25735
diff
changeset
|
22 |
val max_threads_value: unit -> int |
28554 | 23 |
val enabled: unit -> bool |
28149 | 24 |
val no_interrupts: Thread.threadAttribute list |
28160 | 25 |
val regular_interrupts: Thread.threadAttribute list |
30612
cb6421b6a18f
future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents:
29564
diff
changeset
|
26 |
val restricted_interrupts: Thread.threadAttribute list |
28160 | 27 |
val with_attributes: Thread.threadAttribute list -> |
28 |
(Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b |
|
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
29 |
val self_critical: unit -> bool |
25704 | 30 |
val serial: unit -> int |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
31 |
end; |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
32 |
|
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
33 |
structure Multithreading: MULTITHREADING = |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
34 |
struct |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
35 |
|
32185 | 36 |
(* tracing *) |
25735 | 37 |
|
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
38 |
val trace = ref (0: int); |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
39 |
fun tracing _ _ = (); |
32184 | 40 |
fun tracing_time _ _ = (); |
32185 | 41 |
fun real_time f x = (f x; Time.zeroTime); |
42 |
||
43 |
||
44 |
(* options *) |
|
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
45 |
|
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
46 |
val available = false; |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
47 |
val max_threads = ref (1: int); |
28460 | 48 |
fun max_threads_value () = 1: int; |
28554 | 49 |
fun enabled () = false; |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
50 |
|
28187
4062882c7df3
proper values of no_interrupts, regular_interrupts;
wenzelm
parents:
28169
diff
changeset
|
51 |
val no_interrupts = |
4062882c7df3
proper values of no_interrupts, regular_interrupts;
wenzelm
parents:
28169
diff
changeset
|
52 |
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer]; |
4062882c7df3
proper values of no_interrupts, regular_interrupts;
wenzelm
parents:
28169
diff
changeset
|
53 |
|
4062882c7df3
proper values of no_interrupts, regular_interrupts;
wenzelm
parents:
28169
diff
changeset
|
54 |
val regular_interrupts = |
4062882c7df3
proper values of no_interrupts, regular_interrupts;
wenzelm
parents:
28169
diff
changeset
|
55 |
[Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce]; |
28160 | 56 |
|
30612
cb6421b6a18f
future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents:
29564
diff
changeset
|
57 |
val restricted_interrupts = |
cb6421b6a18f
future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents:
29564
diff
changeset
|
58 |
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce]; |
cb6421b6a18f
future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents:
29564
diff
changeset
|
59 |
|
28160 | 60 |
fun with_attributes _ f x = f [] x; |
28149 | 61 |
|
25735 | 62 |
|
63 |
(* critical section *) |
|
64 |
||
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
65 |
fun self_critical () = false; |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
66 |
fun NAMED_CRITICAL _ e = e (); |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
67 |
fun CRITICAL e = e (); |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
68 |
|
25735 | 69 |
|
70 |
(* serial numbers *) |
|
71 |
||
25704 | 72 |
local val count = ref (0: int) |
73 |
in fun serial () = (count := ! count + 1; ! count) end; |
|
74 |
||
28123
53cd972d7db9
provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents:
26082
diff
changeset
|
75 |
end; |
53cd972d7db9
provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents:
26082
diff
changeset
|
76 |
|
53cd972d7db9
provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents:
26082
diff
changeset
|
77 |
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading; |
53cd972d7db9
provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents:
26082
diff
changeset
|
78 |
open BasicMultithreading; |