author | wenzelm |
Mon, 04 Aug 2008 19:25:59 +0200 | |
changeset 27725 | 6d133c2b681f |
parent 26082 | ea11278a0300 |
child 28123 | 53cd972d7db9 |
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 |
ID: $Id$ |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
4 |
|
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
5 |
Dummy implementation of multithreading interface. |
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 |
|
25704 | 8 |
signature BASIC_MULTITHREADING = |
9 |
sig |
|
10 |
val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a |
|
11 |
val CRITICAL: (unit -> 'a) -> 'a |
|
12 |
end; |
|
13 |
||
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
14 |
signature MULTITHREADING = |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
15 |
sig |
25704 | 16 |
include BASIC_MULTITHREADING |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
17 |
val trace: int ref |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
18 |
val tracing: int -> (unit -> string) -> unit |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
19 |
val available: bool |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
20 |
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
|
21 |
val max_threads_value: unit -> int |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
22 |
val self_critical: unit -> bool |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
23 |
datatype 'a task = |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
24 |
Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate; |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
25 |
val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list |
25704 | 26 |
val serial: unit -> int |
25735 | 27 |
val get_data: 'a Universal.tag -> 'a option |
28 |
val put_data: 'a Universal.tag * 'a -> unit |
|
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
29 |
end; |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
30 |
|
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
31 |
structure Multithreading: MULTITHREADING = |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
32 |
struct |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
33 |
|
25735 | 34 |
(* options *) |
35 |
||
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
36 |
val trace = ref (0: int); |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
37 |
fun tracing _ _ = (); |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
38 |
|
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
39 |
val available = false; |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
40 |
val max_threads = ref (1: int); |
25775
90525e67ede7
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents:
25735
diff
changeset
|
41 |
fun max_threads_value () = Int.max (! max_threads, 1); |
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
42 |
|
25735 | 43 |
|
44 |
(* critical section *) |
|
45 |
||
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
46 |
fun self_critical () = false; |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
47 |
fun NAMED_CRITICAL _ e = e (); |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
48 |
fun CRITICAL e = e (); |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
49 |
|
25735 | 50 |
|
51 |
(* scheduling *) |
|
52 |
||
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
53 |
datatype 'a task = |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
54 |
Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate; |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
55 |
|
26074 | 56 |
fun schedule _ _ _ = |
57 |
raise Fail "No multithreading support -- cannot schedule tasks"; |
|
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
58 |
|
25735 | 59 |
|
60 |
(* serial numbers *) |
|
61 |
||
25704 | 62 |
local val count = ref (0: int) |
63 |
in fun serial () = (count := ! count + 1; ! count) end; |
|
64 |
||
25735 | 65 |
|
66 |
(* thread data *) |
|
67 |
||
68 |
local |
|
69 |
||
70 |
val data = ref ([]: Universal.universal ref list); |
|
71 |
||
72 |
fun find_data tag = |
|
73 |
let |
|
74 |
fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs |
|
75 |
| find [] = NONE; |
|
76 |
in find (! data) end; |
|
77 |
||
78 |
in |
|
79 |
||
80 |
fun get_data tag = Option.map (Universal.tagProject tag o !) (find_data tag); |
|
81 |
||
82 |
fun put_data (tag, x) = |
|
83 |
(case find_data tag of |
|
84 |
SOME r => r := Universal.tagInject tag x |
|
85 |
| NONE => data := ref (Universal.tagInject tag x) :: ! data); |
|
86 |
||
87 |
end; |
|
88 |
||
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
89 |
end; |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
90 |
|
25704 | 91 |
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading; |
92 |
open BasicMultithreading; |
|
93 |