author | wenzelm |
Wed, 02 Jan 2008 16:32:53 +0100 | |
changeset 25775 | 90525e67ede7 |
parent 25735 | 4d147263f71f |
child 26074 | 44c5419cd9f1 |
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 |
|
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
56 |
fun schedule _ _ _ = raise Fail "No multithreading support"; |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
57 |
|
25735 | 58 |
|
59 |
(* serial numbers *) |
|
60 |
||
25704 | 61 |
local val count = ref (0: int) |
62 |
in fun serial () = (count := ! count + 1; ! count) end; |
|
63 |
||
25735 | 64 |
|
65 |
(* thread data *) |
|
66 |
||
67 |
local |
|
68 |
||
69 |
val data = ref ([]: Universal.universal ref list); |
|
70 |
||
71 |
fun find_data tag = |
|
72 |
let |
|
73 |
fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs |
|
74 |
| find [] = NONE; |
|
75 |
in find (! data) end; |
|
76 |
||
77 |
in |
|
78 |
||
79 |
fun get_data tag = Option.map (Universal.tagProject tag o !) (find_data tag); |
|
80 |
||
81 |
fun put_data (tag, x) = |
|
82 |
(case find_data tag of |
|
83 |
SOME r => r := Universal.tagInject tag x |
|
84 |
| NONE => data := ref (Universal.tagInject tag x) :: ! data); |
|
85 |
||
86 |
end; |
|
87 |
||
24690
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
88 |
end; |
c661dae1070a
renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff
changeset
|
89 |
|
25704 | 90 |
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading; |
91 |
open BasicMultithreading; |
|
92 |