src/Pure/ML-Systems/multithreading.ML
author wenzelm
Tue Dec 18 22:21:42 2007 +0100 (2007-12-18)
changeset 25704 df9c8074ff09
parent 24690 c661dae1070a
child 25735 4d147263f71f
permissions -rw-r--r--
signature BASIC_MULTITHREADING;
added specific serial number generator, which avoid the global CRITICAL lock;
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@24690
    26
end;
wenzelm@24690
    27
wenzelm@24690
    28
structure Multithreading: MULTITHREADING =
wenzelm@24690
    29
struct
wenzelm@24690
    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@24690
    36
wenzelm@24690
    37
fun self_critical () = false;
wenzelm@24690
    38
fun NAMED_CRITICAL _ e = e ();
wenzelm@24690
    39
fun CRITICAL e = e ();
wenzelm@24690
    40
wenzelm@24690
    41
datatype 'a task =
wenzelm@24690
    42
  Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
wenzelm@24690
    43
wenzelm@24690
    44
fun schedule _ _ _ = raise Fail "No multithreading support";
wenzelm@24690
    45
wenzelm@25704
    46
local val count = ref (0: int)
wenzelm@25704
    47
in fun serial () = (count := ! count + 1; ! count) end;
wenzelm@25704
    48
wenzelm@24690
    49
end;
wenzelm@24690
    50
wenzelm@25704
    51
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
wenzelm@25704
    52
open BasicMultithreading;
wenzelm@25704
    53