src/Pure/ML-Systems/multithreading.ML
author wenzelm
Fri Mar 20 20:20:09 2009 +0100 (2009-03-20 ago)
changeset 30612 cb6421b6a18f
parent 29564 f8b933a62151
child 32184 cfa0ef0c0c5f
permissions -rw-r--r--
future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
     1 (*  Title:      Pure/ML-Systems/multithreading.ML
     2     Author:     Makarius
     3 
     4 Dummy implementation of multithreading setup.
     5 *)
     6 
     7 signature BASIC_MULTITHREADING =
     8 sig
     9   val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
    10   val CRITICAL: (unit -> 'a) -> 'a
    11 end;
    12 
    13 signature MULTITHREADING =
    14 sig
    15   include BASIC_MULTITHREADING
    16   val trace: int ref
    17   val tracing: int -> (unit -> string) -> unit
    18   val available: bool
    19   val max_threads: int ref
    20   val max_threads_value: unit -> int
    21   val enabled: unit -> bool
    22   val no_interrupts: Thread.threadAttribute list
    23   val regular_interrupts: Thread.threadAttribute list
    24   val restricted_interrupts: Thread.threadAttribute list
    25   val with_attributes: Thread.threadAttribute list ->
    26     (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
    27   val self_critical: unit -> bool
    28   val serial: unit -> int
    29 end;
    30 
    31 structure Multithreading: MULTITHREADING =
    32 struct
    33 
    34 (* options *)
    35 
    36 val trace = ref (0: int);
    37 fun tracing _ _ = ();
    38 
    39 val available = false;
    40 val max_threads = ref (1: int);
    41 fun max_threads_value () = 1: int;
    42 fun enabled () = false;
    43 
    44 val no_interrupts =
    45   [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
    46 
    47 val regular_interrupts =
    48   [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
    49 
    50 val restricted_interrupts =
    51   [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
    52 
    53 fun with_attributes _ f x = f [] x;
    54 
    55 
    56 (* critical section *)
    57 
    58 fun self_critical () = false;
    59 fun NAMED_CRITICAL _ e = e ();
    60 fun CRITICAL e = e ();
    61 
    62 
    63 (* serial numbers *)
    64 
    65 local val count = ref (0: int)
    66 in fun serial () = (count := ! count + 1; ! count) end;
    67 
    68 end;
    69 
    70 structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
    71 open BasicMultithreading;