--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Mon Feb 08 13:02:42 1999 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Mon Feb 08 13:02:56 1999 +0100
@@ -9,7 +9,9 @@
RPC-Memory example: Memory implementation
*)
-MemoryImplementation = Memory + RPC + MemClerk + MIParameters +
+MemoryImplementation = Memory + RPC + MemClerk + Datatype +
+
+datatype histState = histA | histB
types
histType = "(PrIds => histState) stfun" (* the type of the history variable *)
@@ -19,8 +21,7 @@
(* channel (external) *)
memCh :: "memChType"
(* internal variables *)
- mem :: "memType"
- resbar :: "histType => resType" (* defined by refinement mapping *)
+ mm :: "memType"
(* the state variables of the implementation *)
(* channels *)
@@ -28,7 +29,7 @@
crCh :: "rpcSndChType"
rmCh :: "rpcRcvChType"
(* internal variables *)
- (* identity refinement mapping for mem -- simply reused *)
+ (* identity refinement mapping for mm -- simply reused *)
rst :: "rpcStType"
cst :: "mClkStType"
ires :: "resType"
@@ -36,153 +37,145 @@
rmhist :: "histType"
*)
+constdefs
+ (* auxiliary predicates *)
+ MVOKBARF :: "Vals => bool"
+ "MVOKBARF v == (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)"
+ MVOKBA :: "Vals => bool"
+ "MVOKBA v == (v : MemVal) | (v = OK) | (v = BadArg)"
+ MVNROKBA :: "Vals => bool"
+ "MVNROKBA v == (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)"
+
+ (* tuples of state functions changed by the various components *)
+ e :: "PrIds => (bit * memOp) stfun"
+ "e p == PRED (caller memCh!p)"
+ c :: "PrIds => (mClkState * (bit * Vals) * (bit * rpcOp)) stfun"
+ "c p == PRED (cst!p, rtrner memCh!p, caller crCh!p)"
+ r :: "PrIds => (rpcState * (bit * Vals) * (bit * memOp)) stfun"
+ "r p == PRED (rst!p, rtrner crCh!p, caller rmCh!p)"
+ m :: "PrIds => ((bit * Vals) * Vals) stfun"
+ "m p == PRED (rtrner rmCh!p, ires!p)"
+
(* the environment action *)
ENext :: "PrIds => action"
+ "ENext p == ACT (? l. #l : #MemLoc & Call memCh p #(read l))"
+
(* specification of the history variable *)
HInit :: "histType => PrIds => stpred"
+ "HInit rmhist p == PRED rmhist!p = #histA"
+
HNext :: "histType => PrIds => action"
+ "HNext rmhist p == ACT (rmhist!p)$ =
+ (if (MemReturn rmCh ires p | RPCFail crCh rmCh rst p)
+ then #histB
+ else if (MClkReply memCh crCh cst p)
+ then #histA
+ else $(rmhist!p))"
+
HistP :: "histType => PrIds => temporal"
+ "HistP rmhist p == TEMP Init HInit rmhist p
+ & [][HNext rmhist p]_(c p,r p,m p, rmhist!p)"
+
Hist :: "histType => temporal"
+ "Hist rmhist == TEMP (!p. HistP rmhist p)"
(* the implementation *)
+ IPImp :: "PrIds => temporal"
+ "IPImp p == TEMP ( Init ~Calling memCh p & [][ENext p]_(e p)
+ & MClkIPSpec memCh crCh cst p
+ & RPCIPSpec crCh rmCh rst p
+ & RPSpec rmCh mm ires p
+ & (! l. #l : #MemLoc --> MSpec rmCh mm ires l))"
+
ImpInit :: "PrIds => stpred"
+ "ImpInit p == PRED ( ~Calling memCh p
+ & MClkInit crCh cst p
+ & RPCInit rmCh rst p
+ & PInit ires p)"
+
ImpNext :: "PrIds => action"
+ "ImpNext p == ACT [ENext p]_(e p)
+ & [MClkNext memCh crCh cst p]_(c p)
+ & [RPCNext crCh rmCh rst p]_(r p)
+ & [RNext rmCh mm ires p]_(m p)"
+
ImpLive :: "PrIds => temporal"
- IPImp :: "PrIds => temporal"
+ "ImpLive p == TEMP WF(MClkFwd memCh crCh cst p)_(c p)
+ & SF(MClkReply memCh crCh cst p)_(c p)
+ & WF(RPCNext crCh rmCh rst p)_(r p)
+ & WF(RNext rmCh mm ires p)_(m p)
+ & WF(MemReturn rmCh ires p)_(m p)"
+
Implementation :: "temporal"
- ImpInv :: "histType => PrIds => stpred"
-
- (* tuples of state functions changed by the various components *)
- e :: "PrIds => (bit * memArgType) stfun"
- c :: "PrIds => (mClkState * (bit * Vals) * (bit * rpcArgType)) stfun"
- r :: "PrIds => (rpcState * (bit * Vals) * (bit * memArgType)) stfun"
- m :: "PrIds => ((bit * Vals) * Vals) stfun"
+ "Implementation == TEMP ( (!p. Init (~Calling memCh p) & [][ENext p]_(e p))
+ & MClkISpec memCh crCh cst
+ & RPCISpec crCh rmCh rst
+ & IRSpec rmCh mm ires)"
(* the predicate S describes the states of the implementation.
- slight simplification: two "histState" parameters instead of a (one- or
- two-element) set. *)
- S :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred"
+ slight simplification: two "histState" parameters instead of a
+ (one- or two-element) set.
+ NB: The second conjunct of the definition in the paper is taken care of by
+ the type definitions. The last conjunct is asserted separately as the memory
+ invariant MemInv, proved in Memory.ML. *)
+ S :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred"
+ "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p == PRED
+ Calling memCh p = #ecalling
+ & Calling crCh p = #ccalling
+ & (#ccalling --> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
+ & (~ #ccalling & cst!p = #clkB --> MVOKBARF<res<crCh!p>>)
+ & Calling rmCh p = #rcalling
+ & (#rcalling --> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
+ & (~ #rcalling --> ires!p = #NotAResult)
+ & (~ #rcalling & rst!p = #rpcB --> MVOKBA<res<rmCh!p>>)
+ & cst!p = #cs
+ & rst!p = #rs
+ & (rmhist!p = #hs1 | rmhist!p = #hs2)
+ & MVNROKBA<ires!p>"
(* predicates S1 -- S6 define special instances of S *)
S1 :: "histType => PrIds => stpred"
+ "S1 rmhist p == S rmhist False False False clkA rpcA histA histA p"
S2 :: "histType => PrIds => stpred"
+ "S2 rmhist p == S rmhist True False False clkA rpcA histA histA p"
S3 :: "histType => PrIds => stpred"
+ "S3 rmhist p == S rmhist True True False clkB rpcA histA histB p"
S4 :: "histType => PrIds => stpred"
+ "S4 rmhist p == S rmhist True True True clkB rpcB histA histB p"
S5 :: "histType => PrIds => stpred"
+ "S5 rmhist p == S rmhist True True False clkB rpcB histB histB p"
S6 :: "histType => PrIds => stpred"
+ "S6 rmhist p == S rmhist True False False clkB rpcA histB histB p"
- (* auxiliary predicates *)
- MVOKBARF :: "Vals => bool"
- MVOKBA :: "Vals => bool"
- MVNROKBA :: "Vals => bool"
+ (* The invariant asserts that the system is always in one of S1 - S6, for every p *)
+ ImpInv :: "histType => PrIds => stpred"
+ "ImpInv rmhist p == PRED ( S1 rmhist p | S2 rmhist p | S3 rmhist p
+ | S4 rmhist p | S5 rmhist p | S6 rmhist p)"
+
+ resbar :: "histType => resType" (* refinement mapping *)
+ "resbar rmhist s p ==
+ (if (S1 rmhist p s | S2 rmhist p s)
+ then ires s p
+ else if S3 rmhist p s
+ then if rmhist s p = histA
+ then ires s p else MemFailure
+ else if S4 rmhist p s
+ then if (rmhist s p = histB & ires s p = NotAResult)
+ then MemFailure else ires s p
+ else if S5 rmhist p s
+ then res (rmCh s p)
+ else if S6 rmhist p s
+ then if res (crCh s p) = RPCFailure
+ then MemFailure else res (crCh s p)
+ else NotAResult)" (* dummy value *)
rules
- MVOKBARF_def "MVOKBARF v == (MemVal v) | (v = OK) | (v = BadArg) | (v = RPCFailure)"
- MVOKBA_def "MVOKBA v == (MemVal v) | (v = OK) | (v = BadArg)"
- MVNROKBA_def "MVNROKBA v == (MemVal v) | (v = NotAResult) | (v = OK) | (v = BadArg)"
-
(* the "base" variables: everything except resbar and hist (for any index) *)
- MI_base "base_var <caller memCh @ p, rtrner memCh @ p,
- caller crCh @ p, rtrner crCh @ p,
- caller rmCh @ p, rtrner rmCh @ p,
- rst@p, cst@p, mem@l, ires@p>"
-
- (* Environment's next-state relation *)
- ENext_def "ENext p == REX l. #(MemLoc l) .& Call memCh p (#(Inl (read,l)))"
-
- (* Specification of the history variable used in the proof *)
- HInit_def "$(HInit rmhist p) .= ($(rmhist@p) .= #histA)"
- HNext_def "HNext rmhist p ==
- (rmhist@p)$ .=
- (.if (MemReturn rmCh ires p .| RPCFail crCh rmCh rst p)
- .then #histB
- .else .if (MClkReply memCh crCh cst p)
- .then #histA
- .else $(rmhist@p))"
- HistP_def "HistP rmhist p ==
- Init($(HInit rmhist p))
- .& [][HNext rmhist p]_<c p,r p,m p, rmhist@p>"
- Hist_def "Hist rmhist == RALL p. HistP rmhist p"
-
- (* definitions of e,c,r,m *)
- e_def "e p == caller memCh @ p"
- c_def "c p == <cst@p, rtrner memCh @ p, caller crCh @ p>"
- r_def "r p == <rst@p, rtrner crCh @ p, caller rmCh @ p>"
- m_def "m p == <rtrner rmCh @ p, ires@p>"
-
- (* definition of the implementation (without the history variable) *)
- IPImp_def "IPImp p == Init(.~ $(Calling memCh p)) .& [][ENext p]_(e p)
- .& MClkIPSpec memCh crCh cst p
- .& RPCIPSpec crCh rmCh rst p
- .& RPSpec rmCh mem ires p
- .& (RALL l. #(MemLoc l) .-> MSpec rmCh mem ires l)"
-
- ImpInit_def "$(ImpInit p) .= ( .~ $(Calling memCh p) \
-\ .& $(MClkInit crCh cst p) \
-\ .& $(RPCInit rmCh rst p) \
-\ .& $(PInit ires p))"
-
- ImpNext_def "ImpNext p == [ENext p]_(e p)
- .& [MClkNext memCh crCh cst p]_(c p)
- .& [RPCNext crCh rmCh rst p]_(r p)
- .& [RNext rmCh mem ires p]_(m p)"
-
- ImpLive_def "ImpLive p == WF(MClkFwd memCh crCh cst p)_(c p)
- .& SF(MClkReply memCh crCh cst p)_(c p)
- .& WF(RPCNext crCh rmCh rst p)_(r p)
- .& WF(RNext rmCh mem ires p)_(m p)
- .& WF(MemReturn rmCh ires p)_(m p)"
-
- Impl_def "Implementation == (RALL p. Init(.~ $(Calling memCh p)) .& [][ENext p]_(e p))
- .& MClkISpec memCh crCh cst
- .& RPCISpec crCh rmCh rst
- .& IRSpec rmCh mem ires"
-
- ImpInv_def "$(ImpInv rmhist p) .= ($(S1 rmhist p) .| $(S2 rmhist p) .| $(S3 rmhist p) .|
- $(S4 rmhist p) .| $(S5 rmhist p) .| $(S6 rmhist p))"
-
- (* Definition of predicate S.
- NB: The second conjunct of the definition in the paper is taken care of by
- the type definitions. The last conjunct is asserted separately as the memory
- invariant MemInv, proved in Memory.ML. *)
- S_def "$(S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p) .=
- ( ($(Calling memCh p) .= # ecalling)
- .& ($(Calling crCh p) .= # ccalling)
- .& (# ccalling .-> (arg[ $(crCh@p)] .= MClkRelayArg[ arg[$(memCh@p)] ]))
- .& ((.~ # ccalling .& ($(cst@p) .= # clkB)) .-> MVOKBARF[ res[$(crCh@p)] ])
- .& ($(Calling rmCh p) .= # rcalling)
- .& (# rcalling .-> (arg[ $(rmCh@p)] .= RPCRelayArg[ arg[$(crCh@p)] ]))
- .& (.~ # rcalling .-> ($(ires@p) .= # NotAResult))
- .& ((.~ # rcalling .& ($(rst@p) .= # rpcB)) .-> MVOKBA[ res[$(rmCh@p)] ])
- .& ($(cst@p) .= # cs)
- .& ($(rst@p) .= # rs)
- .& (($(rmhist@p) .= #hs1) .| ($(rmhist@p) .= #hs2))
- .& (MVNROKBA[ $(ires@p)]))"
-
- S1_def "$(S1 rmhist p) .= $(S rmhist False False False clkA rpcA histA histA p)"
- S2_def "$(S2 rmhist p) .= $(S rmhist True False False clkA rpcA histA histA p)"
- S3_def "$(S3 rmhist p) .= $(S rmhist True True False clkB rpcA histA histB p)"
- S4_def "$(S4 rmhist p) .= $(S rmhist True True True clkB rpcB histA histB p)"
- S5_def "$(S5 rmhist p) .= $(S rmhist True True False clkB rpcB histB histB p)"
- S6_def "$(S6 rmhist p) .= $(S rmhist True False False clkB rpcA histB histB p)"
-
- (* Definition of the refinement mapping resbar for result *)
- resbar_def "$((resbar rmhist) @ p) .=
- (.if ($(S1 rmhist p) .| $(S2 rmhist p))
- .then $(ires@p)
- .else .if $(S3 rmhist p)
- .then .if $(rmhist@p) .= #histA
- .then $(ires@p) .else # MemFailure
- .else .if $(S4 rmhist p)
- .then .if ($(rmhist@p) .= #histB) .& ($(ires@p) .= # NotAResult)
- .then #MemFailure .else $(ires@p)
- .else .if $(S5 rmhist p)
- .then res[$(rmCh@p)]
- .else .if $(S6 rmhist p)
- .then .if res[$(crCh@p)] .= #RPCFailure
- .then #MemFailure .else res[$(crCh@p)]
- .else #NotAResult)" (* dummy value *)
+ MI_base "basevars (caller memCh!p,
+ (rtrner memCh!p, caller crCh!p, cst!p),
+ (rtrner crCh!p, caller rmCh!p, rst!p),
+ (mm!l, rtrner rmCh!p, ires!p))"
end