-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathKHeap_A.thy
261 lines (207 loc) · 8.78 KB
/
KHeap_A.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
(*
* Copyright 2014, General Dynamics C4 Systems
*
* SPDX-License-Identifier: GPL-2.0-only
*)
(*
Functions to access kernel memory.
*)
chapter \<open>Accessing the Kernel Heap\<close>
theory KHeap_A
imports Exceptions_A
begin
text \<open>This theory gives auxiliary getter and setter methods
for kernel objects.\<close>
section "General Object Access"
definition
get_object :: "obj_ref \<Rightarrow> (kernel_object,'z::state_ext) s_monad"
where
"get_object ptr \<equiv> do
kh \<leftarrow> gets kheap;
assert (kh ptr \<noteq> None);
return $ the $ kh ptr
od"
definition
set_object :: "obj_ref \<Rightarrow> kernel_object \<Rightarrow> (unit,'z::state_ext) s_monad"
where
"set_object ptr obj \<equiv> do
kobj <- get_object ptr;
assert (a_type kobj = a_type obj);
s \<leftarrow> get;
put (s\<lparr>kheap := kheap s(ptr \<mapsto> obj)\<rparr>)
od"
section "TCBs"
definition
get_tcb :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> tcb option"
where
"get_tcb tcb_ref state \<equiv>
case kheap state tcb_ref of
None \<Rightarrow> None
| Some kobj \<Rightarrow> (case kobj of
TCB tcb \<Rightarrow> Some tcb
| _ \<Rightarrow> None)"
definition
thread_get :: "(tcb \<Rightarrow> 'a) \<Rightarrow> obj_ref \<Rightarrow> ('a,'z::state_ext) s_monad"
where
"thread_get f tptr \<equiv> do
tcb \<leftarrow> gets_the $ get_tcb tptr;
return $ f tcb
od"
definition
thread_set :: "(tcb \<Rightarrow> tcb) \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
where
"thread_set f tptr \<equiv> do
tcb \<leftarrow> gets_the $ get_tcb tptr;
set_object tptr $ TCB $ f tcb
od"
definition
arch_thread_get :: "(arch_tcb \<Rightarrow> 'a) \<Rightarrow> obj_ref \<Rightarrow> ('a,'z::state_ext) s_monad"
where
"arch_thread_get f tptr \<equiv> do
tcb \<leftarrow> gets_the $ get_tcb tptr;
return $ f (tcb_arch tcb)
od"
definition
arch_thread_set :: "(arch_tcb \<Rightarrow> arch_tcb) \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
where
"arch_thread_set f tptr \<equiv> do
tcb \<leftarrow> gets_the $ get_tcb tptr;
set_object tptr $ TCB $ tcb \<lparr> tcb_arch := f (tcb_arch tcb) \<rparr>
od"
definition
get_thread_state :: "obj_ref \<Rightarrow> (thread_state,'z::state_ext) s_monad"
where
"get_thread_state ref \<equiv> thread_get tcb_state ref"
definition
get_bound_notification :: "obj_ref \<Rightarrow> (obj_ref option,'z::state_ext) s_monad"
where
"get_bound_notification ref \<equiv> thread_get tcb_bound_notification ref"
definition
set_bound_notification :: "obj_ref \<Rightarrow> obj_ref option \<Rightarrow> (unit, 'z::state_ext) s_monad"
where
"set_bound_notification ref ntfn \<equiv> do
tcb \<leftarrow> gets_the $ get_tcb ref;
set_object ref (TCB (tcb \<lparr> tcb_bound_notification := ntfn \<rparr>))
od"
definition set_thread_state_ext :: "obj_ref \<Rightarrow> unit det_ext_monad" where
"set_thread_state_ext t \<equiv> do
ts \<leftarrow> get_thread_state t;
cur \<leftarrow> gets cur_thread;
action \<leftarrow> gets scheduler_action;
when (\<not> (runnable ts) \<and> cur = t \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od"
definition
set_thread_state :: "obj_ref \<Rightarrow> thread_state \<Rightarrow> (unit,'z::state_ext) s_monad"
where
"set_thread_state ref ts \<equiv> do
tcb \<leftarrow> gets_the $ get_tcb ref;
set_object ref (TCB (tcb \<lparr> tcb_state := ts \<rparr>));
do_extended_op (set_thread_state_ext ref)
od"
definition
set_priority :: "obj_ref \<Rightarrow> priority \<Rightarrow> unit det_ext_monad" where
"set_priority tptr prio \<equiv> do
tcb_sched_action tcb_sched_dequeue tptr;
thread_set_priority tptr prio;
ts \<leftarrow> get_thread_state tptr;
when (runnable ts) $ do
cur \<leftarrow> gets cur_thread;
if tptr = cur then reschedule_required else possible_switch_to tptr
od
od"
definition
set_mcpriority :: "obj_ref \<Rightarrow> priority \<Rightarrow> (unit, 'z::state_ext) s_monad" where
"set_mcpriority ref mcp \<equiv> thread_set (\<lambda>tcb. tcb\<lparr>tcb_mcpriority:=mcp\<rparr>) ref "
section "simple kernel objects"
(* to be used for abstraction unifying kernel objects other than TCB and CNode *)
definition
partial_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a option)"
where
"partial_inv f x = (if \<exists>!y. f y = x then Some (THE y. f y = x) else None)"
lemma proj_inj: "inj f \<Longrightarrow> (partial_inv f ko = Some v) = (f v = ko)"
by (auto simp: partial_inv_def the_equality injD)
lemma inj_Endpoint: "inj Endpoint" by (auto intro: injI)
lemma inj_Notification: "inj Notification" by (auto intro: injI)
lemmas proj_inj_ep[simp] = proj_inj[OF inj_Endpoint]
lemma proj_ko_type_ep[simp]: "(\<exists>v. partial_inv Endpoint ko = Some (v::endpoint)) = (a_type ko = AEndpoint)"
by (cases ko; auto simp: partial_inv_def a_type_def)
lemmas proj_inj_ntfn[simp] = proj_inj[OF inj_Notification]
lemma proj_ko_type_ntfn[simp]:
"(\<exists>v. partial_inv Notification ko = Some (v::notification)) = (a_type ko = ANTFN)"
by (cases ko; auto simp: partial_inv_def a_type_def)
abbreviation
"is_simple_type \<equiv> (\<lambda>ob. a_type ob \<in> {AEndpoint, ANTFN})"
definition
get_simple_ko :: "('a \<Rightarrow> kernel_object) \<Rightarrow> obj_ref \<Rightarrow> ('a,'z::state_ext) s_monad"
where
"get_simple_ko f ptr \<equiv> do
kobj \<leftarrow> get_object ptr;
assert (is_simple_type kobj);
(case partial_inv f kobj of Some e \<Rightarrow> return e | _ \<Rightarrow> fail)
od"
definition
set_simple_ko :: "('a \<Rightarrow> kernel_object) \<Rightarrow> obj_ref \<Rightarrow> 'a \<Rightarrow> (unit,'z::state_ext) s_monad"
where
"set_simple_ko f ptr ep \<equiv> do
obj \<leftarrow> get_object ptr;
assert (is_simple_type obj);
assert (partial_inv f obj \<noteq> None);
set_object ptr (f ep)
od"
section \<open>Synchronous and Asyncronous Endpoints\<close>
abbreviation
get_endpoint :: "obj_ref \<Rightarrow> (endpoint,'z::state_ext) s_monad" where
"get_endpoint \<equiv> get_simple_ko Endpoint"
abbreviation
set_endpoint :: "obj_ref \<Rightarrow> endpoint \<Rightarrow> (unit,'z::state_ext) s_monad" where
"set_endpoint \<equiv> set_simple_ko Endpoint"
abbreviation
get_notification :: "obj_ref \<Rightarrow> (notification,'z::state_ext) s_monad" where
"get_notification \<equiv> get_simple_ko Notification"
abbreviation
set_notification :: "obj_ref \<Rightarrow> notification \<Rightarrow> (unit,'z::state_ext) s_monad" where
"set_notification \<equiv> set_simple_ko Notification"
abbreviation
ntfn_set_bound_tcb :: "notification \<Rightarrow> obj_ref option \<Rightarrow> notification" where
"ntfn_set_bound_tcb ntfn t \<equiv> ntfn \<lparr> ntfn_bound_tcb := t \<rparr>"
abbreviation
ntfn_set_obj :: "notification \<Rightarrow> ntfn \<Rightarrow> notification" where
"ntfn_set_obj ntfn a \<equiv> ntfn \<lparr> ntfn_obj := a \<rparr>"
section \<open>IRQ State and Slot\<close>
definition
get_irq_state :: "irq \<Rightarrow> (irq_state,'z::state_ext) s_monad" where
"get_irq_state irq \<equiv> gets (\<lambda>s. interrupt_states s irq)"
definition
set_irq_state :: "irq_state \<Rightarrow> irq \<Rightarrow> (unit,'z::state_ext) s_monad" where
"set_irq_state state irq \<equiv> do
modify (\<lambda>s. s \<lparr> interrupt_states := (interrupt_states s) (irq := state)\<rparr>);
do_machine_op $ maskInterrupt (state = IRQInactive) irq
od"
definition
get_irq_slot :: "irq \<Rightarrow> (cslot_ptr,'z::state_ext) s_monad" where
"get_irq_slot irq \<equiv> gets (\<lambda>st. (interrupt_irq_node st irq, []))"
text \<open>Tests whether an IRQ identifier is in use.\<close>
definition
is_irq_active :: "irq \<Rightarrow> (bool,'z::state_ext) s_monad" where
"is_irq_active irq \<equiv> liftM (\<lambda>st. st \<noteq> IRQInactive) $ get_irq_state irq"
section "User Context"
text \<open>
Changes user context of specified thread by running
specified user monad.
\<close>
definition
as_user :: "obj_ref \<Rightarrow> 'a user_monad \<Rightarrow> ('a,'z::state_ext) s_monad"
where
"as_user tptr f \<equiv> do
tcb \<leftarrow> gets_the $ get_tcb tptr;
uc \<leftarrow> return $ arch_tcb_context_get (tcb_arch tcb);
(a, uc') \<leftarrow> select_f $ f uc;
new_tcb \<leftarrow> return $ tcb \<lparr> tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>;
set_object tptr (TCB new_tcb);
return a
od"
text \<open>Raise an exception if a property does not hold.\<close>
definition
throw_on_false :: "'e \<Rightarrow> (bool,'z::state_ext) s_monad \<Rightarrow> ('e + unit,'z::state_ext) s_monad" where
"throw_on_false ex f \<equiv> doE v \<leftarrow> liftE f; unlessE v $ throwError ex odE"
end