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