author | wenzelm |
Tue, 26 Sep 2023 14:42:33 +0200 | |
changeset 78720 | 909dc00766a0 |
parent 78715 | 9506b852ebdf |
permissions | -rw-r--r-- |
62923 | 1 |
(* Title: Pure/Concurrent/thread_attributes.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Thread attributes for interrupt handling. |
|
5 |
*) |
|
6 |
||
7 |
signature THREAD_ATTRIBUTES = |
|
8 |
sig |
|
64557
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
9 |
type attributes |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
10 |
val get_attributes: unit -> attributes |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
11 |
val set_attributes: attributes -> unit |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
12 |
val convert_attributes: attributes -> Thread.Thread.threadAttribute list |
62923 | 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 |
|
78720 | 21 |
val uninterruptible_body: ((('b -> 'c) -> 'b -> 'c) -> 'a) -> 'a |
62923 | 22 |
end; |
23 |
||
24 |
structure Thread_Attributes: THREAD_ATTRIBUTES = |
|
25 |
struct |
|
26 |
||
64557
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
27 |
abstype attributes = Attributes of Word.word |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
28 |
with |
62923 | 29 |
|
64557
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
30 |
(* thread attributes *) |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
31 |
|
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
32 |
val thread_attributes = 0w7; |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
33 |
|
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
34 |
val broadcast = 0w1; |
62923 | 35 |
|
64557
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
36 |
val interrupt_state = 0w6; |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
37 |
val interrupt_defer = 0w0; |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
38 |
val interrupt_synch = 0w2; |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
39 |
val interrupt_asynch = 0w4; |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
40 |
val interrupt_asynch_once = 0w6; |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
41 |
|
62923 | 42 |
|
64557
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
43 |
(* access thread flags *) |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
44 |
|
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
45 |
val thread_flags = 0w1; |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
46 |
|
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
47 |
fun load_word () : word = |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
48 |
RunCall.loadWord (RunCall.unsafeCast (Thread.Thread.self ()), thread_flags); |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
49 |
|
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
50 |
fun get_attributes () = Attributes (Word.andb (load_word (), thread_attributes)); |
62923 | 51 |
|
64557
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
52 |
fun set_attributes (Attributes w) = |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
53 |
let |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
54 |
val w' = Word.orb (Word.andb (load_word (), Word.notb thread_attributes), w); |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
55 |
val _ = RunCall.storeWord (RunCall.unsafeCast (Thread.Thread.self ()), thread_flags, w'); |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
56 |
in |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
57 |
if Word.andb (w', interrupt_asynch) = interrupt_asynch |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
58 |
then Thread.Thread.testInterrupt () else () |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
59 |
end; |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
60 |
|
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
61 |
fun convert_attributes (Attributes w) = |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
62 |
[Thread.Thread.EnableBroadcastInterrupt (Word.andb (w, broadcast) = broadcast), |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
63 |
Thread.Thread.InterruptState |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
64 |
let val w' = Word.andb (w, interrupt_state) in |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
65 |
if w' = interrupt_defer then Thread.Thread.InterruptDefer |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
66 |
else if w' = interrupt_synch then Thread.Thread.InterruptSynch |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
67 |
else if w' = interrupt_asynch then Thread.Thread.InterruptAsynch |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
68 |
else Thread.Thread.InterruptAsynchOnce |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
69 |
end]; |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
70 |
|
62923 | 71 |
|
64557
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
72 |
(* common configurations *) |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
73 |
|
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
74 |
val no_interrupts = Attributes interrupt_defer; |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
75 |
val test_interrupts = Attributes interrupt_synch; |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
76 |
val public_interrupts = Attributes (Word.orb (broadcast, interrupt_asynch_once)); |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
77 |
val private_interrupts = Attributes interrupt_asynch_once; |
62923 | 78 |
|
64557
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
79 |
fun sync_interrupts (Attributes w) = |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
80 |
let |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
81 |
val w' = Word.andb (w, interrupt_state); |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
82 |
val w'' = Word.andb (w, Word.notb interrupt_state); |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
83 |
in Attributes (if w' = interrupt_defer then w else Word.orb (w'', interrupt_synch)) end; |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
84 |
|
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
85 |
fun safe_interrupts (Attributes w) = |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
86 |
let |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
87 |
val w' = Word.andb (w, interrupt_state); |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
88 |
val w'' = Word.andb (w, Word.notb interrupt_state); |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
89 |
in Attributes (if w' = interrupt_asynch then Word.orb (w'', interrupt_asynch_once) else w) end; |
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62924
diff
changeset
|
90 |
|
62923 | 91 |
fun with_attributes new_atts e = |
92 |
let |
|
64564 | 93 |
val atts1 = safe_interrupts (get_attributes ()); |
94 |
val atts2 = safe_interrupts new_atts; |
|
95 |
in |
|
96 |
if atts1 = atts2 then e atts1 |
|
97 |
else |
|
98 |
let |
|
78715
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78713
diff
changeset
|
99 |
val result = Exn.capture0 (fn () => (set_attributes atts2; e atts1)) (); |
64564 | 100 |
val _ = set_attributes atts1; |
101 |
in Exn.release result end |
|
102 |
end; |
|
103 |
||
104 |
end; |
|
62923 | 105 |
|
106 |
fun uninterruptible f x = |
|
107 |
with_attributes no_interrupts (fn atts => |
|
108 |
f (fn g => fn y => with_attributes atts (fn _ => g y)) x); |
|
109 |
||
78720 | 110 |
fun uninterruptible_body body = |
111 |
uninterruptible (fn run => fn () => body run) (); |
|
112 |
||
62923 | 113 |
end; |