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