1 header {* \chapter{Case Study: Single and Multi-Mutator Garbage Collection Algorithms} |
|
2 |
|
3 \section {Formalization of the Memory} *} |
|
4 |
|
5 theory Graph imports Main begin |
|
6 |
|
7 datatype node = Black | White |
|
8 |
|
9 types |
|
10 nodes = "node list" |
|
11 edge = "nat \<times> nat" |
|
12 edges = "edge list" |
|
13 |
|
14 consts Roots :: "nat set" |
|
15 |
|
16 constdefs |
|
17 Proper_Roots :: "nodes \<Rightarrow> bool" |
|
18 "Proper_Roots M \<equiv> Roots\<noteq>{} \<and> Roots \<subseteq> {i. i<length M}" |
|
19 |
|
20 Proper_Edges :: "(nodes \<times> edges) \<Rightarrow> bool" |
|
21 "Proper_Edges \<equiv> (\<lambda>(M,E). \<forall>i<length E. fst(E!i)<length M \<and> snd(E!i)<length M)" |
|
22 |
|
23 BtoW :: "(edge \<times> nodes) \<Rightarrow> bool" |
|
24 "BtoW \<equiv> (\<lambda>(e,M). (M!fst e)=Black \<and> (M!snd e)\<noteq>Black)" |
|
25 |
|
26 Blacks :: "nodes \<Rightarrow> nat set" |
|
27 "Blacks M \<equiv> {i. i<length M \<and> M!i=Black}" |
|
28 |
|
29 Reach :: "edges \<Rightarrow> nat set" |
|
30 "Reach E \<equiv> {x. (\<exists>path. 1<length path \<and> path!(length path - 1)\<in>Roots \<and> x=path!0 |
|
31 \<and> (\<forall>i<length path - 1. (\<exists>j<length E. E!j=(path!(i+1), path!i)))) |
|
32 \<or> x\<in>Roots}" |
|
33 |
|
34 text{* Reach: the set of reachable nodes is the set of Roots together with the |
|
35 nodes reachable from some Root by a path represented by a list of |
|
36 nodes (at least two since we traverse at least one edge), where two |
|
37 consecutive nodes correspond to an edge in E. *} |
|
38 |
|
39 subsection {* Proofs about Graphs *} |
|
40 |
|
41 lemmas Graph_defs= Blacks_def Proper_Roots_def Proper_Edges_def BtoW_def |
|
42 declare Graph_defs [simp] |
|
43 |
|
44 subsubsection{* Graph 1 *} |
|
45 |
|
46 lemma Graph1_aux [rule_format]: |
|
47 "\<lbrakk> Roots\<subseteq>Blacks M; \<forall>i<length E. \<not>BtoW(E!i,M)\<rbrakk> |
|
48 \<Longrightarrow> 1< length path \<longrightarrow> (path!(length path - 1))\<in>Roots \<longrightarrow> |
|
49 (\<forall>i<length path - 1. (\<exists>j. j < length E \<and> E!j=(path!(Suc i), path!i))) |
|
50 \<longrightarrow> M!(path!0) = Black" |
|
51 apply(induct_tac "path") |
|
52 apply force |
|
53 apply clarify |
|
54 apply simp |
|
55 apply(case_tac "list") |
|
56 apply force |
|
57 apply simp |
|
58 apply(rotate_tac -2) |
|
59 apply(erule_tac x = "0" in all_dupE) |
|
60 apply simp |
|
61 apply clarify |
|
62 apply(erule allE , erule (1) notE impE) |
|
63 apply simp |
|
64 apply(erule mp) |
|
65 apply(case_tac "lista") |
|
66 apply force |
|
67 apply simp |
|
68 apply(erule mp) |
|
69 apply clarify |
|
70 apply(erule_tac x = "Suc i" in allE) |
|
71 apply force |
|
72 done |
|
73 |
|
74 lemma Graph1: |
|
75 "\<lbrakk>Roots\<subseteq>Blacks M; Proper_Edges(M, E); \<forall>i<length E. \<not>BtoW(E!i,M) \<rbrakk> |
|
76 \<Longrightarrow> Reach E\<subseteq>Blacks M" |
|
77 apply (unfold Reach_def) |
|
78 apply simp |
|
79 apply clarify |
|
80 apply(erule disjE) |
|
81 apply clarify |
|
82 apply(rule conjI) |
|
83 apply(subgoal_tac "0< length path - Suc 0") |
|
84 apply(erule allE , erule (1) notE impE) |
|
85 apply force |
|
86 apply simp |
|
87 apply(rule Graph1_aux) |
|
88 apply auto |
|
89 done |
|
90 |
|
91 subsubsection{* Graph 2 *} |
|
92 |
|
93 lemma Ex_first_occurrence [rule_format]: |
|
94 "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i. i<m \<longrightarrow> \<not> P i))"; |
|
95 apply(rule nat_less_induct) |
|
96 apply clarify |
|
97 apply(case_tac "\<forall>m. m<n \<longrightarrow> \<not> P m") |
|
98 apply auto |
|
99 done |
|
100 |
|
101 lemma Compl_lemma: "(n::nat)\<le>l \<Longrightarrow> (\<exists>m. m\<le>l \<and> n=l - m)" |
|
102 apply(rule_tac x = "l - n" in exI) |
|
103 apply arith |
|
104 done |
|
105 |
|
106 lemma Ex_last_occurrence: |
|
107 "\<lbrakk>P (n::nat); n\<le>l\<rbrakk> \<Longrightarrow> (\<exists>m. P (l - m) \<and> (\<forall>i. i<m \<longrightarrow> \<not>P (l - i)))" |
|
108 apply(drule Compl_lemma) |
|
109 apply clarify |
|
110 apply(erule Ex_first_occurrence) |
|
111 done |
|
112 |
|
113 lemma Graph2: |
|
114 "\<lbrakk>T \<in> Reach E; R<length E\<rbrakk> \<Longrightarrow> T \<in> Reach (E[R:=(fst(E!R), T)])" |
|
115 apply (unfold Reach_def) |
|
116 apply clarify |
|
117 apply simp |
|
118 apply(case_tac "\<forall>z<length path. fst(E!R)\<noteq>path!z") |
|
119 apply(rule_tac x = "path" in exI) |
|
120 apply simp |
|
121 apply clarify |
|
122 apply(erule allE , erule (1) notE impE) |
|
123 apply clarify |
|
124 apply(rule_tac x = "j" in exI) |
|
125 apply(case_tac "j=R") |
|
126 apply(erule_tac x = "Suc i" in allE) |
|
127 apply simp |
|
128 apply (force simp add:nth_list_update) |
|
129 apply simp |
|
130 apply(erule exE) |
|
131 apply(subgoal_tac "z \<le> length path - Suc 0") |
|
132 prefer 2 apply arith |
|
133 apply(drule_tac P = "\<lambda>m. m<length path \<and> fst(E!R)=path!m" in Ex_last_occurrence) |
|
134 apply assumption |
|
135 apply clarify |
|
136 apply simp |
|
137 apply(rule_tac x = "(path!0)#(drop (length path - Suc m) path)" in exI) |
|
138 apply simp |
|
139 apply(case_tac "length path - (length path - Suc m)") |
|
140 apply arith |
|
141 apply simp |
|
142 apply(subgoal_tac "(length path - Suc m) + nat \<le> length path") |
|
143 prefer 2 apply arith |
|
144 apply(drule nth_drop) |
|
145 apply simp |
|
146 apply(subgoal_tac "length path - Suc m + nat = length path - Suc 0") |
|
147 prefer 2 apply arith |
|
148 apply simp |
|
149 apply clarify |
|
150 apply(case_tac "i") |
|
151 apply(force simp add: nth_list_update) |
|
152 apply simp |
|
153 apply(subgoal_tac "(length path - Suc m) + nata \<le> length path") |
|
154 prefer 2 apply arith |
|
155 apply(subgoal_tac "(length path - Suc m) + (Suc nata) \<le> length path") |
|
156 prefer 2 apply arith |
|
157 apply simp |
|
158 apply(erule_tac x = "length path - Suc m + nata" in allE) |
|
159 apply simp |
|
160 apply clarify |
|
161 apply(rule_tac x = "j" in exI) |
|
162 apply(case_tac "R=j") |
|
163 prefer 2 apply force |
|
164 apply simp |
|
165 apply(drule_tac t = "path ! (length path - Suc m)" in sym) |
|
166 apply simp |
|
167 apply(case_tac " length path - Suc 0 < m") |
|
168 apply(subgoal_tac "(length path - Suc m)=0") |
|
169 prefer 2 apply arith |
|
170 apply(simp del: diff_is_0_eq) |
|
171 apply(subgoal_tac "Suc nata\<le>nat") |
|
172 prefer 2 apply arith |
|
173 apply(drule_tac n = "Suc nata" in Compl_lemma) |
|
174 apply clarify |
|
175 using [[linarith_split_limit = 0]] |
|
176 apply force |
|
177 using [[linarith_split_limit = 9]] |
|
178 apply(drule leI) |
|
179 apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)") |
|
180 apply(erule_tac x = "m - (Suc nata)" in allE) |
|
181 apply(case_tac "m") |
|
182 apply simp |
|
183 apply simp |
|
184 apply simp |
|
185 done |
|
186 |
|
187 |
|
188 subsubsection{* Graph 3 *} |
|
189 |
|
190 lemma Graph3: |
|
191 "\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E" |
|
192 apply (unfold Reach_def) |
|
193 apply clarify |
|
194 apply simp |
|
195 apply(case_tac "\<exists>i<length path - 1. (fst(E!R),T)=(path!(Suc i),path!i)") |
|
196 --{* the changed edge is part of the path *} |
|
197 apply(erule exE) |
|
198 apply(drule_tac P = "\<lambda>i. i<length path - 1 \<and> (fst(E!R),T)=(path!Suc i,path!i)" in Ex_first_occurrence) |
|
199 apply clarify |
|
200 apply(erule disjE) |
|
201 --{* T is NOT a root *} |
|
202 apply clarify |
|
203 apply(rule_tac x = "(take m path)@patha" in exI) |
|
204 apply(subgoal_tac "\<not>(length path\<le>m)") |
|
205 prefer 2 apply arith |
|
206 apply(simp) |
|
207 apply(rule conjI) |
|
208 apply(subgoal_tac "\<not>(m + length patha - 1 < m)") |
|
209 prefer 2 apply arith |
|
210 apply(simp add: nth_append) |
|
211 apply(rule conjI) |
|
212 apply(case_tac "m") |
|
213 apply force |
|
214 apply(case_tac "path") |
|
215 apply force |
|
216 apply force |
|
217 apply clarify |
|
218 apply(case_tac "Suc i\<le>m") |
|
219 apply(erule_tac x = "i" in allE) |
|
220 apply simp |
|
221 apply clarify |
|
222 apply(rule_tac x = "j" in exI) |
|
223 apply(case_tac "Suc i<m") |
|
224 apply(simp add: nth_append) |
|
225 apply(case_tac "R=j") |
|
226 apply(simp add: nth_list_update) |
|
227 apply(case_tac "i=m") |
|
228 apply force |
|
229 apply(erule_tac x = "i" in allE) |
|
230 apply force |
|
231 apply(force simp add: nth_list_update) |
|
232 apply(simp add: nth_append) |
|
233 apply(subgoal_tac "i=m - 1") |
|
234 prefer 2 apply arith |
|
235 apply(case_tac "R=j") |
|
236 apply(erule_tac x = "m - 1" in allE) |
|
237 apply(simp add: nth_list_update) |
|
238 apply(force simp add: nth_list_update) |
|
239 apply(simp add: nth_append) |
|
240 apply(rotate_tac -4) |
|
241 apply(erule_tac x = "i - m" in allE) |
|
242 apply(subgoal_tac "Suc (i - m)=(Suc i - m)" ) |
|
243 prefer 2 apply arith |
|
244 apply simp |
|
245 --{* T is a root *} |
|
246 apply(case_tac "m=0") |
|
247 apply force |
|
248 apply(rule_tac x = "take (Suc m) path" in exI) |
|
249 apply(subgoal_tac "\<not>(length path\<le>Suc m)" ) |
|
250 prefer 2 apply arith |
|
251 apply clarsimp |
|
252 apply(erule_tac x = "i" in allE) |
|
253 apply simp |
|
254 apply clarify |
|
255 apply(case_tac "R=j") |
|
256 apply(force simp add: nth_list_update) |
|
257 apply(force simp add: nth_list_update) |
|
258 --{* the changed edge is not part of the path *} |
|
259 apply(rule_tac x = "path" in exI) |
|
260 apply simp |
|
261 apply clarify |
|
262 apply(erule_tac x = "i" in allE) |
|
263 apply clarify |
|
264 apply(case_tac "R=j") |
|
265 apply(erule_tac x = "i" in allE) |
|
266 apply simp |
|
267 apply(force simp add: nth_list_update) |
|
268 done |
|
269 |
|
270 subsubsection{* Graph 4 *} |
|
271 |
|
272 lemma Graph4: |
|
273 "\<lbrakk>T \<in> Reach E; Roots\<subseteq>Blacks M; I\<le>length E; T<length M; R<length E; |
|
274 \<forall>i<I. \<not>BtoW(E!i,M); R<I; M!fst(E!R)=Black; M!T\<noteq>Black\<rbrakk> \<Longrightarrow> |
|
275 (\<exists>r. I\<le>r \<and> r<length E \<and> BtoW(E[R:=(fst(E!R),T)]!r,M))" |
|
276 apply (unfold Reach_def) |
|
277 apply simp |
|
278 apply(erule disjE) |
|
279 prefer 2 apply force |
|
280 apply clarify |
|
281 --{* there exist a black node in the path to T *} |
|
282 apply(case_tac "\<exists>m<length path. M!(path!m)=Black") |
|
283 apply(erule exE) |
|
284 apply(drule_tac P = "\<lambda>m. m<length path \<and> M!(path!m)=Black" in Ex_first_occurrence) |
|
285 apply clarify |
|
286 apply(case_tac "ma") |
|
287 apply force |
|
288 apply simp |
|
289 apply(case_tac "length path") |
|
290 apply force |
|
291 apply simp |
|
292 apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> ?P i" and x = "nat" in allE) |
|
293 apply simp |
|
294 apply clarify |
|
295 apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE) |
|
296 apply simp |
|
297 apply(case_tac "j<I") |
|
298 apply(erule_tac x = "j" in allE) |
|
299 apply force |
|
300 apply(rule_tac x = "j" in exI) |
|
301 apply(force simp add: nth_list_update) |
|
302 apply simp |
|
303 apply(rotate_tac -1) |
|
304 apply(erule_tac x = "length path - 1" in allE) |
|
305 apply(case_tac "length path") |
|
306 apply force |
|
307 apply force |
|
308 done |
|
309 |
|
310 subsubsection {* Graph 5 *} |
|
311 |
|
312 lemma Graph5: |
|
313 "\<lbrakk> T \<in> Reach E ; Roots \<subseteq> Blacks M; \<forall>i<R. \<not>BtoW(E!i,M); T<length M; |
|
314 R<length E; M!fst(E!R)=Black; M!snd(E!R)=Black; M!T \<noteq> Black\<rbrakk> |
|
315 \<Longrightarrow> (\<exists>r. R<r \<and> r<length E \<and> BtoW(E[R:=(fst(E!R),T)]!r,M))" |
|
316 apply (unfold Reach_def) |
|
317 apply simp |
|
318 apply(erule disjE) |
|
319 prefer 2 apply force |
|
320 apply clarify |
|
321 --{* there exist a black node in the path to T*} |
|
322 apply(case_tac "\<exists>m<length path. M!(path!m)=Black") |
|
323 apply(erule exE) |
|
324 apply(drule_tac P = "\<lambda>m. m<length path \<and> M!(path!m)=Black" in Ex_first_occurrence) |
|
325 apply clarify |
|
326 apply(case_tac "ma") |
|
327 apply force |
|
328 apply simp |
|
329 apply(case_tac "length path") |
|
330 apply force |
|
331 apply simp |
|
332 apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> ?P i" and x = "nat" in allE) |
|
333 apply simp |
|
334 apply clarify |
|
335 apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE) |
|
336 apply simp |
|
337 apply(case_tac "j\<le>R") |
|
338 apply(drule le_imp_less_or_eq [of _ R]) |
|
339 apply(erule disjE) |
|
340 apply(erule allE , erule (1) notE impE) |
|
341 apply force |
|
342 apply force |
|
343 apply(rule_tac x = "j" in exI) |
|
344 apply(force simp add: nth_list_update) |
|
345 apply simp |
|
346 apply(rotate_tac -1) |
|
347 apply(erule_tac x = "length path - 1" in allE) |
|
348 apply(case_tac "length path") |
|
349 apply force |
|
350 apply force |
|
351 done |
|
352 |
|
353 subsubsection {* Other lemmas about graphs *} |
|
354 |
|
355 lemma Graph6: |
|
356 "\<lbrakk>Proper_Edges(M,E); R<length E ; T<length M\<rbrakk> \<Longrightarrow> Proper_Edges(M,E[R:=(fst(E!R),T)])" |
|
357 apply (unfold Proper_Edges_def) |
|
358 apply(force simp add: nth_list_update) |
|
359 done |
|
360 |
|
361 lemma Graph7: |
|
362 "\<lbrakk>Proper_Edges(M,E)\<rbrakk> \<Longrightarrow> Proper_Edges(M[T:=a],E)" |
|
363 apply (unfold Proper_Edges_def) |
|
364 apply force |
|
365 done |
|
366 |
|
367 lemma Graph8: |
|
368 "\<lbrakk>Proper_Roots(M)\<rbrakk> \<Longrightarrow> Proper_Roots(M[T:=a])" |
|
369 apply (unfold Proper_Roots_def) |
|
370 apply force |
|
371 done |
|
372 |
|
373 text{* Some specific lemmata for the verification of garbage collection algorithms. *} |
|
374 |
|
375 lemma Graph9: "j<length M \<Longrightarrow> Blacks M\<subseteq>Blacks (M[j := Black])" |
|
376 apply (unfold Blacks_def) |
|
377 apply(force simp add: nth_list_update) |
|
378 done |
|
379 |
|
380 lemma Graph10 [rule_format (no_asm)]: "\<forall>i. M!i=a \<longrightarrow>M[i:=a]=M" |
|
381 apply(induct_tac "M") |
|
382 apply auto |
|
383 apply(case_tac "i") |
|
384 apply auto |
|
385 done |
|
386 |
|
387 lemma Graph11 [rule_format (no_asm)]: |
|
388 "\<lbrakk> M!j\<noteq>Black;j<length M\<rbrakk> \<Longrightarrow> Blacks M \<subset> Blacks (M[j := Black])" |
|
389 apply (unfold Blacks_def) |
|
390 apply(rule psubsetI) |
|
391 apply(force simp add: nth_list_update) |
|
392 apply safe |
|
393 apply(erule_tac c = "j" in equalityCE) |
|
394 apply auto |
|
395 done |
|
396 |
|
397 lemma Graph12: "\<lbrakk>a\<subseteq>Blacks M;j<length M\<rbrakk> \<Longrightarrow> a\<subseteq>Blacks (M[j := Black])" |
|
398 apply (unfold Blacks_def) |
|
399 apply(force simp add: nth_list_update) |
|
400 done |
|
401 |
|
402 lemma Graph13: "\<lbrakk>a\<subset> Blacks M;j<length M\<rbrakk> \<Longrightarrow> a \<subset> Blacks (M[j := Black])" |
|
403 apply (unfold Blacks_def) |
|
404 apply(erule psubset_subset_trans) |
|
405 apply(force simp add: nth_list_update) |
|
406 done |
|
407 |
|
408 declare Graph_defs [simp del] |
|
409 |
|
410 end |
|