src/Pure/ML-Systems/multithreading.ML
author wenzelm
Sat Jul 25 00:39:05 2009 +0200 (2009-07-25)
changeset 32185 57ecfab3bcfe
parent 32184 cfa0ef0c0c5f
child 32186 8026b73cd357
permissions -rw-r--r--
added Multithreading.real_time;
     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 tracing_time: Time.time -> (unit -> string) -> unit
    19   val real_time: ('a -> unit) -> 'a -> Time.time
    20   val available: bool
    21   val max_threads: int ref
    22   val max_threads_value: unit -> int
    23   val enabled: unit -> bool
    24   val no_interrupts: Thread.threadAttribute list
    25   val regular_interrupts: Thread.threadAttribute list
    26   val restricted_interrupts: Thread.threadAttribute list
    27   val with_attributes: Thread.threadAttribute list ->
    28     (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
    29   val self_critical: unit -> bool
    30   val serial: unit -> int
    31 end;
    32 
    33 structure Multithreading: MULTITHREADING =
    34 struct
    35 
    36 (* tracing *)
    37 
    38 val trace = ref (0: int);
    39 fun tracing _ _ = ();
    40 fun tracing_time _ _ = ();
    41 fun real_time f x = (f x; Time.zeroTime);
    42 
    43 
    44 (* options *)
    45 
    46 val available = false;
    47 val max_threads = ref (1: int);
    48 fun max_threads_value () = 1: int;
    49 fun enabled () = false;
    50 
    51 val no_interrupts =
    52   [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
    53 
    54 val regular_interrupts =
    55   [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
    56 
    57 val restricted_interrupts =
    58   [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
    59 
    60 fun with_attributes _ f x = f [] x;
    61 
    62 
    63 (* critical section *)
    64 
    65 fun self_critical () = false;
    66 fun NAMED_CRITICAL _ e = e ();
    67 fun CRITICAL e = e ();
    68 
    69 
    70 (* serial numbers *)
    71 
    72 local val count = ref (0: int)
    73 in fun serial () = (count := ! count + 1; ! count) end;
    74 
    75 end;
    76 
    77 structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
    78 open BasicMultithreading;