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;
     1 (*  Title:      Pure/ML-Systems/multithreading.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Dummy implementation of multithreading interface.
     6 *)
     7 
     8 signature BASIC_MULTITHREADING =
     9 sig
    10   val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
    11   val CRITICAL: (unit -> 'a) -> 'a
    12 end;
    13 
    14 signature MULTITHREADING =
    15 sig
    16   include BASIC_MULTITHREADING
    17   val trace: int ref
    18   val tracing: int -> (unit -> string) -> unit
    19   val available: bool
    20   val max_threads: int ref
    21   val self_critical: unit -> bool
    22   datatype 'a task =
    23     Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    24   val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
    25   val serial: unit -> int
    26 end;
    27 
    28 structure Multithreading: MULTITHREADING =
    29 struct
    30 
    31 val trace = ref (0: int);
    32 fun tracing _ _ = ();
    33 
    34 val available = false;
    35 val max_threads = ref (1: int);
    36 
    37 fun self_critical () = false;
    38 fun NAMED_CRITICAL _ e = e ();
    39 fun CRITICAL e = e ();
    40 
    41 datatype 'a task =
    42   Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    43 
    44 fun schedule _ _ _ = raise Fail "No multithreading support";
    45 
    46 local val count = ref (0: int)
    47 in fun serial () = (count := ! count + 1; ! count) end;
    48 
    49 end;
    50 
    51 structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
    52 open BasicMultithreading;
    53