signature BASIC_MULTITHREADING;
authorwenzelm
Tue Dec 18 22:21:42 2007 +0100 (2007-12-18)
changeset 25704df9c8074ff09
parent 25703 832073e402ae
child 25705 45a2ffc5911e
signature BASIC_MULTITHREADING;
added specific serial number generator, which avoid the global CRITICAL lock;
src/Pure/ML-Systems/multithreading.ML
src/Pure/ML-Systems/multithreading_polyml.ML
     1.1 --- a/src/Pure/ML-Systems/multithreading.ML	Tue Dec 18 22:21:41 2007 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Tue Dec 18 22:21:42 2007 +0100
     1.3 @@ -5,18 +5,24 @@
     1.4  Dummy implementation of multithreading interface.
     1.5  *)
     1.6  
     1.7 +signature BASIC_MULTITHREADING =
     1.8 +sig
     1.9 +  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
    1.10 +  val CRITICAL: (unit -> 'a) -> 'a
    1.11 +end;
    1.12 +
    1.13  signature MULTITHREADING =
    1.14  sig
    1.15 +  include BASIC_MULTITHREADING
    1.16    val trace: int ref
    1.17    val tracing: int -> (unit -> string) -> unit
    1.18    val available: bool
    1.19    val max_threads: int ref
    1.20    val self_critical: unit -> bool
    1.21 -  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
    1.22 -  val CRITICAL: (unit -> 'a) -> 'a
    1.23    datatype 'a task =
    1.24      Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    1.25    val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
    1.26 +  val serial: unit -> int
    1.27  end;
    1.28  
    1.29  structure Multithreading: MULTITHREADING =
    1.30 @@ -37,7 +43,11 @@
    1.31  
    1.32  fun schedule _ _ _ = raise Fail "No multithreading support";
    1.33  
    1.34 +local val count = ref (0: int)
    1.35 +in fun serial () = (count := ! count + 1; ! count) end;
    1.36 +
    1.37  end;
    1.38  
    1.39 -val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
    1.40 -val CRITICAL = Multithreading.CRITICAL;
    1.41 +structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
    1.42 +open BasicMultithreading;
    1.43 +
     2.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Dec 18 22:21:41 2007 +0100
     2.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Dec 18 22:21:42 2007 +0100
     2.3 @@ -2,17 +2,28 @@
     2.4      ID:         $Id$
     2.5      Author:     Makarius
     2.6  
     2.7 -Multithreading in Poly/ML 5.1 or later (cf. polyml/basis/Thread.sml).
     2.8 +Multithreading in Poly/ML 5.1 (cf. polyml/basis/Thread.sml).
     2.9  *)
    2.10  
    2.11  open Thread;
    2.12  
    2.13 +signature MULTITHREADING_POLYML =
    2.14 +sig
    2.15 +  val ignore_interrupt: ('a -> 'b) -> 'a -> 'b
    2.16 +  val raise_interrupt: ('a -> 'b) -> 'a -> 'b
    2.17 +  structure TimeLimit: TIME_LIMIT
    2.18 +end;
    2.19 +
    2.20 +signature BASIC_MULTITHREADING =
    2.21 +sig
    2.22 +  include BASIC_MULTITHREADING
    2.23 +  include MULTITHREADING_POLYML
    2.24 +end;
    2.25 +
    2.26  signature MULTITHREADING =
    2.27  sig
    2.28    include MULTITHREADING
    2.29 -  val ignore_interrupt: ('a -> 'b) -> 'a -> 'b
    2.30 -  val raise_interrupt: ('a -> 'b) -> 'a -> 'b
    2.31 -  structure TimeLimit: TIME_LIMIT
    2.32 +  include MULTITHREADING_POLYML
    2.33  end;
    2.34  
    2.35  structure Multithreading: MULTITHREADING =
    2.36 @@ -227,13 +238,26 @@
    2.37  
    2.38    in ! status end);
    2.39  
    2.40 +
    2.41 +(* serial numbers *)
    2.42 +
    2.43 +local
    2.44 +
    2.45 +val serial_lock = Mutex.mutex ();
    2.46 +val serial_count = ref 0;
    2.47 +
    2.48 +in
    2.49 +
    2.50 +val serial = uninterruptible (fn _ => fn () =>
    2.51 +  let
    2.52 +    val _ = Mutex.lock serial_lock;
    2.53 +    val res = inc serial_count;
    2.54 +    val _ = Mutex.unlock serial_lock;
    2.55 +  in res end);
    2.56 +
    2.57  end;
    2.58  
    2.59 -val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
    2.60 -val CRITICAL = Multithreading.CRITICAL;
    2.61 +end;
    2.62  
    2.63 -val ignore_interrupt = Multithreading.ignore_interrupt;
    2.64 -val raise_interrupt = Multithreading.raise_interrupt;
    2.65 -
    2.66 -structure TimeLimit = Multithreading.TimeLimit;
    2.67 -
    2.68 +structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
    2.69 +open BasicMultithreading;