author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
child 58871  c399ae4b836f 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

1 
(* Title: ZF/UNITY/Mutex.thy 
11479  2 
Author: Sidi O Ehmety, Computer Laboratory 
3 
Copyright 2001 University of Cambridge 

24893  4 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24893
diff
changeset

5 
Based on "A Family of 2Process Mutual Exclusion Algorithms" by J Misra. 
24893  6 

7 
Variables' types are introduced globally so that type verification 

8 
reduces to the usual ZF typechecking \<in> an illtyed expression will 

9 
reduce to the empty set. 

11479  10 
*) 
11 

15634  12 
header{*Mutual Exclusion*} 
13 

14 
theory Mutex 

15 
imports SubstAx 

16 
begin 

17 

18 
text{*Based on "A Family of 2Process Mutual Exclusion Algorithms" by J Misra 

19 

20 
Variables' types are introduced globally so that type verification reduces to 

21 
the usual ZF typechecking: an illtyed expressions reduce to the empty set. 

22 
*} 

23 

24892  24 
abbreviation "p == Var([0])" 
25 
abbreviation "m == Var([1])" 

26 
abbreviation "n == Var([0,0])" 

27 
abbreviation "u == Var([0,1])" 

28 
abbreviation "v == Var([1,0])" 

29 

41779  30 
axiomatization where {** Type declarations **} 
31 
p_type: "type_of(p)=bool & default_val(p)=0" and 

32 
m_type: "type_of(m)=int & default_val(m)=#0" and 

33 
n_type: "type_of(n)=int & default_val(n)=#0" and 

34 
u_type: "type_of(u)=bool & default_val(u)=0" and 

15634  35 
v_type: "type_of(v)=bool & default_val(v)=0" 
24892  36 

24893  37 
definition 
11479  38 
(** The program for process U **) 
24893  39 
"U0 == {<s,t>:state*state. t = s(u:=1, m:=#1) & s`m = #0}" 
11479  40 

24893  41 
definition 
11479  42 
"U1 == {<s,t>:state*state. t = s(p:= s`v, m:=#2) & s`m = #1}" 
43 

24893  44 
definition 
45 
"U2 == {<s,t>:state*state. t = s(m:=#3) & s`p=0 & s`m = #2}" 

11479  46 

24893  47 
definition 
48 
"U3 == {<s,t>:state*state. t=s(u:=0, m:=#4) & s`m = #3}" 

11479  49 

24893  50 
definition 
51 
"U4 == {<s,t>:state*state. t = s(p:=1, m:=#0) & s`m = #4}" 

11479  52 

24892  53 

11479  54 
(** The program for process V **) 
24892  55 

24893  56 
definition 
57 
"V0 == {<s,t>:state*state. t = s (v:=1, n:=#1) & s`n = #0}" 

11479  58 

24893  59 
definition 
60 
"V1 == {<s,t>:state*state. t = s(p:=not(s`u), n:=#2) & s`n = #1}" 

11479  61 

24893  62 
definition 
63 
"V2 == {<s,t>:state*state. t = s(n:=#3) & s`p=1 & s`n = #2}" 

11479  64 

24893  65 
definition 
11479  66 
"V3 == {<s,t>:state*state. t = s (v:=0, n:=#4) & s`n = #3}" 
67 

24893  68 
definition 
69 
"V4 == {<s,t>:state*state. t = s (p:=0, n:=#0) & s`n = #4}" 

11479  70 

24893  71 
definition 
72 
"Mutex == mk_program({s:state. s`u=0 & s`v=0 & s`m = #0 & s`n = #0}, 

14046  73 
{U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, Pow(state*state))" 
11479  74 

75 
(** The correct invariants **) 

76 

24893  77 
definition 
46823  78 
"IU == {s:state. (s`u = 1\<longleftrightarrow>(#1 $<= s`m & s`m $<= #3)) 
79 
& (s`m = #3 \<longrightarrow> s`p=0)}" 

11479  80 

24893  81 
definition 
46823  82 
"IV == {s:state. (s`v = 1 \<longleftrightarrow> (#1 $<= s`n & s`n $<= #3)) 
83 
& (s`n = #3 \<longrightarrow> s`p=1)}" 

11479  84 

85 
(** The faulty invariant (for U alone) **) 

86 

24893  87 
definition 
46823  88 
"bad_IU == {s:state. (s`u = 1 \<longleftrightarrow> (#1 $<= s`m & s`m $<= #3))& 
89 
(#3 $<= s`m & s`m $<= #4 \<longrightarrow> s`p=0)}" 

11479  90 

15634  91 

92 
(** Variables' types **) 

93 

94 
declare p_type [simp] u_type [simp] v_type [simp] m_type [simp] n_type [simp] 

95 

96 
lemma u_value_type: "s \<in> state ==>s`u \<in> bool" 

97 
apply (unfold state_def) 

98 
apply (drule_tac a = u in apply_type, auto) 

99 
done 

100 

101 
lemma v_value_type: "s \<in> state ==> s`v \<in> bool" 

102 
apply (unfold state_def) 

103 
apply (drule_tac a = v in apply_type, auto) 

104 
done 

105 

106 
lemma p_value_type: "s \<in> state ==> s`p \<in> bool" 

107 
apply (unfold state_def) 

108 
apply (drule_tac a = p in apply_type, auto) 

109 
done 

110 

111 
lemma m_value_type: "s \<in> state ==> s`m \<in> int" 

112 
apply (unfold state_def) 

113 
apply (drule_tac a = m in apply_type, auto) 

114 
done 

115 

116 
lemma n_value_type: "s \<in> state ==>s`n \<in> int" 

117 
apply (unfold state_def) 

118 
apply (drule_tac a = n in apply_type, auto) 

119 
done 

120 

121 
declare p_value_type [simp] u_value_type [simp] v_value_type [simp] 

122 
m_value_type [simp] n_value_type [simp] 

123 

124 
declare p_value_type [TC] u_value_type [TC] v_value_type [TC] 

125 
m_value_type [TC] n_value_type [TC] 

126 

127 

128 

129 
text{*Mutex is a program*} 

130 

131 
lemma Mutex_in_program [simp,TC]: "Mutex \<in> program" 

132 
by (simp add: Mutex_def) 

133 

134 

135 
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

136 
declare Mutex_def [program] 
15634  137 

138 
declare U0_def [THEN def_act_simp, simp] 

139 
declare U1_def [THEN def_act_simp, simp] 

140 
declare U2_def [THEN def_act_simp, simp] 

141 
declare U3_def [THEN def_act_simp, simp] 

142 
declare U4_def [THEN def_act_simp, simp] 

143 

144 
declare V0_def [THEN def_act_simp, simp] 

145 
declare V1_def [THEN def_act_simp, simp] 

146 
declare V2_def [THEN def_act_simp, simp] 

147 
declare V3_def [THEN def_act_simp, simp] 

148 
declare V4_def [THEN def_act_simp, simp] 

149 

150 
declare U0_def [THEN def_set_simp, simp] 

151 
declare U1_def [THEN def_set_simp, simp] 

152 
declare U2_def [THEN def_set_simp, simp] 

153 
declare U3_def [THEN def_set_simp, simp] 

154 
declare U4_def [THEN def_set_simp, simp] 

155 

156 
declare V0_def [THEN def_set_simp, simp] 

157 
declare V1_def [THEN def_set_simp, simp] 

158 
declare V2_def [THEN def_set_simp, simp] 

159 
declare V3_def [THEN def_set_simp, simp] 

160 
declare V4_def [THEN def_set_simp, simp] 

161 

162 
declare IU_def [THEN def_set_simp, simp] 

163 
declare IV_def [THEN def_set_simp, simp] 

164 
declare bad_IU_def [THEN def_set_simp, simp] 

165 

166 
lemma IU: "Mutex \<in> Always(IU)" 

24892  167 
apply (rule AlwaysI, force) 
168 
apply (unfold Mutex_def, safety, auto) 

15634  169 
done 
170 

171 
lemma IV: "Mutex \<in> Always(IV)" 

24892  172 
apply (rule AlwaysI, force) 
173 
apply (unfold Mutex_def, safety) 

15634  174 
done 
175 

176 
(*The safety property: mutual exclusion*) 

177 
lemma mutual_exclusion: "Mutex \<in> Always({s \<in> state. ~(s`m = #3 & s`n = #3)})" 

24892  178 
apply (rule Always_weaken) 
15634  179 
apply (rule Always_Int_I [OF IU IV], auto) 
180 
done 

181 

182 
(*The bad invariant FAILS in V1*) 

183 

184 
lemma less_lemma: "[ x$<#1; #3 $<= x ] ==> P" 

185 
apply (drule_tac j = "#1" and k = "#3" in zless_zle_trans) 

186 
apply (drule_tac [2] j = x in zle_zless_trans, auto) 

187 
done 

188 

189 
lemma "Mutex \<in> Always(bad_IU)" 

24892  190 
apply (rule AlwaysI, force) 
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15634
diff
changeset

191 
apply (unfold Mutex_def, safety, auto) 
15634  192 
apply (subgoal_tac "#1 $<= #3") 
193 
apply (drule_tac x = "#1" and y = "#3" in zle_trans, auto) 

194 
apply (simp (no_asm) add: not_zless_iff_zle [THEN iff_sym]) 

195 
apply auto 

24892  196 
(*Resulting state: n=1, p=false, m=4, u=false. 
15634  197 
Execution of V1 (the command of process v guarded by n=1) sets p:=true, 
198 
violating the invariant!*) 

199 
oops 

200 

201 

202 

203 
(*** Progress for U ***) 

204 

205 
lemma U_F0: "Mutex \<in> {s \<in> state. s`m=#2} Unless {s \<in> state. s`m=#3}" 

24893  206 
by (unfold op_Unless_def Mutex_def, safety) 
15634  207 

208 
lemma U_F1: 

209 
"Mutex \<in> {s \<in> state. s`m=#1} LeadsTo {s \<in> state. s`p = s`v & s`m = #2}" 

42814  210 
by (unfold Mutex_def, ensures U1) 
15634  211 

212 
lemma U_F2: "Mutex \<in> {s \<in> state. s`p =0 & s`m = #2} LeadsTo {s \<in> state. s`m = #3}" 

213 
apply (cut_tac IU) 

42814  214 
apply (unfold Mutex_def, ensures U2) 
15634  215 
done 
216 

217 
lemma U_F3: "Mutex \<in> {s \<in> state. s`m = #3} LeadsTo {s \<in> state. s`p=1}" 

218 
apply (rule_tac B = "{s \<in> state. s`m = #4}" in LeadsTo_Trans) 

219 
apply (unfold Mutex_def) 

42814  220 
apply (ensures U3) 
221 
apply (ensures U4) 

15634  222 
done 
223 

224 

225 
lemma U_lemma2: "Mutex \<in> {s \<in> state. s`m = #2} LeadsTo {s \<in> state. s`p=1}" 

226 
apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L 

227 
Int_lower2 [THEN subset_imp_LeadsTo]]) 

228 
apply (rule LeadsTo_Trans [OF U_F2 U_F3], auto) 

229 
apply (auto dest!: p_value_type simp add: bool_def) 

230 
done 

231 

232 
lemma U_lemma1: "Mutex \<in> {s \<in> state. s`m = #1} LeadsTo {s \<in> state. s`p =1}" 

233 
by (rule LeadsTo_Trans [OF U_F1 [THEN LeadsTo_weaken_R] U_lemma2], blast) 

234 

46823  235 
lemma eq_123: "i \<in> int ==> (#1 $<= i & i $<= #3) \<longleftrightarrow> (i=#1  i=#2  i=#3)" 
15634  236 
apply auto 
237 
apply (auto simp add: neq_iff_zless) 

238 
apply (drule_tac [4] j = "#3" and i = i in zle_zless_trans) 

239 
apply (drule_tac [2] j = i and i = "#1" in zle_zless_trans) 

240 
apply (drule_tac j = i and i = "#1" in zle_zless_trans, auto) 

241 
apply (rule zle_anti_sym) 

242 
apply (simp_all (no_asm_simp) add: zless_add1_iff_zle [THEN iff_sym]) 

243 
done 

244 

245 

246 
lemma U_lemma123: "Mutex \<in> {s \<in> state. #1 $<= s`m & s`m $<= #3} LeadsTo {s \<in> state. s`p=1}" 

247 
by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib U_lemma1 U_lemma2 U_F3) 

248 

249 

