diff -r f6335d319e9f -r db63752140c7 src/HOL/TLA/Memory/MemoryImplementation.thy --- 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 = MClkRelayArg>) + & (~ #ccalling & cst!p = #clkB --> MVOKBARF>) + & Calling rmCh p = #rcalling + & (#rcalling --> arg = RPCRelayArg>) + & (~ #rcalling --> ires!p = #NotAResult) + & (~ #rcalling & rst!p = #rpcB --> MVOKBA>) + & cst!p = #cs + & rst!p = #rs + & (rmhist!p = #hs1 | rmhist!p = #hs2) + & MVNROKBA" (* 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 " - - (* 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]_" - 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 == " - r_def "r p == " - m_def "m 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