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 |
(* the history variable : not defined as a constant
|
|
37 |
rmhist :: "histType"
|
|
38 |
*)
|
|
39 |
|
6255
|
40 |
constdefs
|
|
41 |
(* auxiliary predicates *)
|
|
42 |
MVOKBARF :: "Vals => bool"
|
|
43 |
"MVOKBARF v == (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)"
|
|
44 |
MVOKBA :: "Vals => bool"
|
|
45 |
"MVOKBA v == (v : MemVal) | (v = OK) | (v = BadArg)"
|
|
46 |
MVNROKBA :: "Vals => bool"
|
|
47 |
"MVNROKBA v == (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)"
|
|
48 |
|
|
49 |
(* tuples of state functions changed by the various components *)
|
|
50 |
e :: "PrIds => (bit * memOp) stfun"
|
|
51 |
"e p == PRED (caller memCh!p)"
|
|
52 |
c :: "PrIds => (mClkState * (bit * Vals) * (bit * rpcOp)) stfun"
|
|
53 |
"c p == PRED (cst!p, rtrner memCh!p, caller crCh!p)"
|
|
54 |
r :: "PrIds => (rpcState * (bit * Vals) * (bit * memOp)) stfun"
|
|
55 |
"r p == PRED (rst!p, rtrner crCh!p, caller rmCh!p)"
|
|
56 |
m :: "PrIds => ((bit * Vals) * Vals) stfun"
|
|
57 |
"m p == PRED (rtrner rmCh!p, ires!p)"
|
|
58 |
|
3807
|
59 |
(* the environment action *)
|
|
60 |
ENext :: "PrIds => action"
|
6255
|
61 |
"ENext p == ACT (? l. #l : #MemLoc & Call memCh p #(read l))"
|
|
62 |
|
3807
|
63 |
|
|
64 |
(* specification of the history variable *)
|
|
65 |
HInit :: "histType => PrIds => stpred"
|
6255
|
66 |
"HInit rmhist p == PRED rmhist!p = #histA"
|
|
67 |
|
3807
|
68 |
HNext :: "histType => PrIds => action"
|
6255
|
69 |
"HNext rmhist p == ACT (rmhist!p)$ =
|
|
70 |
(if (MemReturn rmCh ires p | RPCFail crCh rmCh rst p)
|
|
71 |
then #histB
|
|
72 |
else if (MClkReply memCh crCh cst p)
|
|
73 |
then #histA
|
|
74 |
else $(rmhist!p))"
|
|
75 |
|
3807
|
76 |
HistP :: "histType => PrIds => temporal"
|
6255
|
77 |
"HistP rmhist p == TEMP Init HInit rmhist p
|
|
78 |
& [][HNext rmhist p]_(c p,r p,m p, rmhist!p)"
|
|
79 |
|
3807
|
80 |
Hist :: "histType => temporal"
|
6255
|
81 |
"Hist rmhist == TEMP (!p. HistP rmhist p)"
|
3807
|
82 |
|
|
83 |
(* the implementation *)
|
6255
|
84 |
IPImp :: "PrIds => temporal"
|
|
85 |
"IPImp p == TEMP ( Init ~Calling memCh p & [][ENext p]_(e p)
|
|
86 |
& MClkIPSpec memCh crCh cst p
|
|
87 |
& RPCIPSpec crCh rmCh rst p
|
|
88 |
& RPSpec rmCh mm ires p
|
|
89 |
& (! l. #l : #MemLoc --> MSpec rmCh mm ires l))"
|
|
90 |
|
3807
|
91 |
ImpInit :: "PrIds => stpred"
|
6255
|
92 |
"ImpInit p == PRED ( ~Calling memCh p
|
|
93 |
& MClkInit crCh cst p
|
|
94 |
& RPCInit rmCh rst p
|
|
95 |
& PInit ires p)"
|
|
96 |
|
3807
|
97 |
ImpNext :: "PrIds => action"
|
6255
|
98 |
"ImpNext p == ACT [ENext p]_(e p)
|
|
99 |
& [MClkNext memCh crCh cst p]_(c p)
|
|
100 |
& [RPCNext crCh rmCh rst p]_(r p)
|
|
101 |
& [RNext rmCh mm ires p]_(m p)"
|
|
102 |
|
3807
|
103 |
ImpLive :: "PrIds => temporal"
|
6255
|
104 |
"ImpLive p == TEMP WF(MClkFwd memCh crCh cst p)_(c p)
|
|
105 |
& SF(MClkReply memCh crCh cst p)_(c p)
|
|
106 |
& WF(RPCNext crCh rmCh rst p)_(r p)
|
|
107 |
& WF(RNext rmCh mm ires p)_(m p)
|
|
108 |
& WF(MemReturn rmCh ires p)_(m p)"
|
|
109 |
|
3807
|
110 |
Implementation :: "temporal"
|
6255
|
111 |
"Implementation == TEMP ( (!p. Init (~Calling memCh p) & [][ENext p]_(e p))
|
|
112 |
& MClkISpec memCh crCh cst
|
|
113 |
& RPCISpec crCh rmCh rst
|
|
114 |
& IRSpec rmCh mm ires)"
|
3807
|
115 |
|
|
116 |
(* the predicate S describes the states of the implementation.
|
6255
|
117 |
slight simplification: two "histState" parameters instead of a
|
|
118 |
(one- or two-element) set.
|
|
119 |
NB: The second conjunct of the definition in the paper is taken care of by
|
|
120 |
the type definitions. The last conjunct is asserted separately as the memory
|
|
121 |
invariant MemInv, proved in Memory.ML. *)
|
|
122 |
S :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred"
|
|
123 |
"S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p == PRED
|
|
124 |
Calling memCh p = #ecalling
|
|
125 |
& Calling crCh p = #ccalling
|
|
126 |
& (#ccalling --> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
|
|
127 |
& (~ #ccalling & cst!p = #clkB --> MVOKBARF<res<crCh!p>>)
|
|
128 |
& Calling rmCh p = #rcalling
|
|
129 |
& (#rcalling --> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
|
|
130 |
& (~ #rcalling --> ires!p = #NotAResult)
|
|
131 |
& (~ #rcalling & rst!p = #rpcB --> MVOKBA<res<rmCh!p>>)
|
|
132 |
& cst!p = #cs
|
|
133 |
& rst!p = #rs
|
|
134 |
& (rmhist!p = #hs1 | rmhist!p = #hs2)
|
|
135 |
& MVNROKBA<ires!p>"
|
3807
|
136 |
|
|
137 |
(* predicates S1 -- S6 define special instances of S *)
|
|
138 |
S1 :: "histType => PrIds => stpred"
|
6255
|
139 |
"S1 rmhist p == S rmhist False False False clkA rpcA histA histA p"
|
3807
|
140 |
S2 :: "histType => PrIds => stpred"
|
6255
|
141 |
"S2 rmhist p == S rmhist True False False clkA rpcA histA histA p"
|
3807
|
142 |
S3 :: "histType => PrIds => stpred"
|
6255
|
143 |
"S3 rmhist p == S rmhist True True False clkB rpcA histA histB p"
|
3807
|
144 |
S4 :: "histType => PrIds => stpred"
|
6255
|
145 |
"S4 rmhist p == S rmhist True True True clkB rpcB histA histB p"
|
3807
|
146 |
S5 :: "histType => PrIds => stpred"
|
6255
|
147 |
"S5 rmhist p == S rmhist True True False clkB rpcB histB histB p"
|
3807
|
148 |
S6 :: "histType => PrIds => stpred"
|
6255
|
149 |
"S6 rmhist p == S rmhist True False False clkB rpcA histB histB p"
|
3807
|
150 |
|
6255
|
151 |
(* The invariant asserts that the system is always in one of S1 - S6, for every p *)
|
|
152 |
ImpInv :: "histType => PrIds => stpred"
|
|
153 |
"ImpInv rmhist p == PRED ( S1 rmhist p | S2 rmhist p | S3 rmhist p
|
|
154 |
| S4 rmhist p | S5 rmhist p | S6 rmhist p)"
|
|
155 |
|
|
156 |
resbar :: "histType => resType" (* refinement mapping *)
|
|
157 |
"resbar rmhist s p ==
|
|
158 |
(if (S1 rmhist p s | S2 rmhist p s)
|
|
159 |
then ires s p
|
|
160 |
else if S3 rmhist p s
|
|
161 |
then if rmhist s p = histA
|
|
162 |
then ires s p else MemFailure
|
|
163 |
else if S4 rmhist p s
|
|
164 |
then if (rmhist s p = histB & ires s p = NotAResult)
|
|
165 |
then MemFailure else ires s p
|
|
166 |
else if S5 rmhist p s
|
|
167 |
then res (rmCh s p)
|
|
168 |
else if S6 rmhist p s
|
|
169 |
then if res (crCh s p) = RPCFailure
|
|
170 |
then MemFailure else res (crCh s p)
|
|
171 |
else NotAResult)" (* dummy value *)
|
3807
|
172 |
|
|
173 |
rules
|
|
174 |
(* the "base" variables: everything except resbar and hist (for any index) *)
|
6255
|
175 |
MI_base "basevars (caller memCh!p,
|
|
176 |
(rtrner memCh!p, caller crCh!p, cst!p),
|
|
177 |
(rtrner crCh!p, caller rmCh!p, rst!p),
|
|
178 |
(mm!l, rtrner rmCh!p, ires!p))"
|
3807
|
179 |
|
|
180 |
end
|
|
181 |
|