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