85
|
1 |
section {*
|
|
2 |
This file contains lemmas used to guide the recalculation of current precedence
|
|
3 |
after every system call (or system operation)
|
|
4 |
*}
|
105
|
5 |
theory Implementation
|
|
6 |
imports PIPBasics
|
85
|
7 |
begin
|
|
8 |
|
|
9 |
text {* (* ddd *)
|
|
10 |
One beauty of our modelling is that we follow the definitional extension tradition of HOL.
|
|
11 |
The benefit of such a concise and miniature model is that large number of intuitively
|
|
12 |
obvious facts are derived as lemmas, rather than asserted as axioms.
|
|
13 |
*}
|
|
14 |
|
|
15 |
text {*
|
|
16 |
However, the lemmas in the forthcoming several locales are no longer
|
|
17 |
obvious. These lemmas show how the current precedences should be recalculated
|
|
18 |
after every execution step (in our model, every step is represented by an event,
|
|
19 |
which in turn, represents a system call, or operation). Each operation is
|
|
20 |
treated in a separate locale.
|
|
21 |
|
|
22 |
The complication of current precedence recalculation comes
|
|
23 |
because the changing of RAG needs to be taken into account,
|
|
24 |
in addition to the changing of precedence.
|
|
25 |
|
|
26 |
The reason RAG changing affects current precedence is that,
|
|
27 |
according to the definition, current precedence
|
|
28 |
of a thread is the maximum of the precedences of every threads in its subtree,
|
|
29 |
where the notion of sub-tree in RAG is defined in RTree.thy.
|
|
30 |
|
|
31 |
Therefore, for each operation, lemmas about the change of precedences
|
|
32 |
and RAG are derived first, on which lemmas about current precedence
|
|
33 |
recalculation are based on.
|
|
34 |
*}
|
|
35 |
|
|
36 |
section {* The @{term Set} operation *}
|
|
37 |
|
|
38 |
context valid_trace_set
|
|
39 |
begin
|
|
40 |
|
|
41 |
text {* (* ddd *)
|
|
42 |
The following two lemmas confirm that @{text "Set"}-operation
|
|
43 |
only changes the precedence of the initiating thread (or actor)
|
|
44 |
of the operation (or event).
|
|
45 |
*}
|
|
46 |
|
|
47 |
|
|
48 |
lemma eq_preced:
|
|
49 |
assumes "th' \<noteq> th"
|
|
50 |
shows "preced th' (e#s) = preced th' s"
|
|
51 |
proof -
|
|
52 |
from assms show ?thesis
|
|
53 |
by (unfold is_set, auto simp:preced_def)
|
|
54 |
qed
|
|
55 |
|
|
56 |
lemma eq_the_preced:
|
|
57 |
assumes "th' \<noteq> th"
|
|
58 |
shows "the_preced (e#s) th' = the_preced s th'"
|
|
59 |
using assms
|
|
60 |
by (unfold the_preced_def, intro eq_preced, simp)
|
|
61 |
|
|
62 |
|
|
63 |
text {* (* ddd *)
|
|
64 |
Th following lemma @{text "eq_cp_pre"} says that the priority change of @{text "th"}
|
|
65 |
only affects those threads, which as @{text "Th th"} in their sub-trees.
|
|
66 |
|
|
67 |
The proof of this lemma is simplified by using the alternative definition
|
|
68 |
of @{text "cp"}.
|
|
69 |
*}
|
|
70 |
|
|
71 |
lemma eq_cp_pre:
|
|
72 |
assumes nd: "Th th \<notin> subtree (RAG s) (Th th')"
|
|
73 |
shows "cp (e#s) th' = cp s th'"
|
|
74 |
proof -
|
|
75 |
-- {* After unfolding using the alternative definition, elements
|
|
76 |
affecting the @{term "cp"}-value of threads become explicit.
|
|
77 |
We only need to prove the following: *}
|
|
78 |
have "Max (the_preced (e#s) ` {th'a. Th th'a \<in> subtree (RAG (e#s)) (Th th')}) =
|
|
79 |
Max (the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')})"
|
|
80 |
(is "Max (?f ` ?S1) = Max (?g ` ?S2)")
|
|
81 |
proof -
|
|
82 |
-- {* The base sets are equal. *}
|
|
83 |
have "?S1 = ?S2" using RAG_unchanged by simp
|
|
84 |
-- {* The function values on the base set are equal as well. *}
|
|
85 |
moreover have "\<forall> e \<in> ?S2. ?f e = ?g e"
|
|
86 |
proof
|
|
87 |
fix th1
|
|
88 |
assume "th1 \<in> ?S2"
|
|
89 |
with nd have "th1 \<noteq> th" by (auto)
|
|
90 |
from eq_the_preced[OF this]
|
|
91 |
show "the_preced (e#s) th1 = the_preced s th1" .
|
|
92 |
qed
|
|
93 |
-- {* Therefore, the image of the functions are equal. *}
|
|
94 |
ultimately have "(?f ` ?S1) = (?g ` ?S2)" by (auto intro!:f_image_eq)
|
|
95 |
thus ?thesis by simp
|
|
96 |
qed
|
|
97 |
thus ?thesis by (simp add:cp_alt_def)
|
|
98 |
qed
|
|
99 |
|
|
100 |
text {*
|
|
101 |
The following lemma shows that @{term "th"} is not in the
|
|
102 |
sub-tree of any other thread.
|
|
103 |
*}
|
|
104 |
lemma th_in_no_subtree:
|
|
105 |
assumes "th' \<noteq> th"
|
|
106 |
shows "Th th \<notin> subtree (RAG s) (Th th')"
|
|
107 |
proof -
|
|
108 |
from readys_in_no_subtree[OF th_ready_s assms(1)]
|
|
109 |
show ?thesis by blast
|
|
110 |
qed
|
|
111 |
|
|
112 |
text {*
|
|
113 |
By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"},
|
|
114 |
it is obvious that the change of priority only affects the @{text "cp"}-value
|
|
115 |
of the initiating thread @{text "th"}.
|
|
116 |
*}
|
|
117 |
lemma eq_cp:
|
|
118 |
assumes "th' \<noteq> th"
|
|
119 |
shows "cp (e#s) th' = cp s th'"
|
|
120 |
by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]])
|
|
121 |
|
|
122 |
end
|
|
123 |
|
|
124 |
section {* The @{term V} operation *}
|
|
125 |
|
|
126 |
text {*
|
|
127 |
The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.
|
|
128 |
*}
|
|
129 |
|
|
130 |
|
|
131 |
context valid_trace_v
|
|
132 |
begin
|
|
133 |
|
|
134 |
lemma ancestors_th: "ancestors (RAG s) (Th th) = {}"
|
|
135 |
proof -
|
|
136 |
from readys_root[OF th_ready_s]
|
|
137 |
show ?thesis
|
|
138 |
by (unfold root_def, simp)
|
|
139 |
qed
|
|
140 |
|
|
141 |
lemma edge_of_th:
|
|
142 |
"(Cs cs, Th th) \<in> RAG s"
|
|
143 |
proof -
|
|
144 |
from holding_th_cs_s
|
|
145 |
show ?thesis
|
|
146 |
by (unfold s_RAG_def holding_eq, auto)
|
|
147 |
qed
|
|
148 |
|
|
149 |
lemma ancestors_cs:
|
|
150 |
"ancestors (RAG s) (Cs cs) = {Th th}"
|
|
151 |
proof -
|
|
152 |
have "ancestors (RAG s) (Cs cs) = ancestors (RAG s) (Th th) \<union> {Th th}"
|
|
153 |
by (rule rtree_RAG.ancestors_accum[OF edge_of_th])
|
|
154 |
from this[unfolded ancestors_th] show ?thesis by simp
|
|
155 |
qed
|
|
156 |
|
|
157 |
end
|
|
158 |
|
|
159 |
text {*
|
|
160 |
The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation,
|
|
161 |
which represents the case when there is another thread @{text "th'"}
|
|
162 |
to take over the critical resource released by the initiating thread @{text "th"}.
|
|
163 |
*}
|
|
164 |
|
|
165 |
context valid_trace_v_n
|
|
166 |
begin
|
|
167 |
|
|
168 |
lemma sub_RAGs':
|
|
169 |
"{(Cs cs, Th th), (Th taker, Cs cs)} \<subseteq> RAG s"
|
|
170 |
using next_th_RAG[OF next_th_taker] .
|
|
171 |
|
|
172 |
lemma ancestors_th':
|
|
173 |
"ancestors (RAG s) (Th taker) = {Th th, Cs cs}"
|
|
174 |
proof -
|
|
175 |
have "ancestors (RAG s) (Th taker) = ancestors (RAG s) (Cs cs) \<union> {Cs cs}"
|
|
176 |
proof(rule rtree_RAG.ancestors_accum)
|
|
177 |
from sub_RAGs' show "(Th taker, Cs cs) \<in> RAG s" by auto
|
|
178 |
qed
|
|
179 |
thus ?thesis using ancestors_th ancestors_cs by auto
|
|
180 |
qed
|
|
181 |
|
|
182 |
lemma RAG_s:
|
|
183 |
"RAG (e#s) = (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) \<union>
|
|
184 |
{(Cs cs, Th taker)}"
|
|
185 |
by (unfold RAG_es waiting_set_eq holding_set_eq, auto)
|
|
186 |
|
|
187 |
lemma subtree_kept: (* ddd *)
|
|
188 |
assumes "th1 \<notin> {th, taker}"
|
|
189 |
shows "subtree (RAG (e#s)) (Th th1) =
|
|
190 |
subtree (RAG s) (Th th1)" (is "_ = ?R")
|
|
191 |
proof -
|
|
192 |
let ?RAG' = "(RAG s - {(Cs cs, Th th), (Th taker, Cs cs)})"
|
|
193 |
let ?RAG'' = "?RAG' \<union> {(Cs cs, Th taker)}"
|
|
194 |
have "subtree ?RAG' (Th th1) = ?R"
|
|
195 |
proof(rule subset_del_subtree_outside)
|
|
196 |
show "Range {(Cs cs, Th th), (Th taker, Cs cs)} \<inter> subtree (RAG s) (Th th1) = {}"
|
|
197 |
proof -
|
|
198 |
have "(Th th) \<notin> subtree (RAG s) (Th th1)"
|
|
199 |
proof(rule subtree_refute)
|
|
200 |
show "Th th1 \<notin> ancestors (RAG s) (Th th)"
|
|
201 |
by (unfold ancestors_th, simp)
|
|
202 |
next
|
|
203 |
from assms show "Th th1 \<noteq> Th th" by simp
|
|
204 |
qed
|
|
205 |
moreover have "(Cs cs) \<notin> subtree (RAG s) (Th th1)"
|
|
206 |
proof(rule subtree_refute)
|
|
207 |
show "Th th1 \<notin> ancestors (RAG s) (Cs cs)"
|
|
208 |
by (unfold ancestors_cs, insert assms, auto)
|
|
209 |
qed simp
|
|
210 |
ultimately have "{Th th, Cs cs} \<inter> subtree (RAG s) (Th th1) = {}" by auto
|
|
211 |
thus ?thesis by simp
|
|
212 |
qed
|
|
213 |
qed
|
|
214 |
moreover have "subtree ?RAG'' (Th th1) = subtree ?RAG' (Th th1)"
|
|
215 |
proof(rule subtree_insert_next)
|
|
216 |
show "Th taker \<notin> subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1)"
|
|
217 |
proof(rule subtree_refute)
|
|
218 |
show "Th th1 \<notin> ancestors (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th taker)"
|
|
219 |
(is "_ \<notin> ?R")
|
|
220 |
proof -
|
|
221 |
have "?R \<subseteq> ancestors (RAG s) (Th taker)" by (rule ancestors_mono, auto)
|
|
222 |
moreover have "Th th1 \<notin> ..." using ancestors_th' assms by simp
|
|
223 |
ultimately show ?thesis by auto
|
|
224 |
qed
|
|
225 |
next
|
|
226 |
from assms show "Th th1 \<noteq> Th taker" by simp
|
|
227 |
qed
|
|
228 |
qed
|
|
229 |
ultimately show ?thesis by (unfold RAG_s, simp)
|
|
230 |
qed
|
|
231 |
|
|
232 |
lemma cp_kept:
|
|
233 |
assumes "th1 \<notin> {th, taker}"
|
|
234 |
shows "cp (e#s) th1 = cp s th1"
|
|
235 |
by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp)
|
|
236 |
|
|
237 |
end
|
|
238 |
|
|
239 |
|
|
240 |
context valid_trace_v_e
|
|
241 |
begin
|
|
242 |
|
|
243 |
find_theorems RAG s e
|
|
244 |
|
|
245 |
lemma RAG_s: "RAG (e#s) = RAG s - {(Cs cs, Th th)}"
|
|
246 |
by (unfold RAG_es waiting_set_eq holding_set_eq, simp)
|
|
247 |
|
|
248 |
lemma subtree_kept:
|
|
249 |
assumes "th1 \<noteq> th"
|
|
250 |
shows "subtree (RAG (e#s)) (Th th1) = subtree (RAG s) (Th th1)"
|
|
251 |
proof(unfold RAG_s, rule subset_del_subtree_outside)
|
|
252 |
show "Range {(Cs cs, Th th)} \<inter> subtree (RAG s) (Th th1) = {}"
|
|
253 |
proof -
|
|
254 |
have "(Th th) \<notin> subtree (RAG s) (Th th1)"
|
|
255 |
proof(rule subtree_refute)
|
|
256 |
show "Th th1 \<notin> ancestors (RAG s) (Th th)"
|
|
257 |
by (unfold ancestors_th, simp)
|
|
258 |
next
|
|
259 |
from assms show "Th th1 \<noteq> Th th" by simp
|
|
260 |
qed
|
|
261 |
thus ?thesis by auto
|
|
262 |
qed
|
|
263 |
qed
|
|
264 |
|
|
265 |
lemma cp_kept_1:
|
|
266 |
assumes "th1 \<noteq> th"
|
|
267 |
shows "cp (e#s) th1 = cp s th1"
|
|
268 |
by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp)
|
|
269 |
|
|
270 |
lemma subtree_cs: "subtree (RAG s) (Cs cs) = {Cs cs}"
|
|
271 |
proof -
|
|
272 |
{ fix n
|
|
273 |
have "(Cs cs) \<notin> ancestors (RAG s) n"
|
|
274 |
proof
|
|
275 |
assume "Cs cs \<in> ancestors (RAG s) n"
|
|
276 |
hence "(n, Cs cs) \<in> (RAG s)^+" by (auto simp:ancestors_def)
|
|
277 |
from tranclE[OF this] obtain nn where h: "(nn, Cs cs) \<in> RAG s" by auto
|
|
278 |
then obtain th' where "nn = Th th'"
|
|
279 |
by (unfold s_RAG_def, auto)
|
|
280 |
from h[unfolded this] have "(Th th', Cs cs) \<in> RAG s" .
|
|
281 |
from this[unfolded s_RAG_def]
|
|
282 |
have "waiting (wq s) th' cs" by auto
|
|
283 |
from this[unfolded cs_waiting_def]
|
|
284 |
have "1 < length (wq s cs)"
|
|
285 |
by (cases "wq s cs", auto)
|
|
286 |
from holding_next_thI[OF holding_th_cs_s this]
|
|
287 |
obtain th' where "next_th s th cs th'" by auto
|
|
288 |
thus False using no_taker by blast
|
|
289 |
qed
|
|
290 |
} note h = this
|
|
291 |
{ fix n
|
|
292 |
assume "n \<in> subtree (RAG s) (Cs cs)"
|
|
293 |
hence "n = (Cs cs)"
|
|
294 |
by (elim subtreeE, insert h, auto)
|
|
295 |
} moreover have "(Cs cs) \<in> subtree (RAG s) (Cs cs)"
|
|
296 |
by (auto simp:subtree_def)
|
|
297 |
ultimately show ?thesis by auto
|
|
298 |
qed
|
|
299 |
|
|
300 |
lemma subtree_th:
|
|
301 |
"subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}"
|
|
302 |
proof(unfold RAG_s, fold subtree_cs, rule rtree_RAG.subtree_del_inside)
|
|
303 |
from edge_of_th
|
|
304 |
show "(Cs cs, Th th) \<in> edges_in (RAG s) (Th th)"
|
|
305 |
by (unfold edges_in_def, auto simp:subtree_def)
|
|
306 |
qed
|
|
307 |
|
|
308 |
lemma cp_kept_2:
|
|
309 |
shows "cp (e#s) th = cp s th"
|
|
310 |
by (unfold cp_alt_def subtree_th the_preced_es, auto)
|
|
311 |
|
|
312 |
lemma eq_cp:
|
|
313 |
shows "cp (e#s) th' = cp s th'"
|
|
314 |
using cp_kept_1 cp_kept_2
|
|
315 |
by (cases "th' = th", auto)
|
|
316 |
|
|
317 |
end
|
|
318 |
|
|
319 |
|
|
320 |
section {* The @{term P} operation *}
|
|
321 |
|
|
322 |
context valid_trace_p
|
|
323 |
begin
|
|
324 |
|
|
325 |
lemma root_th: "root (RAG s) (Th th)"
|
|
326 |
by (simp add: ready_th_s readys_root)
|
|
327 |
|
|
328 |
lemma in_no_others_subtree:
|
|
329 |
assumes "th' \<noteq> th"
|
|
330 |
shows "Th th \<notin> subtree (RAG s) (Th th')"
|
|
331 |
proof
|
|
332 |
assume "Th th \<in> subtree (RAG s) (Th th')"
|
|
333 |
thus False
|
|
334 |
proof(cases rule:subtreeE)
|
|
335 |
case 1
|
|
336 |
with assms show ?thesis by auto
|
|
337 |
next
|
|
338 |
case 2
|
|
339 |
with root_th show ?thesis by (auto simp:root_def)
|
|
340 |
qed
|
|
341 |
qed
|
|
342 |
|
|
343 |
lemma preced_kept: "the_preced (e#s) = the_preced s"
|
|
344 |
proof
|
|
345 |
fix th'
|
|
346 |
show "the_preced (e # s) th' = the_preced s th'"
|
|
347 |
by (unfold the_preced_def is_p preced_def, simp)
|
|
348 |
qed
|
|
349 |
|
|
350 |
end
|
|
351 |
|
|
352 |
|
|
353 |
context valid_trace_p_h
|
|
354 |
begin
|
|
355 |
|
|
356 |
lemma subtree_kept:
|
|
357 |
assumes "th' \<noteq> th"
|
|
358 |
shows "subtree (RAG (e#s)) (Th th') = subtree (RAG s) (Th th')"
|
|
359 |
proof(unfold RAG_es, rule subtree_insert_next)
|
|
360 |
from in_no_others_subtree[OF assms]
|
|
361 |
show "Th th \<notin> subtree (RAG s) (Th th')" .
|
|
362 |
qed
|
|
363 |
|
|
364 |
lemma cp_kept:
|
|
365 |
assumes "th' \<noteq> th"
|
|
366 |
shows "cp (e#s) th' = cp s th'"
|
|
367 |
proof -
|
|
368 |
have "(the_preced (e#s) ` {th'a. Th th'a \<in> subtree (RAG (e#s)) (Th th')}) =
|
|
369 |
(the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')})"
|
|
370 |
by (unfold preced_kept subtree_kept[OF assms], simp)
|
|
371 |
thus ?thesis by (unfold cp_alt_def, simp)
|
|
372 |
qed
|
|
373 |
|
|
374 |
end
|
|
375 |
|
|
376 |
context valid_trace_p_w
|
|
377 |
begin
|
|
378 |
|
|
379 |
lemma cs_held: "(Cs cs, Th holder) \<in> RAG s"
|
|
380 |
using holding_s_holder
|
|
381 |
by (unfold s_RAG_def, fold holding_eq, auto)
|
|
382 |
|
|
383 |
lemma tRAG_s:
|
|
384 |
"tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}"
|
|
385 |
using local.RAG_tRAG_transfer[OF RAG_es cs_held] .
|
|
386 |
|
|
387 |
lemma cp_kept:
|
|
388 |
assumes "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)"
|
|
389 |
shows "cp (e#s) th'' = cp s th''"
|
|
390 |
proof -
|
|
391 |
have h: "subtree (tRAG (e#s)) (Th th'') = subtree (tRAG s) (Th th'')"
|
|
392 |
proof -
|
|
393 |
have "Th holder \<notin> subtree (tRAG s) (Th th'')"
|
|
394 |
proof
|
|
395 |
assume "Th holder \<in> subtree (tRAG s) (Th th'')"
|
|
396 |
thus False
|
|
397 |
proof(rule subtreeE)
|
|
398 |
assume "Th holder = Th th''"
|
|
399 |
from assms[unfolded tRAG_s ancestors_def, folded this]
|
|
400 |
show ?thesis by auto
|
|
401 |
next
|
|
402 |
assume "Th th'' \<in> ancestors (tRAG s) (Th holder)"
|
|
403 |
moreover have "... \<subseteq> ancestors (tRAG (e#s)) (Th holder)"
|
|
404 |
proof(rule ancestors_mono)
|
|
405 |
show "tRAG s \<subseteq> tRAG (e#s)" by (unfold tRAG_s, auto)
|
|
406 |
qed
|
|
407 |
ultimately have "Th th'' \<in> ancestors (tRAG (e#s)) (Th holder)" by auto
|
|
408 |
moreover have "Th holder \<in> ancestors (tRAG (e#s)) (Th th)"
|
|
409 |
by (unfold tRAG_s, auto simp:ancestors_def)
|
|
410 |
ultimately have "Th th'' \<in> ancestors (tRAG (e#s)) (Th th)"
|
|
411 |
by (auto simp:ancestors_def)
|
|
412 |
with assms show ?thesis by auto
|
|
413 |
qed
|
|
414 |
qed
|
|
415 |
from subtree_insert_next[OF this]
|
|
416 |
have "subtree (tRAG s \<union> {(Th th, Th holder)}) (Th th'') = subtree (tRAG s) (Th th'')" .
|
|
417 |
from this[folded tRAG_s] show ?thesis .
|
|
418 |
qed
|
|
419 |
show ?thesis by (unfold cp_alt_def1 h preced_kept, simp)
|
|
420 |
qed
|
|
421 |
|
|
422 |
lemma cp_gen_update_stop: (* ddd *)
|
|
423 |
assumes "u \<in> ancestors (tRAG (e#s)) (Th th)"
|
|
424 |
and "cp_gen (e#s) u = cp_gen s u"
|
|
425 |
and "y \<in> ancestors (tRAG (e#s)) u"
|
|
426 |
shows "cp_gen (e#s) y = cp_gen s y"
|
|
427 |
using assms(3)
|
105
|
428 |
proof(induct rule:wf_induct[OF vat_es.fsbttRAGs.wf])
|
85
|
429 |
case (1 x)
|
|
430 |
show ?case (is "?L = ?R")
|
|
431 |
proof -
|
|
432 |
from tRAG_ancestorsE[OF 1(2)]
|
|
433 |
obtain th2 where eq_x: "x = Th th2" by blast
|
105
|
434 |
from vat_es.cp_gen_rec[OF this]
|
85
|
435 |
have "?L =
|
|
436 |
Max ({the_preced (e#s) th2} \<union> cp_gen (e#s) ` RTree.children (tRAG (e#s)) x)" .
|
|
437 |
also have "... =
|
|
438 |
Max ({the_preced s th2} \<union> cp_gen s ` RTree.children (tRAG s) x)"
|
|
439 |
proof -
|
|
440 |
from preced_kept have "the_preced (e#s) th2 = the_preced s th2" by simp
|
|
441 |
moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x =
|
|
442 |
cp_gen s ` RTree.children (tRAG s) x"
|
|
443 |
proof -
|
|
444 |
have "RTree.children (tRAG (e#s)) x = RTree.children (tRAG s) x"
|
|
445 |
proof(unfold tRAG_s, rule children_union_kept)
|
|
446 |
have start: "(Th th, Th holder) \<in> tRAG (e#s)"
|
|
447 |
by (unfold tRAG_s, auto)
|
|
448 |
note x_u = 1(2)
|
|
449 |
show "x \<notin> Range {(Th th, Th holder)}"
|
|
450 |
proof
|
|
451 |
assume "x \<in> Range {(Th th, Th holder)}"
|
|
452 |
hence eq_x: "x = Th holder" using RangeE by auto
|
|
453 |
show False
|
105
|
454 |
proof(cases rule:vat_es.ancestors_headE[OF assms(1) start])
|
85
|
455 |
case 1
|
105
|
456 |
from x_u[folded this, unfolded eq_x] vat_es.acyclic_tRAG
|
85
|
457 |
show ?thesis by (auto simp:ancestors_def acyclic_def)
|
|
458 |
next
|
|
459 |
case 2
|
|
460 |
with x_u[unfolded eq_x]
|
|
461 |
have "(Th holder, Th holder) \<in> (tRAG (e#s))^+" by (auto simp:ancestors_def)
|
105
|
462 |
with vat_es.acyclic_tRAG show ?thesis by (auto simp:acyclic_def)
|
85
|
463 |
qed
|
|
464 |
qed
|
|
465 |
qed
|
|
466 |
moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x =
|
|
467 |
cp_gen s ` RTree.children (tRAG (e#s)) x" (is "?f ` ?A = ?g ` ?A")
|
|
468 |
proof(rule f_image_eq)
|
|
469 |
fix a
|
|
470 |
assume a_in: "a \<in> ?A"
|
|
471 |
from 1(2)
|
|
472 |
show "?f a = ?g a"
|
105
|
473 |
proof(cases rule:vat_es.rtree_s.ancestors_childrenE[case_names in_ch out_ch])
|
85
|
474 |
case in_ch
|
|
475 |
show ?thesis
|
|
476 |
proof(cases "a = u")
|
|
477 |
case True
|
|
478 |
from assms(2)[folded this] show ?thesis .
|
|
479 |
next
|
|
480 |
case False
|
|
481 |
have a_not_in: "a \<notin> ancestors (tRAG (e#s)) (Th th)"
|
|
482 |
proof
|
|
483 |
assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
|
|
484 |
have "a = u"
|
105
|
485 |
proof(rule vat_es.rtree_s.ancestors_children_unique)
|
85
|
486 |
from a_in' a_in show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter>
|
|
487 |
RTree.children (tRAG (e#s)) x" by auto
|
|
488 |
next
|
|
489 |
from assms(1) in_ch show "u \<in> ancestors (tRAG (e#s)) (Th th) \<inter>
|
|
490 |
RTree.children (tRAG (e#s)) x" by auto
|
|
491 |
qed
|
|
492 |
with False show False by simp
|
|
493 |
qed
|
|
494 |
from a_in obtain th_a where eq_a: "a = Th th_a"
|
|
495 |
by (unfold RTree.children_def tRAG_alt_def, auto)
|
|
496 |
from cp_kept[OF a_not_in[unfolded eq_a]]
|
|
497 |
have "cp (e#s) th_a = cp s th_a" .
|
|
498 |
from this [unfolded cp_gen_def_cond[OF eq_a], folded eq_a]
|
|
499 |
show ?thesis .
|
|
500 |
qed
|
|
501 |
next
|
|
502 |
case (out_ch z)
|
|
503 |
hence h: "z \<in> ancestors (tRAG (e#s)) u" "z \<in> RTree.children (tRAG (e#s)) x" by auto
|
|
504 |
show ?thesis
|
|
505 |
proof(cases "a = z")
|
|
506 |
case True
|
|
507 |
from h(2) have zx_in: "(z, x) \<in> (tRAG (e#s))" by (auto simp:RTree.children_def)
|
|
508 |
from 1(1)[rule_format, OF this h(1)]
|
|
509 |
have eq_cp_gen: "cp_gen (e#s) z = cp_gen s z" .
|
|
510 |
with True show ?thesis by metis
|
|
511 |
next
|
|
512 |
case False
|
|
513 |
from a_in obtain th_a where eq_a: "a = Th th_a"
|
|
514 |
by (auto simp:RTree.children_def tRAG_alt_def)
|
|
515 |
have "a \<notin> ancestors (tRAG (e#s)) (Th th)"
|
|
516 |
proof
|
|
517 |
assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
|
|
518 |
have "a = z"
|
105
|
519 |
proof(rule vat_es.rtree_s.ancestors_children_unique)
|
85
|
520 |
from assms(1) h(1) have "z \<in> ancestors (tRAG (e#s)) (Th th)"
|
|
521 |
by (auto simp:ancestors_def)
|
|
522 |
with h(2) show " z \<in> ancestors (tRAG (e#s)) (Th th) \<inter>
|
|
523 |
RTree.children (tRAG (e#s)) x" by auto
|
|
524 |
next
|
|
525 |
from a_in a_in'
|
|
526 |
show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> RTree.children (tRAG (e#s)) x"
|
|
527 |
by auto
|
|
528 |
qed
|
|
529 |
with False show False by auto
|
|
530 |
qed
|
|
531 |
from cp_kept[OF this[unfolded eq_a]]
|
|
532 |
have "cp (e#s) th_a = cp s th_a" .
|
|
533 |
from this[unfolded cp_gen_def_cond[OF eq_a], folded eq_a]
|
|
534 |
show ?thesis .
|
|
535 |
qed
|
|
536 |
qed
|
|
537 |
qed
|
|
538 |
ultimately show ?thesis by metis
|
|
539 |
qed
|
|
540 |
ultimately show ?thesis by simp
|
|
541 |
qed
|
|
542 |
also have "... = ?R"
|
|
543 |
by (fold cp_gen_rec[OF eq_x], simp)
|
|
544 |
finally show ?thesis .
|
|
545 |
qed
|
|
546 |
qed
|
|
547 |
|
|
548 |
lemma cp_up:
|
|
549 |
assumes "(Th th') \<in> ancestors (tRAG (e#s)) (Th th)"
|
|
550 |
and "cp (e#s) th' = cp s th'"
|
|
551 |
and "(Th th'') \<in> ancestors (tRAG (e#s)) (Th th')"
|
|
552 |
shows "cp (e#s) th'' = cp s th''"
|
|
553 |
proof -
|
|
554 |
have "cp_gen (e#s) (Th th'') = cp_gen s (Th th'')"
|
|
555 |
proof(rule cp_gen_update_stop[OF assms(1) _ assms(3)])
|
|
556 |
from assms(2) cp_gen_def_cond[OF refl[of "Th th'"]]
|
|
557 |
show "cp_gen (e#s) (Th th') = cp_gen s (Th th')" by metis
|
|
558 |
qed
|
|
559 |
with cp_gen_def_cond[OF refl[of "Th th''"]]
|
|
560 |
show ?thesis by metis
|
|
561 |
qed
|
|
562 |
|
|
563 |
end
|
|
564 |
|
|
565 |
section {* The @{term Create} operation *}
|
|
566 |
|
|
567 |
context valid_trace_create
|
|
568 |
begin
|
|
569 |
|
|
570 |
lemma tRAG_kept: "tRAG (e#s) = tRAG s"
|
|
571 |
by (unfold tRAG_alt_def RAG_unchanged, auto)
|
|
572 |
|
|
573 |
lemma preced_kept:
|
|
574 |
assumes "th' \<noteq> th"
|
|
575 |
shows "the_preced (e#s) th' = the_preced s th'"
|
|
576 |
by (unfold the_preced_def preced_def is_create, insert assms, auto)
|
|
577 |
|
|
578 |
lemma th_not_in: "Th th \<notin> Field (tRAG s)"
|
|
579 |
by (meson not_in_thread_isolated subsetCE tRAG_Field th_not_live_s)
|
|
580 |
|
|
581 |
lemma eq_cp:
|
|
582 |
assumes neq_th: "th' \<noteq> th"
|
|
583 |
shows "cp (e#s) th' = cp s th'"
|
|
584 |
proof -
|
|
585 |
have "(the_preced (e#s) \<circ> the_thread) ` subtree (tRAG (e#s)) (Th th') =
|
|
586 |
(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th')"
|
|
587 |
proof(unfold tRAG_kept, rule f_image_eq)
|
|
588 |
fix a
|
|
589 |
assume a_in: "a \<in> subtree (tRAG s) (Th th')"
|
|
590 |
then obtain th_a where eq_a: "a = Th th_a"
|
|
591 |
proof(cases rule:subtreeE)
|
|
592 |
case 2
|
|
593 |
from ancestors_Field[OF 2(2)]
|
|
594 |
and that show ?thesis by (unfold tRAG_alt_def, auto)
|
|
595 |
qed auto
|
|
596 |
have neq_th_a: "th_a \<noteq> th"
|
|
597 |
proof -
|
|
598 |
have "(Th th) \<notin> subtree (tRAG s) (Th th')"
|
|
599 |
proof
|
|
600 |
assume "Th th \<in> subtree (tRAG s) (Th th')"
|
|
601 |
thus False
|
|
602 |
proof(cases rule:subtreeE)
|
|
603 |
case 2
|
|
604 |
from ancestors_Field[OF this(2)]
|
|
605 |
and th_not_in[unfolded Field_def]
|
|
606 |
show ?thesis by auto
|
|
607 |
qed (insert assms, auto)
|
|
608 |
qed
|
|
609 |
with a_in[unfolded eq_a] show ?thesis by auto
|
|
610 |
qed
|
|
611 |
from preced_kept[OF this]
|
|
612 |
show "(the_preced (e#s) \<circ> the_thread) a = (the_preced s \<circ> the_thread) a"
|
|
613 |
by (unfold eq_a, simp)
|
|
614 |
qed
|
|
615 |
thus ?thesis by (unfold cp_alt_def1, simp)
|
|
616 |
qed
|
|
617 |
|
|
618 |
lemma children_of_th: "RTree.children (tRAG (e#s)) (Th th) = {}"
|
|
619 |
proof -
|
|
620 |
{ fix a
|
|
621 |
assume "a \<in> RTree.children (tRAG (e#s)) (Th th)"
|
|
622 |
hence "(a, Th th) \<in> tRAG (e#s)" by (auto simp:RTree.children_def)
|
|
623 |
with th_not_in have False
|
|
624 |
by (unfold Field_def tRAG_kept, auto)
|
|
625 |
} thus ?thesis by auto
|
|
626 |
qed
|
|
627 |
|
|
628 |
lemma eq_cp_th: "cp (e#s) th = preced th (e#s)"
|
105
|
629 |
by (unfold vat_es.cp_rec children_of_th, simp add:the_preced_def)
|
85
|
630 |
|
|
631 |
end
|
|
632 |
|
|
633 |
|
|
634 |
context valid_trace_exit
|
|
635 |
begin
|
|
636 |
|
|
637 |
lemma preced_kept:
|
|
638 |
assumes "th' \<noteq> th"
|
|
639 |
shows "the_preced (e#s) th' = the_preced s th'"
|
|
640 |
using assms
|
|
641 |
by (unfold the_preced_def is_exit preced_def, simp)
|
|
642 |
|
|
643 |
lemma tRAG_kept: "tRAG (e#s) = tRAG s"
|
|
644 |
by (unfold tRAG_alt_def RAG_unchanged, auto)
|
|
645 |
|
|
646 |
lemma th_RAG: "Th th \<notin> Field (RAG s)"
|
|
647 |
proof -
|
|
648 |
have "Th th \<notin> Range (RAG s)"
|
|
649 |
proof
|
|
650 |
assume "Th th \<in> Range (RAG s)"
|
|
651 |
then obtain cs where "holding (wq s) th cs"
|
|
652 |
by (unfold Range_iff s_RAG_def, auto)
|
|
653 |
with holdents_th_s[unfolded holdents_def]
|
|
654 |
show False by (unfold holding_eq, auto)
|
|
655 |
qed
|
|
656 |
moreover have "Th th \<notin> Domain (RAG s)"
|
|
657 |
proof
|
|
658 |
assume "Th th \<in> Domain (RAG s)"
|
|
659 |
then obtain cs where "waiting (wq s) th cs"
|
|
660 |
by (unfold Domain_iff s_RAG_def, auto)
|
|
661 |
with th_ready_s show False by (unfold readys_def waiting_eq, auto)
|
|
662 |
qed
|
|
663 |
ultimately show ?thesis by (auto simp:Field_def)
|
|
664 |
qed
|
|
665 |
|
|
666 |
lemma th_tRAG: "(Th th) \<notin> Field (tRAG s)"
|
|
667 |
using th_RAG tRAG_Field by auto
|
|
668 |
|
|
669 |
lemma eq_cp:
|
|
670 |
assumes neq_th: "th' \<noteq> th"
|
|
671 |
shows "cp (e#s) th' = cp s th'"
|
|
672 |
proof -
|
|
673 |
have "(the_preced (e#s) \<circ> the_thread) ` subtree (tRAG (e#s)) (Th th') =
|
|
674 |
(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th')"
|
|
675 |
proof(unfold tRAG_kept, rule f_image_eq)
|
|
676 |
fix a
|
|
677 |
assume a_in: "a \<in> subtree (tRAG s) (Th th')"
|
|
678 |
then obtain th_a where eq_a: "a = Th th_a"
|
|
679 |
proof(cases rule:subtreeE)
|
|
680 |
case 2
|
|
681 |
from ancestors_Field[OF 2(2)]
|
|
682 |
and that show ?thesis by (unfold tRAG_alt_def, auto)
|
|
683 |
qed auto
|
|
684 |
have neq_th_a: "th_a \<noteq> th"
|
|
685 |
proof -
|
|
686 |
from readys_in_no_subtree[OF th_ready_s assms]
|
|
687 |
have "(Th th) \<notin> subtree (RAG s) (Th th')" .
|
|
688 |
with tRAG_subtree_RAG[of s "Th th'"]
|
|
689 |
have "(Th th) \<notin> subtree (tRAG s) (Th th')" by auto
|
|
690 |
with a_in[unfolded eq_a] show ?thesis by auto
|
|
691 |
qed
|
|
692 |
from preced_kept[OF this]
|
|
693 |
show "(the_preced (e#s) \<circ> the_thread) a = (the_preced s \<circ> the_thread) a"
|
|
694 |
by (unfold eq_a, simp)
|
|
695 |
qed
|
|
696 |
thus ?thesis by (unfold cp_alt_def1, simp)
|
|
697 |
qed
|
|
698 |
|
|
699 |
end
|
|
700 |
|
|
701 |
end
|
|
702 |
|