src/Pure/ML-Systems/multithreading.ML
author wenzelm
Thu Dec 20 21:12:02 2007 +0100 (2007-12-20 ago)
changeset 25735 4d147263f71f
parent 25704 df9c8074ff09
child 25775 90525e67ede7
permissions -rw-r--r--
added get/put_data;
wenzelm@24690
     1
(*  Title:      Pure/ML-Systems/multithreading.ML
wenzelm@24690
     2
    ID:         $Id$
wenzelm@24690
     3
    Author:     Makarius
wenzelm@24690
     4
wenzelm@24690
     5
Dummy implementation of multithreading interface.
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@24690
    21
  val self_critical: unit -> bool
wenzelm@24690
    22
  datatype 'a task =
wenzelm@24690
    23
    Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
wenzelm@24690
    24
  val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
wenzelm@25704
    25
  val serial: unit -> int
wenzelm@25735
    26
  val get_data: 'a Universal.tag -> 'a option
wenzelm@25735
    27
  val put_data: 'a Universal.tag * 'a -> unit
wenzelm@24690
    28
end;
wenzelm@24690
    29
wenzelm@24690
    30
structure Multithreading: MULTITHREADING =
wenzelm@24690
    31
struct
wenzelm@24690
    32
wenzelm@25735
    33
(* options *)
wenzelm@25735
    34
wenzelm@24690
    35
val trace = ref (0: int);
wenzelm@24690
    36
fun tracing _ _ = ();
wenzelm@24690
    37
wenzelm@24690
    38
val available = false;
wenzelm@24690
    39
val max_threads = ref (1: int);
wenzelm@24690
    40
wenzelm@25735
    41
wenzelm@25735
    42
(* critical section *)
wenzelm@25735
    43
wenzelm@24690
    44
fun self_critical () = false;
wenzelm@24690
    45
fun NAMED_CRITICAL _ e = e ();
wenzelm@24690
    46
fun CRITICAL e = e ();
wenzelm@24690
    47
wenzelm@25735
    48
wenzelm@25735
    49
(* scheduling *)
wenzelm@25735
    50
wenzelm@24690
    51
datatype 'a task =
wenzelm@24690
    52
  Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
wenzelm@24690
    53
wenzelm@24690
    54
fun schedule _ _ _ = raise Fail "No multithreading support";
wenzelm@24690
    55
wenzelm@25735
    56
wenzelm@25735
    57
(* serial numbers *)
wenzelm@25735
    58
wenzelm@25704
    59
local val count = ref (0: int)
wenzelm@25704
    60
in fun serial () = (count := ! count + 1; ! count) end;
wenzelm@25704
    61
wenzelm@25735
    62
wenzelm@25735
    63
(* thread data *)
wenzelm@25735
    64
wenzelm@25735
    65
local
wenzelm@25735
    66
wenzelm@25735
    67
val data = ref ([]: Universal.universal ref list);
wenzelm@25735
    68
wenzelm@25735
    69
fun find_data tag =
wenzelm@25735
    70
  let
wenzelm@25735
    71
    fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
wenzelm@25735
    72
      | find [] = NONE;
wenzelm@25735
    73
  in find (! data) end;
wenzelm@25735
    74
wenzelm@25735
    75
in
wenzelm@25735
    76
wenzelm@25735
    77
fun get_data tag = Option.map (Universal.tagProject tag o !) (find_data tag);
wenzelm@25735
    78
wenzelm@25735
    79
fun put_data (tag, x) =
wenzelm@25735
    80
  (case find_data tag of
wenzelm@25735
    81
    SOME r => r := Universal.tagInject tag x
wenzelm@25735
    82
  | NONE => data := ref (Universal.tagInject tag x) :: ! data);
wenzelm@25735
    83
wenzelm@25735
    84
end;
wenzelm@25735
    85
wenzelm@24690
    86
end;
wenzelm@24690
    87
wenzelm@25704
    88
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
wenzelm@25704
    89
open BasicMultithreading;
wenzelm@25704
    90