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