src/Pure/ML-Systems/multithreading.ML
author wenzelm
Sat, 01 Aug 2009 00:09:45 +0200
changeset 32295 400cc493d466
parent 32286 1fb5db48002d
child 32776 1504f9c2d060
permissions -rw-r--r--
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts; renamed Multithreading.restricted_interrupts to Multithreading.private_interrupts; added Multithreading.sync_interrupts; Multithreading.sync_wait: more careful treatment of attributes; Multithreading.tracing: uninterruptible; Multithreading.system_out: signal within critical region, more careful sync_wait; eliminated redundant Thread.testInterrupt; Future.wait_timeout: uniform Multithreading.sync_wait; future scheduler: interruptible body (sync!), to improve reactivity; future_job: reject duplicate assignments -- system error; misc tuning;
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 available: bool
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    17
  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
    18
  val max_threads_value: unit -> int
28554
a6065ce44984 added enabled;
wenzelm
parents: 28460
diff changeset
    19
  val enabled: unit -> bool
28149
26bd1245a46b added no_interrupts;
wenzelm
parents: 28123
diff changeset
    20
  val no_interrupts: Thread.threadAttribute list
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    21
  val public_interrupts: Thread.threadAttribute list
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    22
  val private_interrupts: Thread.threadAttribute list
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    23
  val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    24
  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
    25
  val sync_wait: Thread.threadAttribute list option -> Time.time option ->
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    26
    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    27
  val trace: int ref
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    28
  val tracing: int -> (unit -> string) -> unit
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    29
  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    30
  val real_time: ('a -> unit) -> 'a -> Time.time
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    31
  val self_critical: unit -> bool
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    32
  val serial: unit -> int
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    33
end;
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
structure Multithreading: MULTITHREADING =
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    36
struct
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    37
32185
57ecfab3bcfe added Multithreading.real_time;
wenzelm
parents: 32184
diff changeset
    38
(* options *)
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    39
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    40
val available = false;
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    41
val max_threads = ref (1: int);
28460
455ef74607d7 max_threads_value always 1 for dummy version;
wenzelm
parents: 28187
diff changeset
    42
fun max_threads_value () = 1: int;
28554
a6065ce44984 added enabled;
wenzelm
parents: 28460
diff changeset
    43
fun enabled () = false;
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    44
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
    45
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
    46
(* 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
    47
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    48
val no_interrupts = [];
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    49
val public_interrupts = [];
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    50
val private_interrupts = [];
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    51
fun sync_interrupts _ = [];
28187
4062882c7df3 proper values of no_interrupts, regular_interrupts;
wenzelm
parents: 28169
diff changeset
    52
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    53
fun with_attributes _ e = e [];
28160
e0177b67ecd9 added sync_interrupts, regular_interrupts;
wenzelm
parents: 28149
diff changeset
    54
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    55
fun sync_wait _ _ _ _ = Exn.Result true;
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    56
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    57
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    58
(* tracing *)
30612
cb6421b6a18f future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents: 29564
diff changeset
    59
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    60
val trace = ref (0: int);
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    61
fun tracing _ _ = ();
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    62
fun tracing_time _ _ _ = ();
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    63
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
    64
25735
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    65
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    66
(* critical section *)
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    67
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    68
fun self_critical () = false;
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    69
fun NAMED_CRITICAL _ e = e ();
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    70
fun CRITICAL e = e ();
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    71
25735
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    72
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    73
(* serial numbers *)
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    74
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    75
local val count = ref (0: int)
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    76
in fun serial () = (count := ! count + 1; ! count) end;
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    77
28123
53cd972d7db9 provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents: 26082
diff changeset
    78
end;
53cd972d7db9 provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents: 26082
diff changeset
    79
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
    80
structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
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
    81
open Basic_Multithreading;