1(*  Title:      Pure/Concurrent/thread_attributes.ML
2    Author:     Makarius
3
4Thread attributes for interrupt handling.
5*)
6
7signature THREAD_ATTRIBUTES =
8sig
9  type attributes
10  val get_attributes: unit -> attributes
11  val set_attributes: attributes -> unit
12  val convert_attributes: attributes -> Thread.Thread.threadAttribute list
13  val no_interrupts: attributes
14  val test_interrupts: attributes
15  val public_interrupts: attributes
16  val private_interrupts: attributes
17  val sync_interrupts: attributes -> attributes
18  val safe_interrupts: attributes -> attributes
19  val with_attributes: attributes -> (attributes -> 'a) -> 'a
20  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
21  val expose_interrupt: unit -> unit  (*exception Interrupt*)
22end;
23
24structure Thread_Attributes: THREAD_ATTRIBUTES =
25struct
26
27abstype attributes = Attributes of Word.word
28with
29
30(* thread attributes *)
31
32val thread_attributes = 0w7;
33
34val broadcast = 0w1;
35
36val interrupt_state = 0w6;
37val interrupt_defer = 0w0;
38val interrupt_synch = 0w2;
39val interrupt_asynch = 0w4;
40val interrupt_asynch_once = 0w6;
41
42
43(* access thread flags *)
44
45val thread_flags = 0w1;
46
47fun load_word () : word =
48  RunCall.loadWord (RunCall.unsafeCast (Thread.Thread.self ()), thread_flags);
49
50fun get_attributes () = Attributes (Word.andb (load_word (), thread_attributes));
51
52fun set_attributes (Attributes w) =
53  let
54    val w' = Word.orb (Word.andb (load_word (), Word.notb thread_attributes), w);
55    val _ = RunCall.storeWord (RunCall.unsafeCast (Thread.Thread.self ()), thread_flags, w');
56  in
57    if Word.andb (w', interrupt_asynch) = interrupt_asynch
58    then Thread.Thread.testInterrupt () else ()
59  end;
60
61fun convert_attributes (Attributes w) =
62  [Thread.Thread.EnableBroadcastInterrupt (Word.andb (w, broadcast) = broadcast),
63   Thread.Thread.InterruptState
64      let val w' = Word.andb (w, interrupt_state) in
65        if w' = interrupt_defer then Thread.Thread.InterruptDefer
66        else if w' = interrupt_synch then Thread.Thread.InterruptSynch
67        else if w' = interrupt_asynch then Thread.Thread.InterruptAsynch
68        else Thread.Thread.InterruptAsynchOnce
69      end];
70
71
72(* common configurations *)
73
74val no_interrupts = Attributes interrupt_defer;
75val test_interrupts = Attributes interrupt_synch;
76val public_interrupts = Attributes (Word.orb (broadcast, interrupt_asynch_once));
77val private_interrupts = Attributes interrupt_asynch_once;
78
79fun sync_interrupts (Attributes w) =
80  let
81    val w' = Word.andb (w, interrupt_state);
82    val w'' = Word.andb (w, Word.notb interrupt_state);
83  in Attributes (if w' = interrupt_defer then w else Word.orb (w'', interrupt_synch)) end;
84
85fun safe_interrupts (Attributes w) =
86  let
87    val w' = Word.andb (w, interrupt_state);
88    val w'' = Word.andb (w, Word.notb interrupt_state);
89  in Attributes (if w' = interrupt_asynch then Word.orb (w'', interrupt_asynch_once) else w) end;
90
91fun with_attributes new_atts e =
92  let
93    val atts1 = get_attributes ()
94    val atts2 = safe_interrupts new_atts
95  in
96    if atts1 = atts2 then e atts1
97    else
98      let
99        val result = Exn.capture (fn () => (set_attributes atts2; e atts1)) ();
100        val _ = set_attributes atts1;
101      in Exn.release result end
102  end;
103
104end;
105
106fun uninterruptible f x =
107  with_attributes no_interrupts (fn atts =>
108    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
109
110fun expose_interrupt () =
111  let
112    val orig_atts = safe_interrupts (get_attributes ());
113    val _ = set_attributes test_interrupts;
114    val test = Exn.capture Thread.Thread.testInterrupt ();
115    val _ = set_attributes orig_atts;
116  in Exn.release test end;
117
118end;
119