Quelle thread_attributes.ML Sprache: SML

(*  Title:      Pure/Concurrent/thread_attributes.ML
    Author:     Makarius

Thread attributes for interrupt handling.
*)

signature THREAD_ATTRIBUTES =
sig
  type attributes
  val get_attributes: unit -> attributes
  val set_attributes: attributes -> unit
  val convert_attributes: attributes -> Thread.Thread.threadAttribute list
  val no_interrupts: attributes
  val test_interrupts: attributes
  val public_interrupts: attributes
  val private_interrupts: attributes
  val sync_interrupts: attributes -> attributes
  val safe_interrupts: attributes -> attributes
  val with_attributes: attributes -> (attributes -> 'a) -> 'a
  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
  val uninterruptible_body: ((('b -> 'c) -> 'b -> 'c) -> 'a) -> 'a
end;

structure Thread_Attributes: THREAD_ATTRIBUTES =
struct

abstype attributes = Attributes of Word.word
with

(* thread attributes *)

val thread_attributes = 0w7;

val broadcast = 0w1;

val interrupt_state = 0w6;
val interrupt_defer = 0w0;
val interrupt_synch = 0w2;
val interrupt_asynch = 0w4;
val interrupt_asynch_once = 0w6;

(* access thread flags *)

val thread_flags = 0w1;

fun load_word () : word =
  RunCall.loadWord (RunCall.unsafeCast (Thread.Thread.self ()), thread_flags);

fun get_attributes () = Attributes (Word.andb (load_word (), thread_attributes));

fun set_attributes (Attributes w) =
  let
    val w' = Word.orb (Word.andb (load_word (), Word.notb thread_attributes), w);
    val _ = RunCall.storeWord (RunCall.unsafeCast (Thread.Thread.self ()), thread_flags, w');
  in
    if Word.andb (w', interrupt_asynch) = interrupt_asynch
    then Thread.Thread.testInterrupt () else ()
  end;

fun convert_attributes (Attributes w) =
  [Thread.Thread.EnableBroadcastInterrupt (Word.andb (w, broadcast) = broadcast),
   Thread.Thread.InterruptState
      let val w' = Word.andb (w, interrupt_state) in
        if w' = interrupt_defer then Thread.Thread.InterruptDefer
        else if w' = interrupt_synch then Thread.Thread.InterruptSynch
        else if w' = interrupt_asynch then Thread.Thread.InterruptAsynch
        else Thread.Thread.InterruptAsynchOnce
      end];

(* common configurations *)

val no_interrupts = Attributes interrupt_defer;
val test_interrupts = Attributes interrupt_synch;
val public_interrupts = Attributes (Word.orb (broadcast, interrupt_asynch_once));
val private_interrupts = Attributes interrupt_asynch_once;

fun sync_interrupts (Attributes w) =
  let
    val w' = Word.andb (w, interrupt_state);
    val w'' = Word.andb (w, Word.notb interrupt_state);
  in Attributes (if w' = interrupt_defer then w else Word.orb (w'', interrupt_synch)) end;

fun safe_interrupts (Attributes w) =
  let
    val w' = Word.andb (w, interrupt_state);
    val w'' = Word.andb (w, Word.notb interrupt_state);
  in Attributes (if w' = interrupt_asynch then Word.orb (w'', interrupt_asynch_once) else w) end;

fun with_attributes new_atts e =
  let
    val atts1 = safe_interrupts (get_attributes ());
    val atts2 = safe_interrupts new_atts;
  in
    if atts1 = atts2 then e atts1
    else
      let
        val result = Exn.capture0 (fn () => (set_attributes atts2; e atts1)) ();
        val _ = set_attributes atts1;
      in Exn.release result end
  end;

end;

fun uninterruptible f x =
  with_attributes no_interrupts (fn atts =>
    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);

fun uninterruptible_body body =
  uninterruptible (fn run => fn () => body run) ();

end;

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.