src/Pure/Concurrent/simple_thread.ML
author wenzelm
Sat Jul 25 00:13:39 2009 +0200 (2009-07-25)
changeset 32184 cfa0ef0c0c5f
parent 32051 82a9875b8707
child 32185 57ecfab3bcfe
permissions -rw-r--r--
simplified/unified Multithreading.tracing_time;
tuned;
wenzelm@28241
     1
(*  Title:      Pure/Concurrent/simple_thread.ML
wenzelm@28241
     2
    Author:     Makarius
wenzelm@28241
     3
wenzelm@28577
     4
Simplified thread operations.
wenzelm@28241
     5
*)
wenzelm@28241
     6
wenzelm@28241
     7
signature SIMPLE_THREAD =
wenzelm@28241
     8
sig
wenzelm@28241
     9
  val fork: bool -> (unit -> unit) -> Thread.thread
wenzelm@28550
    10
  val interrupt: Thread.thread -> unit
wenzelm@28577
    11
  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
wenzelm@28241
    12
end;
wenzelm@28241
    13
wenzelm@28241
    14
structure SimpleThread: SIMPLE_THREAD =
wenzelm@28241
    15
struct
wenzelm@28241
    16
wenzelm@28241
    17
fun fork interrupts body =
wenzelm@28241
    18
  Thread.fork (fn () => exception_trace (fn () => body ()),
wenzelm@28241
    19
    if interrupts then Multithreading.regular_interrupts else Multithreading.no_interrupts);
wenzelm@28241
    20
wenzelm@28550
    21
fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
wenzelm@28550
    22
wenzelm@28577
    23
wenzelm@28577
    24
(* basic synchronization *)
wenzelm@28577
    25
wenzelm@28577
    26
fun synchronized name lock e = Exn.release (uninterruptible (fn restore_attributes => fn () =>
wenzelm@28577
    27
  let
wenzelm@32051
    28
    val immediate =
wenzelm@32051
    29
      if Mutex.trylock lock then true
wenzelm@28577
    30
      else
wenzelm@32184
    31
        let
wenzelm@32184
    32
          val timer = Timer.startRealTimer ();
wenzelm@32184
    33
          val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
wenzelm@32184
    34
          val _ = Mutex.lock lock;
wenzelm@32184
    35
          val time = Timer.checkRealTimer timer;
wenzelm@32184
    36
          val _ = Multithreading.tracing_time time (fn () =>
wenzelm@32184
    37
            name ^ ": locked after " ^ Time.toString time);
wenzelm@32184
    38
        in false end;
wenzelm@28577
    39
    val result = Exn.capture (restore_attributes e) ();
wenzelm@32051
    40
    val _ =
wenzelm@32184
    41
      if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ...");
wenzelm@28577
    42
    val _ = Mutex.unlock lock;
wenzelm@28577
    43
  in result end) ());
wenzelm@28577
    44
wenzelm@28241
    45
end;