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