src/Pure/ML-Systems/multithreading.ML
author wenzelm
Sun, 31 May 2009 14:51:21 +0200
changeset 31312 1c00e4ff3c99
parent 30612 cb6421b6a18f
child 32184 cfa0ef0c0c5f
permissions -rw-r--r--
more modular setup of runtime compilation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
26bd1245a46b added no_interrupts;
wenzelm
parents: 28123
diff changeset
     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
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
     7
signature BASIC_MULTITHREADING =
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
     8
sig
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
     9
  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    10
  val CRITICAL: (unit -> 'a) -> 'a
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    11
end;
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    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
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    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
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    18
  val available: bool
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    19
  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
    20
  val max_threads_value: unit -> int
28554
a6065ce44984 added enabled;
wenzelm
parents: 28460
diff changeset
    21
  val enabled: unit -> bool
28149
26bd1245a46b added no_interrupts;
wenzelm
parents: 28123
diff changeset
    22
  val no_interrupts: Thread.threadAttribute list
28160
e0177b67ecd9 added sync_interrupts, regular_interrupts;
wenzelm
parents: 28149
diff changeset
    23
  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
    24
  val restricted_interrupts: Thread.threadAttribute list
28160
e0177b67ecd9 added sync_interrupts, regular_interrupts;
wenzelm
parents: 28149
diff changeset
    25
  val with_attributes: Thread.threadAttribute list ->
e0177b67ecd9 added sync_interrupts, regular_interrupts;
wenzelm
parents: 28149
diff changeset
    26
    (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    27
  val self_critical: unit -> bool
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    28
  val serial: unit -> int
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
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    34
(* options *)
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    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);
28460
455ef74607d7 max_threads_value always 1 for dummy version;
wenzelm
parents: 28187
diff changeset
    41
fun max_threads_value () = 1: int;
28554
a6065ce44984 added enabled;
wenzelm
parents: 28460
diff changeset
    42
fun enabled () = false;
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    43
28187
4062882c7df3 proper values of no_interrupts, regular_interrupts;
wenzelm
parents: 28169
diff changeset
    44
val no_interrupts =
4062882c7df3 proper values of no_interrupts, regular_interrupts;
wenzelm
parents: 28169
diff changeset
    45
  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
4062882c7df3 proper values of no_interrupts, regular_interrupts;
wenzelm
parents: 28169
diff changeset
    46
4062882c7df3 proper values of no_interrupts, regular_interrupts;
wenzelm
parents: 28169
diff changeset
    47
val regular_interrupts =
4062882c7df3 proper values of no_interrupts, regular_interrupts;
wenzelm
parents: 28169
diff changeset
    48
  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
28160
e0177b67ecd9 added sync_interrupts, regular_interrupts;
wenzelm
parents: 28149
diff changeset
    49
30612
cb6421b6a18f future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents: 29564
diff changeset
    50
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
    51
  [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
    52
28160
e0177b67ecd9 added sync_interrupts, regular_interrupts;
wenzelm
parents: 28149
diff changeset
    53
fun with_attributes _ f x = f [] x;
28149
26bd1245a46b added no_interrupts;
wenzelm
parents: 28123
diff changeset
    54
25735
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    55
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    56
(* critical section *)
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    57
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    58
fun self_critical () = false;
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    59
fun NAMED_CRITICAL _ e = e ();
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    60
fun CRITICAL e = e ();
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    61
25735
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    62
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    63
(* serial numbers *)
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    64
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    65
local val count = ref (0: int)
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    66
in fun serial () = (count := ! count + 1; ! count) end;
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    67
28123
53cd972d7db9 provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents: 26082
diff changeset
    68
end;
53cd972d7db9 provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents: 26082
diff changeset
    69
53cd972d7db9 provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents: 26082
diff changeset
    70
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
53cd972d7db9 provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents: 26082
diff changeset
    71
open BasicMultithreading;