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