author | wenzelm |
Sun, 07 Oct 2007 15:49:25 +0200 | |
changeset 24892 | c663e675e177 |
parent 24051 | 896fb015079c |
child 24893 | b8ef7afe3a6b |
permissions | -rw-r--r-- |
15634 | 1 |
(* ID: $Id$ |
11479 | 2 |
Author: Sidi O Ehmety, Computer Laboratory |
3 |
Copyright 2001 University of Cambridge |
|
4 |
*) |
|
5 |
||
15634 | 6 |
header{*Mutual Exclusion*} |
7 |
||
8 |
theory Mutex |
|
9 |
imports SubstAx |
|
10 |
begin |
|
11 |
||
12 |
text{*Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra |
|
13 |
||
14 |
Variables' types are introduced globally so that type verification reduces to |
|
15 |
the usual ZF typechecking: an ill-tyed expressions reduce to the empty set. |
|
16 |
*} |
|
17 |
||
24892 | 18 |
abbreviation "p == Var([0])" |
19 |
abbreviation "m == Var([1])" |
|
20 |
abbreviation "n == Var([0,0])" |
|
21 |
abbreviation "u == Var([0,1])" |
|
22 |
abbreviation "v == Var([1,0])" |
|
23 |
||
15634 | 24 |
axioms --{** Type declarations **} |
25 |
p_type: "type_of(p)=bool & default_val(p)=0" |
|
26 |
m_type: "type_of(m)=int & default_val(m)=#0" |
|
27 |
n_type: "type_of(n)=int & default_val(n)=#0" |
|
28 |
u_type: "type_of(u)=bool & default_val(u)=0" |
|
29 |
v_type: "type_of(v)=bool & default_val(v)=0" |
|
24892 | 30 |
|
11479 | 31 |
constdefs |
32 |
(** The program for process U **) |
|
33 |
U0 :: i |
|
34 |
"U0 == {<s,t>:state*state. t = s(u:=1, m:=#1) & s`m = #0}" |
|
35 |
||
36 |
U1 :: i |
|
37 |
"U1 == {<s,t>:state*state. t = s(p:= s`v, m:=#2) & s`m = #1}" |
|
38 |
||
39 |
U2 :: i |
|
40 |
"U2 == {<s,t>:state*state. t = s(m:=#3) & s`p=0 & s`m = #2}" |
|
41 |
||
42 |
U3 :: i |
|
43 |
"U3 == {<s,t>:state*state. t=s(u:=0, m:=#4) & s`m = #3}" |
|
44 |
||
45 |
U4 :: i |
|
46 |
"U4 == {<s,t>:state*state. t = s(p:=1, m:=#0) & s`m = #4}" |
|
47 |
||
24892 | 48 |
|
11479 | 49 |
(** The program for process V **) |
24892 | 50 |
|
11479 | 51 |
V0 :: i |
52 |
"V0 == {<s,t>:state*state. t = s (v:=1, n:=#1) & s`n = #0}" |
|
53 |
||
54 |
V1 :: i |
|
55 |
"V1 == {<s,t>:state*state. t = s(p:=not(s`u), n:=#2) & s`n = #1}" |
|
56 |
||
57 |
V2 :: i |
|
58 |
"V2 == {<s,t>:state*state. t = s(n:=#3) & s`p=1 & s`n = #2}" |
|
59 |
||
60 |
V3 :: i |
|
61 |
"V3 == {<s,t>:state*state. t = s (v:=0, n:=#4) & s`n = #3}" |
|
62 |
||
63 |
V4 :: i |
|
64 |
"V4 == {<s,t>:state*state. t = s (p:=0, n:=#0) & s`n = #4}" |
|
65 |
||
66 |
Mutex :: i |
|
67 |
"Mutex == mk_program({s:state. s`u=0 & s`v=0 & s`m = #0 & s`n = #0}, |
|
14046 | 68 |
{U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, Pow(state*state))" |
11479 | 69 |
|
70 |
(** The correct invariants **) |
|
71 |
||
72 |
IU :: i |
|
73 |
"IU == {s:state. (s`u = 1<->(#1 $<= s`m & s`m $<= #3)) |
|
74 |
& (s`m = #3 --> s`p=0)}" |
|
75 |
||
76 |
IV :: i |
|
77 |
"IV == {s:state. (s`v = 1 <-> (#1 $<= s`n & s`n $<= #3)) |
|
78 |
& (s`n = #3 --> s`p=1)}" |
|
79 |
||
80 |
(** The faulty invariant (for U alone) **) |
|
81 |
||
82 |
bad_IU :: i |
|
83 |
"bad_IU == {s:state. (s`u = 1 <-> (#1 $<= s`m & s`m $<= #3))& |
|
84 |
(#3 $<= s`m & s`m $<= #4 --> s`p=0)}" |
|
85 |
||
15634 | 86 |
|
87 |
(* Title: ZF/UNITY/Mutex.ML |
|
88 |
ID: $Id \<in> Mutex.ML,v 1.4 2003/05/27 09:39:05 paulson Exp $ |
|
89 |
Author: Sidi O Ehmety, Computer Laboratory |
|
90 |
Copyright 2001 University of Cambridge |
|
91 |
||
92 |
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra |
|
93 |
||
94 |
Variables' types are introduced globally so that type verification |
|
95 |
reduces to the usual ZF typechecking \<in> an ill-tyed expression will |
|
96 |
reduce to the empty set. |
|
97 |
||
98 |
*) |
|
99 |
||
100 |
(** Variables' types **) |
|
101 |
||
102 |
declare p_type [simp] u_type [simp] v_type [simp] m_type [simp] n_type [simp] |
|
103 |
||
104 |
lemma u_value_type: "s \<in> state ==>s`u \<in> bool" |
|
105 |
apply (unfold state_def) |
|
106 |
apply (drule_tac a = u in apply_type, auto) |
|
107 |
done |
|
108 |
||
109 |
lemma v_value_type: "s \<in> state ==> s`v \<in> bool" |
|
110 |
apply (unfold state_def) |
|
111 |
apply (drule_tac a = v in apply_type, auto) |
|
112 |
done |
|
113 |
||
114 |
lemma p_value_type: "s \<in> state ==> s`p \<in> bool" |
|
115 |
apply (unfold state_def) |
|
116 |
apply (drule_tac a = p in apply_type, auto) |
|
117 |
done |
|
118 |
||
119 |
lemma m_value_type: "s \<in> state ==> s`m \<in> int" |
|
120 |
apply (unfold state_def) |
|
121 |
apply (drule_tac a = m in apply_type, auto) |
|
122 |
done |
|
123 |
||
124 |
lemma n_value_type: "s \<in> state ==>s`n \<in> int" |
|
125 |
apply (unfold state_def) |
|
126 |
apply (drule_tac a = n in apply_type, auto) |
|
127 |
done |
|
128 |
||
129 |
declare p_value_type [simp] u_value_type [simp] v_value_type [simp] |
|
130 |
m_value_type [simp] n_value_type [simp] |
|
131 |
||
132 |
declare p_value_type [TC] u_value_type [TC] v_value_type [TC] |
|
133 |
m_value_type [TC] n_value_type [TC] |
|
134 |
||
135 |
||
136 |
||
137 |
text{*Mutex is a program*} |
|
138 |
||
139 |
lemma Mutex_in_program [simp,TC]: "Mutex \<in> program" |
|
140 |
by (simp add: Mutex_def) |
|
141 |
||
142 |
||
143 |
declare Mutex_def [THEN def_prg_Init, simp] |
|
24051
896fb015079c
replaced program_defs_ref by proper context data (via attribute "program");
wenzelm
parents:
16183
diff
changeset
|
144 |
declare Mutex_def [program] |
15634 | 145 |
|
146 |
declare U0_def [THEN def_act_simp, simp] |
|
147 |
declare U1_def [THEN def_act_simp, simp] |
|
148 |
declare U2_def [THEN def_act_simp, simp] |
|
149 |
declare U3_def [THEN def_act_simp, simp] |
|
150 |
declare U4_def [THEN def_act_simp, simp] |
|
151 |
||
152 |
declare V0_def [THEN def_act_simp, simp] |
|
153 |
declare V1_def [THEN def_act_simp, simp] |
|
154 |
declare V2_def [THEN def_act_simp, simp] |
|
155 |
declare V3_def [THEN def_act_simp, simp] |
|
156 |
declare V4_def [THEN def_act_simp, simp] |
|
157 |
||
158 |
declare U0_def [THEN def_set_simp, simp] |
|
159 |
declare U1_def [THEN def_set_simp, simp] |
|
160 |
declare U2_def [THEN def_set_simp, simp] |
|
161 |
declare U3_def [THEN def_set_simp, simp] |
|
162 |
declare U4_def [THEN def_set_simp, simp] |
|
163 |
||
164 |
declare V0_def [THEN def_set_simp, simp] |
|
165 |
declare V1_def [THEN def_set_simp, simp] |
|
166 |
declare V2_def [THEN def_set_simp, simp] |
|
167 |
declare V3_def [THEN def_set_simp, simp] |
|
168 |
declare V4_def [THEN def_set_simp, simp] |
|
169 |
||
170 |
declare IU_def [THEN def_set_simp, simp] |
|
171 |
declare IV_def [THEN def_set_simp, simp] |
|
172 |
declare bad_IU_def [THEN def_set_simp, simp] |
|
173 |
||
174 |
lemma IU: "Mutex \<in> Always(IU)" |
|
24892 | 175 |
apply (rule AlwaysI, force) |
176 |
apply (unfold Mutex_def, safety, auto) |
|
15634 | 177 |
done |
178 |
||
179 |
lemma IV: "Mutex \<in> Always(IV)" |
|
24892 | 180 |
apply (rule AlwaysI, force) |
181 |
apply (unfold Mutex_def, safety) |
|
15634 | 182 |
done |
183 |
||
184 |
(*The safety property: mutual exclusion*) |
|
185 |
lemma mutual_exclusion: "Mutex \<in> Always({s \<in> state. ~(s`m = #3 & s`n = #3)})" |
|
24892 | 186 |
apply (rule Always_weaken) |
15634 | 187 |
apply (rule Always_Int_I [OF IU IV], auto) |
188 |
done |
|
189 |
||
190 |
(*The bad invariant FAILS in V1*) |
|
191 |
||
192 |
lemma less_lemma: "[| x$<#1; #3 $<= x |] ==> P" |
|
193 |
apply (drule_tac j = "#1" and k = "#3" in zless_zle_trans) |
|
194 |
apply (drule_tac [2] j = x in zle_zless_trans, auto) |
|
195 |
done |
|
196 |
||
197 |
lemma "Mutex \<in> Always(bad_IU)" |
|
24892 | 198 |
apply (rule AlwaysI, force) |
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15634
diff
changeset
|
199 |
apply (unfold Mutex_def, safety, auto) |
15634 | 200 |
apply (subgoal_tac "#1 $<= #3") |
201 |
apply (drule_tac x = "#1" and y = "#3" in zle_trans, auto) |
|
202 |
apply (simp (no_asm) add: not_zless_iff_zle [THEN iff_sym]) |
|
203 |
apply auto |
|
24892 | 204 |
(*Resulting state: n=1, p=false, m=4, u=false. |
15634 | 205 |
Execution of V1 (the command of process v guarded by n=1) sets p:=true, |
206 |
violating the invariant!*) |
|
207 |
oops |
|
208 |
||
209 |
||
210 |
||
211 |
(*** Progress for U ***) |
|
212 |
||
213 |
lemma U_F0: "Mutex \<in> {s \<in> state. s`m=#2} Unless {s \<in> state. s`m=#3}" |
|
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15634
diff
changeset
|
214 |
by (unfold Unless_def Mutex_def, safety) |
15634 | 215 |
|
216 |
lemma U_F1: |
|
217 |
"Mutex \<in> {s \<in> state. s`m=#1} LeadsTo {s \<in> state. s`p = s`v & s`m = #2}" |
|
218 |
by (unfold Mutex_def, ensures_tac U1) |
|
219 |
||
220 |
lemma U_F2: "Mutex \<in> {s \<in> state. s`p =0 & s`m = #2} LeadsTo {s \<in> state. s`m = #3}" |
|
221 |
apply (cut_tac IU) |
|
222 |
apply (unfold Mutex_def, ensures_tac U2) |
|
223 |
done |
|
224 |
||
225 |
lemma U_F3: "Mutex \<in> {s \<in> state. s`m = #3} LeadsTo {s \<in> state. s`p=1}" |
|
226 |
apply (rule_tac B = "{s \<in> state. s`m = #4}" in LeadsTo_Trans) |
|
227 |
apply (unfold Mutex_def) |
|
228 |
apply (ensures_tac U3) |
|
229 |
apply (ensures_tac U4) |
|
230 |
done |
|
231 |
||
232 |
||
233 |
lemma U_lemma2: "Mutex \<in> {s \<in> state. s`m = #2} LeadsTo {s \<in> state. s`p=1}" |
|
234 |
apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L |
|
235 |
Int_lower2 [THEN subset_imp_LeadsTo]]) |
|
236 |
apply (rule LeadsTo_Trans [OF U_F2 U_F3], auto) |
|
237 |
apply (auto dest!: p_value_type simp add: bool_def) |
|
238 |
done |
|
239 |
||
240 |
lemma U_lemma1: "Mutex \<in> {s \<in> state. s`m = #1} LeadsTo {s \<in> state. s`p =1}" |
|
241 |
by (rule LeadsTo_Trans [OF U_F1 [THEN LeadsTo_weaken_R] U_lemma2], blast) |
|
242 |
||
243 |
lemma eq_123: "i \<in> int ==> (#1 $<= i & i $<= #3) <-> (i=#1 | i=#2 | i=#3)" |
|
244 |
apply auto |
|
245 |
apply (auto simp add: neq_iff_zless) |
|
246 |
apply (drule_tac [4] j = "#3" and i = i in zle_zless_trans) |
|
247 |
apply (drule_tac [2] j = i and i = "#1" in zle_zless_trans) |
|
248 |
apply (drule_tac j = i and i = "#1" in zle_zless_trans, auto) |
|
249 |
apply (rule zle_anti_sym) |
|
250 |
apply (simp_all (no_asm_simp) add: zless_add1_iff_zle [THEN iff_sym]) |
|
251 |
done |
|
252 |
||
253 |
||
254 |
lemma U_lemma123: "Mutex \<in> {s \<in> state. #1 $<= s`m & s`m $<= #3} LeadsTo {s \<in> state. s`p=1}" |
|
255 |
by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib U_lemma1 U_lemma2 U_F3) |
|
256 |
||
257 |
||
258 |
(*Misra's F4*) |
|
259 |
lemma u_Leadsto_p: "Mutex \<in> {s \<in> state. s`u = 1} LeadsTo {s \<in> state. s`p=1}" |
|
260 |
by (rule Always_LeadsTo_weaken [OF IU U_lemma123], auto) |
|
261 |
||
262 |
||
263 |
(*** Progress for V ***) |
|
264 |
||
265 |
lemma V_F0: "Mutex \<in> {s \<in> state. s`n=#2} Unless {s \<in> state. s`n=#3}" |
|
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15634
diff
changeset
|
266 |
by (unfold Unless_def Mutex_def, safety) |
15634 | 267 |
|
268 |
lemma V_F1: "Mutex \<in> {s \<in> state. s`n=#1} LeadsTo {s \<in> state. s`p = not(s`u) & s`n = #2}" |
|
269 |
by (unfold Mutex_def, ensures_tac "V1") |
|
270 |
||
271 |
lemma V_F2: "Mutex \<in> {s \<in> state. s`p=1 & s`n = #2} LeadsTo {s \<in> state. s`n = #3}" |
|
272 |
apply (cut_tac IV) |
|
273 |
apply (unfold Mutex_def, ensures_tac "V2") |
|
274 |
done |
|
275 |
||
276 |
lemma V_F3: "Mutex \<in> {s \<in> state. s`n = #3} LeadsTo {s \<in> state. s`p=0}" |
|
277 |
apply (rule_tac B = "{s \<in> state. s`n = #4}" in LeadsTo_Trans) |
|
278 |
apply (unfold Mutex_def) |
|
279 |
apply (ensures_tac V3) |
|
280 |
apply (ensures_tac V4) |
|
281 |
done |
|
282 |
||
283 |
lemma V_lemma2: "Mutex \<in> {s \<in> state. s`n = #2} LeadsTo {s \<in> state. s`p=0}" |
|
284 |
apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L |
|
285 |
Int_lower2 [THEN subset_imp_LeadsTo]]) |
|
24892 | 286 |
apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto) |
15634 | 287 |
apply (auto dest!: p_value_type simp add: bool_def) |
288 |
done |
|
289 |
||
290 |
lemma V_lemma1: "Mutex \<in> {s \<in> state. s`n = #1} LeadsTo {s \<in> state. s`p = 0}" |
|
291 |
by (rule LeadsTo_Trans [OF V_F1 [THEN LeadsTo_weaken_R] V_lemma2], blast) |
|
292 |
||
293 |
lemma V_lemma123: "Mutex \<in> {s \<in> state. #1 $<= s`n & s`n $<= #3} LeadsTo {s \<in> state. s`p = 0}" |
|
294 |
by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib V_lemma1 V_lemma2 V_F3) |
|
295 |
||
296 |
(*Misra's F4*) |
|
297 |
lemma v_Leadsto_not_p: "Mutex \<in> {s \<in> state. s`v = 1} LeadsTo {s \<in> state. s`p = 0}" |
|
298 |
by (rule Always_LeadsTo_weaken [OF IV V_lemma123], auto) |
|
299 |
||
300 |
||
301 |
(** Absence of starvation **) |
|
302 |
||
303 |
(*Misra's F6*) |
|
304 |
lemma m1_Leadsto_3: "Mutex \<in> {s \<in> state. s`m = #1} LeadsTo {s \<in> state. s`m = #3}" |
|
305 |
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) |
|
306 |
apply (rule_tac [2] U_F2) |
|
307 |
apply (simp add: Collect_conj_eq) |
|
308 |
apply (subst Un_commute) |
|
309 |
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) |
|
310 |
apply (rule_tac [2] PSP_Unless [OF v_Leadsto_not_p U_F0]) |
|
311 |
apply (rule U_F1 [THEN LeadsTo_weaken_R], auto) |
|
312 |
apply (auto dest!: v_value_type simp add: bool_def) |
|
313 |
done |
|
314 |
||
315 |
||
316 |
(*The same for V*) |
|
317 |
lemma n1_Leadsto_3: "Mutex \<in> {s \<in> state. s`n = #1} LeadsTo {s \<in> state. s`n = #3}" |
|
318 |
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) |
|
319 |
apply (rule_tac [2] V_F2) |
|
320 |
apply (simp add: Collect_conj_eq) |
|
321 |
apply (subst Un_commute) |
|
322 |
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) |
|
323 |
apply (rule_tac [2] PSP_Unless [OF u_Leadsto_p V_F0]) |
|
324 |
apply (rule V_F1 [THEN LeadsTo_weaken_R], auto) |
|
325 |
apply (auto dest!: u_value_type simp add: bool_def) |
|
326 |
done |
|
327 |
||
11479 | 328 |
end |