src/Pure/Concurrent/simple_thread.ML
author haftmann
Thu Oct 22 13:48:06 2009 +0200 (2009-10-22)
changeset 33063 4d462963a7db
parent 32295 400cc493d466
child 33220 11a1af478dac
permissions -rw-r--r--
map_range (and map_index) combinator
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@32295
    19
    if interrupts then Multithreading.public_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 _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
wenzelm@32185
    33
          val time = Multithreading.real_time Mutex.lock lock;
wenzelm@32186
    34
          val _ = Multithreading.tracing_time true time
wenzelm@32185
    35
            (fn () => name ^ ": locked after " ^ Time.toString time);
wenzelm@32184
    36
        in false end;
wenzelm@28577
    37
    val result = Exn.capture (restore_attributes e) ();
wenzelm@32051
    38
    val _ =
wenzelm@32184
    39
      if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ...");
wenzelm@28577
    40
    val _ = Mutex.unlock lock;
wenzelm@28577
    41
  in result end) ());
wenzelm@28577
    42
wenzelm@28241
    43
end;