src/Pure/ML-Systems/multithreading.ML
author wenzelm
Sat Jul 25 00:53:47 2009 +0200 (2009-07-25)
changeset 32186 8026b73cd357
parent 32185 57ecfab3bcfe
child 32286 1fb5db48002d
permissions -rw-r--r--
tuned tracing;
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@32186
    18
  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
wenzelm@32185
    19
  val real_time: ('a -> unit) -> 'a -> Time.time
wenzelm@24690
    20
  val available: bool
wenzelm@24690
    21
  val max_threads: int ref
wenzelm@25775
    22
  val max_threads_value: unit -> int
wenzelm@28554
    23
  val enabled: unit -> bool
wenzelm@28149
    24
  val no_interrupts: Thread.threadAttribute list
wenzelm@28160
    25
  val regular_interrupts: Thread.threadAttribute list
wenzelm@30612
    26
  val restricted_interrupts: Thread.threadAttribute list
wenzelm@28160
    27
  val with_attributes: Thread.threadAttribute list ->
wenzelm@28160
    28
    (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
wenzelm@24690
    29
  val self_critical: unit -> bool
wenzelm@25704
    30
  val serial: unit -> int
wenzelm@24690
    31
end;
wenzelm@24690
    32
wenzelm@24690
    33
structure Multithreading: MULTITHREADING =
wenzelm@24690
    34
struct
wenzelm@24690
    35
wenzelm@32185
    36
(* tracing *)
wenzelm@25735
    37
wenzelm@24690
    38
val trace = ref (0: int);
wenzelm@24690
    39
fun tracing _ _ = ();
wenzelm@32186
    40
fun tracing_time _ _ _ = ();
wenzelm@32185
    41
fun real_time f x = (f x; Time.zeroTime);
wenzelm@32185
    42
wenzelm@32185
    43
wenzelm@32185
    44
(* options *)
wenzelm@24690
    45
wenzelm@24690
    46
val available = false;
wenzelm@24690
    47
val max_threads = ref (1: int);
wenzelm@28460
    48
fun max_threads_value () = 1: int;
wenzelm@28554
    49
fun enabled () = false;
wenzelm@24690
    50
wenzelm@28187
    51
val no_interrupts =
wenzelm@28187
    52
  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
wenzelm@28187
    53
wenzelm@28187
    54
val regular_interrupts =
wenzelm@28187
    55
  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
wenzelm@28160
    56
wenzelm@30612
    57
val restricted_interrupts =
wenzelm@30612
    58
  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
wenzelm@30612
    59
wenzelm@28160
    60
fun with_attributes _ f x = f [] x;
wenzelm@28149
    61
wenzelm@25735
    62
wenzelm@25735
    63
(* critical section *)
wenzelm@25735
    64
wenzelm@24690
    65
fun self_critical () = false;
wenzelm@24690
    66
fun NAMED_CRITICAL _ e = e ();
wenzelm@24690
    67
fun CRITICAL e = e ();
wenzelm@24690
    68
wenzelm@25735
    69
wenzelm@25735
    70
(* serial numbers *)
wenzelm@25735
    71
wenzelm@25704
    72
local val count = ref (0: int)
wenzelm@25704
    73
in fun serial () = (count := ! count + 1; ! count) end;
wenzelm@25704
    74
wenzelm@28123
    75
end;
wenzelm@28123
    76
wenzelm@28123
    77
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
wenzelm@28123
    78
open BasicMultithreading;