src/Pure/ML-Systems/multithreading.ML
author wenzelm
Tue Mar 25 13:18:10 2014 +0100 (2014-03-25 ago)
changeset 56275 600f432ab556
parent 54717 42c209a6c225
child 59054 61b723761dff
permissions -rw-r--r--
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
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 available: bool
wenzelm@25775
    17
  val max_threads_value: unit -> int
wenzelm@54717
    18
  val max_threads_update: int -> unit
wenzelm@54717
    19
  val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b
wenzelm@28554
    20
  val enabled: unit -> bool
wenzelm@28149
    21
  val no_interrupts: Thread.threadAttribute list
wenzelm@32295
    22
  val public_interrupts: Thread.threadAttribute list
wenzelm@32295
    23
  val private_interrupts: Thread.threadAttribute list
wenzelm@32295
    24
  val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
wenzelm@41713
    25
  val interrupted: unit -> unit  (*exception Interrupt*)
wenzelm@32295
    26
  val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
wenzelm@32295
    27
  val sync_wait: Thread.threadAttribute list option -> Time.time option ->
wenzelm@32295
    28
    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
wenzelm@39616
    29
  val trace: int ref
wenzelm@32295
    30
  val tracing: int -> (unit -> string) -> unit
wenzelm@32295
    31
  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
wenzelm@32295
    32
  val real_time: ('a -> unit) -> 'a -> Time.time
wenzelm@24690
    33
  val self_critical: unit -> bool
wenzelm@25704
    34
  val serial: unit -> int
wenzelm@24690
    35
end;
wenzelm@24690
    36
wenzelm@24690
    37
structure Multithreading: MULTITHREADING =
wenzelm@24690
    38
struct
wenzelm@24690
    39
wenzelm@32185
    40
(* options *)
wenzelm@24690
    41
wenzelm@24690
    42
val available = false;
wenzelm@28460
    43
fun max_threads_value () = 1: int;
wenzelm@54717
    44
fun max_threads_update _ = ();
wenzelm@54717
    45
fun max_threads_setmp _ f x = f x;
wenzelm@28554
    46
fun enabled () = false;
wenzelm@24690
    47
wenzelm@32286
    48
wenzelm@32286
    49
(* attributes *)
wenzelm@32286
    50
wenzelm@32295
    51
val no_interrupts = [];
wenzelm@32295
    52
val public_interrupts = [];
wenzelm@32295
    53
val private_interrupts = [];
wenzelm@32295
    54
fun sync_interrupts _ = [];
wenzelm@28187
    55
wenzelm@41713
    56
fun interrupted () = ();
wenzelm@41713
    57
wenzelm@32295
    58
fun with_attributes _ e = e [];
wenzelm@28160
    59
wenzelm@43761
    60
fun sync_wait _ _ _ _ = Exn.Res true;
wenzelm@32295
    61
wenzelm@32295
    62
wenzelm@32295
    63
(* tracing *)
wenzelm@30612
    64
wenzelm@39616
    65
val trace = ref (0: int);
wenzelm@32295
    66
fun tracing _ _ = ();
wenzelm@32295
    67
fun tracing_time _ _ _ = ();
wenzelm@32295
    68
fun real_time f x = (f x; Time.zeroTime);
wenzelm@32286
    69
wenzelm@25735
    70
wenzelm@25735
    71
(* critical section *)
wenzelm@25735
    72
wenzelm@24690
    73
fun self_critical () = false;
wenzelm@24690
    74
fun NAMED_CRITICAL _ e = e ();
wenzelm@24690
    75
fun CRITICAL e = e ();
wenzelm@24690
    76
wenzelm@25735
    77
wenzelm@25735
    78
(* serial numbers *)
wenzelm@25735
    79
wenzelm@39616
    80
local val count = ref (0: int)
wenzelm@25704
    81
in fun serial () = (count := ! count + 1; ! count) end;
wenzelm@25704
    82
wenzelm@28123
    83
end;
wenzelm@28123
    84
wenzelm@32286
    85
structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
wenzelm@32286
    86
open Basic_Multithreading;