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;
     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   val get_data: 'a Universal.tag -> 'a option
    27   val put_data: 'a Universal.tag * 'a -> unit
    28 end;
    29 
    30 structure Multithreading: MULTITHREADING =
    31 struct
    32 
    33 (* options *)
    34 
    35 val trace = ref (0: int);
    36 fun tracing _ _ = ();
    37 
    38 val available = false;
    39 val max_threads = ref (1: int);
    40 
    41 
    42 (* critical section *)
    43 
    44 fun self_critical () = false;
    45 fun NAMED_CRITICAL _ e = e ();
    46 fun CRITICAL e = e ();
    47 
    48 
    49 (* scheduling *)
    50 
    51 datatype 'a task =
    52   Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    53 
    54 fun schedule _ _ _ = raise Fail "No multithreading support";
    55 
    56 
    57 (* serial numbers *)
    58 
    59 local val count = ref (0: int)
    60 in fun serial () = (count := ! count + 1; ! count) end;
    61 
    62 
    63 (* thread data *)
    64 
    65 local
    66 
    67 val data = ref ([]: Universal.universal ref list);
    68 
    69 fun find_data tag =
    70   let
    71     fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
    72       | find [] = NONE;
    73   in find (! data) end;
    74 
    75 in
    76 
    77 fun get_data tag = Option.map (Universal.tagProject tag o !) (find_data tag);
    78 
    79 fun put_data (tag, x) =
    80   (case find_data tag of
    81     SOME r => r := Universal.tagInject tag x
    82   | NONE => data := ref (Universal.tagInject tag x) :: ! data);
    83 
    84 end;
    85 
    86 end;
    87 
    88 structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
    89 open BasicMultithreading;
    90