src/Pure/ML-Systems/multithreading.ML
author wenzelm
Thu Sep 04 16:03:46 2008 +0200 (2008-09-04)
changeset 28123 53cd972d7db9
parent 26082 ea11278a0300
child 28149 26bd1245a46b
permissions -rw-r--r--
provide dummy thread structures, including proper Thread.getLocal/setLocal;
moved task/schedule to Concurrent/schedule.ML;
wenzelm@24690
     1
(*  Title:      Pure/ML-Systems/multithreading.ML
wenzelm@24690
     2
    ID:         $Id$
wenzelm@24690
     3
    Author:     Makarius
wenzelm@24690
     4
wenzelm@28123
     5
Default implementation of multithreading interface -- mostly dummies.
wenzelm@24690
     6
*)
wenzelm@24690
     7
wenzelm@25704
     8
signature BASIC_MULTITHREADING =
wenzelm@25704
     9
sig
wenzelm@25704
    10
  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
wenzelm@25704
    11
  val CRITICAL: (unit -> 'a) -> 'a
wenzelm@25704
    12
end;
wenzelm@25704
    13
wenzelm@24690
    14
signature MULTITHREADING =
wenzelm@24690
    15
sig
wenzelm@25704
    16
  include BASIC_MULTITHREADING
wenzelm@24690
    17
  val trace: int ref
wenzelm@24690
    18
  val tracing: int -> (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@24690
    22
  val self_critical: unit -> bool
wenzelm@25704
    23
  val serial: unit -> int
wenzelm@24690
    24
end;
wenzelm@24690
    25
wenzelm@24690
    26
structure Multithreading: MULTITHREADING =
wenzelm@24690
    27
struct
wenzelm@24690
    28
wenzelm@25735
    29
(* options *)
wenzelm@25735
    30
wenzelm@24690
    31
val trace = ref (0: int);
wenzelm@24690
    32
fun tracing _ _ = ();
wenzelm@24690
    33
wenzelm@24690
    34
val available = false;
wenzelm@24690
    35
val max_threads = ref (1: int);
wenzelm@25775
    36
fun max_threads_value () = Int.max (! max_threads, 1);
wenzelm@24690
    37
wenzelm@25735
    38
wenzelm@25735
    39
(* critical section *)
wenzelm@25735
    40
wenzelm@24690
    41
fun self_critical () = false;
wenzelm@24690
    42
fun NAMED_CRITICAL _ e = e ();
wenzelm@24690
    43
fun CRITICAL e = e ();
wenzelm@24690
    44
wenzelm@25735
    45
wenzelm@25735
    46
(* serial numbers *)
wenzelm@25735
    47
wenzelm@25704
    48
local val count = ref (0: int)
wenzelm@25704
    49
in fun serial () = (count := ! count + 1; ! count) end;
wenzelm@25704
    50
wenzelm@28123
    51
end;
wenzelm@28123
    52
wenzelm@28123
    53
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
wenzelm@28123
    54
open BasicMultithreading;
wenzelm@28123
    55
wenzelm@28123
    56
wenzelm@28123
    57
wenzelm@28123
    58
(** dummy thread structures (cf. polyml/basis/Thread.sml) **)
wenzelm@28123
    59
wenzelm@28123
    60
exception Thread of string;
wenzelm@28123
    61
wenzelm@28123
    62
local fun fail _ = raise Thread "No multithreading support on this ML platform" in
wenzelm@28123
    63
wenzelm@28123
    64
structure Mutex =
wenzelm@28123
    65
struct
wenzelm@28123
    66
  type mutex = unit;
wenzelm@28123
    67
  fun mutex _ = fail ();
wenzelm@28123
    68
  fun lock _ = fail ();
wenzelm@28123
    69
  fun unlock _ = fail ();
wenzelm@28123
    70
  fun trylock _ = fail ();
wenzelm@28123
    71
end;
wenzelm@28123
    72
wenzelm@28123
    73
structure ConditionVar =
wenzelm@28123
    74
struct
wenzelm@28123
    75
  type conditionVar = unit;
wenzelm@28123
    76
  fun conditionVar _ = fail ();
wenzelm@28123
    77
  fun wait _ = fail ();
wenzelm@28123
    78
  fun waitUntil _ = fail ();
wenzelm@28123
    79
  fun signal _ = fail ();
wenzelm@28123
    80
  fun broadcast _ = fail ();
wenzelm@28123
    81
end;
wenzelm@28123
    82
wenzelm@28123
    83
structure Thread =
wenzelm@28123
    84
struct
wenzelm@28123
    85
  type thread = unit;
wenzelm@28123
    86
wenzelm@28123
    87
  datatype threadAttribute = EnableBroadcastInterrupt of bool | InterruptState of interruptState
wenzelm@28123
    88
    and interruptState = InterruptDefer | InterruptSynch | InterruptAsynch | InterruptAsynchOnce;
wenzelm@28123
    89
wenzelm@28123
    90
  fun fork _ = fail ();
wenzelm@28123
    91
  fun exit _ = fail ();
wenzelm@28123
    92
  fun isActive _ = fail ();
wenzelm@28123
    93
wenzelm@28123
    94
  fun equal _ = fail ();
wenzelm@28123
    95
  fun self _ = fail ();
wenzelm@28123
    96
wenzelm@28123
    97
  fun interrupt _ = fail ();
wenzelm@28123
    98
  fun broadcastInterrupt _ = fail ();
wenzelm@28123
    99
  fun testInterrupt _ = fail ();
wenzelm@28123
   100
wenzelm@28123
   101
  fun kill _ = fail ();
wenzelm@28123
   102
wenzelm@28123
   103
  fun setAttributes _ = fail ();
wenzelm@28123
   104
  fun getAttributes _ = fail ();
wenzelm@28123
   105
wenzelm@28123
   106
  fun numProcessors _ = fail ();
wenzelm@28123
   107
wenzelm@25735
   108
wenzelm@25735
   109
(* thread data *)
wenzelm@25735
   110
wenzelm@25735
   111
local
wenzelm@25735
   112
wenzelm@25735
   113
val data = ref ([]: Universal.universal ref list);
wenzelm@25735
   114
wenzelm@25735
   115
fun find_data tag =
wenzelm@25735
   116
  let
wenzelm@25735
   117
    fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
wenzelm@25735
   118
      | find [] = NONE;
wenzelm@25735
   119
  in find (! data) end;
wenzelm@25735
   120
wenzelm@25735
   121
in
wenzelm@25735
   122
wenzelm@28123
   123
fun getLocal tag = Option.map (Universal.tagProject tag o !) (find_data tag);
wenzelm@25735
   124
wenzelm@28123
   125
fun setLocal (tag, x) =
wenzelm@25735
   126
  (case find_data tag of
wenzelm@25735
   127
    SOME r => r := Universal.tagInject tag x
wenzelm@25735
   128
  | NONE => data := ref (Universal.tagInject tag x) :: ! data);
wenzelm@25735
   129
wenzelm@25735
   130
end;
wenzelm@24690
   131
end;
wenzelm@28123
   132
end;