src/HOL/UNITY/Simple/Mutex.thy
 changeset 13785 e2fcd88be55d parent 11868 56db9f3a6b3e child 13806 fd40c9d9076b
```     1.1 --- a/src/HOL/UNITY/Simple/Mutex.thy	Thu Jan 23 10:30:14 2003 +0100
1.2 +++ b/src/HOL/UNITY/Simple/Mutex.thy	Fri Jan 24 14:06:49 2003 +0100
1.3 @@ -6,7 +6,7 @@
1.4  Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
1.5  *)
1.6
1.7 -Mutex = SubstAx +
1.8 +theory Mutex = UNITY_Main:
1.9
1.10  record state =
1.11    p :: bool
1.12 @@ -53,7 +53,7 @@
1.13    V4 :: command
1.14      "V4 == {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}"
1.15
1.16 -  Mutex :: state program
1.17 +  Mutex :: "state program"
1.18      "Mutex == mk_program ({s. ~ u s & ~ v s & m s = 0 & n s = 0},
1.19  		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
1.20  			  UNIV)"
1.21 @@ -61,16 +61,166 @@
1.22
1.23    (** The correct invariants **)
1.24
1.25 -  IU :: state set
1.26 +  IU :: "state set"
1.27      "IU == {s. (u s = (1 <= m s & m s <= 3)) & (m s = 3 --> ~ p s)}"
1.28
1.29 -  IV :: state set
1.30 +  IV :: "state set"
1.31      "IV == {s. (v s = (1 <= n s & n s <= 3)) & (n s = 3 --> p s)}"
1.32
1.33    (** The faulty invariant (for U alone) **)
1.34
1.35 -  bad_IU :: state set
1.36 +  bad_IU :: "state set"
1.37      "bad_IU == {s. (u s = (1 <= m s & m s <= 3)) &
1.38  	           (3 <= m s & m s <= 4 --> ~ p s)}"
1.39
1.40 +
1.41 +declare Mutex_def [THEN def_prg_Init, simp]
1.42 +
1.43 +declare U0_def [THEN def_act_simp, simp]
1.44 +declare U1_def [THEN def_act_simp, simp]
1.45 +declare U2_def [THEN def_act_simp, simp]
1.46 +declare U3_def [THEN def_act_simp, simp]
1.47 +declare U4_def [THEN def_act_simp, simp]
1.48 +declare V0_def [THEN def_act_simp, simp]
1.49 +declare V1_def [THEN def_act_simp, simp]
1.50 +declare V2_def [THEN def_act_simp, simp]
1.51 +declare V3_def [THEN def_act_simp, simp]
1.52 +declare V4_def [THEN def_act_simp, simp]
1.53 +
1.54 +declare IU_def [THEN def_set_simp, simp]
1.55 +declare IV_def [THEN def_set_simp, simp]
1.56 +declare bad_IU_def [THEN def_set_simp, simp]
1.57 +
1.58 +lemma IU: "Mutex : Always IU"
1.59 +apply (rule AlwaysI, force)
1.60 +apply (unfold Mutex_def, constrains)
1.61 +done
1.62 +
1.63 +
1.64 +lemma IV: "Mutex : Always IV"
1.65 +apply (rule AlwaysI, force)
1.66 +apply (unfold Mutex_def, constrains)
1.67 +done
1.68 +
1.69 +(*The safety property: mutual exclusion*)
1.70 +lemma mutual_exclusion: "Mutex : Always {s. ~ (m s = 3 & n s = 3)}"
1.71 +apply (rule Always_weaken)
1.72 +apply (rule Always_Int_I [OF IU IV], auto)
1.73 +done
1.74 +
1.75 +
1.76 +(*The bad invariant FAILS in V1*)
1.77 +lemma "Mutex : Always bad_IU"
1.78 +apply (rule AlwaysI, force)
1.79 +apply (unfold Mutex_def, constrains, auto)
1.80 +(*Resulting state: n=1, p=false, m=4, u=false.
1.81 +  Execution of V1 (the command of process v guarded by n=1) sets p:=true,
1.82 +  violating the invariant!*)
1.83 +oops
1.84 +
1.85 +
1.86 +lemma eq_123: "((1::int) <= i & i <= 3) = (i = 1 | i = 2 | i = 3)"
1.87 +by arith
1.88 +
1.89 +
1.90 +(*** Progress for U ***)
1.91 +
1.92 +lemma U_F0: "Mutex : {s. m s=2} Unless {s. m s=3}"
1.93 +by (unfold Unless_def Mutex_def, constrains)
1.94 +
1.95 +lemma U_F1: "Mutex : {s. m s=1} LeadsTo {s. p s = v s & m s = 2}"
1.96 +by (unfold Mutex_def, ensures_tac "U1")
1.97 +
1.98 +lemma U_F2: "Mutex : {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}"
1.99 +apply (cut_tac IU)
1.100 +apply (unfold Mutex_def, ensures_tac U2)
1.101 +done
1.102 +
1.103 +lemma U_F3: "Mutex : {s. m s = 3} LeadsTo {s. p s}"
1.104 +apply (rule_tac B = "{s. m s = 4}" in LeadsTo_Trans)
1.105 + apply (unfold Mutex_def)
1.106 + apply (ensures_tac U3)
1.107 +apply (ensures_tac U4)
1.108 +done
1.109 +
1.110 +lemma U_lemma2: "Mutex : {s. m s = 2} LeadsTo {s. p s}"
1.113 +apply (rule LeadsTo_Trans [OF U_F2 U_F3], auto)
1.114 +done
1.115 +
1.116 +lemma U_lemma1: "Mutex : {s. m s = 1} LeadsTo {s. p s}"
1.118 +
1.119 +lemma U_lemma123: "Mutex : {s. 1 <= m s & m s <= 3} LeadsTo {s. p s}"
1.121 +
1.122 +(*Misra's F4*)
1.123 +lemma u_Leadsto_p: "Mutex : {s. u s} LeadsTo {s. p s}"
1.124 +by (rule Always_LeadsTo_weaken [OF IU U_lemma123], auto)
1.125 +
1.126 +
1.127 +(*** Progress for V ***)
1.128 +
1.129 +
1.130 +lemma V_F0: "Mutex : {s. n s=2} Unless {s. n s=3}"
1.131 +by (unfold Unless_def Mutex_def, constrains)
1.132 +
1.133 +lemma V_F1: "Mutex : {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}"
1.134 +by (unfold Mutex_def, ensures_tac "V1")
1.135 +
1.136 +lemma V_F2: "Mutex : {s. p s & n s = 2} LeadsTo {s. n s = 3}"
1.137 +apply (cut_tac IV)
1.138 +apply (unfold Mutex_def, ensures_tac "V2")
1.139 +done
1.140 +
1.141 +lemma V_F3: "Mutex : {s. n s = 3} LeadsTo {s. ~ p s}"
1.142 +apply (rule_tac B = "{s. n s = 4}" in LeadsTo_Trans)
1.143 + apply (unfold Mutex_def)
1.144 + apply (ensures_tac V3)
1.145 +apply (ensures_tac V4)
1.146 +done
1.147 +
1.148 +lemma V_lemma2: "Mutex : {s. n s = 2} LeadsTo {s. ~ p s}"
1.151 +apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto)
1.152 +done
1.153 +
1.154 +lemma V_lemma1: "Mutex : {s. n s = 1} LeadsTo {s. ~ p s}"
1.156 +
1.157 +lemma V_lemma123: "Mutex : {s. 1 <= n s & n s <= 3} LeadsTo {s. ~ p s}"
1.159 +
1.160 +
1.161 +(*Misra's F4*)
1.162 +lemma v_Leadsto_not_p: "Mutex : {s. v s} LeadsTo {s. ~ p s}"
1.163 +by (rule Always_LeadsTo_weaken [OF IV V_lemma123], auto)
1.164 +
1.165 +
1.166 +(** Absence of starvation **)
1.167 +
1.168 +(*Misra's F6*)
1.169 +lemma m1_Leadsto_3: "Mutex : {s. m s = 1} LeadsTo {s. m s = 3}"
1.171 +apply (rule_tac [2] U_F2)
1.173 +apply (subst Un_commute)
1.175 + apply (rule_tac [2] PSP_Unless [OF v_Leadsto_not_p U_F0])
1.176 +apply (rule U_F1 [THEN LeadsTo_weaken_R], auto)
1.177 +done
1.178 +
1.179 +(*The same for V*)
1.180 +lemma n1_Leadsto_3: "Mutex : {s. n s = 1} LeadsTo {s. n s = 3}"