author | wenzelm |
Mon, 11 Jan 2016 22:23:03 +0100 | |
changeset 62146 | 324bc1ffba12 |
parent 62145 | 5b946c81dfbf |
child 67613 | ce654b0e6d69 |
permissions | -rw-r--r-- |
41589 | 1 |
(* Title: HOL/TLA/Memory/Memory.thy |
2 |
Author: Stephan Merz, University of Munich |
|
21624 | 3 |
*) |
3807 | 4 |
|
60592 | 5 |
section \<open>RPC-Memory example: Memory specification\<close> |
3807 | 6 |
|
17309 | 7 |
theory Memory |
8 |
imports MemoryParameters ProcedureInterface |
|
9 |
begin |
|
3807 | 10 |
|
42018 | 11 |
type_synonym memChType = "(memOp, Vals) channel" |
60588 | 12 |
type_synonym memType = "(Locs \<Rightarrow> Vals) stfun" (* intention: MemLocs \<Rightarrow> MemVals *) |
13 |
type_synonym resType = "(PrIds \<Rightarrow> Vals) stfun" |
|
3807 | 14 |
|
62145 | 15 |
|
16 |
(* state predicates *) |
|
17 |
||
18 |
definition MInit :: "memType \<Rightarrow> Locs \<Rightarrow> stpred" |
|
19 |
where "MInit mm l == PRED mm!l = #InitVal" |
|
20 |
||
21 |
definition PInit :: "resType \<Rightarrow> PrIds \<Rightarrow> stpred" |
|
22 |
where "PInit rs p == PRED rs!p = #NotAResult" |
|
23 |
||
24 |
||
25 |
(* auxiliary predicates: is there a pending read/write request for |
|
26 |
some process id and location/value? *) |
|
27 |
||
28 |
definition RdRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> stpred" |
|
29 |
where "RdRequest ch p l == PRED Calling ch p \<and> (arg<ch!p> = #(read l))" |
|
30 |
||
31 |
definition WrRequest :: "memChType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> stpred" |
|
32 |
where "WrRequest ch p l v == PRED Calling ch p \<and> (arg<ch!p> = #(write l v))" |
|
33 |
||
34 |
||
35 |
(* actions *) |
|
36 |
||
37 |
(* a read that doesn't raise BadArg *) |
|
38 |
definition GoodRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action" |
|
39 |
where "GoodRead mm rs p l == ACT #l \<in> #MemLoc \<and> ((rs!p)$ = $(mm!l))" |
|
40 |
||
41 |
(* a read that raises BadArg *) |
|
42 |
definition BadRead :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action" |
|
43 |
where "BadRead mm rs p l == ACT #l \<notin> #MemLoc \<and> ((rs!p)$ = #BadArg)" |
|
3807 | 44 |
|
62145 | 45 |
(* the read action with l visible *) |
46 |
definition ReadInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action" |
|
47 |
where "ReadInner ch mm rs p l == ACT |
|
48 |
$(RdRequest ch p l) |
|
49 |
\<and> (GoodRead mm rs p l \<or> BadRead mm rs p l) |
|
50 |
\<and> unchanged (rtrner ch ! p)" |
|
51 |
||
52 |
(* the read action with l quantified *) |
|
53 |
definition Read :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action" |
|
54 |
where "Read ch mm rs p == ACT (\<exists>l. ReadInner ch mm rs p l)" |
|
3807 | 55 |
|
62145 | 56 |
(* similar definitions for the write action *) |
57 |
definition GoodWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action" |
|
58 |
where "GoodWrite mm rs p l v == |
|
59 |
ACT #l \<in> #MemLoc \<and> #v \<in> #MemVal |
|
60 |
\<and> ((mm!l)$ = #v) \<and> ((rs!p)$ = #OK)" |
|
3807 | 61 |
|
62145 | 62 |
definition BadWrite :: "memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action" |
63 |
where "BadWrite mm rs p l v == ACT |
|
64 |
\<not> (#l \<in> #MemLoc \<and> #v \<in> #MemVal) |
|
65 |
\<and> ((rs!p)$ = #BadArg) \<and> unchanged (mm!l)" |
|
3807 | 66 |
|
62145 | 67 |
definition WriteInner :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> Vals \<Rightarrow> action" |
68 |
where "WriteInner ch mm rs p l v == ACT |
|
69 |
$(WrRequest ch p l v) |
|
70 |
\<and> (GoodWrite mm rs p l v \<or> BadWrite mm rs p l v) |
|
71 |
\<and> unchanged (rtrner ch ! p)" |
|
3807 | 72 |
|
62145 | 73 |
definition Write :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> Locs \<Rightarrow> action" |
74 |
where "Write ch mm rs p l == ACT (\<exists>v. WriteInner ch mm rs p l v)" |
|
75 |
||
3807 | 76 |
|
62145 | 77 |
(* the return action *) |
78 |
definition MemReturn :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action" |
|
79 |
where "MemReturn ch rs p == ACT |
|
80 |
( ($(rs!p) \<noteq> #NotAResult) |
|
81 |
\<and> ((rs!p)$ = #NotAResult) |
|
82 |
\<and> Return ch p (rs!p))" |
|
83 |
||
84 |
(* the failure action of the unreliable memory *) |
|
85 |
definition MemFail :: "memChType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action" |
|
86 |
where "MemFail ch rs p == ACT |
|
87 |
$(Calling ch p) |
|
88 |
\<and> ((rs!p)$ = #MemFailure) |
|
89 |
\<and> unchanged (rtrner ch ! p)" |
|
3807 | 90 |
|
62145 | 91 |
(* next-state relations for reliable / unreliable memory *) |
92 |
definition RNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action" |
|
93 |
where "RNext ch mm rs p == ACT |
|
94 |
( Read ch mm rs p |
|
95 |
\<or> (\<exists>l. Write ch mm rs p l) |
|
96 |
\<or> MemReturn ch rs p)" |
|
97 |
||
98 |
definition UNext :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> action" |
|
99 |
where "UNext ch mm rs p == ACT (RNext ch mm rs p \<or> MemFail ch rs p)" |
|
3807 | 100 |
|
62145 | 101 |
|
102 |
(* temporal formulas *) |
|
103 |
||
104 |
definition RPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal" |
|
105 |
where "RPSpec ch mm rs p == TEMP |
|
106 |
Init(PInit rs p) |
|
107 |
\<and> \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p) |
|
108 |
\<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p) |
|
109 |
\<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)" |
|
6255 | 110 |
|
62145 | 111 |
definition UPSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> PrIds \<Rightarrow> temporal" |
112 |
where "UPSpec ch mm rs p == TEMP |
|
113 |
Init(PInit rs p) |
|
114 |
\<and> \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p) |
|
115 |
\<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p) |
|
116 |
\<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)" |
|
117 |
||
118 |
definition MSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> Locs \<Rightarrow> temporal" |
|
119 |
where "MSpec ch mm rs l == TEMP |
|
120 |
Init(MInit mm l) |
|
121 |
\<and> \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)" |
|
122 |
||
123 |
definition IRSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal" |
|
124 |
where "IRSpec ch mm rs == TEMP |
|
125 |
(\<forall>p. RPSpec ch mm rs p) |
|
126 |
\<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)" |
|
3807 | 127 |
|
62145 | 128 |
definition IUSpec :: "memChType \<Rightarrow> memType \<Rightarrow> resType \<Rightarrow> temporal" |
129 |
where "IUSpec ch mm rs == TEMP |
|
130 |
(\<forall>p. UPSpec ch mm rs p) |
|
131 |
\<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)" |
|
132 |
||
133 |
definition RSpec :: "memChType \<Rightarrow> resType \<Rightarrow> temporal" |
|
134 |
where "RSpec ch rs == TEMP (\<exists>\<exists>mm. IRSpec ch mm rs)" |
|
3807 | 135 |
|
62145 | 136 |
definition USpec :: "memChType \<Rightarrow> temporal" |
137 |
where "USpec ch == TEMP (\<exists>\<exists>mm rs. IUSpec ch mm rs)" |
|
3807 | 138 |
|
62145 | 139 |
(* memory invariant: in the paper, the invariant is hidden in the definition of |
140 |
the predicate S used in the implementation proof, but it is easier to verify |
|
141 |
at this level. *) |
|
142 |
definition MemInv :: "memType \<Rightarrow> Locs \<Rightarrow> stpred" |
|
143 |
where "MemInv mm l == PRED #l \<in> #MemLoc \<longrightarrow> mm!l \<in> #MemVal" |
|
17309 | 144 |
|
21624 | 145 |
lemmas RM_action_defs = |
146 |
MInit_def PInit_def RdRequest_def WrRequest_def MemInv_def |
|
147 |
GoodRead_def BadRead_def ReadInner_def Read_def |
|
148 |
GoodWrite_def BadWrite_def WriteInner_def Write_def |
|
149 |
MemReturn_def RNext_def |
|
150 |
||
151 |
lemmas UM_action_defs = RM_action_defs MemFail_def UNext_def |
|
152 |
||
153 |
lemmas RM_temp_defs = RPSpec_def MSpec_def IRSpec_def |
|
154 |
lemmas UM_temp_defs = UPSpec_def MSpec_def IUSpec_def |
|
155 |
||
156 |
||
157 |
(* The reliable memory is an implementation of the unreliable one *) |
|
60588 | 158 |
lemma ReliableImplementsUnReliable: "\<turnstile> IRSpec ch mm rs \<longrightarrow> IUSpec ch mm rs" |
21624 | 159 |
by (force simp: UNext_def UPSpec_def IUSpec_def RM_temp_defs elim!: STL4E [temp_use] squareE) |
160 |
||
161 |
(* The memory spec implies the memory invariant *) |
|
60588 | 162 |
lemma MemoryInvariant: "\<turnstile> MSpec ch mm rs l \<longrightarrow> \<box>(MemInv mm l)" |
42769 | 163 |
by (auto_invariant simp: RM_temp_defs RM_action_defs) |
21624 | 164 |
|
165 |
(* The invariant is trivial for non-locations *) |
|
60588 | 166 |
lemma NonMemLocInvariant: "\<turnstile> #l \<notin> #MemLoc \<longrightarrow> \<box>(MemInv mm l)" |
21624 | 167 |
by (auto simp: MemInv_def intro!: necT [temp_use]) |
168 |
||
169 |
lemma MemoryInvariantAll: |
|
60591 | 170 |
"\<turnstile> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l) \<longrightarrow> (\<forall>l. \<box>(MemInv mm l))" |
21624 | 171 |
apply clarify |
172 |
apply (auto elim!: MemoryInvariant [temp_use] NonMemLocInvariant [temp_use]) |
|
173 |
done |
|
174 |
||
175 |
(* The memory engages in an action for process p only if there is an |
|
176 |
unanswered call from p. |
|
177 |
We need this only for the reliable memory. |
|
178 |
*) |
|
179 |
||
60588 | 180 |
lemma Memoryidle: "\<turnstile> \<not>$(Calling ch p) \<longrightarrow> \<not> RNext ch mm rs p" |
62146 | 181 |
by (auto simp: AReturn_def RM_action_defs) |
21624 | 182 |
|
183 |
(* Enabledness conditions *) |
|
184 |
||
60588 | 185 |
lemma MemReturn_change: "\<turnstile> MemReturn ch rs p \<longrightarrow> <MemReturn ch rs p>_(rtrner ch ! p, rs!p)" |
21624 | 186 |
by (force simp: MemReturn_def angle_def) |
187 |
||
60588 | 188 |
lemma MemReturn_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) \<Longrightarrow> |
60591 | 189 |
\<turnstile> Calling ch p \<and> (rs!p \<noteq> #NotAResult) |
60588 | 190 |
\<longrightarrow> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))" |
21624 | 191 |
apply (tactic |
60592 | 192 |
\<open>action_simp_tac @{context} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1\<close>) |
21624 | 193 |
apply (tactic |
62146 | 194 |
\<open>action_simp_tac (@{context} addsimps [@{thm MemReturn_def}, @{thm AReturn_def}, |
60592 | 195 |
@{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>) |
21624 | 196 |
done |
197 |
||
60588 | 198 |
lemma ReadInner_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) \<Longrightarrow> |
60591 | 199 |
\<turnstile> Calling ch p \<and> (arg<ch!p> = #(read l)) \<longrightarrow> Enabled (ReadInner ch mm rs p l)" |
21624 | 200 |
apply (case_tac "l : MemLoc") |
201 |
apply (force simp: ReadInner_def GoodRead_def BadRead_def RdRequest_def |
|
202 |
intro!: exI elim!: base_enabled [temp_use])+ |
|
203 |
done |
|
204 |
||
60588 | 205 |
lemma WriteInner_enabled: "\<And>p. basevars (mm!l, rtrner ch ! p, rs!p) \<Longrightarrow> |
60591 | 206 |
\<turnstile> Calling ch p \<and> (arg<ch!p> = #(write l v)) |
60588 | 207 |
\<longrightarrow> Enabled (WriteInner ch mm rs p l v)" |
21624 | 208 |
apply (case_tac "l:MemLoc & v:MemVal") |
209 |
apply (force simp: WriteInner_def GoodWrite_def BadWrite_def WrRequest_def |
|
210 |
intro!: exI elim!: base_enabled [temp_use])+ |
|
211 |
done |
|
212 |
||
60591 | 213 |
lemma ReadResult: "\<turnstile> Read ch mm rs p \<and> (\<forall>l. $(MemInv mm l)) \<longrightarrow> (rs!p)` \<noteq> #NotAResult" |
21624 | 214 |
by (force simp: Read_def ReadInner_def GoodRead_def BadRead_def MemInv_def) |
215 |
||
60588 | 216 |
lemma WriteResult: "\<turnstile> Write ch mm rs p l \<longrightarrow> (rs!p)` \<noteq> #NotAResult" |
21624 | 217 |
by (auto simp: Write_def WriteInner_def GoodWrite_def BadWrite_def) |
218 |
||
60591 | 219 |
lemma ReturnNotReadWrite: "\<turnstile> (\<forall>l. $MemInv mm l) \<and> MemReturn ch rs p |
220 |
\<longrightarrow> \<not> Read ch mm rs p \<and> (\<forall>l. \<not> Write ch mm rs p l)" |
|
21624 | 221 |
by (auto simp: MemReturn_def dest!: WriteResult [temp_use] ReadResult [temp_use]) |
222 |
||
60591 | 223 |
lemma RWRNext_enabled: "\<turnstile> (rs!p = #NotAResult) \<and> (\<forall>l. MemInv mm l) |
224 |
\<and> Enabled (Read ch mm rs p \<or> (\<exists>l. Write ch mm rs p l)) |
|
60588 | 225 |
\<longrightarrow> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))" |
21624 | 226 |
by (force simp: RNext_def angle_def elim!: enabled_mono2 |
227 |
dest: ReadResult [temp_use] WriteResult [temp_use]) |
|
228 |
||
229 |
||
230 |
(* Combine previous lemmas: the memory can make a visible step if there is an |
|
231 |
outstanding call for which no result has been produced. |
|
232 |
*) |
|
60588 | 233 |
lemma RNext_enabled: "\<And>p. \<forall>l. basevars (mm!l, rtrner ch!p, rs!p) \<Longrightarrow> |
60591 | 234 |
\<turnstile> (rs!p = #NotAResult) \<and> Calling ch p \<and> (\<forall>l. MemInv mm l) |
60588 | 235 |
\<longrightarrow> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))" |
21624 | 236 |
apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use]) |
237 |
apply (case_tac "arg (ch w p)") |
|
60592 | 238 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm Read_def}, |
239 |
temp_rewrite @{context} @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1\<close>) |
|
21624 | 240 |
apply (force dest: base_pair [temp_use]) |
241 |
apply (erule contrapos_np) |
|
60592 | 242 |
apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm Write_def}, |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
243 |
temp_rewrite @{context} @{thm enabled_ex}]) |
60592 | 244 |
[@{thm WriteInner_enabled}, exI] [] 1\<close>) |
21624 | 245 |
done |
17309 | 246 |
|
3807 | 247 |
end |