|
1 (* Title: ZF/UNITY/Mutex.ML |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Computer Laboratory |
|
4 Copyright 2001 University of Cambridge |
|
5 |
|
6 Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra |
|
7 |
|
8 *) |
|
9 |
|
10 (** Variables' types **) |
|
11 |
|
12 AddIffs [p_type, u_type, v_type, m_type, n_type]; |
|
13 |
|
14 Goal "!!s. s:state ==> s`u:bool"; |
|
15 by (dres_inst_tac [("a", "u"), ("A", "variable")] |
|
16 apply_type 1); |
|
17 by (auto_tac (claset(), simpset() addsimps [u_type])); |
|
18 qed "u_apply_type"; |
|
19 |
|
20 Goal "!!s. s:state ==> s`v:bool"; |
|
21 by (dres_inst_tac [("a", "v"), ("A", "variable")] |
|
22 apply_type 1); |
|
23 by (auto_tac (claset(), simpset() addsimps [v_type])); |
|
24 qed "v_apply_type"; |
|
25 |
|
26 |
|
27 Goal "!!s. s:state ==> s`p:bool"; |
|
28 by (dres_inst_tac [("a", "p"), ("A", "variable")] |
|
29 apply_type 1); |
|
30 by (auto_tac (claset(), simpset() addsimps [p_type])); |
|
31 qed "p_apply_type"; |
|
32 |
|
33 Goal "!!s. s:state ==> s`m:int"; |
|
34 by (dres_inst_tac [("a", "m"), ("A", "variable")] |
|
35 apply_type 1); |
|
36 by (auto_tac (claset(), simpset() addsimps [m_type])); |
|
37 qed "m_apply_type"; |
|
38 |
|
39 Goal "!!s. s:state ==> s`n:int"; |
|
40 by (dres_inst_tac [("a", "n"), ("A", "variable")] |
|
41 apply_type 1); |
|
42 by (auto_tac (claset(), simpset() addsimps [n_type])); |
|
43 qed "n_apply_type"; |
|
44 |
|
45 Addsimps [p_apply_type, u_apply_type, v_apply_type, m_apply_type, n_apply_type]; |
|
46 |
|
47 |
|
48 (** Mutex is a program **) |
|
49 |
|
50 Goalw [Mutex_def] |
|
51 "Mutex:program"; |
|
52 by Auto_tac; |
|
53 qed "Mutex_in_program"; |
|
54 AddIffs [Mutex_in_program]; |
|
55 |
|
56 Addsimps [Mutex_def RS def_prg_Init]; |
|
57 program_defs_ref := [Mutex_def]; |
|
58 |
|
59 Addsimps (map simp_of_act |
|
60 [U0_def, U1_def, U2_def, U3_def, U4_def, |
|
61 V0_def, V1_def, V2_def, V3_def, V4_def]); |
|
62 |
|
63 Addsimps (map simp_of_set [U0_def, U1_def, U2_def, U3_def, U4_def, |
|
64 V0_def, V1_def, V2_def, V3_def, V4_def]); |
|
65 |
|
66 Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]); |
|
67 |
|
68 Addsimps [condition_def, actionSet_def]; |
|
69 |
|
70 |
|
71 Addsimps variable.intrs; |
|
72 AddIs variable.intrs; |
|
73 |
|
74 (** In case one wants to be sure that the initial state is not empty **) |
|
75 Goal "some(u:=0,v:=0, m:= #0,n:= #0):Init(Mutex)"; |
|
76 by Auto_tac; |
|
77 by (REPEAT(rtac update_type2 1)); |
|
78 by (auto_tac (claset(), simpset() addsimps [lam_type])); |
|
79 qed "Mutex_Init_not_empty"; |
|
80 |
|
81 Goal "Mutex : Always(IU)"; |
|
82 by (always_tac 1); |
|
83 by Auto_tac; |
|
84 qed "IU"; |
|
85 |
|
86 Goal "Mutex : Always(IV)"; |
|
87 by (always_tac 1); |
|
88 by Auto_tac; |
|
89 qed "IV"; |
|
90 |
|
91 |
|
92 (*The safety property: mutual exclusion*) |
|
93 Goal "Mutex : Always({s:state. ~(s`m = #3 & s`n = #3)})"; |
|
94 by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1); |
|
95 by Auto_tac; |
|
96 qed "mutual_exclusion"; |
|
97 |
|
98 (*The bad invariant FAILS in V1*) |
|
99 |
|
100 Goal "[| x$<#1; #3 $<= x |] ==> P"; |
|
101 by (dres_inst_tac [("j", "#1"), ("k", "#3")] zless_zle_trans 1); |
|
102 by (dres_inst_tac [("j", "x")] zle_zless_trans 2); |
|
103 by Auto_tac; |
|
104 qed "less_lemma"; |
|
105 |
|
106 Goal "Mutex : Always(bad_IU)"; |
|
107 by (always_tac 1); |
|
108 by (auto_tac (claset(), simpset() addsimps [not_zle_iff_zless])); |
|
109 by (auto_tac (claset() addSDs [u_apply_type], simpset() addsimps [bool_def])); |
|
110 by (subgoal_tac "#1 $<= #3" 1); |
|
111 by (dres_inst_tac [("x", "#1"), ("y", "#3")] zle_trans 1); |
|
112 by Auto_tac; |
|
113 by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1); |
|
114 by Auto_tac; |
|
115 (*Resulting state: n=1, p=false, m=4, u=false. |
|
116 Execution of V1 (the command of process v guarded by n=1) sets p:=true, |
|
117 violating the invariant!*) |
|
118 (*Check that subgoals remain: proof failed.*) |
|
119 getgoal 1; |
|
120 |
|
121 |
|
122 (*** Progress for U ***) |
|
123 |
|
124 Goalw [Unless_def] |
|
125 "Mutex : {s:state. s`m=#2} Unless {s:state. s`m=#3}"; |
|
126 by (constrains_tac 1); |
|
127 by Auto_tac; |
|
128 qed "U_F0"; |
|
129 |
|
130 Goal "Mutex : {s:state. s`m=#1} LeadsTo {s:state. s`p = s`v & s`m = #2}"; |
|
131 by (ensures_tac "U1" 1); |
|
132 by Auto_tac; |
|
133 qed "U_F1"; |
|
134 |
|
135 Goal "Mutex : {s:state. s`p =0 & s`m = #2} LeadsTo {s:state. s`m = #3}"; |
|
136 by (cut_facts_tac [IU] 1); |
|
137 by (ensures_tac "U2" 1); |
|
138 by Auto_tac; |
|
139 qed "U_F2"; |
|
140 |
|
141 Goal "Mutex : {s:state. s`m = #3} LeadsTo {s:state. s`p=1}"; |
|
142 by (res_inst_tac [("B", "{s:state. s`m = #4}")] LeadsTo_Trans 1); |
|
143 by (ensures_tac "U4" 2); |
|
144 by (ensures_tac "U3" 1); |
|
145 by Auto_tac; |
|
146 qed "U_F3"; |
|
147 |
|
148 |
|
149 Goal "Mutex : {s:state. s`m = #2} LeadsTo {s:state. s`p=1}"; |
|
150 by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] |
|
151 MRS LeadsTo_Diff) 1); |
|
152 by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1); |
|
153 by Auto_tac; |
|
154 by (auto_tac (claset() addSDs [p_apply_type], simpset() addsimps [bool_def])); |
|
155 val U_lemma2 = result(); |
|
156 |
|
157 Goal "Mutex : {s:state. s`m = #1} LeadsTo {s:state. s`p =1}"; |
|
158 by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1); |
|
159 by Auto_tac; |
|
160 val U_lemma1 = result(); |
|
161 |
|
162 Goal "i:int ==> (#1 $<= i & i $<= #3) <-> (i=#1 | i=#2 | i=#3)"; |
|
163 by Auto_tac; |
|
164 by (auto_tac (claset(), simpset() addsimps [neq_iff_zless])); |
|
165 by (dres_inst_tac [("j", "#3"), ("i", "i")] zle_zless_trans 4); |
|
166 by (dres_inst_tac [("j", "i"), ("i", "#1")] zle_zless_trans 2); |
|
167 by (dres_inst_tac [("j", "i"), ("i", "#1")] zle_zless_trans 1); |
|
168 by Auto_tac; |
|
169 by (rtac zle_anti_sym 1); |
|
170 by (ALLGOALS(asm_simp_tac (simpset() |
|
171 addsimps [zless_add1_iff_zle RS iff_sym]))); |
|
172 qed "eq_123"; |
|
173 |
|
174 |
|
175 Goal "Mutex : {s:state. #1 $<= s`m & s`m $<= #3} LeadsTo {s:state. s`p=1}"; |
|
176 by (simp_tac (simpset() addsimps [m_apply_type RS eq_123, Collect_disj_eq, |
|
177 LeadsTo_Un_distrib, |
|
178 U_lemma1, U_lemma2, U_F3] ) 1); |
|
179 val U_lemma123 = result(); |
|
180 |
|
181 |
|
182 (*Misra's F4*) |
|
183 Goal "Mutex : {s:state. s`u = 1} LeadsTo {s:state. s`p=1}"; |
|
184 by (rtac ([IU, U_lemma123] MRS Always_LeadsTo_weaken) 1); |
|
185 by Auto_tac; |
|
186 qed "u_Leadsto_p"; |
|
187 |
|
188 |
|
189 (*** Progress for V ***) |
|
190 |
|
191 Goalw [Unless_def] |
|
192 "Mutex : {s:state. s`n=#2} Unless {s:state. s`n=#3}"; |
|
193 by (constrains_tac 1); |
|
194 by Auto_tac; |
|
195 qed "V_F0"; |
|
196 |
|
197 Goal "Mutex : {s:state. s`n=#1} LeadsTo {s:state. s`p = not(s`u) & s`n = #2}"; |
|
198 by (ensures_tac "V1" 1); |
|
199 by (auto_tac (claset() addIs [not_type], simpset())); |
|
200 qed "V_F1"; |
|
201 |
|
202 Goal "Mutex : {s:state. s`p=1 & s`n = #2} LeadsTo {s:state. s`n = #3}"; |
|
203 by (cut_facts_tac [IV] 1); |
|
204 by (ensures_tac "V2" 1); |
|
205 by Auto_tac; |
|
206 qed "V_F2"; |
|
207 |
|
208 Goal "Mutex : {s:state. s`n = #3} LeadsTo {s:state. s`p=0}"; |
|
209 by (res_inst_tac [("B", "{s:state. s`n = #4}")] LeadsTo_Trans 1); |
|
210 by (ensures_tac "V4" 2); |
|
211 by (ensures_tac "V3" 1); |
|
212 by Auto_tac; |
|
213 qed "V_F3"; |
|
214 |
|
215 |
|
216 Goal "Mutex : {s:state. s`n = #2} LeadsTo {s:state. s`p=0}"; |
|
217 by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] |
|
218 MRS LeadsTo_Diff) 1); |
|
219 by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1); |
|
220 by Auto_tac; |
|
221 by (auto_tac (claset() addSDs [p_apply_type], simpset() addsimps [bool_def])); |
|
222 val V_lemma2 = result(); |
|
223 |
|
224 Goal "Mutex : {s:state. s`n = #1} LeadsTo {s:state. s`p = 0}"; |
|
225 by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1); |
|
226 by Auto_tac; |
|
227 val V_lemma1 = result(); |
|
228 |
|
229 Goal "Mutex : {s:state. #1 $<= s`n & s`n $<= #3} LeadsTo {s:state. s`p = 0}"; |
|
230 by (simp_tac (simpset() addsimps |
|
231 [n_apply_type RS eq_123, Collect_disj_eq, LeadsTo_Un_distrib, |
|
232 V_lemma1, V_lemma2, V_F3] ) 1); |
|
233 val V_lemma123 = result(); |
|
234 |
|
235 |
|
236 (*Misra's F4*) |
|
237 Goal "Mutex : {s:state. s`v = 1} LeadsTo {s:state. s`p = 0}"; |
|
238 by (rtac ([IV, V_lemma123] MRS Always_LeadsTo_weaken) 1); |
|
239 by Auto_tac; |
|
240 qed "v_Leadsto_not_p"; |
|
241 |
|
242 (** Absence of starvation **) |
|
243 |
|
244 (*Misra's F6*) |
|
245 Goal "Mutex : {s:state. s`m = #1} LeadsTo {s:state. s`m = #3}"; |
|
246 by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1); |
|
247 by (rtac U_F2 2); |
|
248 by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1); |
|
249 by (stac Un_commute 1); |
|
250 by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1); |
|
251 by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless) 2); |
|
252 by (rtac (U_F1 RS LeadsTo_weaken_R) 1); |
|
253 by Auto_tac; |
|
254 by (auto_tac (claset() addSDs [v_apply_type], simpset() addsimps [bool_def])); |
|
255 qed "m1_Leadsto_3"; |
|
256 |
|
257 |
|
258 (*The same for V*) |
|
259 Goal "Mutex : {s:state. s`n = #1} LeadsTo {s:state. s`n = #3}"; |
|
260 by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1); |
|
261 by (rtac V_F2 2); |
|
262 by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1); |
|
263 by (stac Un_commute 1); |
|
264 by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1); |
|
265 by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless) 2); |
|
266 by (rtac (V_F1 RS LeadsTo_weaken_R) 1); |
|
267 by Auto_tac; |
|
268 by (auto_tac (claset() addSDs [u_apply_type], simpset() addsimps [bool_def])); |
|
269 qed "n1_Leadsto_3"; |