1(* Title: HOL/UNITY/Simple/Mutex.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1998 University of Cambridge 4 5Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra. 6*) 7 8theory Mutex imports "../UNITY_Main" begin 9 10record state = 11 p :: bool 12 m :: int 13 n :: int 14 u :: bool 15 v :: bool 16 17type_synonym command = "(state*state) set" 18 19 20 (** The program for process U **) 21 22definition U0 :: command 23 where "U0 = {(s,s'). s' = s (|u:=True, m:=1|) & m s = 0}" 24 25definition U1 :: command 26 where "U1 = {(s,s'). s' = s (|p:= v s, m:=2|) & m s = 1}" 27 28definition U2 :: command 29 where "U2 = {(s,s'). s' = s (|m:=3|) & ~ p s & m s = 2}" 30 31definition U3 :: command 32 where "U3 = {(s,s'). s' = s (|u:=False, m:=4|) & m s = 3}" 33 34definition U4 :: command 35 where "U4 = {(s,s'). s' = s (|p:=True, m:=0|) & m s = 4}" 36 37 (** The program for process V **) 38 39definition V0 :: command 40 where "V0 = {(s,s'). s' = s (|v:=True, n:=1|) & n s = 0}" 41 42definition V1 :: command 43 where "V1 = {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = 1}" 44 45definition V2 :: command 46 where "V2 = {(s,s'). s' = s (|n:=3|) & p s & n s = 2}" 47 48definition V3 :: command 49 where "V3 = {(s,s'). s' = s (|v:=False, n:=4|) & n s = 3}" 50 51definition V4 :: command 52 where "V4 = {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}" 53 54definition Mutex :: "state program" 55 where "Mutex = mk_total_program 56 ({s. ~ u s & ~ v s & m s = 0 & n s = 0}, 57 {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, 58 UNIV)" 59 60 61 (** The correct invariants **) 62 63definition IU :: "state set" 64 where "IU = {s. (u s = (1 \<le> m s & m s \<le> 3)) & (m s = 3 --> ~ p s)}" 65 66definition IV :: "state set" 67 where "IV = {s. (v s = (1 \<le> n s & n s \<le> 3)) & (n s = 3 --> p s)}" 68 69 (** The faulty invariant (for U alone) **) 70 71definition bad_IU :: "state set" 72 where "bad_IU = {s. (u s = (1 \<le> m s & m s \<le> 3)) & 73 (3 \<le> m s & m s \<le> 4 --> ~ p s)}" 74 75 76declare Mutex_def [THEN def_prg_Init, simp] 77 78declare U0_def [THEN def_act_simp, simp] 79declare U1_def [THEN def_act_simp, simp] 80declare U2_def [THEN def_act_simp, simp] 81declare U3_def [THEN def_act_simp, simp] 82declare U4_def [THEN def_act_simp, simp] 83declare V0_def [THEN def_act_simp, simp] 84declare V1_def [THEN def_act_simp, simp] 85declare V2_def [THEN def_act_simp, simp] 86declare V3_def [THEN def_act_simp, simp] 87declare V4_def [THEN def_act_simp, simp] 88 89declare IU_def [THEN def_set_simp, simp] 90declare IV_def [THEN def_set_simp, simp] 91declare bad_IU_def [THEN def_set_simp, simp] 92 93lemma IU: "Mutex \<in> Always IU" 94apply (rule AlwaysI, force) 95apply (unfold Mutex_def, safety) 96done 97 98 99lemma IV: "Mutex \<in> Always IV" 100apply (rule AlwaysI, force) 101apply (unfold Mutex_def, safety) 102done 103 104(*The safety property: mutual exclusion*) 105lemma mutual_exclusion: "Mutex \<in> Always {s. ~ (m s = 3 & n s = 3)}" 106apply (rule Always_weaken) 107apply (rule Always_Int_I [OF IU IV], auto) 108done 109 110 111(*The bad invariant FAILS in V1*) 112lemma "Mutex \<in> Always bad_IU" 113apply (rule AlwaysI, force) 114apply (unfold Mutex_def, safety, auto) 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!*) 118oops 119 120 121lemma eq_123: "((1::int) \<le> i & i \<le> 3) = (i = 1 | i = 2 | i = 3)" 122by arith 123 124 125(*** Progress for U ***) 126 127lemma U_F0: "Mutex \<in> {s. m s=2} Unless {s. m s=3}" 128by (unfold Unless_def Mutex_def, safety) 129 130lemma U_F1: "Mutex \<in> {s. m s=1} LeadsTo {s. p s = v s & m s = 2}" 131by (unfold Mutex_def, ensures_tac U1) 132 133lemma U_F2: "Mutex \<in> {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}" 134apply (cut_tac IU) 135apply (unfold Mutex_def, ensures_tac U2) 136done 137 138lemma U_F3: "Mutex \<in> {s. m s = 3} LeadsTo {s. p s}" 139apply (rule_tac B = "{s. m s = 4}" in LeadsTo_Trans) 140 apply (unfold Mutex_def) 141 apply (ensures_tac U3) 142apply (ensures_tac U4) 143done 144 145lemma U_lemma2: "Mutex \<in> {s. m s = 2} LeadsTo {s. p s}" 146apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L 147 Int_lower2 [THEN subset_imp_LeadsTo]]) 148apply (rule LeadsTo_Trans [OF U_F2 U_F3], auto) 149done 150 151lemma U_lemma1: "Mutex \<in> {s. m s = 1} LeadsTo {s. p s}" 152by (rule LeadsTo_Trans [OF U_F1 [THEN LeadsTo_weaken_R] U_lemma2], blast) 153 154lemma U_lemma123: "Mutex \<in> {s. 1 \<le> m s & m s \<le> 3} LeadsTo {s. p s}" 155by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib U_lemma1 U_lemma2 U_F3) 156 157(*Misra's F4*) 158lemma u_Leadsto_p: "Mutex \<in> {s. u s} LeadsTo {s. p s}" 159by (rule Always_LeadsTo_weaken [OF IU U_lemma123], auto) 160 161 162(*** Progress for V ***) 163 164 165lemma V_F0: "Mutex \<in> {s. n s=2} Unless {s. n s=3}" 166by (unfold Unless_def Mutex_def, safety) 167 168lemma V_F1: "Mutex \<in> {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}" 169by (unfold Mutex_def, ensures_tac "V1") 170 171lemma V_F2: "Mutex \<in> {s. p s & n s = 2} LeadsTo {s. n s = 3}" 172apply (cut_tac IV) 173apply (unfold Mutex_def, ensures_tac "V2") 174done 175 176lemma V_F3: "Mutex \<in> {s. n s = 3} LeadsTo {s. ~ p s}" 177apply (rule_tac B = "{s. n s = 4}" in LeadsTo_Trans) 178 apply (unfold Mutex_def) 179 apply (ensures_tac V3) 180apply (ensures_tac V4) 181done 182 183lemma V_lemma2: "Mutex \<in> {s. n s = 2} LeadsTo {s. ~ p s}" 184apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L 185 Int_lower2 [THEN subset_imp_LeadsTo]]) 186apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto) 187done 188 189lemma V_lemma1: "Mutex \<in> {s. n s = 1} LeadsTo {s. ~ p s}" 190by (rule LeadsTo_Trans [OF V_F1 [THEN LeadsTo_weaken_R] V_lemma2], blast) 191 192lemma V_lemma123: "Mutex \<in> {s. 1 \<le> n s & n s \<le> 3} LeadsTo {s. ~ p s}" 193by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib V_lemma1 V_lemma2 V_F3) 194 195 196(*Misra's F4*) 197lemma v_Leadsto_not_p: "Mutex \<in> {s. v s} LeadsTo {s. ~ p s}" 198by (rule Always_LeadsTo_weaken [OF IV V_lemma123], auto) 199 200 201(** Absence of starvation **) 202 203(*Misra's F6*) 204lemma m1_Leadsto_3: "Mutex \<in> {s. m s = 1} LeadsTo {s. m s = 3}" 205apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) 206apply (rule_tac [2] U_F2) 207apply (simp add: Collect_conj_eq) 208apply (subst Un_commute) 209apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) 210 apply (rule_tac [2] PSP_Unless [OF v_Leadsto_not_p U_F0]) 211apply (rule U_F1 [THEN LeadsTo_weaken_R], auto) 212done 213 214(*The same for V*) 215lemma n1_Leadsto_3: "Mutex \<in> {s. n s = 1} LeadsTo {s. n s = 3}" 216apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) 217apply (rule_tac [2] V_F2) 218apply (simp add: Collect_conj_eq) 219apply (subst Un_commute) 220apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) 221 apply (rule_tac [2] PSP_Unless [OF u_Leadsto_p V_F0]) 222apply (rule V_F1 [THEN LeadsTo_weaken_R], auto) 223done 224 225end 226