author | paulson |
Tue, 30 Aug 2005 12:47:53 +0200 | |
changeset 17189 | b15f8e094874 |
parent 11703 | 6e5de8d4290a |
child 17309 | c43ed29bd197 |
permissions | -rw-r--r-- |
3807 | 1 |
(* |
2 |
File: MemoryImplementation.thy |
|
3 |
Author: Stephan Merz |
|
4 |
Copyright: 1997 University of Munich |
|
5 |
||
6 |
Theory Name: MemoryImplementation |
|
7 |
Logic Image: TLA |
|
8 |
||
9 |
RPC-Memory example: Memory implementation |
|
10 |
*) |
|
11 |
||
6255 | 12 |
MemoryImplementation = Memory + RPC + MemClerk + Datatype + |
13 |
||
14 |
datatype histState = histA | histB |
|
3807 | 15 |
|
16 |
types |
|
17 |
histType = "(PrIds => histState) stfun" (* the type of the history variable *) |
|
18 |
||
19 |
consts |
|
20 |
(* the specification *) |
|
21 |
(* channel (external) *) |
|
22 |
memCh :: "memChType" |
|
23 |
(* internal variables *) |
|
6255 | 24 |
mm :: "memType" |
3807 | 25 |
|
26 |
(* the state variables of the implementation *) |
|
27 |
(* channels *) |
|
28 |
(* same interface channel memCh *) |
|
29 |
crCh :: "rpcSndChType" |
|
30 |
rmCh :: "rpcRcvChType" |
|
31 |
(* internal variables *) |
|
6255 | 32 |
(* identity refinement mapping for mm -- simply reused *) |
3807 | 33 |
rst :: "rpcStType" |
34 |
cst :: "mClkStType" |
|
35 |
ires :: "resType" |
|
36 |
||
6255 | 37 |
constdefs |
38 |
(* auxiliary predicates *) |
|
39 |
MVOKBARF :: "Vals => bool" |
|
40 |
"MVOKBARF v == (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)" |
|
41 |
MVOKBA :: "Vals => bool" |
|
42 |
"MVOKBA v == (v : MemVal) | (v = OK) | (v = BadArg)" |
|
43 |
MVNROKBA :: "Vals => bool" |
|
44 |
"MVNROKBA v == (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)" |
|
45 |
||
46 |
(* tuples of state functions changed by the various components *) |
|
47 |
e :: "PrIds => (bit * memOp) stfun" |
|
48 |
"e p == PRED (caller memCh!p)" |
|
49 |
c :: "PrIds => (mClkState * (bit * Vals) * (bit * rpcOp)) stfun" |
|
50 |
"c p == PRED (cst!p, rtrner memCh!p, caller crCh!p)" |
|
51 |
r :: "PrIds => (rpcState * (bit * Vals) * (bit * memOp)) stfun" |
|
52 |
"r p == PRED (rst!p, rtrner crCh!p, caller rmCh!p)" |
|
53 |
m :: "PrIds => ((bit * Vals) * Vals) stfun" |
|
54 |
"m p == PRED (rtrner rmCh!p, ires!p)" |
|
55 |
||
3807 | 56 |
(* the environment action *) |
57 |
ENext :: "PrIds => action" |
|
6255 | 58 |
"ENext p == ACT (? l. #l : #MemLoc & Call memCh p #(read l))" |
59 |
||
3807 | 60 |
|
61 |
(* specification of the history variable *) |
|
62 |
HInit :: "histType => PrIds => stpred" |
|
6255 | 63 |
"HInit rmhist p == PRED rmhist!p = #histA" |
64 |
||
3807 | 65 |
HNext :: "histType => PrIds => action" |
6255 | 66 |
"HNext rmhist p == ACT (rmhist!p)$ = |
67 |
(if (MemReturn rmCh ires p | RPCFail crCh rmCh rst p) |
|
68 |
then #histB |
|
69 |
else if (MClkReply memCh crCh cst p) |
|
70 |
then #histA |
|
71 |
else $(rmhist!p))" |
|
72 |
||
3807 | 73 |
HistP :: "histType => PrIds => temporal" |
6255 | 74 |
"HistP rmhist p == TEMP Init HInit rmhist p |
75 |
& [][HNext rmhist p]_(c p,r p,m p, rmhist!p)" |
|
76 |
||
3807 | 77 |
Hist :: "histType => temporal" |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
78 |
"Hist rmhist == TEMP (ALL p. HistP rmhist p)" |
3807 | 79 |
|
80 |
(* the implementation *) |
|
6255 | 81 |
IPImp :: "PrIds => temporal" |
82 |
"IPImp p == TEMP ( Init ~Calling memCh p & [][ENext p]_(e p) |
|
83 |
& MClkIPSpec memCh crCh cst p |
|
84 |
& RPCIPSpec crCh rmCh rst p |
|
85 |
& RPSpec rmCh mm ires p |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
86 |
& (ALL l. #l : #MemLoc --> MSpec rmCh mm ires l))" |
6255 | 87 |
|
3807 | 88 |
ImpInit :: "PrIds => stpred" |
6255 | 89 |
"ImpInit p == PRED ( ~Calling memCh p |
90 |
& MClkInit crCh cst p |
|
91 |
& RPCInit rmCh rst p |
|
92 |
& PInit ires p)" |
|
93 |
||
3807 | 94 |
ImpNext :: "PrIds => action" |
6255 | 95 |
"ImpNext p == ACT [ENext p]_(e p) |
96 |
& [MClkNext memCh crCh cst p]_(c p) |
|
97 |
& [RPCNext crCh rmCh rst p]_(r p) |
|
98 |
& [RNext rmCh mm ires p]_(m p)" |
|
99 |
||
3807 | 100 |
ImpLive :: "PrIds => temporal" |
6255 | 101 |
"ImpLive p == TEMP WF(MClkFwd memCh crCh cst p)_(c p) |
102 |
& SF(MClkReply memCh crCh cst p)_(c p) |
|
103 |
& WF(RPCNext crCh rmCh rst p)_(r p) |
|
104 |
& WF(RNext rmCh mm ires p)_(m p) |
|
105 |
& WF(MemReturn rmCh ires p)_(m p)" |
|
106 |
||
3807 | 107 |
Implementation :: "temporal" |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
108 |
"Implementation == TEMP ( (ALL p. Init (~Calling memCh p) & [][ENext p]_(e p)) |
6255 | 109 |
& MClkISpec memCh crCh cst |
110 |
& RPCISpec crCh rmCh rst |
|
111 |
& IRSpec rmCh mm ires)" |
|
3807 | 112 |
|
113 |
(* the predicate S describes the states of the implementation. |
|
6255 | 114 |
slight simplification: two "histState" parameters instead of a |
115 |
(one- or two-element) set. |
|
116 |
NB: The second conjunct of the definition in the paper is taken care of by |
|
117 |
the type definitions. The last conjunct is asserted separately as the memory |
|
118 |
invariant MemInv, proved in Memory.ML. *) |
|
119 |
S :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred" |
|
120 |
"S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p == PRED |
|
121 |
Calling memCh p = #ecalling |
|
122 |
& Calling crCh p = #ccalling |
|
123 |
& (#ccalling --> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>) |
|
124 |
& (~ #ccalling & cst!p = #clkB --> MVOKBARF<res<crCh!p>>) |
|
125 |
& Calling rmCh p = #rcalling |
|
126 |
& (#rcalling --> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>) |
|
127 |
& (~ #rcalling --> ires!p = #NotAResult) |
|
128 |
& (~ #rcalling & rst!p = #rpcB --> MVOKBA<res<rmCh!p>>) |
|
129 |
& cst!p = #cs |
|
130 |
& rst!p = #rs |
|
131 |
& (rmhist!p = #hs1 | rmhist!p = #hs2) |
|
132 |
& MVNROKBA<ires!p>" |
|
3807 | 133 |
|
134 |
(* predicates S1 -- S6 define special instances of S *) |
|
135 |
S1 :: "histType => PrIds => stpred" |
|
6255 | 136 |
"S1 rmhist p == S rmhist False False False clkA rpcA histA histA p" |
3807 | 137 |
S2 :: "histType => PrIds => stpred" |
6255 | 138 |
"S2 rmhist p == S rmhist True False False clkA rpcA histA histA p" |
3807 | 139 |
S3 :: "histType => PrIds => stpred" |
6255 | 140 |
"S3 rmhist p == S rmhist True True False clkB rpcA histA histB p" |
3807 | 141 |
S4 :: "histType => PrIds => stpred" |
6255 | 142 |
"S4 rmhist p == S rmhist True True True clkB rpcB histA histB p" |
3807 | 143 |
S5 :: "histType => PrIds => stpred" |
6255 | 144 |
"S5 rmhist p == S rmhist True True False clkB rpcB histB histB p" |
3807 | 145 |
S6 :: "histType => PrIds => stpred" |
6255 | 146 |
"S6 rmhist p == S rmhist True False False clkB rpcA histB histB p" |
3807 | 147 |
|
6255 | 148 |
(* The invariant asserts that the system is always in one of S1 - S6, for every p *) |
149 |
ImpInv :: "histType => PrIds => stpred" |
|
150 |
"ImpInv rmhist p == PRED ( S1 rmhist p | S2 rmhist p | S3 rmhist p |
|
151 |
| S4 rmhist p | S5 rmhist p | S6 rmhist p)" |
|
152 |
||
153 |
resbar :: "histType => resType" (* refinement mapping *) |
|
154 |
"resbar rmhist s p == |
|
155 |
(if (S1 rmhist p s | S2 rmhist p s) |
|
156 |
then ires s p |
|
157 |
else if S3 rmhist p s |
|
158 |
then if rmhist s p = histA |
|
159 |
then ires s p else MemFailure |
|
160 |
else if S4 rmhist p s |
|
161 |
then if (rmhist s p = histB & ires s p = NotAResult) |
|
162 |
then MemFailure else ires s p |
|
163 |
else if S5 rmhist p s |
|
164 |
then res (rmCh s p) |
|
165 |
else if S6 rmhist p s |
|
166 |
then if res (crCh s p) = RPCFailure |
|
167 |
then MemFailure else res (crCh s p) |
|
168 |
else NotAResult)" (* dummy value *) |
|
3807 | 169 |
|
170 |
rules |
|
171 |
(* the "base" variables: everything except resbar and hist (for any index) *) |
|
6255 | 172 |
MI_base "basevars (caller memCh!p, |
173 |
(rtrner memCh!p, caller crCh!p, cst!p), |
|
174 |
(rtrner crCh!p, caller rmCh!p, rst!p), |
|
175 |
(mm!l, rtrner rmCh!p, ires!p))" |
|
3807 | 176 |
|
177 |
end |