author | wenzelm |
Wed, 23 Dec 2015 23:09:13 +0100 | |
changeset 61925 | ab52f183f020 |
parent 59180 | src/Pure/ML-Systems/multithreading.ML@c0fa3b3bdabd |
child 62359 | 6709e51d5c11 |
permissions | -rw-r--r-- |
61925 | 1 |
(* Title: Pure/RAW/multithreading.ML |
24690
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 |
|
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
7 |
signature MULTITHREADING = |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
8 |
sig |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
9 |
val available: bool |
25775
90525e67ede7
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents:
25735
diff
changeset
|
10 |
val max_threads_value: unit -> int |
54717 | 11 |
val max_threads_update: int -> unit |
12 |
val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b |
|
28554 | 13 |
val enabled: unit -> bool |
28149 | 14 |
val no_interrupts: Thread.threadAttribute list |
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
15 |
val public_interrupts: Thread.threadAttribute list |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
16 |
val private_interrupts: Thread.threadAttribute list |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
17 |
val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list |
41713
a21084741b37
added Multithreading.interrupted (cf. java.lang.Thread.interrupted);
wenzelm
parents:
39616
diff
changeset
|
18 |
val interrupted: unit -> unit (*exception Interrupt*) |
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
19 |
val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
20 |
val sync_wait: Thread.threadAttribute list option -> Time.time option -> |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
21 |
ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result |
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
32777
diff
changeset
|
22 |
val trace: int ref |
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
23 |
val tracing: int -> (unit -> string) -> unit |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
24 |
val tracing_time: bool -> Time.time -> (unit -> string) -> unit |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
25 |
val real_time: ('a -> unit) -> 'a -> Time.time |
59054
61b723761dff
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents:
54717
diff
changeset
|
26 |
val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a |
25704 | 27 |
val serial: unit -> int |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
28 |
end; |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
29 |
|
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
30 |
structure Multithreading: MULTITHREADING = |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
31 |
struct |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
32 |
|
32185 | 33 |
(* options *) |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
34 |
|
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
35 |
val available = false; |
28460 | 36 |
fun max_threads_value () = 1: int; |
54717 | 37 |
fun max_threads_update _ = (); |
38 |
fun max_threads_setmp _ f x = f x; |
|
28554 | 39 |
fun enabled () = false; |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
40 |
|
32286
1fb5db48002d
added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
wenzelm
parents:
32186
diff
changeset
|
41 |
|
1fb5db48002d
added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
wenzelm
parents:
32186
diff
changeset
|
42 |
(* attributes *) |
1fb5db48002d
added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
wenzelm
parents:
32186
diff
changeset
|
43 |
|
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
44 |
val no_interrupts = []; |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
45 |
val public_interrupts = []; |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
46 |
val private_interrupts = []; |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
47 |
fun sync_interrupts _ = []; |
28187
4062882c7df3
proper values of no_interrupts, regular_interrupts;
wenzelm
parents:
28169
diff
changeset
|
48 |
|
41713
a21084741b37
added Multithreading.interrupted (cf. java.lang.Thread.interrupted);
wenzelm
parents:
39616
diff
changeset
|
49 |
fun interrupted () = (); |
a21084741b37
added Multithreading.interrupted (cf. java.lang.Thread.interrupted);
wenzelm
parents:
39616
diff
changeset
|
50 |
|
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
51 |
fun with_attributes _ e = e []; |
28160 | 52 |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
41713
diff
changeset
|
53 |
fun sync_wait _ _ _ _ = Exn.Res true; |
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
54 |
|
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
55 |
|
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
56 |
(* tracing *) |
30612
cb6421b6a18f
future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents:
29564
diff
changeset
|
57 |
|
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
32777
diff
changeset
|
58 |
val trace = ref (0: int); |
32295
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
59 |
fun tracing _ _ = (); |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
60 |
fun tracing_time _ _ _ = (); |
400cc493d466
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents:
32286
diff
changeset
|
61 |
fun real_time f x = (f x; Time.zeroTime); |
32286
1fb5db48002d
added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
wenzelm
parents:
32186
diff
changeset
|
62 |
|
25735 | 63 |
|
59180
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59054
diff
changeset
|
64 |
(* synchronized evaluation *) |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
65 |
|
59054
61b723761dff
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents:
54717
diff
changeset
|
66 |
fun synchronized _ _ e = e (); |
61b723761dff
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents:
54717
diff
changeset
|
67 |
|
25735 | 68 |
|
69 |
(* serial numbers *) |
|
70 |
||
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
32777
diff
changeset
|
71 |
local val count = ref (0: int) |
25704 | 72 |
in fun serial () = (count := ! count + 1; ! count) end; |
73 |
||
28123
53cd972d7db9
provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents:
26082
diff
changeset
|
74 |
end; |
53cd972d7db9
provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents:
26082
diff
changeset
|
75 |