src/Pure/ML-Systems/multithreading.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 32777 8ae3a48c69d9
child 39616 8052101883c3
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
     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 available: bool
    17   val max_threads: int Unsynchronized.ref
    18   val max_threads_value: unit -> int
    19   val enabled: unit -> bool
    20   val no_interrupts: Thread.threadAttribute list
    21   val public_interrupts: Thread.threadAttribute list
    22   val private_interrupts: Thread.threadAttribute list
    23   val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
    24   val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
    25   val sync_wait: Thread.threadAttribute list option -> Time.time option ->
    26     ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
    27   val trace: int Unsynchronized.ref
    28   val tracing: int -> (unit -> string) -> unit
    29   val tracing_time: bool -> Time.time -> (unit -> string) -> unit
    30   val real_time: ('a -> unit) -> 'a -> Time.time
    31   val self_critical: unit -> bool
    32   val serial: unit -> int
    33 end;
    34 
    35 structure Multithreading: MULTITHREADING =
    36 struct
    37 
    38 (* options *)
    39 
    40 val available = false;
    41 val max_threads = Unsynchronized.ref (1: int);
    42 fun max_threads_value () = 1: int;
    43 fun enabled () = false;
    44 
    45 
    46 (* attributes *)
    47 
    48 val no_interrupts = [];
    49 val public_interrupts = [];
    50 val private_interrupts = [];
    51 fun sync_interrupts _ = [];
    52 
    53 fun with_attributes _ e = e [];
    54 
    55 fun sync_wait _ _ _ _ = Exn.Result true;
    56 
    57 
    58 (* tracing *)
    59 
    60 val trace = Unsynchronized.ref (0: int);
    61 fun tracing _ _ = ();
    62 fun tracing_time _ _ _ = ();
    63 fun real_time f x = (f x; Time.zeroTime);
    64 
    65 
    66 (* critical section *)
    67 
    68 fun self_critical () = false;
    69 fun NAMED_CRITICAL _ e = e ();
    70 fun CRITICAL e = e ();
    71 
    72 
    73 (* serial numbers *)
    74 
    75 local val count = Unsynchronized.ref (0: int)
    76 in fun serial () = (count := ! count + 1; ! count) end;
    77 
    78 end;
    79 
    80 structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
    81 open Basic_Multithreading;