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