wneuper/isa: src/ZF/UNITY/Mutex.thy@5af15f1e2ef6

     1 (*  Title:      ZF/UNITY/Mutex.thy

     2     Author:     Sidi O Ehmety, Computer Laboratory

     3     Copyright   2001  University of Cambridge

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

     7 Variables' types are introduced globally so that type verification

     8 reduces to the usual ZF typechecking \<in> an ill-tyed expression will

     9 reduce to the empty set.

    10 *)

    12 header{*Mutual Exclusion*}

    14 theory Mutex

    15 imports SubstAx

    16 begin

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

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

    21 the usual ZF typechecking: an ill-tyed expressions reduce to the empty set.

    22 *}

    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])"

    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

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

    37 definition

    38   (** The program for process U **)

    39   "U0 == {<s,t>:state*state. t = s(u:=1, m:=#1) & s`m = #0}"

    41 definition

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

    44 definition

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

    47 definition

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

    50 definition

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

    54    (** The program for process V **)

    56 definition

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

    59 definition

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

    62 definition

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

    65 definition

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

    68 definition

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

    71 definition

    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))"

    75   (** The correct invariants **)

    77 definition

    78   "IU == {s:state. (s`u = 1<->(#1 $<= s`m & s`m $<= #3))

    79                      & (s`m = #3 --> s`p=0)}"

    81 definition

    82   "IV == {s:state. (s`v = 1 <-> (#1 $<= s`n & s`n $<= #3))

    83                       & (s`n = #3 --> s`p=1)}"

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

    87 definition

    88   "bad_IU == {s:state. (s`u = 1 <-> (#1 $<= s`m & s`m  $<= #3))&

    89                    (#3 $<= s`m & s`m $<= #4 --> s`p=0)}"

    92 (** Variables' types **)

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

    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

   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

   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

   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

   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

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

   122         m_value_type [simp] n_value_type [simp]

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

   125         m_value_type [TC] n_value_type [TC]

   129 text{*Mutex is a program*}

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

   132 by (simp add: Mutex_def)

   135 declare Mutex_def [THEN def_prg_Init, simp]

   136 declare Mutex_def [program]

   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]

   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]

   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]

   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]

   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]

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

   167 apply (rule AlwaysI, force)

   168 apply (unfold Mutex_def, safety, auto)

   169 done

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

   172 apply (rule AlwaysI, force)

   173 apply (unfold Mutex_def, safety)

   174 done

   176 (*The safety property: mutual exclusion*)

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

   178 apply (rule Always_weaken)

   179 apply (rule Always_Int_I [OF IU IV], auto)

   180 done

   182 (*The bad invariant FAILS in V1*)

   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

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

   190 apply (rule AlwaysI, force)

   191 apply (unfold Mutex_def, safety, auto)

   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

   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!*)

   199 oops

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

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

   206 by (unfold op_Unless_def Mutex_def, safety)

   208 lemma U_F1:

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

   210 by (unfold Mutex_def, ensures U1)

   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)

   214 apply (unfold Mutex_def, ensures U2)

   215 done

   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)

   220  apply (ensures U3)

   221 apply (ensures U4)

   222 done

   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

   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)

   235 lemma eq_123: "i \<in> int ==> (#1 $<= i & i $<= #3) <-> (i=#1 | i=#2 | i=#3)"

   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

   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)

   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)

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

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

   258 by (unfold op_Unless_def Mutex_def, safety)

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

   261 by (unfold Mutex_def, ensures "V1")

   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)

   265 apply (unfold Mutex_def, ensures "V2")

   266 done

   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)

   271  apply (ensures V3)

   272 apply (ensures V4)

   273 done

   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]])

   278 apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto)

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

   280 done

   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)

   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)

   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)

   293 (** Absence of starvation **)

   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

   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

   320 end

author	wenzelm
	Sun, 15 May 2011 17:45:53 +0200
changeset 43685	5af15f1e2ef6
parent 42650	a68f503805ed
child 47694	57bf0cecb366
permissions	-rw-r--r--