author | wenzelm |
Sat Jul 25 00:13:39 2009 +0200 (2009-07-25) | |
changeset 32184 | cfa0ef0c0c5f |
parent 30612 | cb6421b6a18f |
child 32185 | 57ecfab3bcfe |
permissions | -rw-r--r-- |
wenzelm@24690 | 1 |
(* Title: Pure/ML-Systems/multithreading.ML |
wenzelm@24690 | 2 |
Author: Makarius |
wenzelm@24690 | 3 |
|
wenzelm@28149 | 4 |
Dummy implementation of multithreading setup. |
wenzelm@24690 | 5 |
*) |
wenzelm@24690 | 6 |
|
wenzelm@25704 | 7 |
signature BASIC_MULTITHREADING = |
wenzelm@25704 | 8 |
sig |
wenzelm@25704 | 9 |
val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a |
wenzelm@25704 | 10 |
val CRITICAL: (unit -> 'a) -> 'a |
wenzelm@25704 | 11 |
end; |
wenzelm@25704 | 12 |
|
wenzelm@24690 | 13 |
signature MULTITHREADING = |
wenzelm@24690 | 14 |
sig |
wenzelm@25704 | 15 |
include BASIC_MULTITHREADING |
wenzelm@24690 | 16 |
val trace: int ref |
wenzelm@24690 | 17 |
val tracing: int -> (unit -> string) -> unit |
wenzelm@32184 | 18 |
val tracing_time: Time.time -> (unit -> string) -> unit |
wenzelm@24690 | 19 |
val available: bool |
wenzelm@24690 | 20 |
val max_threads: int ref |
wenzelm@25775 | 21 |
val max_threads_value: unit -> int |
wenzelm@28554 | 22 |
val enabled: unit -> bool |
wenzelm@28149 | 23 |
val no_interrupts: Thread.threadAttribute list |
wenzelm@28160 | 24 |
val regular_interrupts: Thread.threadAttribute list |
wenzelm@30612 | 25 |
val restricted_interrupts: Thread.threadAttribute list |
wenzelm@28160 | 26 |
val with_attributes: Thread.threadAttribute list -> |
wenzelm@28160 | 27 |
(Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b |
wenzelm@24690 | 28 |
val self_critical: unit -> bool |
wenzelm@25704 | 29 |
val serial: unit -> int |
wenzelm@24690 | 30 |
end; |
wenzelm@24690 | 31 |
|
wenzelm@24690 | 32 |
structure Multithreading: MULTITHREADING = |
wenzelm@24690 | 33 |
struct |
wenzelm@24690 | 34 |
|
wenzelm@25735 | 35 |
(* options *) |
wenzelm@25735 | 36 |
|
wenzelm@24690 | 37 |
val trace = ref (0: int); |
wenzelm@24690 | 38 |
fun tracing _ _ = (); |
wenzelm@32184 | 39 |
fun tracing_time _ _ = (); |
wenzelm@24690 | 40 |
|
wenzelm@24690 | 41 |
val available = false; |
wenzelm@24690 | 42 |
val max_threads = ref (1: int); |
wenzelm@28460 | 43 |
fun max_threads_value () = 1: int; |
wenzelm@28554 | 44 |
fun enabled () = false; |
wenzelm@24690 | 45 |
|
wenzelm@28187 | 46 |
val no_interrupts = |
wenzelm@28187 | 47 |
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer]; |
wenzelm@28187 | 48 |
|
wenzelm@28187 | 49 |
val regular_interrupts = |
wenzelm@28187 | 50 |
[Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce]; |
wenzelm@28160 | 51 |
|
wenzelm@30612 | 52 |
val restricted_interrupts = |
wenzelm@30612 | 53 |
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce]; |
wenzelm@30612 | 54 |
|
wenzelm@28160 | 55 |
fun with_attributes _ f x = f [] x; |
wenzelm@28149 | 56 |
|
wenzelm@25735 | 57 |
|
wenzelm@25735 | 58 |
(* critical section *) |
wenzelm@25735 | 59 |
|
wenzelm@24690 | 60 |
fun self_critical () = false; |
wenzelm@24690 | 61 |
fun NAMED_CRITICAL _ e = e (); |
wenzelm@24690 | 62 |
fun CRITICAL e = e (); |
wenzelm@24690 | 63 |
|
wenzelm@25735 | 64 |
|
wenzelm@25735 | 65 |
(* serial numbers *) |
wenzelm@25735 | 66 |
|
wenzelm@25704 | 67 |
local val count = ref (0: int) |
wenzelm@25704 | 68 |
in fun serial () = (count := ! count + 1; ! count) end; |
wenzelm@25704 | 69 |
|
wenzelm@28123 | 70 |
end; |
wenzelm@28123 | 71 |
|
wenzelm@28123 | 72 |
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading; |
wenzelm@28123 | 73 |
open BasicMultithreading; |