|
1 |
|
2 header {* \section{The Single Mutator Case} *} |
|
3 |
|
4 theory Gar_Coll imports Graph OG_Syntax begin |
|
5 |
|
6 declare psubsetE [rule del] |
|
7 |
|
8 text {* Declaration of variables: *} |
|
9 |
|
10 record gar_coll_state = |
|
11 M :: nodes |
|
12 E :: edges |
|
13 bc :: "nat set" |
|
14 obc :: "nat set" |
|
15 Ma :: nodes |
|
16 ind :: nat |
|
17 k :: nat |
|
18 z :: bool |
|
19 |
|
20 subsection {* The Mutator *} |
|
21 |
|
22 text {* The mutator first redirects an arbitrary edge @{text "R"} from |
|
23 an arbitrary accessible node towards an arbitrary accessible node |
|
24 @{text "T"}. It then colors the new target @{text "T"} black. |
|
25 |
|
26 We declare the arbitrarily selected node and edge as constants:*} |
|
27 |
|
28 consts R :: nat T :: nat |
|
29 |
|
30 text {* \noindent The following predicate states, given a list of |
|
31 nodes @{text "m"} and a list of edges @{text "e"}, the conditions |
|
32 under which the selected edge @{text "R"} and node @{text "T"} are |
|
33 valid: *} |
|
34 |
|
35 constdefs |
|
36 Mut_init :: "gar_coll_state \<Rightarrow> bool" |
|
37 "Mut_init \<equiv> \<guillemotleft> T \<in> Reach \<acute>E \<and> R < length \<acute>E \<and> T < length \<acute>M \<guillemotright>" |
|
38 |
|
39 text {* \noindent For the mutator we |
|
40 consider two modules, one for each action. An auxiliary variable |
|
41 @{text "\<acute>z"} is set to false if the mutator has already redirected an |
|
42 edge but has not yet colored the new target. *} |
|
43 |
|
44 constdefs |
|
45 Redirect_Edge :: "gar_coll_state ann_com" |
|
46 "Redirect_Edge \<equiv> .{\<acute>Mut_init \<and> \<acute>z}. \<langle>\<acute>E:=\<acute>E[R:=(fst(\<acute>E!R), T)],, \<acute>z:= (\<not>\<acute>z)\<rangle>" |
|
47 |
|
48 Color_Target :: "gar_coll_state ann_com" |
|
49 "Color_Target \<equiv> .{\<acute>Mut_init \<and> \<not>\<acute>z}. \<langle>\<acute>M:=\<acute>M[T:=Black],, \<acute>z:= (\<not>\<acute>z)\<rangle>" |
|
50 |
|
51 Mutator :: "gar_coll_state ann_com" |
|
52 "Mutator \<equiv> |
|
53 .{\<acute>Mut_init \<and> \<acute>z}. |
|
54 WHILE True INV .{\<acute>Mut_init \<and> \<acute>z}. |
|
55 DO Redirect_Edge ;; Color_Target OD" |
|
56 |
|
57 subsubsection {* Correctness of the mutator *} |
|
58 |
|
59 lemmas mutator_defs = Mut_init_def Redirect_Edge_def Color_Target_def |
|
60 |
|
61 lemma Redirect_Edge: |
|
62 "\<turnstile> Redirect_Edge pre(Color_Target)" |
|
63 apply (unfold mutator_defs) |
|
64 apply annhoare |
|
65 apply(simp_all) |
|
66 apply(force elim:Graph2) |
|
67 done |
|
68 |
|
69 lemma Color_Target: |
|
70 "\<turnstile> Color_Target .{\<acute>Mut_init \<and> \<acute>z}." |
|
71 apply (unfold mutator_defs) |
|
72 apply annhoare |
|
73 apply(simp_all) |
|
74 done |
|
75 |
|
76 lemma Mutator: |
|
77 "\<turnstile> Mutator .{False}." |
|
78 apply(unfold Mutator_def) |
|
79 apply annhoare |
|
80 apply(simp_all add:Redirect_Edge Color_Target) |
|
81 apply(simp add:mutator_defs Redirect_Edge_def) |
|
82 done |
|
83 |
|
84 subsection {* The Collector *} |
|
85 |
|
86 text {* \noindent A constant @{text "M_init"} is used to give @{text "\<acute>Ma"} a |
|
87 suitable first value, defined as a list of nodes where only the @{text |
|
88 "Roots"} are black. *} |
|
89 |
|
90 consts M_init :: nodes |
|
91 |
|
92 constdefs |
|
93 Proper_M_init :: "gar_coll_state \<Rightarrow> bool" |
|
94 "Proper_M_init \<equiv> \<guillemotleft> Blacks M_init=Roots \<and> length M_init=length \<acute>M \<guillemotright>" |
|
95 |
|
96 Proper :: "gar_coll_state \<Rightarrow> bool" |
|
97 "Proper \<equiv> \<guillemotleft> Proper_Roots \<acute>M \<and> Proper_Edges(\<acute>M, \<acute>E) \<and> \<acute>Proper_M_init \<guillemotright>" |
|
98 |
|
99 Safe :: "gar_coll_state \<Rightarrow> bool" |
|
100 "Safe \<equiv> \<guillemotleft> Reach \<acute>E \<subseteq> Blacks \<acute>M \<guillemotright>" |
|
101 |
|
102 lemmas collector_defs = Proper_M_init_def Proper_def Safe_def |
|
103 |
|
104 subsubsection {* Blackening the roots *} |
|
105 |
|
106 constdefs |
|
107 Blacken_Roots :: " gar_coll_state ann_com" |
|
108 "Blacken_Roots \<equiv> |
|
109 .{\<acute>Proper}. |
|
110 \<acute>ind:=0;; |
|
111 .{\<acute>Proper \<and> \<acute>ind=0}. |
|
112 WHILE \<acute>ind<length \<acute>M |
|
113 INV .{\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind\<le>length \<acute>M}. |
|
114 DO .{\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M}. |
|
115 IF \<acute>ind\<in>Roots THEN |
|
116 .{\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<in>Roots}. |
|
117 \<acute>M:=\<acute>M[\<acute>ind:=Black] FI;; |
|
118 .{\<acute>Proper \<and> (\<forall>i<\<acute>ind+1. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M}. |
|
119 \<acute>ind:=\<acute>ind+1 |
|
120 OD" |
|
121 |
|
122 lemma Blacken_Roots: |
|
123 "\<turnstile> Blacken_Roots .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M}." |
|
124 apply (unfold Blacken_Roots_def) |
|
125 apply annhoare |
|
126 apply(simp_all add:collector_defs Graph_defs) |
|
127 apply safe |
|
128 apply(simp_all add:nth_list_update) |
|
129 apply (erule less_SucE) |
|
130 apply simp+ |
|
131 apply force |
|
132 apply force |
|
133 done |
|
134 |
|
135 subsubsection {* Propagating black *} |
|
136 |
|
137 constdefs |
|
138 PBInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" |
|
139 "PBInv \<equiv> \<guillemotleft> \<lambda>ind. \<acute>obc < Blacks \<acute>M \<or> (\<forall>i <ind. \<not>BtoW (\<acute>E!i, \<acute>M) \<or> |
|
140 (\<not>\<acute>z \<and> i=R \<and> (snd(\<acute>E!R)) = T \<and> (\<exists>r. ind \<le> r \<and> r < length \<acute>E \<and> BtoW(\<acute>E!r,\<acute>M))))\<guillemotright>" |
|
141 |
|
142 constdefs |
|
143 Propagate_Black_aux :: "gar_coll_state ann_com" |
|
144 "Propagate_Black_aux \<equiv> |
|
145 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M}. |
|
146 \<acute>ind:=0;; |
|
147 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> \<acute>ind=0}. |
|
148 WHILE \<acute>ind<length \<acute>E |
|
149 INV .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
150 \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E}. |
|
151 DO .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
152 \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E}. |
|
153 IF \<acute>M!(fst (\<acute>E!\<acute>ind)) = Black THEN |
|
154 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
155 \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> \<acute>M!fst(\<acute>E!\<acute>ind)=Black}. |
|
156 \<acute>M:=\<acute>M[snd(\<acute>E!\<acute>ind):=Black];; |
|
157 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
158 \<and> \<acute>PBInv (\<acute>ind + 1) \<and> \<acute>ind<length \<acute>E}. |
|
159 \<acute>ind:=\<acute>ind+1 |
|
160 FI |
|
161 OD" |
|
162 |
|
163 lemma Propagate_Black_aux: |
|
164 "\<turnstile> Propagate_Black_aux |
|
165 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
166 \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}." |
|
167 apply (unfold Propagate_Black_aux_def PBInv_def collector_defs) |
|
168 apply annhoare |
|
169 apply(simp_all add:Graph6 Graph7 Graph8 Graph12) |
|
170 apply force |
|
171 apply force |
|
172 apply force |
|
173 --{* 4 subgoals left *} |
|
174 apply clarify |
|
175 apply(simp add:Proper_Edges_def Proper_Roots_def Graph6 Graph7 Graph8 Graph12) |
|
176 apply (erule disjE) |
|
177 apply(rule disjI1) |
|
178 apply(erule Graph13) |
|
179 apply force |
|
180 apply (case_tac "M x ! snd (E x ! ind x)=Black") |
|
181 apply (simp add: Graph10 BtoW_def) |
|
182 apply (rule disjI2) |
|
183 apply clarify |
|
184 apply (erule less_SucE) |
|
185 apply (erule_tac x=i in allE , erule (1) notE impE) |
|
186 apply simp |
|
187 apply clarify |
|
188 apply (drule_tac y = r in le_imp_less_or_eq) |
|
189 apply (erule disjE) |
|
190 apply (subgoal_tac "Suc (ind x)\<le>r") |
|
191 apply fast |
|
192 apply arith |
|
193 apply fast |
|
194 apply fast |
|
195 apply(rule disjI1) |
|
196 apply(erule subset_psubset_trans) |
|
197 apply(erule Graph11) |
|
198 apply fast |
|
199 --{* 3 subgoals left *} |
|
200 apply force |
|
201 apply force |
|
202 --{* last *} |
|
203 apply clarify |
|
204 apply simp |
|
205 apply(subgoal_tac "ind x = length (E x)") |
|
206 apply (rotate_tac -1) |
|
207 apply (simp (asm_lr)) |
|
208 apply(drule Graph1) |
|
209 apply simp |
|
210 apply clarify |
|
211 apply(erule allE, erule impE, assumption) |
|
212 apply force |
|
213 apply force |
|
214 apply arith |
|
215 done |
|
216 |
|
217 subsubsection {* Refining propagating black *} |
|
218 |
|
219 constdefs |
|
220 Auxk :: "gar_coll_state \<Rightarrow> bool" |
|
221 "Auxk \<equiv> \<guillemotleft>\<acute>k<length \<acute>M \<and> (\<acute>M!\<acute>k\<noteq>Black \<or> \<not>BtoW(\<acute>E!\<acute>ind, \<acute>M) \<or> |
|
222 \<acute>obc<Blacks \<acute>M \<or> (\<not>\<acute>z \<and> \<acute>ind=R \<and> snd(\<acute>E!R)=T |
|
223 \<and> (\<exists>r. \<acute>ind<r \<and> r<length \<acute>E \<and> BtoW(\<acute>E!r, \<acute>M))))\<guillemotright>" |
|
224 |
|
225 constdefs |
|
226 Propagate_Black :: " gar_coll_state ann_com" |
|
227 "Propagate_Black \<equiv> |
|
228 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M}. |
|
229 \<acute>ind:=0;; |
|
230 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> \<acute>ind=0}. |
|
231 WHILE \<acute>ind<length \<acute>E |
|
232 INV .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
233 \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E}. |
|
234 DO .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
235 \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E}. |
|
236 IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))=Black THEN |
|
237 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
238 \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black}. |
|
239 \<acute>k:=(snd(\<acute>E!\<acute>ind));; |
|
240 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
241 \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black |
|
242 \<and> \<acute>Auxk}. |
|
243 \<langle>\<acute>M:=\<acute>M[\<acute>k:=Black],, \<acute>ind:=\<acute>ind+1\<rangle> |
|
244 ELSE .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
245 \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E}. |
|
246 \<langle>IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))\<noteq>Black THEN \<acute>ind:=\<acute>ind+1 FI\<rangle> |
|
247 FI |
|
248 OD" |
|
249 |
|
250 lemma Propagate_Black: |
|
251 "\<turnstile> Propagate_Black |
|
252 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
253 \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}." |
|
254 apply (unfold Propagate_Black_def PBInv_def Auxk_def collector_defs) |
|
255 apply annhoare |
|
256 apply(simp_all add:Graph6 Graph7 Graph8 Graph12) |
|
257 apply force |
|
258 apply force |
|
259 apply force |
|
260 --{* 5 subgoals left *} |
|
261 apply clarify |
|
262 apply(simp add:BtoW_def Proper_Edges_def) |
|
263 --{* 4 subgoals left *} |
|
264 apply clarify |
|
265 apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12) |
|
266 apply (erule disjE) |
|
267 apply (rule disjI1) |
|
268 apply (erule psubset_subset_trans) |
|
269 apply (erule Graph9) |
|
270 apply (case_tac "M x!k x=Black") |
|
271 apply (case_tac "M x ! snd (E x ! ind x)=Black") |
|
272 apply (simp add: Graph10 BtoW_def) |
|
273 apply (rule disjI2) |
|
274 apply clarify |
|
275 apply (erule less_SucE) |
|
276 apply (erule_tac x=i in allE , erule (1) notE impE) |
|
277 apply simp |
|
278 apply clarify |
|
279 apply (drule_tac y = r in le_imp_less_or_eq) |
|
280 apply (erule disjE) |
|
281 apply (subgoal_tac "Suc (ind x)\<le>r") |
|
282 apply fast |
|
283 apply arith |
|
284 apply fast |
|
285 apply fast |
|
286 apply (simp add: Graph10 BtoW_def) |
|
287 apply (erule disjE) |
|
288 apply (erule disjI1) |
|
289 apply clarify |
|
290 apply (erule less_SucE) |
|
291 apply force |
|
292 apply simp |
|
293 apply (subgoal_tac "Suc R\<le>r") |
|
294 apply fast |
|
295 apply arith |
|
296 apply(rule disjI1) |
|
297 apply(erule subset_psubset_trans) |
|
298 apply(erule Graph11) |
|
299 apply fast |
|
300 --{* 3 subgoals left *} |
|
301 apply force |
|
302 --{* 2 subgoals left *} |
|
303 apply clarify |
|
304 apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12) |
|
305 apply (erule disjE) |
|
306 apply fast |
|
307 apply clarify |
|
308 apply (erule less_SucE) |
|
309 apply (erule_tac x=i in allE , erule (1) notE impE) |
|
310 apply simp |
|
311 apply clarify |
|
312 apply (drule_tac y = r in le_imp_less_or_eq) |
|
313 apply (erule disjE) |
|
314 apply (subgoal_tac "Suc (ind x)\<le>r") |
|
315 apply fast |
|
316 apply arith |
|
317 apply (simp add: BtoW_def) |
|
318 apply (simp add: BtoW_def) |
|
319 --{* last *} |
|
320 apply clarify |
|
321 apply simp |
|
322 apply(subgoal_tac "ind x = length (E x)") |
|
323 apply (rotate_tac -1) |
|
324 apply (simp (asm_lr)) |
|
325 apply(drule Graph1) |
|
326 apply simp |
|
327 apply clarify |
|
328 apply(erule allE, erule impE, assumption) |
|
329 apply force |
|
330 apply force |
|
331 apply arith |
|
332 done |
|
333 |
|
334 subsubsection {* Counting black nodes *} |
|
335 |
|
336 constdefs |
|
337 CountInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" |
|
338 "CountInv \<equiv> \<guillemotleft> \<lambda>ind. {i. i<ind \<and> \<acute>Ma!i=Black}\<subseteq>\<acute>bc \<guillemotright>" |
|
339 |
|
340 constdefs |
|
341 Count :: " gar_coll_state ann_com" |
|
342 "Count \<equiv> |
|
343 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M |
|
344 \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
345 \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>bc={}}. |
|
346 \<acute>ind:=0;; |
|
347 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M |
|
348 \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
349 \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>bc={} |
|
350 \<and> \<acute>ind=0}. |
|
351 WHILE \<acute>ind<length \<acute>M |
|
352 INV .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M |
|
353 \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
354 \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind |
|
355 \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind\<le>length \<acute>M}. |
|
356 DO .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M |
|
357 \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
358 \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind |
|
359 \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M}. |
|
360 IF \<acute>M!\<acute>ind=Black |
|
361 THEN .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M |
|
362 \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
363 \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind |
|
364 \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black}. |
|
365 \<acute>bc:=insert \<acute>ind \<acute>bc |
|
366 FI;; |
|
367 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M |
|
368 \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
369 \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv (\<acute>ind+1) |
|
370 \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M}. |
|
371 \<acute>ind:=\<acute>ind+1 |
|
372 OD" |
|
373 |
|
374 lemma Count: |
|
375 "\<turnstile> Count |
|
376 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M |
|
377 \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> length \<acute>Ma=length \<acute>M |
|
378 \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)}." |
|
379 apply(unfold Count_def) |
|
380 apply annhoare |
|
381 apply(simp_all add:CountInv_def Graph6 Graph7 Graph8 Graph12 Blacks_def collector_defs) |
|
382 apply force |
|
383 apply force |
|
384 apply force |
|
385 apply clarify |
|
386 apply simp |
|
387 apply(fast elim:less_SucE) |
|
388 apply clarify |
|
389 apply simp |
|
390 apply(fast elim:less_SucE) |
|
391 apply force |
|
392 apply force |
|
393 done |
|
394 |
|
395 subsubsection {* Appending garbage nodes to the free list *} |
|
396 |
|
397 consts Append_to_free :: "nat \<times> edges \<Rightarrow> edges" |
|
398 |
|
399 axioms |
|
400 Append_to_free0: "length (Append_to_free (i, e)) = length e" |
|
401 Append_to_free1: "Proper_Edges (m, e) |
|
402 \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))" |
|
403 Append_to_free2: "i \<notin> Reach e |
|
404 \<Longrightarrow> n \<in> Reach (Append_to_free(i, e)) = ( n = i \<or> n \<in> Reach e)" |
|
405 |
|
406 constdefs |
|
407 AppendInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" |
|
408 "AppendInv \<equiv> \<guillemotleft>\<lambda>ind. \<forall>i<length \<acute>M. ind\<le>i \<longrightarrow> i\<in>Reach \<acute>E \<longrightarrow> \<acute>M!i=Black\<guillemotright>" |
|
409 |
|
410 constdefs |
|
411 Append :: " gar_coll_state ann_com" |
|
412 "Append \<equiv> |
|
413 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe}. |
|
414 \<acute>ind:=0;; |
|
415 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe \<and> \<acute>ind=0}. |
|
416 WHILE \<acute>ind<length \<acute>M |
|
417 INV .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>M}. |
|
418 DO .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M}. |
|
419 IF \<acute>M!\<acute>ind=Black THEN |
|
420 .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black}. |
|
421 \<acute>M:=\<acute>M[\<acute>ind:=White] |
|
422 ELSE .{\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<notin>Reach \<acute>E}. |
|
423 \<acute>E:=Append_to_free(\<acute>ind,\<acute>E) |
|
424 FI;; |
|
425 .{\<acute>Proper \<and> \<acute>AppendInv (\<acute>ind+1) \<and> \<acute>ind<length \<acute>M}. |
|
426 \<acute>ind:=\<acute>ind+1 |
|
427 OD" |
|
428 |
|
429 lemma Append: |
|
430 "\<turnstile> Append .{\<acute>Proper}." |
|
431 apply(unfold Append_def AppendInv_def) |
|
432 apply annhoare |
|
433 apply(simp_all add:collector_defs Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) |
|
434 apply(force simp:Blacks_def nth_list_update) |
|
435 apply force |
|
436 apply force |
|
437 apply(force simp add:Graph_defs) |
|
438 apply force |
|
439 apply clarify |
|
440 apply simp |
|
441 apply(rule conjI) |
|
442 apply (erule Append_to_free1) |
|
443 apply clarify |
|
444 apply (drule_tac n = "i" in Append_to_free2) |
|
445 apply force |
|
446 apply force |
|
447 apply force |
|
448 done |
|
449 |
|
450 subsubsection {* Correctness of the Collector *} |
|
451 |
|
452 constdefs |
|
453 Collector :: " gar_coll_state ann_com" |
|
454 "Collector \<equiv> |
|
455 .{\<acute>Proper}. |
|
456 WHILE True INV .{\<acute>Proper}. |
|
457 DO |
|
458 Blacken_Roots;; |
|
459 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M}. |
|
460 \<acute>obc:={};; |
|
461 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={}}. |
|
462 \<acute>bc:=Roots;; |
|
463 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots}. |
|
464 \<acute>Ma:=M_init;; |
|
465 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots \<and> \<acute>Ma=M_init}. |
|
466 WHILE \<acute>obc\<noteq>\<acute>bc |
|
467 INV .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M |
|
468 \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
469 \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)}. |
|
470 DO .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M}. |
|
471 \<acute>obc:=\<acute>bc;; |
|
472 Propagate_Black;; |
|
473 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
474 \<and> (\<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}. |
|
475 \<acute>Ma:=\<acute>M;; |
|
476 .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma |
|
477 \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> length \<acute>Ma=length \<acute>M |
|
478 \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)}. |
|
479 \<acute>bc:={};; |
|
480 Count |
|
481 OD;; |
|
482 Append |
|
483 OD" |
|
484 |
|
485 lemma Collector: |
|
486 "\<turnstile> Collector .{False}." |
|
487 apply(unfold Collector_def) |
|
488 apply annhoare |
|
489 apply(simp_all add: Blacken_Roots Propagate_Black Count Append) |
|
490 apply(simp_all add:Blacken_Roots_def Propagate_Black_def Count_def Append_def collector_defs) |
|
491 apply (force simp add: Proper_Roots_def) |
|
492 apply force |
|
493 apply force |
|
494 apply clarify |
|
495 apply (erule disjE) |
|
496 apply(simp add:psubsetI) |
|
497 apply(force dest:subset_antisym) |
|
498 done |
|
499 |
|
500 subsection {* Interference Freedom *} |
|
501 |
|
502 lemmas modules = Redirect_Edge_def Color_Target_def Blacken_Roots_def |
|
503 Propagate_Black_def Count_def Append_def |
|
504 lemmas Invariants = PBInv_def Auxk_def CountInv_def AppendInv_def |
|
505 lemmas abbrev = collector_defs mutator_defs Invariants |
|
506 |
|
507 lemma interfree_Blacken_Roots_Redirect_Edge: |
|
508 "interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)" |
|
509 apply (unfold modules) |
|
510 apply interfree_aux |
|
511 apply safe |
|
512 apply (simp_all add:Graph6 Graph12 abbrev) |
|
513 done |
|
514 |
|
515 lemma interfree_Redirect_Edge_Blacken_Roots: |
|
516 "interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)" |
|
517 apply (unfold modules) |
|
518 apply interfree_aux |
|
519 apply safe |
|
520 apply(simp add:abbrev)+ |
|
521 done |
|
522 |
|
523 lemma interfree_Blacken_Roots_Color_Target: |
|
524 "interfree_aux (Some Blacken_Roots, {}, Some Color_Target)" |
|
525 apply (unfold modules) |
|
526 apply interfree_aux |
|
527 apply safe |
|
528 apply(simp_all add:Graph7 Graph8 nth_list_update abbrev) |
|
529 done |
|
530 |
|
531 lemma interfree_Color_Target_Blacken_Roots: |
|
532 "interfree_aux (Some Color_Target, {}, Some Blacken_Roots)" |
|
533 apply (unfold modules ) |
|
534 apply interfree_aux |
|
535 apply safe |
|
536 apply(simp add:abbrev)+ |
|
537 done |
|
538 |
|
539 lemma interfree_Propagate_Black_Redirect_Edge: |
|
540 "interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)" |
|
541 apply (unfold modules ) |
|
542 apply interfree_aux |
|
543 --{* 11 subgoals left *} |
|
544 apply(clarify, simp add:abbrev Graph6 Graph12) |
|
545 apply(clarify, simp add:abbrev Graph6 Graph12) |
|
546 apply(clarify, simp add:abbrev Graph6 Graph12) |
|
547 apply(clarify, simp add:abbrev Graph6 Graph12) |
|
548 apply(erule conjE)+ |
|
549 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym) |
|
550 apply(erule Graph4) |
|
551 apply(simp)+ |
|
552 apply (simp add:BtoW_def) |
|
553 apply (simp add:BtoW_def) |
|
554 apply(rule conjI) |
|
555 apply (force simp add:BtoW_def) |
|
556 apply(erule Graph4) |
|
557 apply simp+ |
|
558 --{* 7 subgoals left *} |
|
559 apply(clarify, simp add:abbrev Graph6 Graph12) |
|
560 apply(erule conjE)+ |
|
561 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym) |
|
562 apply(erule Graph4) |
|
563 apply(simp)+ |
|
564 apply (simp add:BtoW_def) |
|
565 apply (simp add:BtoW_def) |
|
566 apply(rule conjI) |
|
567 apply (force simp add:BtoW_def) |
|
568 apply(erule Graph4) |
|
569 apply simp+ |
|
570 --{* 6 subgoals left *} |
|
571 apply(clarify, simp add:abbrev Graph6 Graph12) |
|
572 apply(erule conjE)+ |
|
573 apply(rule conjI) |
|
574 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym) |
|
575 apply(erule Graph4) |
|
576 apply(simp)+ |
|
577 apply (simp add:BtoW_def) |
|
578 apply (simp add:BtoW_def) |
|
579 apply(rule conjI) |
|
580 apply (force simp add:BtoW_def) |
|
581 apply(erule Graph4) |
|
582 apply simp+ |
|
583 apply(simp add:BtoW_def nth_list_update) |
|
584 apply force |
|
585 --{* 5 subgoals left *} |
|
586 apply(clarify, simp add:abbrev Graph6 Graph12) |
|
587 --{* 4 subgoals left *} |
|
588 apply(clarify, simp add:abbrev Graph6 Graph12) |
|
589 apply(rule conjI) |
|
590 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym) |
|
591 apply(erule Graph4) |
|
592 apply(simp)+ |
|
593 apply (simp add:BtoW_def) |
|
594 apply (simp add:BtoW_def) |
|
595 apply(rule conjI) |
|
596 apply (force simp add:BtoW_def) |
|
597 apply(erule Graph4) |
|
598 apply simp+ |
|
599 apply(rule conjI) |
|
600 apply(simp add:nth_list_update) |
|
601 apply force |
|
602 apply(rule impI, rule impI, erule disjE, erule disjI1, case_tac "R = (ind x)" ,case_tac "M x ! T = Black") |
|
603 apply(force simp add:BtoW_def) |
|
604 apply(case_tac "M x !snd (E x ! ind x)=Black") |
|
605 apply(rule disjI2) |
|
606 apply simp |
|
607 apply (erule Graph5) |
|
608 apply simp+ |
|
609 apply(force simp add:BtoW_def) |
|
610 apply(force simp add:BtoW_def) |
|
611 --{* 3 subgoals left *} |
|
612 apply(clarify, simp add:abbrev Graph6 Graph12) |
|
613 --{* 2 subgoals left *} |
|
614 apply(clarify, simp add:abbrev Graph6 Graph12) |
|
615 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym) |
|
616 apply clarify |
|
617 apply(erule Graph4) |
|
618 apply(simp)+ |
|
619 apply (simp add:BtoW_def) |
|
620 apply (simp add:BtoW_def) |
|
621 apply(rule conjI) |
|
622 apply (force simp add:BtoW_def) |
|
623 apply(erule Graph4) |
|
624 apply simp+ |
|
625 done |
|
626 |
|
627 lemma interfree_Redirect_Edge_Propagate_Black: |
|
628 "interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)" |
|
629 apply (unfold modules ) |
|
630 apply interfree_aux |
|
631 apply(clarify, simp add:abbrev)+ |
|
632 done |
|
633 |
|
634 lemma interfree_Propagate_Black_Color_Target: |
|
635 "interfree_aux (Some Propagate_Black, {}, Some Color_Target)" |
|
636 apply (unfold modules ) |
|
637 apply interfree_aux |
|
638 --{* 11 subgoals left *} |
|
639 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)+ |
|
640 apply(erule conjE)+ |
|
641 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, |
|
642 case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify, |
|
643 erule allE, erule impE, assumption, erule impE, assumption, |
|
644 simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) |
|
645 --{* 7 subgoals left *} |
|
646 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) |
|
647 apply(erule conjE)+ |
|
648 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, |
|
649 case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify, |
|
650 erule allE, erule impE, assumption, erule impE, assumption, |
|
651 simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) |
|
652 --{* 6 subgoals left *} |
|
653 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) |
|
654 apply clarify |
|
655 apply (rule conjI) |
|
656 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, |
|
657 case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify, |
|
658 erule allE, erule impE, assumption, erule impE, assumption, |
|
659 simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) |
|
660 apply(simp add:nth_list_update) |
|
661 --{* 5 subgoals left *} |
|
662 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) |
|
663 --{* 4 subgoals left *} |
|
664 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) |
|
665 apply (rule conjI) |
|
666 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, |
|
667 case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify, |
|
668 erule allE, erule impE, assumption, erule impE, assumption, |
|
669 simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) |
|
670 apply(rule conjI) |
|
671 apply(simp add:nth_list_update) |
|
672 apply(rule impI,rule impI, case_tac "M x!T=Black",rotate_tac -1, force simp add: BtoW_def Graph10, |
|
673 erule subset_psubset_trans, erule Graph11, force) |
|
674 --{* 3 subgoals left *} |
|
675 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) |
|
676 --{* 2 subgoals left *} |
|
677 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) |
|
678 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, |
|
679 case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify, |
|
680 erule allE, erule impE, assumption, erule impE, assumption, |
|
681 simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) |
|
682 --{* 3 subgoals left *} |
|
683 apply(simp add:abbrev) |
|
684 done |
|
685 |
|
686 lemma interfree_Color_Target_Propagate_Black: |
|
687 "interfree_aux (Some Color_Target, {}, Some Propagate_Black)" |
|
688 apply (unfold modules ) |
|
689 apply interfree_aux |
|
690 apply(clarify, simp add:abbrev)+ |
|
691 done |
|
692 |
|
693 lemma interfree_Count_Redirect_Edge: |
|
694 "interfree_aux (Some Count, {}, Some Redirect_Edge)" |
|
695 apply (unfold modules) |
|
696 apply interfree_aux |
|
697 --{* 9 subgoals left *} |
|
698 apply(simp_all add:abbrev Graph6 Graph12) |
|
699 --{* 6 subgoals left *} |
|
700 apply(clarify, simp add:abbrev Graph6 Graph12, |
|
701 erule disjE,erule disjI1,rule disjI2,rule subset_trans, erule Graph3,force,force)+ |
|
702 done |
|
703 |
|
704 lemma interfree_Redirect_Edge_Count: |
|
705 "interfree_aux (Some Redirect_Edge, {}, Some Count)" |
|
706 apply (unfold modules ) |
|
707 apply interfree_aux |
|
708 apply(clarify,simp add:abbrev)+ |
|
709 apply(simp add:abbrev) |
|
710 done |
|
711 |
|
712 lemma interfree_Count_Color_Target: |
|
713 "interfree_aux (Some Count, {}, Some Color_Target)" |
|
714 apply (unfold modules ) |
|
715 apply interfree_aux |
|
716 --{* 9 subgoals left *} |
|
717 apply(simp_all add:abbrev Graph7 Graph8 Graph12) |
|
718 --{* 6 subgoals left *} |
|
719 apply(clarify,simp add:abbrev Graph7 Graph8 Graph12, |
|
720 erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)+ |
|
721 --{* 2 subgoals left *} |
|
722 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) |
|
723 apply(rule conjI) |
|
724 apply(erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9) |
|
725 apply(simp add:nth_list_update) |
|
726 --{* 1 subgoal left *} |
|
727 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12, |
|
728 erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9) |
|
729 done |
|
730 |
|
731 lemma interfree_Color_Target_Count: |
|
732 "interfree_aux (Some Color_Target, {}, Some Count)" |
|
733 apply (unfold modules ) |
|
734 apply interfree_aux |
|
735 apply(clarify, simp add:abbrev)+ |
|
736 apply(simp add:abbrev) |
|
737 done |
|
738 |
|
739 lemma interfree_Append_Redirect_Edge: |
|
740 "interfree_aux (Some Append, {}, Some Redirect_Edge)" |
|
741 apply (unfold modules ) |
|
742 apply interfree_aux |
|
743 apply( simp_all add:abbrev Graph6 Append_to_free0 Append_to_free1 Graph12) |
|
744 apply(clarify, simp add:abbrev Graph6 Append_to_free0 Append_to_free1 Graph12, force dest:Graph3)+ |
|
745 done |
|
746 |
|
747 lemma interfree_Redirect_Edge_Append: |
|
748 "interfree_aux (Some Redirect_Edge, {}, Some Append)" |
|
749 apply (unfold modules ) |
|
750 apply interfree_aux |
|
751 apply(clarify, simp add:abbrev Append_to_free0)+ |
|
752 apply (force simp add: Append_to_free2) |
|
753 apply(clarify, simp add:abbrev Append_to_free0)+ |
|
754 done |
|
755 |
|
756 lemma interfree_Append_Color_Target: |
|
757 "interfree_aux (Some Append, {}, Some Color_Target)" |
|
758 apply (unfold modules ) |
|
759 apply interfree_aux |
|
760 apply(clarify, simp add:abbrev Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update)+ |
|
761 apply(simp add:abbrev Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update) |
|
762 done |
|
763 |
|
764 lemma interfree_Color_Target_Append: |
|
765 "interfree_aux (Some Color_Target, {}, Some Append)" |
|
766 apply (unfold modules ) |
|
767 apply interfree_aux |
|
768 apply(clarify, simp add:abbrev Append_to_free0)+ |
|
769 apply (force simp add: Append_to_free2) |
|
770 apply(clarify,simp add:abbrev Append_to_free0)+ |
|
771 done |
|
772 |
|
773 lemmas collector_mutator_interfree = |
|
774 interfree_Blacken_Roots_Redirect_Edge interfree_Blacken_Roots_Color_Target |
|
775 interfree_Propagate_Black_Redirect_Edge interfree_Propagate_Black_Color_Target |
|
776 interfree_Count_Redirect_Edge interfree_Count_Color_Target |
|
777 interfree_Append_Redirect_Edge interfree_Append_Color_Target |
|
778 interfree_Redirect_Edge_Blacken_Roots interfree_Color_Target_Blacken_Roots |
|
779 interfree_Redirect_Edge_Propagate_Black interfree_Color_Target_Propagate_Black |
|
780 interfree_Redirect_Edge_Count interfree_Color_Target_Count |
|
781 interfree_Redirect_Edge_Append interfree_Color_Target_Append |
|
782 |
|
783 subsubsection {* Interference freedom Collector-Mutator *} |
|
784 |
|
785 lemma interfree_Collector_Mutator: |
|
786 "interfree_aux (Some Collector, {}, Some Mutator)" |
|
787 apply(unfold Collector_def Mutator_def) |
|
788 apply interfree_aux |
|
789 apply(simp_all add:collector_mutator_interfree) |
|
790 apply(unfold modules collector_defs mutator_defs) |
|
791 apply(tactic {* TRYALL (interfree_aux_tac) *}) |
|
792 --{* 32 subgoals left *} |
|
793 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) |
|
794 --{* 20 subgoals left *} |
|
795 apply(tactic{* TRYALL (clarify_tac @{claset}) *}) |
|
796 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) |
|
797 apply(tactic {* TRYALL (etac disjE) *}) |
|
798 apply simp_all |
|
799 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *}) |
|
800 apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{clasimpset}]) *}) |
|
801 apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *}) |
|
802 done |
|
803 |
|
804 subsubsection {* Interference freedom Mutator-Collector *} |
|
805 |
|
806 lemma interfree_Mutator_Collector: |
|
807 "interfree_aux (Some Mutator, {}, Some Collector)" |
|
808 apply(unfold Collector_def Mutator_def) |
|
809 apply interfree_aux |
|
810 apply(simp_all add:collector_mutator_interfree) |
|
811 apply(unfold modules collector_defs mutator_defs) |
|
812 apply(tactic {* TRYALL (interfree_aux_tac) *}) |
|
813 --{* 64 subgoals left *} |
|
814 apply(simp_all add:nth_list_update Invariants Append_to_free0)+ |
|
815 apply(tactic{* TRYALL (clarify_tac @{claset}) *}) |
|
816 --{* 4 subgoals left *} |
|
817 apply force |
|
818 apply(simp add:Append_to_free2) |
|
819 apply force |
|
820 apply(simp add:Append_to_free2) |
|
821 done |
|
822 |
|
823 subsubsection {* The Garbage Collection algorithm *} |
|
824 |
|
825 text {* In total there are 289 verification conditions. *} |
|
826 |
|
827 lemma Gar_Coll: |
|
828 "\<parallel>- .{\<acute>Proper \<and> \<acute>Mut_init \<and> \<acute>z}. |
|
829 COBEGIN |
|
830 Collector |
|
831 .{False}. |
|
832 \<parallel> |
|
833 Mutator |
|
834 .{False}. |
|
835 COEND |
|
836 .{False}." |
|
837 apply oghoare |
|
838 apply(force simp add: Mutator_def Collector_def modules) |
|
839 apply(rule Collector) |
|
840 apply(rule Mutator) |
|
841 apply(simp add:interfree_Collector_Mutator) |
|
842 apply(simp add:interfree_Mutator_Collector) |
|
843 apply force |
|
844 done |
|
845 |
|
846 end |