[5fdc19]: thys / DiskPaxos / DiskPaxos_Inv1.thy  Maximize  Restore  History

Download this file

211 lines (185 with data), 5.8 kB

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
(* Title: Proving the Correctness of Disk Paxos
ID: $Id: DiskPaxos_Inv1.thy,v 1.3.2.1 2006-05-17 22:47:48 lsf37 Exp $
Author: Mauro J. Jaskelioff, Stephan Merz, 2005
Maintainer: Mauro J. Jaskelioff <mauro at fceia.unr.edu.ar>
*)
header "Proof of Disk Paxos' Invariant"
theory DiskPaxos_Inv1 imports DiskPaxos_Model begin
subsection {* Invariant 1 *}
text{* This is just a type Invariant. *}
constdefs
Inv1 :: "state \<Rightarrow> bool"
"Inv1 s \<equiv> \<forall>p.
inpt s p \<in> Inputs
\<and> phase s p \<le> 3
\<and> finite (allRdBlks s p)"
constdefs
HInv1 :: "state \<Rightarrow> bool"
"HInv1 s \<equiv>
Inv1 s
\<and> allInput s \<subseteq> Inputs"
declare HInv1_def [simp]
text {*
We added the assertion that the set $allRdBlks p$ is finite
for every process $p$; one may therefore choose a block with a
maximum ballot number in action $EndPhase1$.
*}
text {*
With the following the lemma, it will be enough to prove
Inv1 s' for every action, without taking the history variables in account.
*}
lemma HNextPart_Inv1: "\<lbrakk> HInv1 s; HNextPart s s'; Inv1 s' \<rbrakk> \<Longrightarrow> HInv1 s'"
by(auto simp add: HNextPart_def Inv1_def)
theorem HInit_HInv1: "HInit s \<longrightarrow> HInv1 s"
by(auto simp add: HInit_def Inv1_def Init_def allRdBlks_def)
lemma allRdBlks_finite:
assumes inv: "HInv1 s"
and asm: "\<forall>p. allRdBlks s' p \<subseteq> insert bk (allRdBlks s p)"
shows "\<forall>p. finite (allRdBlks s' p)"
proof
fix pp
from inv
have "\<forall>p. finite (allRdBlks s p)"
by(simp add: Inv1_def)
hence "finite (allRdBlks s pp)"
by blast
with asm
show "finite (allRdBlks s' pp)"
by (auto intro: finite_subset)
qed
theorem HPhase1or2ReadThen_HInv1:
assumes inv1: "HInv1 s"
and act: "HPhase1or2ReadThen s s' p d q"
shows "HInv1 s'"
proof -
-- {* we focus on the last conjunct of Inv1 *}
from act
have "\<forall>p. allRdBlks s' p \<subseteq> allRdBlks s p \<union> {\<lparr>block = disk s d q, proc = q\<rparr>}"
by(auto simp add: Phase1or2ReadThen_def allRdBlks_def
split: split_if_asm)
with inv1
have "\<forall>p. finite (allRdBlks s' p)"
by(blast dest: allRdBlks_finite)
-- {* the others conjuncts are trivial *}
with inv1 act
show ?thesis
by(auto simp add: Inv1_def Phase1or2ReadThen_def HNextPart_def)
qed
theorem HEndPhase1_HInv1:
assumes inv1: "HInv1 s"
and act: "HEndPhase1 s s' p"
shows "HInv1 s'"
proof -
from inv1 act
have "Inv1 s'"
by(auto simp add: Inv1_def EndPhase1_def InitializePhase_def allRdBlks_def)
with inv1 act
show ?thesis
by(auto simp del: HInv1_def dest: HNextPart_Inv1)
qed
theorem HStartBallot_HInv1:
assumes inv1: "HInv1 s"
and act: "HStartBallot s s' p"
shows "HInv1 s'"
proof -
from inv1 act
have "Inv1 s'"
by(auto simp add: Inv1_def StartBallot_def InitializePhase_def allRdBlks_def)
with inv1 act
show ?thesis
by(auto simp del: HInv1_def elim: HNextPart_Inv1)
qed
theorem HPhase1or2Write_HInv1:
assumes inv1: "HInv1 s"
and act: "HPhase1or2Write s s' p d"
shows "HInv1 s'"
proof -
from inv1 act
have "Inv1 s'"
by(auto simp add: Inv1_def Phase1or2Write_def allRdBlks_def)
with inv1 act
show ?thesis
by(auto simp del: HInv1_def elim: HNextPart_Inv1)
qed
theorem HPhase1or2ReadElse_HInv1:
assumes act: "HPhase1or2ReadElse s s' p d q"
and inv1: "HInv1 s"
shows "HInv1 s'"
using HStartBallot_HInv1[OF inv1] act
by(auto simp add: Phase1or2ReadElse_def)
theorem HEndPhase2_HInv1:
assumes inv1: "HInv1 s"
and act: "HEndPhase2 s s' p"
shows "HInv1 s'"
proof -
from inv1 act
have "Inv1 s'"
by(auto simp add: Inv1_def EndPhase2_def InitializePhase_def allRdBlks_def)
with inv1 act
show ?thesis
by(auto simp del: HInv1_def elim: HNextPart_Inv1)
qed
theorem HFail_HInv1:
assumes inv1: "HInv1 s"
and act: "HFail s s' p"
shows "HInv1 s'"
proof -
from inv1 act
have "Inv1 s'"
by(auto simp add: Inv1_def Fail_def InitializePhase_def allRdBlks_def)
with inv1 act show ?thesis
by(auto simp del: HInv1_def elim: HNextPart_Inv1)
qed
theorem HPhase0Read_HInv1:
assumes inv1: "HInv1 s"
and act: "HPhase0Read s s' p d"
shows "HInv1 s'"
proof -
-- {* we focus on the last conjunct of Inv1 *}
from act
have "\<forall>pp. allRdBlks s' pp \<subseteq> allRdBlks s pp \<union> {\<lparr>block = disk s d p, proc = p\<rparr>}"
by(auto simp add: Phase0Read_def allRdBlks_def
split: split_if_asm)
with inv1
have "\<forall>p. finite (allRdBlks s' p)"
by(blast dest: allRdBlks_finite)
-- {* the others conjuncts are trivial *}
with inv1 act
have "Inv1 s'"
by(auto simp add: Inv1_def Phase0Read_def)
with inv1 act
show ?thesis
by(auto simp del: HInv1_def elim: HNextPart_Inv1)
qed
theorem HEndPhase0_HInv1:
assumes inv1: "HInv1 s"
and act: "HEndPhase0 s s' p"
shows "HInv1 s'"
proof -
from inv1 act
have "Inv1 s'"
by(auto simp add: Inv1_def EndPhase0_def allRdBlks_def InitializePhase_def)
with inv1 act
show ?thesis
by(auto simp del: HInv1_def elim: HNextPart_Inv1)
qed
declare HInv1_def [simp del]
text {* $HInv1$ is an invariant of $HNext$ *}
lemma I2a:
assumes nxt: "HNext s s'"
and inv: "HInv1 s"
shows "HInv1 s'"
by(auto!
simp add: HNext_def Next_def,
auto intro: HStartBallot_HInv1,
auto intro: HPhase0Read_HInv1,
auto intro: HPhase1or2Write_HInv1,
auto simp add: Phase1or2Read_def
intro: HPhase1or2ReadThen_HInv1
HPhase1or2ReadElse_HInv1,
auto simp add: EndPhase1or2_def
intro: HEndPhase1_HInv1
HEndPhase2_HInv1,
auto intro: HFail_HInv1,
auto intro: HEndPhase0_HInv1)
end

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks