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