src/Pure/ML-Systems/multithreading.ML
author wenzelm
Thu Sep 04 16:03:47 2008 +0200 (2008-09-04)
changeset 28124 10a1f1f4c6ae
parent 28123 53cd972d7db9
child 28149 26bd1245a46b
permissions -rw-r--r--
moved Multithreading.task/schedule to Concurrent/schedule.ML;
     1 (*  Title:      Pure/ML-Systems/multithreading.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Default implementation of multithreading interface -- mostly dummies.
     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   val serial: unit -> int
    24 end;
    25 
    26 structure Multithreading: MULTITHREADING =
    27 struct
    28 
    29 (* options *)
    30 
    31 val trace = ref (0: int);
    32 fun tracing _ _ = ();
    33 
    34 val available = false;
    35 val max_threads = ref (1: int);
    36 fun max_threads_value () = Int.max (! max_threads, 1);
    37 
    38 
    39 (* critical section *)
    40 
    41 fun self_critical () = false;
    42 fun NAMED_CRITICAL _ e = e ();
    43 fun CRITICAL e = e ();
    44 
    45 
    46 (* serial numbers *)
    47 
    48 local val count = ref (0: int)
    49 in fun serial () = (count := ! count + 1; ! count) end;
    50 
    51 end;
    52 
    53 structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
    54 open BasicMultithreading;
    55 
    56 
    57 
    58 (** dummy thread structures (cf. polyml/basis/Thread.sml) **)
    59 
    60 exception Thread of string;
    61 
    62 local fun fail _ = raise Thread "No multithreading support on this ML platform" in
    63 
    64 structure Mutex =
    65 struct
    66   type mutex = unit;
    67   fun mutex _ = fail ();
    68   fun lock _ = fail ();
    69   fun unlock _ = fail ();
    70   fun trylock _ = fail ();
    71 end;
    72 
    73 structure ConditionVar =
    74 struct
    75   type conditionVar = unit;
    76   fun conditionVar _ = fail ();
    77   fun wait _ = fail ();
    78   fun waitUntil _ = fail ();
    79   fun signal _ = fail ();
    80   fun broadcast _ = fail ();
    81 end;
    82 
    83 structure Thread =
    84 struct
    85   type thread = unit;
    86 
    87   datatype threadAttribute = EnableBroadcastInterrupt of bool | InterruptState of interruptState
    88     and interruptState = InterruptDefer | InterruptSynch | InterruptAsynch | InterruptAsynchOnce;
    89 
    90   fun fork _ = fail ();
    91   fun exit _ = fail ();
    92   fun isActive _ = fail ();
    93 
    94   fun equal _ = fail ();
    95   fun self _ = fail ();
    96 
    97   fun interrupt _ = fail ();
    98   fun broadcastInterrupt _ = fail ();
    99   fun testInterrupt _ = fail ();
   100 
   101   fun kill _ = fail ();
   102 
   103   fun setAttributes _ = fail ();
   104   fun getAttributes _ = fail ();
   105 
   106   fun numProcessors _ = fail ();
   107 
   108 
   109 (* thread data *)
   110 
   111 local
   112 
   113 val data = ref ([]: Universal.universal ref list);
   114 
   115 fun find_data tag =
   116   let
   117     fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
   118       | find [] = NONE;
   119   in find (! data) end;
   120 
   121 in
   122 
   123 fun getLocal tag = Option.map (Universal.tagProject tag o !) (find_data tag);
   124 
   125 fun setLocal (tag, x) =
   126   (case find_data tag of
   127     SOME r => r := Universal.tagInject tag x
   128   | NONE => data := ref (Universal.tagInject tag x) :: ! data);
   129 
   130 end;
   131 end;
   132 end;