src/Pure/ML-Systems/multithreading.ML
author wenzelm
Thu Oct 02 14:22:45 2008 +0200 (2008-10-02)
changeset 28460 455ef74607d7
parent 28187 4062882c7df3
child 28554 a6065ce44984
permissions -rw-r--r--
max_threads_value always 1 for dummy version;
     1 (*  Title:      Pure/ML-Systems/multithreading.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Dummy implementation of multithreading setup.
     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 no_interrupts: Thread.threadAttribute list
    23   val regular_interrupts: Thread.threadAttribute list
    24   val with_attributes: Thread.threadAttribute list ->
    25     (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
    26   val self_critical: unit -> bool
    27   val serial: unit -> int
    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 fun max_threads_value () = 1: int;
    41 
    42 val no_interrupts =
    43   [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
    44 
    45 val regular_interrupts =
    46   [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
    47 
    48 fun with_attributes _ f x = f [] x;
    49 
    50 
    51 (* critical section *)
    52 
    53 fun self_critical () = false;
    54 fun NAMED_CRITICAL _ e = e ();
    55 fun CRITICAL e = e ();
    56 
    57 
    58 (* serial numbers *)
    59 
    60 local val count = ref (0: int)
    61 in fun serial () = (count := ! count + 1; ! count) end;
    62 
    63 end;
    64 
    65 structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
    66 open BasicMultithreading;