250 
(*Misra's F4*) 

251 
lemma u_Leadsto_p: "Mutex \<in> {s \<in> state. s`u = 1} LeadsTo {s \<in> state. s`p=1}" 

252 
by (rule Always_LeadsTo_weaken [OF IU U_lemma123], auto) 

253 

254 

255 
(*** Progress for V ***) 

256 

257 
lemma V_F0: "Mutex \<in> {s \<in> state. s`n=#2} Unless {s \<in> state. s`n=#3}" 

24893  258 
by (unfold op_Unless_def Mutex_def, safety) 
15634  259 

260 
lemma V_F1: "Mutex \<in> {s \<in> state. s`n=#1} LeadsTo {s \<in> state. s`p = not(s`u) & s`n = #2}" 

42814  261 
by (unfold Mutex_def, ensures "V1") 
15634  262 

263 
lemma V_F2: "Mutex \<in> {s \<in> state. s`p=1 & s`n = #2} LeadsTo {s \<in> state. s`n = #3}" 

264 
apply (cut_tac IV) 

42814  265 
apply (unfold Mutex_def, ensures "V2") 
15634  266 
done 
267 

268 
lemma V_F3: "Mutex \<in> {s \<in> state. s`n = #3} LeadsTo {s \<in> state. s`p=0}" 

269 
apply (rule_tac B = "{s \<in> state. s`n = #4}" in LeadsTo_Trans) 

270 
apply (unfold Mutex_def) 

42814  271 
apply (ensures V3) 
272 
apply (ensures V4) 

15634  273 
done 
274 

275 
lemma V_lemma2: "Mutex \<in> {s \<in> state. s`n = #2} LeadsTo {s \<in> state. s`p=0}" 

276 
apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L 

277 
Int_lower2 [THEN subset_imp_LeadsTo]]) 

24892  278 
apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto) 
15634  279 
apply (auto dest!: p_value_type simp add: bool_def) 
280 
done 

281 

282 
lemma V_lemma1: "Mutex \<in> {s \<in> state. s`n = #1} LeadsTo {s \<in> state. s`p = 0}" 

283 
by (rule LeadsTo_Trans [OF V_F1 [THEN LeadsTo_weaken_R] V_lemma2], blast) 

284 

285 
lemma V_lemma123: "Mutex \<in> {s \<in> state. #1 $<= s`n & s`n $<= #3} LeadsTo {s \<in> state. s`p = 0}" 

286 
by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib V_lemma1 V_lemma2 V_F3) 

287 

288 
(*Misra's F4*) 

289 
lemma v_Leadsto_not_p: "Mutex \<in> {s \<in> state. s`v = 1} LeadsTo {s \<in> state. s`p = 0}" 

290 
by (rule Always_LeadsTo_weaken [OF IV V_lemma123], auto) 

291 

292 

293 
(** Absence of starvation **) 

294 

295 
(*Misra's F6*) 

296 
lemma m1_Leadsto_3: "Mutex \<in> {s \<in> state. s`m = #1} LeadsTo {s \<in> state. s`m = #3}" 

297 
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) 

298 
apply (rule_tac [2] U_F2) 

299 
apply (simp add: Collect_conj_eq) 

300 
apply (subst Un_commute) 

301 
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) 

302 
apply (rule_tac [2] PSP_Unless [OF v_Leadsto_not_p U_F0]) 

303 
apply (rule U_F1 [THEN LeadsTo_weaken_R], auto) 

304 
apply (auto dest!: v_value_type simp add: bool_def) 

305 
done 

306 

307 

308 
(*The same for V*) 

309 
lemma n1_Leadsto_3: "Mutex \<in> {s \<in> state. s`n = #1} LeadsTo {s \<in> state. s`n = #3}" 

310 
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) 

311 
apply (rule_tac [2] V_F2) 

312 
apply (simp add: Collect_conj_eq) 

313 
apply (subst Un_commute) 

314 
apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) 

315 
apply (rule_tac [2] PSP_Unless [OF u_Leadsto_p V_F0]) 

316 
apply (rule V_F1 [THEN LeadsTo_weaken_R], auto) 

317 
apply (auto dest!: u_value_type simp add: bool_def) 

318 
done 

319 

11479  320 
end 