provide dummy thread structures, including proper Thread.getLocal/setLocal;
authorwenzelm
Thu Sep 04 16:03:46 2008 +0200 (2008-09-04)
changeset 2812353cd972d7db9
parent 28122 3d099ce624e7
child 28124 10a1f1f4c6ae
provide dummy thread structures, including proper Thread.getLocal/setLocal;
moved task/schedule to Concurrent/schedule.ML;
src/Pure/ML-Systems/multithreading.ML
     1.1 --- a/src/Pure/ML-Systems/multithreading.ML	Thu Sep 04 16:03:44 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Thu Sep 04 16:03:46 2008 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Dummy implementation of multithreading interface.
     1.8 +Default implementation of multithreading interface -- mostly dummies.
     1.9  *)
    1.10  
    1.11  signature BASIC_MULTITHREADING =
    1.12 @@ -20,12 +20,7 @@
    1.13    val max_threads: int ref
    1.14    val max_threads_value: unit -> int
    1.15    val self_critical: unit -> bool
    1.16 -  datatype 'a task =
    1.17 -    Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    1.18 -  val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
    1.19    val serial: unit -> int
    1.20 -  val get_data: 'a Universal.tag -> 'a option
    1.21 -  val put_data: 'a Universal.tag * 'a -> unit
    1.22  end;
    1.23  
    1.24  structure Multithreading: MULTITHREADING =
    1.25 @@ -48,20 +43,68 @@
    1.26  fun CRITICAL e = e ();
    1.27  
    1.28  
    1.29 -(* scheduling *)
    1.30 -
    1.31 -datatype 'a task =
    1.32 -  Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    1.33 -
    1.34 -fun schedule _ _ _ =
    1.35 -  raise Fail "No multithreading support -- cannot schedule tasks";
    1.36 -
    1.37 -
    1.38  (* serial numbers *)
    1.39  
    1.40  local val count = ref (0: int)
    1.41  in fun serial () = (count := ! count + 1; ! count) end;
    1.42  
    1.43 +end;
    1.44 +
    1.45 +structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
    1.46 +open BasicMultithreading;
    1.47 +
    1.48 +
    1.49 +
    1.50 +(** dummy thread structures (cf. polyml/basis/Thread.sml) **)
    1.51 +
    1.52 +exception Thread of string;
    1.53 +
    1.54 +local fun fail _ = raise Thread "No multithreading support on this ML platform" in
    1.55 +
    1.56 +structure Mutex =
    1.57 +struct
    1.58 +  type mutex = unit;
    1.59 +  fun mutex _ = fail ();
    1.60 +  fun lock _ = fail ();
    1.61 +  fun unlock _ = fail ();
    1.62 +  fun trylock _ = fail ();
    1.63 +end;
    1.64 +
    1.65 +structure ConditionVar =
    1.66 +struct
    1.67 +  type conditionVar = unit;
    1.68 +  fun conditionVar _ = fail ();
    1.69 +  fun wait _ = fail ();
    1.70 +  fun waitUntil _ = fail ();
    1.71 +  fun signal _ = fail ();
    1.72 +  fun broadcast _ = fail ();
    1.73 +end;
    1.74 +
    1.75 +structure Thread =
    1.76 +struct
    1.77 +  type thread = unit;
    1.78 +
    1.79 +  datatype threadAttribute = EnableBroadcastInterrupt of bool | InterruptState of interruptState
    1.80 +    and interruptState = InterruptDefer | InterruptSynch | InterruptAsynch | InterruptAsynchOnce;
    1.81 +
    1.82 +  fun fork _ = fail ();
    1.83 +  fun exit _ = fail ();
    1.84 +  fun isActive _ = fail ();
    1.85 +
    1.86 +  fun equal _ = fail ();
    1.87 +  fun self _ = fail ();
    1.88 +
    1.89 +  fun interrupt _ = fail ();
    1.90 +  fun broadcastInterrupt _ = fail ();
    1.91 +  fun testInterrupt _ = fail ();
    1.92 +
    1.93 +  fun kill _ = fail ();
    1.94 +
    1.95 +  fun setAttributes _ = fail ();
    1.96 +  fun getAttributes _ = fail ();
    1.97 +
    1.98 +  fun numProcessors _ = fail ();
    1.99 +
   1.100  
   1.101  (* thread data *)
   1.102  
   1.103 @@ -77,17 +120,13 @@
   1.104  
   1.105  in
   1.106  
   1.107 -fun get_data tag = Option.map (Universal.tagProject tag o !) (find_data tag);
   1.108 +fun getLocal tag = Option.map (Universal.tagProject tag o !) (find_data tag);
   1.109  
   1.110 -fun put_data (tag, x) =
   1.111 +fun setLocal (tag, x) =
   1.112    (case find_data tag of
   1.113      SOME r => r := Universal.tagInject tag x
   1.114    | NONE => data := ref (Universal.tagInject tag x) :: ! data);
   1.115  
   1.116  end;
   1.117 -
   1.118  end;
   1.119 -
   1.120 -structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
   1.121 -open BasicMultithreading;
   1.122 -
   1.123 +end;