src/Pure/ML-Systems/multithreading.ML
author wenzelm
Sat Feb 16 16:44:00 2008 +0100 (2008-02-16)
changeset 26082 ea11278a0300
parent 26074 44c5419cd9f1
child 28123 53cd972d7db9
permissions -rw-r--r--
removed managed_process (cf. General/shell_process.ML);
     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 max_threads_value: unit -> int
    22   val self_critical: unit -> bool
    23   datatype 'a task =
    24     Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    25   val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
    26   val serial: unit -> int
    27   val get_data: 'a Universal.tag -> 'a option
    28   val put_data: 'a Universal.tag * 'a -> unit
    29 end;
    30 
    31 structure Multithreading: MULTITHREADING =
    32 struct
    33 
    34 (* options *)
    35 
    36 val trace = ref (0: int);
    37 fun tracing _ _ = ();
    38 
    39 val available = false;
    40 val max_threads = ref (1: int);
    41 fun max_threads_value () = Int.max (! max_threads, 1);
    42 
    43 
    44 (* critical section *)
    45 
    46 fun self_critical () = false;
    47 fun NAMED_CRITICAL _ e = e ();
    48 fun CRITICAL e = e ();
    49 
    50 
    51 (* scheduling *)
    52 
    53 datatype 'a task =
    54   Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    55 
    56 fun schedule _ _ _ =
    57   raise Fail "No multithreading support -- cannot schedule tasks";
    58 
    59 
    60 (* serial numbers *)
    61 
    62 local val count = ref (0: int)
    63 in fun serial () = (count := ! count + 1; ! count) end;
    64 
    65 
    66 (* thread data *)
    67 
    68 local
    69 
    70 val data = ref ([]: Universal.universal ref list);
    71 
    72 fun find_data tag =
    73   let
    74     fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
    75       | find [] = NONE;
    76   in find (! data) end;
    77 
    78 in
    79 
    80 fun get_data tag = Option.map (Universal.tagProject tag o !) (find_data tag);
    81 
    82 fun put_data (tag, x) =
    83   (case find_data tag of
    84     SOME r => r := Universal.tagInject tag x
    85   | NONE => data := ref (Universal.tagInject tag x) :: ! data);
    86 
    87 end;
    88 
    89 end;
    90 
    91 structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
    92 open BasicMultithreading;
    93