src/Pure/Concurrent/simple_thread.ML
author wenzelm
Sat Aug 01 00:09:45 2009 +0200 (2009-08-01)
changeset 32295 400cc493d466
parent 32186 8026b73cd357
child 33220 11a1af478dac
permissions -rw-r--r--
renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
renamed Multithreading.restricted_interrupts to Multithreading.private_interrupts;
added Multithreading.sync_interrupts;
Multithreading.sync_wait: more careful treatment of attributes;
Multithreading.tracing: uninterruptible;
Multithreading.system_out: signal within critical region, more careful sync_wait;
eliminated redundant Thread.testInterrupt;
Future.wait_timeout: uniform Multithreading.sync_wait;
future scheduler: interruptible body (sync!), to improve reactivity;
future_job: reject duplicate assignments -- system error;
misc tuning;
     1 (*  Title:      Pure/Concurrent/simple_thread.ML
     2     Author:     Makarius
     3 
     4 Simplified thread operations.
     5 *)
     6 
     7 signature SIMPLE_THREAD =
     8 sig
     9   val fork: bool -> (unit -> unit) -> Thread.thread
    10   val interrupt: Thread.thread -> unit
    11   val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
    12 end;
    13 
    14 structure SimpleThread: SIMPLE_THREAD =
    15 struct
    16 
    17 fun fork interrupts body =
    18   Thread.fork (fn () => exception_trace (fn () => body ()),
    19     if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
    20 
    21 fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
    22 
    23 
    24 (* basic synchronization *)
    25 
    26 fun synchronized name lock e = Exn.release (uninterruptible (fn restore_attributes => fn () =>
    27   let
    28     val immediate =
    29       if Mutex.trylock lock then true
    30       else
    31         let
    32           val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
    33           val time = Multithreading.real_time Mutex.lock lock;
    34           val _ = Multithreading.tracing_time true time
    35             (fn () => name ^ ": locked after " ^ Time.toString time);
    36         in false end;
    37     val result = Exn.capture (restore_attributes e) ();
    38     val _ =
    39       if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ...");
    40     val _ = Mutex.unlock lock;
    41   in result end) ());
    42 
    43 end;