diff --git a/specifications/FlashProtocol/APFlashWithMutex.cfg b/specifications/FlashProtocol/APFlashWithMutex.cfg index 4c790ba3..f8b41109 100644 --- a/specifications/FlashProtocol/APFlashWithMutex.cfg +++ b/specifications/FlashProtocol/APFlashWithMutex.cfg @@ -1,7 +1,6 @@ CONSTANT NODE <- NodeVal DATA <- DataVal - Other <- OtherVal Undefined <- UndefinedVal INVARIANT diff --git a/specifications/FlashProtocol/APFlashWithMutex.tla b/specifications/FlashProtocol/APFlashWithMutex.tla index ebf85a3e..5aeb2da8 100644 --- a/specifications/FlashProtocol/APFlashWithMutex.tla +++ b/specifications/FlashProtocol/APFlashWithMutex.tla @@ -19,8 +19,6 @@ CONSTANTS \* @type: Set(Str); DATA, \* @type: Str; - Other, - \* @type: Str; Undefined VARIABLES @@ -57,9 +55,7 @@ VARIABLES \* @type: Str; FwdCmd, \* @type: Str; - FwdSrc, - \* @type: Bool; - Env_o + FwdSrc \* Both components of the variable group are strings, which the type checker \* cannot tell apart from a two-element sequence. The group is shadowed here @@ -77,7 +73,6 @@ INSTANCE FlashWithMutex \* Concrete values for the constants used by APFlashWithMutex.cfg. NodeVal == { "n1", "n2" } DataVal == { "d1", "d2" } -OtherVal == "Other" UndefinedVal == "Undefined" ============================================================================== diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla index 4104630f..cf67397b 100644 --- a/specifications/FlashProtocol/FlashWithMutex.tla +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -1,40 +1,29 @@ ------------------------------ MODULE FlashWithMutex ------------------------------ -(***************************************************************************) -(* A faithful, one-action-per-rule (1:1) translation of *) -(* ProtocolDeadlockFiles/flashWithMutex.m (the FLASH directory-based cache *) -(* coherence protocol with the CMP "Other"-node abstraction, Env_o = TRUE). *) -(* *) -(* Structure mirrors the Murphi model exactly: every field of the Murphi *) -(* record `Sta : STATE` is a top-level variable, next to the scalar *) -(* Home. Enum values use the identical Murphi spelling ("CACHE_I", *) -(* "UNI_Get", ...) and variable and record field names are identical, so *) -(* the equivalence mapping is tiny. *) -(* *) -(* The Murphi auxiliary ghost `LastOtherInvAck` is the only variable whose *) -(* value depends on scalarset iteration order; it gates no transition and *) -(* feeds no kept variable, so it is omitted here and projected away on the *) -(* Murphi side by the comparator's ignorePaths. *) -(***************************************************************************) +(*********************************************************************************) +(* The FLASH directory-based cache coherence protocol *) +(* *) +(* Derived from a one-action-per-rule translation of *) +(* https://github.com/dsethi/ProtocolDeadlockFiles/blob/master/flashWithMutex.m *) +(* *) +(* FlashWithMutexCMP extends this module with the flashWithMutex.m model's CMP *) +(* encoding, which keeps NODE concrete, but additionally encodes the set of all *) +(* other nodes by more non-deterministic actions. Note that there is no *) +(* guarantee that the CMP encoding is sound. *) +(*********************************************************************************) EXTENDS Naturals, FiniteSets CONSTANTS - NODE, \* scalarset(NODE_NUM) -- concrete nodes + NODE, \* scalarset(NODE_NUM) -- the nodes DATA, \* scalarset(DATA_NUM) -- data values - Other, \* the abstract CMP node (enum{Other}) Undefined \* the "undefine"/isundefined sentinel -ASSUME OtherNotInNODE == Other \notin NODE -ASSUME OtherNotInDATA == Other \notin DATA ASSUME UndefNotInNODE == Undefined \notin NODE ASSUME UndefNotInDATA == Undefined \notin DATA -ASSUME UndefNotOther == Undefined # Other ASSUME NODEDATADisjoint == NODE \cap DATA = {} ASSUME NODENonEmpty == NODE # {} ASSUME DATANonEmpty == DATA # {} ASSUME NODEFinite == IsFiniteSet(NODE) -ABS_NODE == NODE \cup {Other} - CACHE_STATE == {"CACHE_I", "CACHE_S", "CACHE_E"} NODE_CMD == {"NODE_None", "NODE_Get", "NODE_GetX"} UNI_CMD == {"UNI_None", "UNI_Get", "UNI_GetX", "UNI_Put", "UNI_PutX", "UNI_Nak"} @@ -46,22 +35,20 @@ NAKC_CMD == {"NAKC_None", "NAKC_Nakc"} ReqCmd == {"Get", "GetX"} \* shared vs. exclusive request flavour DataU == DATA \cup {Undefined} -NodeU == ABS_NODE \cup {Undefined} +NodeU == NODE \cup {Undefined} UniU == UNI_CMD \cup {Undefined} VARIABLES Home, Proc, Dir, MemData, UniMsg, InvMsg, RpMsg, WbMsg, ShWbMsg, NakcMsg, - CurrData, PrevData, PendReqSrc, PendReqCmd, Collecting, FwdCmd, FwdSrc, Env_o + CurrData, PrevData, PendReqSrc, PendReqCmd, Collecting, FwdCmd, FwdSrc vars == <> + CurrData, PrevData, PendReqSrc, PendReqCmd, Collecting, FwdCmd, FwdSrc>> -\* The history variables. CurrData is the value most recently written: -\* the ABS_* actions hand it out as the abstract node's copy, and the data -\* properties check cached copies against it. PrevData snapshots CurrData when -\* an invalidation round opens; nothing but CacheDataProp reads it, to let a -\* sharer still hold the pre-round value while Collecting. +\* The history variables. CurrData is the value most recently written, which +\* the data properties check cached copies against. PrevData snapshots +\* CurrData when an invalidation round opens; nothing but CacheDataProp reads +\* it, to let a sharer still hold the pre-round value while Collecting. \* Variables that most actions leave untouched as a unit, grouped so that the \* frame conditions can name the group instead of listing its members. An @@ -97,7 +84,6 @@ TypeOK == /\ Collecting \in BOOLEAN /\ FwdCmd \in UNI_CMD /\ FwdSrc \in NodeU - /\ Env_o \in BOOLEAN ------------------------------------------------------------------------------- @@ -123,7 +109,6 @@ Init == /\ Collecting = FALSE /\ FwdCmd = "UNI_None" /\ FwdSrc = Undefined - /\ Env_o = TRUE ------------------------------------------------------------------------------- (* Shared fragments of the *_GetX_PutX actions, which grant a line *) @@ -152,7 +137,7 @@ ProcHomeInvalidMarked == THEN TRUE ELSE Proc[Home].InvMarked] ------------------------------------------------------------------------------- -(* Concrete (non-ABS) rules *) +(* Protocol rules *) ------------------------------------------------------------------------------- Store(src, data) == @@ -160,7 +145,7 @@ Store(src, data) == /\ Proc' = [Proc EXCEPT ![src].CacheData = data] /\ CurrData' = data /\ UNCHANGED <> + PrevData, pendVars, fwdVars>> \* Shared/exclusive request from a remote processor (merges the former \* PI_Remote_Get / PI_Remote_GetX). @@ -172,7 +157,7 @@ PI_Remote(src, c) == /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> IF c = "Get" THEN "UNI_Get" ELSE "UNI_GetX", Proc |-> Home, Data |-> Undefined]] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars>> PI_Local_Get_Get == /\ Proc[Home].ProcCmd = "NODE_None" @@ -187,7 +172,7 @@ PI_Local_Get_Get == /\ PendReqCmd' = "UNI_Get" /\ Collecting' = FALSE /\ UNCHANGED <> + PrevData, FwdSrc>> PI_Local_Get_Put == /\ Proc[Home].ProcCmd = "NODE_None" @@ -198,7 +183,7 @@ PI_Local_Get_Put == CacheState |-> IF Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", CacheData |-> IF Proc[Home].InvMarked THEN Undefined ELSE MemData]] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars>> PI_Local_GetX_GetX == /\ Proc[Home].ProcCmd = "NODE_None" @@ -213,7 +198,7 @@ PI_Local_GetX_GetX == /\ PendReqCmd' = "UNI_GetX" /\ Collecting' = FALSE /\ UNCHANGED <> + PrevData, FwdSrc>> \* The line is shared: the sharers and the head are invalidated first, so \* Home's own request goes pending. @@ -242,7 +227,7 @@ PI_Local_GetX_PutX == /\ \/ PI_Local_GetX_PutX_Inv \/ PI_Local_GetX_PutX_Grant /\ UNCHANGED <> + PendReqCmd, fwdVars>> PI_Remote_PutX(dst) == /\ dst # Home @@ -251,7 +236,7 @@ PI_Remote_PutX(dst) == /\ Proc' = [Proc EXCEPT ![dst].CacheState = "CACHE_I", ![dst].CacheData = Undefined] /\ WbMsg' = [Cmd |-> "WB_Wb", Proc |-> dst, Data |-> Proc[dst].CacheData] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars>> PI_Local_PutX == /\ Proc[Home].ProcCmd = "NODE_None" @@ -260,7 +245,7 @@ PI_Local_PutX == /\ Dir' = [Dir EXCEPT !.Dirty = FALSE, !.Local = IF Dir.Pending THEN Dir.Local ELSE FALSE] /\ MemData' = Proc[Home].CacheData /\ UNCHANGED <> + PrevData, pendVars, fwdVars>> PI_Remote_Replace(src) == /\ src # Home @@ -269,7 +254,7 @@ PI_Remote_Replace(src) == /\ Proc' = [Proc EXCEPT ![src].CacheState = "CACHE_I", ![src].CacheData = Undefined] /\ RpMsg' = [RpMsg EXCEPT ![src] = [Cmd |-> "RP_Replace"]] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars>> PI_Local_Replace == /\ Proc[Home].ProcCmd = "NODE_None" @@ -277,7 +262,7 @@ PI_Local_Replace == /\ Dir' = [Dir EXCEPT !.Local = FALSE] /\ Proc' = [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars>> NI_Nak(dst) == /\ UniMsg[dst].Cmd = "UNI_Nak" @@ -285,14 +270,14 @@ NI_Nak(dst) == Data |-> Undefined]] /\ Proc' = [Proc EXCEPT ![dst].ProcCmd = "NODE_None", ![dst].InvMarked = FALSE] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars>> NI_Nak_Clear == /\ NakcMsg.Cmd = "NAKC_Nakc" /\ NakcMsg' = [Cmd |-> "NAKC_None"] /\ Dir' = [Dir EXCEPT !.Pending = FALSE] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars>> NI_Local_Get_Nak(src) == /\ src # Home @@ -304,7 +289,7 @@ NI_Local_Get_Nak(src) == \/ (Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr = src) /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Nak", Proc |-> Home, Data |-> Undefined]] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars>> NI_Local_Get_Get(src) == /\ src # Home @@ -320,7 +305,7 @@ NI_Local_Get_Get(src) == /\ PendReqCmd' = "UNI_Get" /\ Collecting' = FALSE /\ UNCHANGED <> + CurrData, PrevData, FwdSrc>> NI_Local_Get_Put(src) == /\ src # Home @@ -342,7 +327,7 @@ NI_Local_Get_Put(src) == Data |-> Proc[Home].CacheData]] ELSE [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Put", Proc |-> Home, Data |-> MemData]] /\ UNCHANGED <> + pendVars, fwdVars>> \* Remote NAK of a shared/exclusive request (merges the former \* NI_Remote_Get_Nak / NI_Remote_GetX_Nak). @@ -356,7 +341,7 @@ NI_Remote_Nak(src, dst) == /\ FwdCmd' = "UNI_None" /\ FwdSrc' = src /\ UNCHANGED <> + PrevData, pendVars>> NI_Remote_Get_Put(src, dst) == /\ src # dst /\ dst # Home @@ -372,7 +357,7 @@ NI_Remote_Get_Put(src, dst) == THEN [Cmd |-> "SHWB_ShWb", Proc |-> src, Data |-> Proc[dst].CacheData] ELSE ShWbMsg /\ UNCHANGED <> + PrevData, pendVars>> NI_Local_GetX_Nak(src) == /\ src # Home @@ -383,7 +368,7 @@ NI_Local_GetX_Nak(src) == \/ (Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr = src) /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Nak", Proc |-> Home, Data |-> Undefined]] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars>> NI_Local_GetX_GetX(src) == /\ src # Home @@ -398,7 +383,7 @@ NI_Local_GetX_GetX(src) == /\ PendReqCmd' = "UNI_GetX" /\ Collecting' = FALSE /\ UNCHANGED <> + CurrData, PrevData, FwdSrc>> \* Home holds the line exclusively, so it can be handed to src directly. NI_Local_GetX_PutX_Dirty(src) == @@ -446,8 +431,7 @@ NI_Local_GetX_PutX(src) == /\ \/ NI_Local_GetX_PutX_Dirty(src) \/ NI_Local_GetX_PutX_Grant(src) \/ NI_Local_GetX_PutX_Inv(src) - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Remote_GetX_PutX(src, dst) == /\ src # dst /\ dst # Home @@ -463,7 +447,7 @@ NI_Remote_GetX_PutX(src, dst) == THEN [Cmd |-> "SHWB_FAck", Proc |-> src, Data |-> Undefined] ELSE ShWbMsg /\ UNCHANGED <> + PrevData, pendVars>> NI_Local_Put == /\ UniMsg[Home].Cmd = "UNI_Put" @@ -475,7 +459,7 @@ NI_Local_Put == CacheState |-> IF Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", CacheData |-> IF Proc[Home].InvMarked THEN Undefined ELSE UniMsg[Home].Data]] /\ UNCHANGED <> + pendVars, fwdVars>> NI_Remote_Put(dst) == /\ dst # Home @@ -486,7 +470,7 @@ NI_Remote_Put(dst) == CacheState |-> IF Proc[dst].InvMarked THEN "CACHE_I" ELSE "CACHE_S", CacheData |-> IF Proc[dst].InvMarked THEN Undefined ELSE UniMsg[dst].Data]] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars>> NI_Local_PutXAcksDone == /\ UniMsg[Home].Cmd = "UNI_PutX" @@ -496,7 +480,7 @@ NI_Local_PutXAcksDone == /\ Proc' = [Proc EXCEPT ![Home] = [ProcCmd |-> "NODE_None", InvMarked |-> FALSE, CacheState |-> "CACHE_E", CacheData |-> UniMsg[Home].Data]] /\ UNCHANGED <> + PrevData, pendVars, fwdVars>> NI_Remote_PutX(dst) == /\ dst # Home @@ -507,7 +491,7 @@ NI_Remote_PutX(dst) == /\ Proc' = [Proc EXCEPT ![dst] = [ProcCmd |-> "NODE_None", InvMarked |-> FALSE, CacheState |-> "CACHE_E", CacheData |-> UniMsg[dst].Data]] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars>> NI_Inv(dst) == /\ dst # Home @@ -518,7 +502,7 @@ NI_Inv(dst) == ![dst].InvMarked = IF Proc[dst].ProcCmd = "NODE_Get" THEN TRUE ELSE Proc[dst].InvMarked] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars>> \* Acks are still outstanding: only this one is recorded. NI_InvAck_More(src) == @@ -541,7 +525,7 @@ NI_InvAck(src) == /\ \/ NI_InvAck_More(src) \/ NI_InvAck_Last(src) /\ UNCHANGED <> + CurrData, PrevData, PendReqSrc, PendReqCmd, fwdVars>> NI_Wb == /\ WbMsg.Cmd = "WB_Wb" @@ -549,26 +533,24 @@ NI_Wb == /\ Dir' = [Dir EXCEPT !.Dirty = FALSE, !.HeadVld = FALSE, !.HeadPtr = Undefined] /\ MemData' = WbMsg.Data /\ UNCHANGED <> + PrevData, pendVars, fwdVars>> NI_FAck == /\ ShWbMsg.Cmd = "SHWB_FAck" /\ ShWbMsg' = [Cmd |-> "SHWB_None", Proc |-> Undefined, Data |-> Undefined] /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.HeadPtr = IF Dir.Dirty THEN ShWbMsg.Proc ELSE Dir.HeadPtr] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars>> NI_ShWb == /\ ShWbMsg.Cmd = "SHWB_ShWb" /\ ShWbMsg' = [Cmd |-> "SHWB_None", Proc |-> Undefined, Data |-> Undefined] - \* ShWbMsg.Proc is Other when the sharer is the abstract node; only concrete - \* nodes are recorded in the directory. /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.Dirty = FALSE, !.ShrVld = TRUE, - !.ShrSet = Dir.ShrSet \cup ({ShWbMsg.Proc} \cap NODE), - !.InvSet = Dir.ShrSet \cup ({ShWbMsg.Proc} \cap NODE)] + !.ShrSet = Dir.ShrSet \cup {ShWbMsg.Proc}, + !.InvSet = Dir.ShrSet \cup {ShWbMsg.Proc}] /\ MemData' = ShWbMsg.Data /\ UNCHANGED <> + PrevData, pendVars, fwdVars>> NI_Replace(src) == /\ RpMsg[src].Cmd = "RP_Replace" @@ -576,272 +558,11 @@ NI_Replace(src) == /\ Dir' = [Dir EXCEPT !.ShrSet = IF Dir.ShrVld THEN Dir.ShrSet \ {src} ELSE Dir.ShrSet, !.InvSet = IF Dir.ShrVld THEN Dir.InvSet \ {src} ELSE Dir.InvSet] /\ UNCHANGED <> - -------------------------------------------------------------------------------- -(* ABS_* abstract-environment rules *) -------------------------------------------------------------------------------- -(* Shared guard fragment used by the ABS_* environment rules that summarize *) -(* a writeback from the abstract node (Lemma_1 side condition). *) - -AbsDirtyClean == - /\ Dir.Dirty - /\ WbMsg.Cmd # "WB_Wb" - /\ ShWbMsg.Cmd # "SHWB_ShWb" - /\ \A p \in NODE : Proc[p].CacheState # "CACHE_E" - /\ UniMsg[Home].Cmd # "UNI_Put" - /\ \A q \in NODE : UniMsg[q].Cmd # "UNI_PutX" - -ABS_Store(data) == - /\ Env_o - /\ AbsDirtyClean - /\ CurrData' = data - /\ UNCHANGED <> - -ABS_PI_Remote_PutX == - /\ Env_o - /\ AbsDirtyClean - /\ WbMsg' = [Cmd |-> "WB_Wb", Proc |-> Other, Data |-> CurrData] - /\ UNCHANGED <> - -ABS_NI_Local_Get_Get == - /\ Env_o - /\ ~Dir.Pending /\ Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr # Other - /\ Dir' = [Dir EXCEPT !.Pending = TRUE] - /\ FwdCmd' = IF Dir.HeadPtr # Home THEN "UNI_Get" ELSE FwdCmd - /\ PendReqSrc' = Other - /\ PendReqCmd' = "UNI_Get" - /\ Collecting' = FALSE - /\ UNCHANGED <> - -ABS_NI_Local_Get_Put == - /\ Env_o - /\ ~Dir.Pending - /\ (Dir.Dirty => (Dir.Local /\ Proc[Home].CacheState = "CACHE_E")) - /\ Dir' = IF Dir.Dirty - THEN [Dir EXCEPT !.Dirty = FALSE, !.HeadVld = TRUE, !.HeadPtr = Other] - ELSE IF Dir.HeadVld - THEN [Dir EXCEPT !.ShrVld = TRUE, !.InvSet = Dir.ShrSet] - ELSE [Dir EXCEPT !.HeadVld = TRUE, !.HeadPtr = Other] - /\ MemData' = IF Dir.Dirty THEN Proc[Home].CacheData ELSE MemData - /\ Proc' = IF Dir.Dirty THEN [Proc EXCEPT ![Home].CacheState = "CACHE_S"] ELSE Proc - /\ UNCHANGED <> - -\* Abstract remote NAK, source side (merges the former ABS_NI_Remote_Get_Nak_src -\* / ABS_NI_Remote_GetX_Nak_src). -ABS_NI_Remote_Nak_src(dst) == - /\ Env_o /\ dst # Home - /\ Proc[dst].CacheState # "CACHE_E" - /\ Dir.Pending /\ ~Dir.Local - /\ PendReqSrc = Other /\ FwdCmd \in {"UNI_Get", "UNI_GetX"} - /\ NakcMsg' = [Cmd |-> "NAKC_Nakc"] - /\ FwdCmd' = "UNI_None" - /\ FwdSrc' = Other - /\ UNCHANGED <> - -ABS_NI_Remote_Get_Nak_dst(src) == - /\ Env_o - /\ UniMsg[src].Cmd = "UNI_Get" /\ UniMsg[src].Proc = Other - /\ Dir.Pending /\ ~Dir.Local - /\ PendReqSrc = src /\ FwdCmd = "UNI_Get" - /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Nak", Proc |-> Other, Data |-> Undefined]] - /\ NakcMsg' = [Cmd |-> "NAKC_Nakc"] - /\ FwdCmd' = "UNI_None" - /\ FwdSrc' = src - /\ UNCHANGED <> - -\* Abstract remote NAK, both sides abstract (merges the former -\* ABS_NI_Remote_Get_Nak_src_dst / ABS_NI_Remote_GetX_Nak_src_dst). -ABS_NI_Remote_Nak_src_dst == - /\ Env_o - /\ Dir.Pending /\ ~Dir.Local - /\ PendReqSrc = Other /\ FwdCmd \in {"UNI_Get", "UNI_GetX"} - /\ NakcMsg' = [Cmd |-> "NAKC_Nakc"] - /\ FwdCmd' = "UNI_None" - /\ FwdSrc' = Other - /\ UNCHANGED <> - -ABS_NI_Remote_Get_Put_src(dst) == - /\ Env_o /\ dst # Home - /\ Proc[dst].CacheState = "CACHE_E" - /\ Dir.Pending /\ ~Dir.Local - /\ PendReqSrc = Other /\ FwdCmd = "UNI_Get" - /\ Proc' = [Proc EXCEPT ![dst].CacheState = "CACHE_S"] - /\ ShWbMsg' = [Cmd |-> "SHWB_ShWb", Proc |-> Other, Data |-> Proc[dst].CacheData] - /\ FwdCmd' = "UNI_None" - /\ FwdSrc' = Other - /\ UNCHANGED <> - -ABS_NI_Remote_Get_Put_dst(src) == - /\ Env_o - /\ UniMsg[src].Cmd = "UNI_Get" /\ UniMsg[src].Proc = Other - /\ AbsDirtyClean - /\ Dir.Pending /\ ~Dir.Local - /\ PendReqSrc = src /\ FwdCmd = "UNI_Get" - /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Put", Proc |-> Other, Data |-> CurrData]] - /\ FwdCmd' = "UNI_None" - /\ FwdSrc' = src - /\ ShWbMsg' = IF src # Home - THEN [Cmd |-> "SHWB_ShWb", Proc |-> src, Data |-> CurrData] - ELSE ShWbMsg - /\ UNCHANGED <> - -ABS_NI_Remote_Get_Put_src_dst == - /\ Env_o - /\ AbsDirtyClean - /\ Dir.Pending /\ ~Dir.Local - /\ PendReqSrc = Other /\ FwdCmd = "UNI_Get" - /\ ShWbMsg' = [Cmd |-> "SHWB_ShWb", Proc |-> Other, Data |-> CurrData] - /\ FwdCmd' = "UNI_None" - /\ FwdSrc' = Other - /\ UNCHANGED <> - -ABS_NI_Local_GetX_GetX == - /\ Env_o - /\ ~Dir.Pending /\ Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr # Other - /\ Dir' = [Dir EXCEPT !.Pending = TRUE] - /\ FwdCmd' = IF Dir.HeadPtr # Home THEN "UNI_GetX" ELSE FwdCmd - /\ PendReqSrc' = Other - /\ PendReqCmd' = "UNI_GetX" - /\ Collecting' = FALSE - /\ UNCHANGED <> - -\* Home holds the line exclusively; the abstract node takes it over. -ABS_NI_Local_GetX_PutX_Dirty == - /\ Dir.Dirty - /\ Dir' = [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, - !.HeadPtr = Other, !.ShrVld = FALSE, !.ShrSet = {}, !.InvSet = {}] - /\ Proc' = ProcHomeInvalid - /\ UNCHANGED <> - -\* The abstract node is already the head and no concrete node shares the line. -ABS_NI_Local_GetX_PutX_Grant == - /\ ~Dir.Dirty - /\ NoOtherSharers(Other) - /\ Dir' = [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, - !.HeadPtr = Other, !.ShrVld = FALSE, !.ShrSet = {}, !.InvSet = {}] - /\ Proc' = IF Dir.Local THEN ProcHomeInvalidMarked ELSE ProcHomeInvalid - /\ UNCHANGED <> - -\* Concrete nodes share the line: they are invalidated first. -ABS_NI_Local_GetX_PutX_Inv == - /\ ~Dir.Dirty - /\ ~NoOtherSharers(Other) - /\ Dir' = [Pending |-> TRUE, Local |-> FALSE, Dirty |-> TRUE, HeadVld |-> TRUE, - HeadPtr |-> Other, ShrVld |-> FALSE, ShrSet |-> {}, InvSet |-> InvNodes({Home})] - /\ Proc' = IF Dir.Local THEN ProcHomeInvalidMarked ELSE Proc - /\ InvMsg' = [p \in NODE |-> [Cmd |-> IF p \in InvNodes({Home}) - THEN "INV_Inv" ELSE "INV_None"]] - /\ PendReqSrc' = Other - /\ PendReqCmd' = "UNI_GetX" - /\ Collecting' = TRUE - /\ PrevData' = CurrData - -ABS_NI_Local_GetX_PutX == - /\ Env_o - /\ ~Dir.Pending - /\ (Dir.Dirty => (Dir.Local /\ Proc[Home].CacheState = "CACHE_E")) - /\ \/ ABS_NI_Local_GetX_PutX_Dirty - \/ ABS_NI_Local_GetX_PutX_Grant - \/ ABS_NI_Local_GetX_PutX_Inv - /\ UNCHANGED <> - -ABS_NI_Remote_GetX_Nak_dst(src) == - /\ Env_o - /\ UniMsg[src].Cmd = "UNI_GetX" /\ UniMsg[src].Proc = Other - /\ Dir.Pending /\ ~Dir.Local - /\ PendReqSrc = src /\ FwdCmd = "UNI_GetX" - /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Nak", Proc |-> Other, Data |-> Undefined]] - /\ NakcMsg' = [Cmd |-> "NAKC_Nakc"] - /\ FwdCmd' = "UNI_None" - /\ FwdSrc' = src - /\ UNCHANGED <> - -ABS_NI_Remote_GetX_PutX_src(dst) == - /\ Env_o /\ dst # Home - /\ Proc[dst].CacheState = "CACHE_E" - /\ Dir.Pending /\ ~Dir.Local - /\ PendReqSrc = Other /\ FwdCmd = "UNI_GetX" - /\ Proc' = [Proc EXCEPT ![dst].CacheState = "CACHE_I", ![dst].CacheData = Undefined] - /\ ShWbMsg' = [Cmd |-> "SHWB_FAck", Proc |-> Other, Data |-> Undefined] - /\ FwdCmd' = "UNI_None" - /\ FwdSrc' = Other - /\ UNCHANGED <> - -ABS_NI_Remote_GetX_PutX_dst(src) == - /\ Env_o - /\ UniMsg[src].Cmd = "UNI_GetX" /\ UniMsg[src].Proc = Other - /\ AbsDirtyClean - /\ Dir.Pending /\ ~Dir.Local - /\ PendReqSrc = src /\ FwdCmd = "UNI_GetX" - /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_PutX", Proc |-> Other, Data |-> CurrData]] - /\ FwdCmd' = "UNI_None" - /\ FwdSrc' = src - /\ ShWbMsg' = IF src # Home - THEN [Cmd |-> "SHWB_FAck", Proc |-> src, Data |-> Undefined] - ELSE ShWbMsg - /\ UNCHANGED <> - -ABS_NI_Remote_GetX_PutX_src_dst == - /\ Env_o - /\ AbsDirtyClean - /\ Dir.Pending /\ ~Dir.Local - /\ PendReqSrc = Other /\ FwdCmd = "UNI_GetX" - /\ ShWbMsg' = [Cmd |-> "SHWB_FAck", Proc |-> Other, Data |-> Undefined] - /\ FwdCmd' = "UNI_None" - /\ FwdSrc' = Other - /\ UNCHANGED <> - -\* All concrete nodes have acked: the round closes and the request retires. -\* The Murphi rule also fires while acks are still outstanding, but that branch -\* assigns nothing except the dropped ghosts LastInvAck and LastOtherInvAck, so -\* here it would be a stuttering step and is left out. -ABS_NI_InvAck == - /\ Env_o - /\ Dir.Pending /\ Collecting - /\ Dir.InvSet = {} - /\ NakcMsg.Cmd = "NAKC_None" /\ ShWbMsg.Cmd = "SHWB_None" - /\ \A q \in NODE : - /\ ((UniMsg[q].Cmd = "UNI_Get" \/ UniMsg[q].Cmd = "UNI_GetX") - => UniMsg[q].Proc = Home) - /\ (UniMsg[q].Cmd = "UNI_PutX" - => (UniMsg[q].Proc = Home /\ PendReqSrc = q)) - /\ Dir' = [Dir EXCEPT !.Pending = FALSE, - !.Local = IF Dir.Local /\ ~Dir.Dirty THEN FALSE ELSE Dir.Local] - /\ Collecting' = FALSE - /\ UNCHANGED <> - -ABS_NI_ShWb == - /\ Env_o - /\ ShWbMsg.Cmd = "SHWB_ShWb" /\ ShWbMsg.Proc = Other - /\ ShWbMsg' = [Cmd |-> "SHWB_None", Proc |-> Undefined, Data |-> Undefined] - /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.Dirty = FALSE, !.ShrVld = TRUE, - !.InvSet = Dir.ShrSet] - /\ MemData' = ShWbMsg.Data - /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars>> ------------------------------------------------------------------------------- -(* Concrete protocol steps (the modelled nodes and directory). *) -System == +Next == \/ \E src \in NODE, data \in DATA : Store(src, data) \/ \E src \in NODE : \/ \E c \in ReqCmd : PI_Remote(src, c) @@ -861,25 +582,6 @@ System == \/ NI_Nak_Clear \/ NI_Local_Put \/ NI_Local_PutXAcksDone \/ NI_Wb \/ NI_FAck \/ NI_ShWb -(* Abstract environment steps: the CMP `Other`-node interactions summarised *) -(* by the ABS_* rules (all guarded by Env_o). *) -Environment == - \/ \E data \in DATA : ABS_Store(data) - \/ \E src \in NODE : - \/ ABS_NI_Remote_Nak_src(src) - \/ ABS_NI_Remote_Get_Nak_dst(src) - \/ ABS_NI_Remote_Get_Put_src(src) \/ ABS_NI_Remote_Get_Put_dst(src) - \/ ABS_NI_Remote_GetX_Nak_dst(src) - \/ ABS_NI_Remote_GetX_PutX_src(src) \/ ABS_NI_Remote_GetX_PutX_dst(src) - \/ ABS_PI_Remote_PutX - \/ ABS_NI_Local_Get_Get \/ ABS_NI_Local_Get_Put - \/ ABS_NI_Remote_Nak_src_dst \/ ABS_NI_Remote_Get_Put_src_dst - \/ ABS_NI_Local_GetX_GetX \/ ABS_NI_Local_GetX_PutX - \/ ABS_NI_Remote_GetX_PutX_src_dst - \/ ABS_NI_InvAck \/ ABS_NI_ShWb - -Next == System \/ Environment - Spec == Init /\ [][Next]_vars \* TypeOK is defined up with the variables; its theorem has to wait for Spec. @@ -893,9 +595,8 @@ THEOREM TypeCorrect == Spec => []TypeOK (* other actions change while the message waits, so no single handler need be *) (* continuously enabled -- but some handler of the slot's group always is, so *) (* weak fairness on the group suffices and strong fairness is not needed. *) -(* Nothing below constrains the voluntary actions -- Store, the PI_* request *) -(* and eviction rules, and the ABS_* rules by which the abstract node issues *) -(* requests of its own -- so those may happen or not. *) +(* Nothing below constrains the voluntary actions -- Store and the PI_* *) +(* request and eviction rules -- so those may happen or not. *) \* Everything that can consume or rewrite the unicast message in slot n. HandleUni(n) == @@ -907,39 +608,20 @@ HandleUni(n) == \/ \E d \in NODE : \/ NI_Remote_Nak(n, d) \/ NI_Remote_Get_Put(n, d) \/ NI_Remote_GetX_PutX(n, d) - \/ ABS_NI_Remote_Get_Nak_dst(n) \/ ABS_NI_Remote_GetX_Nak_dst(n) - \/ ABS_NI_Remote_Get_Put_dst(n) \/ ABS_NI_Remote_GetX_PutX_dst(n) \* The invalidate/ack handshake on slot n. HandleInv(n) == NI_Inv(n) \/ NI_InvAck(n) \* The shared-writeback slot, which also carries the forward ack. -HandleShWb == NI_FAck \/ NI_ShWb \/ ABS_NI_ShWb - -\* A request Home forwarded to node d on the abstract node's behalf: the reply -\* comes from the abstract node, so it has to be fair or the directory would -\* stay pending forever. -AbsRespond(d) == - \/ ABS_NI_Remote_Nak_src(d) - \/ ABS_NI_Remote_Get_Put_src(d) - \/ ABS_NI_Remote_GetX_PutX_src(d) - -\* As AbsRespond, with the forwarding target abstract as well. -AbsRespondSrcDst == - \/ ABS_NI_Remote_Nak_src_dst - \/ ABS_NI_Remote_Get_Put_src_dst - \/ ABS_NI_Remote_GetX_PutX_src_dst +HandleShWb == NI_FAck \/ NI_ShWb Fairness == /\ \A n \in NODE : /\ WF_vars(HandleUni(n)) /\ WF_vars(HandleInv(n)) /\ WF_vars(NI_Replace(n)) - /\ WF_vars(AbsRespond(n)) /\ WF_vars(NI_Nak_Clear) /\ WF_vars(NI_Wb) /\ WF_vars(HandleShWb) - /\ WF_vars(ABS_NI_InvAck) - /\ WF_vars(AbsRespondSrcDst) FairSpec == Init /\ [][Next]_vars /\ Fairness @@ -979,7 +661,7 @@ THEOREM NakcProgressCorrect == FairSpec => NakcProgress \* Starvation freedom, which does NOT hold and is not checked -- it is here to \* mark the boundary of what the properties above claim. TLC returns a lasso in -\* which n2 asks for the line, Home asks too, the abstract node serves Home, n2 +\* which one node asks for the line, another asks too and is served, the first \* is NAKed, retries, and the cycle repeats. Every state of that cycle has a \* continuation rule enabled, so the Murphi progress invariants hold throughout \* it: an enabledness invariant cannot see starvation, only a temporal property @@ -1011,20 +693,21 @@ THEOREM MemDataCorrect == Spec => []MemDataProp ------------------------------------------------------------------------------- (* The Murphi `Lemma_*` invariants. Unlike the three properties above these *) -(* are not statements about the protocol a user cares about; they are the *) -(* side conditions that make the CMP `Other`-node abstraction sound, and the *) -(* Murphi rules cite them by name in comments on the guards they justify. *) -(* Keeping them as invariants is what turns those citations into claims TLC *) -(* and Apalache can check. *) +(* are not statements about the protocol a user cares about: the CMP *) +(* iteration produced them as the side conditions that made the `Other`-node *) +(* abstraction sound, and the Murphi rules cite them by name in comments on *) +(* the guards they justify -- guards that now live in FlashWithMutexCMP. *) +(* They are stated here because they are invariants of the protocol, not of *) +(* the abstraction, and because they are the natural candidates for the *) +(* strengthening that makes the safety properties above inductive, which is *) +(* what a TLAPS proof needs and what TLC and Apalache can check directly. *) (* *) (* Each Murphi lemma opens with `forall h : NODE do h = Home -> ...`, which *) (* only instantiates h to the Home node; the translations below write Home *) (* directly. *) \* An exclusive copy is unique and no grant or writeback is in flight that -\* could produce a second one. `AbsDirtyClean` is this consequent stated for -\* the abstract node, which is why the ABS_* rules that hand out `CurrData` -\* are guarded by it -- the Murphi rules mark those guards "by Lemma_1". +\* could produce a second one. Lemma_1 == \A dst \in NODE : Proc[dst].CacheState = "CACHE_E" => @@ -1036,8 +719,9 @@ Lemma_1 == /\ \A q \in NODE : UniMsg[q].Cmd # "UNI_PutX" THEOREM Lemma_1_Correct == Spec => []Lemma_1 -\* A Get that Home forwarded to a third node is the request Home is working -\* on, so the ABS_* rules may read PendReqSrc/FwdCmd instead of the message. +\* A Get that Home forwarded to a third node is the request Home is working on, +\* so the message and Home's PendReqSrc/FwdCmd agree and a rule that has one of +\* them may read off the other. Lemma_2 == \A src, dst \in NODE : (/\ src # dst /\ dst # Home @@ -1055,9 +739,9 @@ Lemma_3 == /\ PendReqSrc = src /\ FwdCmd = "UNI_GetX" THEOREM Lemma_3_Correct == Spec => []Lemma_3 -\* An outstanding invalidation ack pins down the rest of the network: the -\* consequent is ABS_NI_InvAck's guard, which is why that rule may fire on -\* behalf of the abstract node without inspecting it. +\* An outstanding invalidation ack pins down the rest of the network: an +\* invalidation round is open, no NAK or shared writeback is in flight, and +\* every request or grant is addressed to Home. Lemma_4 == \A p \in NODE : (p # Home /\ InvMsg[p].Cmd = "INV_InvAck") => @@ -1068,10 +752,9 @@ Lemma_4 == /\ (UniMsg[q].Cmd = "UNI_PutX" => (UniMsg[q].Proc = Home /\ PendReqSrc = q)) THEOREM Lemma_4_Correct == Spec => []Lemma_4 -\* An exclusive copy holds the most recently written value, so the ABS_* rules -\* may hand out CurrData as the abstract node's copy. This is also the first -\* conjunct of CacheDataProp; it is restated here to keep the correspondence -\* with the Murphi invariants one-to-one. +\* An exclusive copy holds the most recently written value. This is also the +\* first conjunct of CacheDataProp; it is restated here to keep the +\* correspondence with the Murphi invariants one-to-one. Lemma_5 == \A p \in NODE : Proc[p].CacheState = "CACHE_E" => Proc[p].CacheData = CurrData THEOREM Lemma_5_Correct == Spec => []Lemma_5 diff --git a/specifications/FlashProtocol/FlashWithMutexCMP.tla b/specifications/FlashProtocol/FlashWithMutexCMP.tla new file mode 100644 index 00000000..bd843e8f --- /dev/null +++ b/specifications/FlashProtocol/FlashWithMutexCMP.tla @@ -0,0 +1,410 @@ +--------------------------- MODULE FlashWithMutexCMP --------------------------- +(****************************************************************************) +(* The CMP encoding of flashWithMutex.m, after the method of Chou, Mannava *) +(* and Park: keep the nodes in NODE concrete, summarize all other nodes in *) +(* one node `Other`, and let the ABS_* rules stand in for them. Those *) +(* rules cannot see a summarized node's local state, which is not modelled, *) +(* so they are more non-deterministic than the rules they replace. *) +(* *) +(* One finite model is then meant to say something about every node count, *) +(* which is how flashWithMutex.m was checked: Murphi fixes one NODE_NUM per *) +(* run just as TLC fixes one NODE. That it does say anything is not *) +(* established here -- it would need every behaviour of FlashWithMutex, at *) +(* any node count, to be a behaviour of this module, and no such refinement *) +(* is stated, let alone proved. The encoding may under-approximate just as *) +(* easily as over-approximate. *) +(* *) +(* It is kept apart from FlashWithMutex because the protocol does not need *) +(* it: NODE is a CONSTANT there, so TLAPS can reason about all sizes at *) +(* once instead of one at a time. *) +(* *) +(* Three definitions are restated rather than inherited. ABS_TypeOK widens *) +(* the six fields that hold a node pointer, since each may now point at *) +(* `Other`; the directory's sharer sets are not among them, `Other` never *) +(* being recorded as a sharer. CMPNext subtracts the one inherited step *) +(* that would record it and adds the ABS_* rules. CMPFairness re-forms the *) +(* weak fairness groups, because a message slot the summarized nodes answer *) +(* is only served if its ABS_* responder is fair too. *) +(****************************************************************************) +EXTENDS FlashWithMutex + +CONSTANT Other \* the abstract CMP node (enum{Other}) + +ASSUME OtherNotInNODE == Other \notin NODE +ASSUME OtherNotInDATA == Other \notin DATA +ASSUME UndefNotOther == Undefined # Other + +ABS_NODE == NODE \cup {Other} +ABS_NodeU == ABS_NODE \cup {Undefined} + +------------------------------------------------------------------------------- + +\* TypeOK with every node-pointer field widened by the abstract node. The +\* directory's ShrSet and InvSet stay subsets of NODE. +ABS_TypeOK == + /\ Home \in NODE + /\ Proc \in [NODE -> [ProcCmd : NODE_CMD, InvMarked : BOOLEAN, + CacheState : CACHE_STATE, CacheData : DataU]] + /\ Dir \in [Pending : BOOLEAN, Local : BOOLEAN, Dirty : BOOLEAN, + HeadVld : BOOLEAN, HeadPtr : ABS_NodeU, ShrVld : BOOLEAN, + ShrSet : SUBSET NODE, InvSet : SUBSET NODE] + /\ MemData \in DATA + /\ UniMsg \in [NODE -> [Cmd : UNI_CMD, Proc : ABS_NodeU, Data : DataU]] + /\ InvMsg \in [NODE -> [Cmd : INV_CMD]] + /\ RpMsg \in [NODE -> [Cmd : RP_CMD]] + /\ WbMsg \in [Cmd : WB_CMD, Proc : ABS_NodeU, Data : DataU] + /\ ShWbMsg \in [Cmd : SHWB_CMD, Proc : ABS_NodeU, Data : DataU] + /\ NakcMsg \in [Cmd : NAKC_CMD] + /\ CurrData \in DATA + /\ PrevData \in DATA + /\ PendReqSrc \in ABS_NodeU + /\ PendReqCmd \in UniU + /\ Collecting \in BOOLEAN + /\ FwdCmd \in UNI_CMD + /\ FwdSrc \in ABS_NodeU + +------------------------------------------------------------------------------- +(* ABS_* abstract-environment rules *) +------------------------------------------------------------------------------- +(* Shared guard fragment used by the ABS_* rules that summarize a writeback *) +(* from the abstract node (Lemma_1 side condition). *) + +AbsDirtyClean == + /\ Dir.Dirty + /\ WbMsg.Cmd # "WB_Wb" + /\ ShWbMsg.Cmd # "SHWB_ShWb" + /\ \A p \in NODE : Proc[p].CacheState # "CACHE_E" + /\ UniMsg[Home].Cmd # "UNI_Put" + /\ \A q \in NODE : UniMsg[q].Cmd # "UNI_PutX" + +ABS_Store(data) == + /\ AbsDirtyClean + /\ CurrData' = data + /\ UNCHANGED <> + +ABS_PI_Remote_PutX == + /\ AbsDirtyClean + /\ WbMsg' = [Cmd |-> "WB_Wb", Proc |-> Other, Data |-> CurrData] + /\ UNCHANGED <> + +ABS_NI_Local_Get_Get == + /\ ~Dir.Pending /\ Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr # Other + /\ Dir' = [Dir EXCEPT !.Pending = TRUE] + /\ FwdCmd' = IF Dir.HeadPtr # Home THEN "UNI_Get" ELSE FwdCmd + /\ PendReqSrc' = Other + /\ PendReqCmd' = "UNI_Get" + /\ Collecting' = FALSE + /\ UNCHANGED <> + +ABS_NI_Local_Get_Put == + /\ ~Dir.Pending + /\ (Dir.Dirty => (Dir.Local /\ Proc[Home].CacheState = "CACHE_E")) + /\ Dir' = IF Dir.Dirty + THEN [Dir EXCEPT !.Dirty = FALSE, !.HeadVld = TRUE, !.HeadPtr = Other] + ELSE IF Dir.HeadVld + THEN [Dir EXCEPT !.ShrVld = TRUE, !.InvSet = Dir.ShrSet] + ELSE [Dir EXCEPT !.HeadVld = TRUE, !.HeadPtr = Other] + /\ MemData' = IF Dir.Dirty THEN Proc[Home].CacheData ELSE MemData + /\ Proc' = IF Dir.Dirty THEN [Proc EXCEPT ![Home].CacheState = "CACHE_S"] ELSE Proc + /\ UNCHANGED <> + +\* Abstract remote NAK, source side (merges the former ABS_NI_Remote_Get_Nak_src +\* / ABS_NI_Remote_GetX_Nak_src). +ABS_NI_Remote_Nak_src(dst) == + /\ dst # Home + /\ Proc[dst].CacheState # "CACHE_E" + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = Other /\ FwdCmd \in {"UNI_Get", "UNI_GetX"} + /\ NakcMsg' = [Cmd |-> "NAKC_Nakc"] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = Other + /\ UNCHANGED <> + +ABS_NI_Remote_Get_Nak_dst(src) == + /\ UniMsg[src].Cmd = "UNI_Get" /\ UniMsg[src].Proc = Other + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = src /\ FwdCmd = "UNI_Get" + /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Nak", Proc |-> Other, Data |-> Undefined]] + /\ NakcMsg' = [Cmd |-> "NAKC_Nakc"] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = src + /\ UNCHANGED <> + +\* Abstract remote NAK, both sides abstract (merges the former +\* ABS_NI_Remote_Get_Nak_src_dst / ABS_NI_Remote_GetX_Nak_src_dst). +ABS_NI_Remote_Nak_src_dst == + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = Other /\ FwdCmd \in {"UNI_Get", "UNI_GetX"} + /\ NakcMsg' = [Cmd |-> "NAKC_Nakc"] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = Other + /\ UNCHANGED <> + +ABS_NI_Remote_Get_Put_src(dst) == + /\ dst # Home + /\ Proc[dst].CacheState = "CACHE_E" + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = Other /\ FwdCmd = "UNI_Get" + /\ Proc' = [Proc EXCEPT ![dst].CacheState = "CACHE_S"] + /\ ShWbMsg' = [Cmd |-> "SHWB_ShWb", Proc |-> Other, Data |-> Proc[dst].CacheData] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = Other + /\ UNCHANGED <> + +ABS_NI_Remote_Get_Put_dst(src) == + /\ UniMsg[src].Cmd = "UNI_Get" /\ UniMsg[src].Proc = Other + /\ AbsDirtyClean + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = src /\ FwdCmd = "UNI_Get" + /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Put", Proc |-> Other, Data |-> CurrData]] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = src + /\ ShWbMsg' = IF src # Home + THEN [Cmd |-> "SHWB_ShWb", Proc |-> src, Data |-> CurrData] + ELSE ShWbMsg + /\ UNCHANGED <> + +ABS_NI_Remote_Get_Put_src_dst == + /\ AbsDirtyClean + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = Other /\ FwdCmd = "UNI_Get" + /\ ShWbMsg' = [Cmd |-> "SHWB_ShWb", Proc |-> Other, Data |-> CurrData] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = Other + /\ UNCHANGED <> + +ABS_NI_Local_GetX_GetX == + /\ ~Dir.Pending /\ Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr # Other + /\ Dir' = [Dir EXCEPT !.Pending = TRUE] + /\ FwdCmd' = IF Dir.HeadPtr # Home THEN "UNI_GetX" ELSE FwdCmd + /\ PendReqSrc' = Other + /\ PendReqCmd' = "UNI_GetX" + /\ Collecting' = FALSE + /\ UNCHANGED <> + +\* Home holds the line exclusively; the abstract node takes it over. +ABS_NI_Local_GetX_PutX_Dirty == + /\ Dir.Dirty + /\ Dir' = [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, + !.HeadPtr = Other, !.ShrVld = FALSE, !.ShrSet = {}, !.InvSet = {}] + /\ Proc' = ProcHomeInvalid + /\ UNCHANGED <> + +\* The abstract node is already the head and no concrete node shares the line. +ABS_NI_Local_GetX_PutX_Grant == + /\ ~Dir.Dirty + /\ NoOtherSharers(Other) + /\ Dir' = [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, + !.HeadPtr = Other, !.ShrVld = FALSE, !.ShrSet = {}, !.InvSet = {}] + /\ Proc' = IF Dir.Local THEN ProcHomeInvalidMarked ELSE ProcHomeInvalid + /\ UNCHANGED <> + +\* Concrete nodes share the line: they are invalidated first. +ABS_NI_Local_GetX_PutX_Inv == + /\ ~Dir.Dirty + /\ ~NoOtherSharers(Other) + /\ Dir' = [Pending |-> TRUE, Local |-> FALSE, Dirty |-> TRUE, HeadVld |-> TRUE, + HeadPtr |-> Other, ShrVld |-> FALSE, ShrSet |-> {}, InvSet |-> InvNodes({Home})] + /\ Proc' = IF Dir.Local THEN ProcHomeInvalidMarked ELSE Proc + /\ InvMsg' = [p \in NODE |-> [Cmd |-> IF p \in InvNodes({Home}) + THEN "INV_Inv" ELSE "INV_None"]] + /\ PendReqSrc' = Other + /\ PendReqCmd' = "UNI_GetX" + /\ Collecting' = TRUE + /\ PrevData' = CurrData + +ABS_NI_Local_GetX_PutX == + /\ ~Dir.Pending + /\ (Dir.Dirty => (Dir.Local /\ Proc[Home].CacheState = "CACHE_E")) + /\ \/ ABS_NI_Local_GetX_PutX_Dirty + \/ ABS_NI_Local_GetX_PutX_Grant + \/ ABS_NI_Local_GetX_PutX_Inv + /\ UNCHANGED <> + +ABS_NI_Remote_GetX_Nak_dst(src) == + /\ UniMsg[src].Cmd = "UNI_GetX" /\ UniMsg[src].Proc = Other + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = src /\ FwdCmd = "UNI_GetX" + /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Nak", Proc |-> Other, Data |-> Undefined]] + /\ NakcMsg' = [Cmd |-> "NAKC_Nakc"] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = src + /\ UNCHANGED <> + +ABS_NI_Remote_GetX_PutX_src(dst) == + /\ dst # Home + /\ Proc[dst].CacheState = "CACHE_E" + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = Other /\ FwdCmd = "UNI_GetX" + /\ Proc' = [Proc EXCEPT ![dst].CacheState = "CACHE_I", ![dst].CacheData = Undefined] + /\ ShWbMsg' = [Cmd |-> "SHWB_FAck", Proc |-> Other, Data |-> Undefined] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = Other + /\ UNCHANGED <> + +ABS_NI_Remote_GetX_PutX_dst(src) == + /\ UniMsg[src].Cmd = "UNI_GetX" /\ UniMsg[src].Proc = Other + /\ AbsDirtyClean + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = src /\ FwdCmd = "UNI_GetX" + /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_PutX", Proc |-> Other, Data |-> CurrData]] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = src + /\ ShWbMsg' = IF src # Home + THEN [Cmd |-> "SHWB_FAck", Proc |-> src, Data |-> Undefined] + ELSE ShWbMsg + /\ UNCHANGED <> + +ABS_NI_Remote_GetX_PutX_src_dst == + /\ AbsDirtyClean + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = Other /\ FwdCmd = "UNI_GetX" + /\ ShWbMsg' = [Cmd |-> "SHWB_FAck", Proc |-> Other, Data |-> Undefined] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = Other + /\ UNCHANGED <> + +\* All concrete nodes have acked: the round closes and the request retires. +\* The Murphi rule also fires while acks are still outstanding, but that branch +\* assigns nothing except the dropped ghosts LastInvAck and LastOtherInvAck, so +\* here it would be a stuttering step and is left out. +ABS_NI_InvAck == + /\ Dir.Pending /\ Collecting + /\ Dir.InvSet = {} + /\ NakcMsg.Cmd = "NAKC_None" /\ ShWbMsg.Cmd = "SHWB_None" + /\ \A q \in NODE : + /\ ((UniMsg[q].Cmd = "UNI_Get" \/ UniMsg[q].Cmd = "UNI_GetX") + => UniMsg[q].Proc = Home) + /\ (UniMsg[q].Cmd = "UNI_PutX" + => (UniMsg[q].Proc = Home /\ PendReqSrc = q)) + /\ Dir' = [Dir EXCEPT !.Pending = FALSE, + !.Local = IF Dir.Local /\ ~Dir.Dirty THEN FALSE ELSE Dir.Local] + /\ Collecting' = FALSE + /\ UNCHANGED <> + +\* Stands in for NI_ShWb when the sharer is the abstract node: the writeback is +\* taken, but no sharer is recorded, the directory not tracking that node. +ABS_NI_ShWb == + /\ ShWbMsg.Cmd = "SHWB_ShWb" /\ ShWbMsg.Proc = Other + /\ ShWbMsg' = [Cmd |-> "SHWB_None", Proc |-> Undefined, Data |-> Undefined] + /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.Dirty = FALSE, !.ShrVld = TRUE, + !.InvSet = Dir.ShrSet] + /\ MemData' = ShWbMsg.Data + /\ UNCHANGED <> + +------------------------------------------------------------------------------- + +(* Abstract environment steps: the `Other`-node interactions summarised by the *) +(* ABS_* rules. *) +Environment == + \/ \E data \in DATA : ABS_Store(data) + \/ \E src \in NODE : + \/ ABS_NI_Remote_Nak_src(src) + \/ ABS_NI_Remote_Get_Nak_dst(src) + \/ ABS_NI_Remote_Get_Put_src(src) \/ ABS_NI_Remote_Get_Put_dst(src) + \/ ABS_NI_Remote_GetX_Nak_dst(src) + \/ ABS_NI_Remote_GetX_PutX_src(src) \/ ABS_NI_Remote_GetX_PutX_dst(src) + \/ ABS_PI_Remote_PutX + \/ ABS_NI_Local_Get_Get \/ ABS_NI_Local_Get_Put + \/ ABS_NI_Remote_Nak_src_dst \/ ABS_NI_Remote_Get_Put_src_dst + \/ ABS_NI_Local_GetX_GetX \/ ABS_NI_Local_GetX_PutX + \/ ABS_NI_Remote_GetX_PutX_src_dst + \/ ABS_NI_InvAck \/ ABS_NI_ShWb + +(* The protocol's next-state relation, less one step, plus the ABS_* rules. *) +(* NI_ShWb records the sender of a shared writeback as a sharer, and here that *) +(* sender may be `Other`, which the directory does not track, so an NI_ShWb *) +(* step on the abstract node's behalf is subtracted and ABS_NI_ShWb serves it. *) +CMPNext == + \/ Next /\ ~(ShWbMsg.Proc = Other /\ NI_ShWb) + \/ Environment + +CMPSpec == Init /\ [][CMPNext]_vars + +THEOREM ABS_TypeCorrect == CMPSpec => []ABS_TypeOK + +------------------------------------------------------------------------------- +(* Fairness. The inherited groups are extended with the ABS_* rules that *) +(* serve the same message slot, and the abstract node's replies to a forwarded *) +(* request get groups of their own: Home forwards to the abstract node and *) +(* waits, so without fairness there the directory could stay pending forever. *) +(* As in FlashWithMutex nothing constrains the voluntary actions, which here *) +(* also covers the ABS_* rules by which the abstract node issues requests. *) + +ABS_HandleUni(n) == + \/ HandleUni(n) + \/ ABS_NI_Remote_Get_Nak_dst(n) \/ ABS_NI_Remote_GetX_Nak_dst(n) + \/ ABS_NI_Remote_Get_Put_dst(n) \/ ABS_NI_Remote_GetX_PutX_dst(n) + +ABS_HandleShWb == HandleShWb \/ ABS_NI_ShWb + +\* A request Home forwarded to node d on the abstract node's behalf: the reply +\* comes from the abstract node, so it has to be fair or the directory would +\* stay pending forever. +AbsRespond(d) == + \/ ABS_NI_Remote_Nak_src(d) + \/ ABS_NI_Remote_Get_Put_src(d) + \/ ABS_NI_Remote_GetX_PutX_src(d) + +\* As AbsRespond, with the forwarding target abstract as well. +AbsRespondSrcDst == + \/ ABS_NI_Remote_Nak_src_dst + \/ ABS_NI_Remote_Get_Put_src_dst + \/ ABS_NI_Remote_GetX_PutX_src_dst + +CMPFairness == + /\ \A n \in NODE : /\ WF_vars(ABS_HandleUni(n)) + /\ WF_vars(HandleInv(n)) + /\ WF_vars(NI_Replace(n)) + /\ WF_vars(AbsRespond(n)) + /\ WF_vars(NI_Nak_Clear) + /\ WF_vars(NI_Wb) + /\ WF_vars(ABS_HandleShWb) + /\ WF_vars(ABS_NI_InvAck) + /\ WF_vars(AbsRespondSrcDst) + +CMPFairSpec == Init /\ [][CMPNext]_vars /\ CMPFairness + +------------------------------------------------------------------------------- +(* The properties are inherited verbatim: each quantifies over NODE, so under *) +(* the abstraction each states that the concrete nodes make progress and stay *) +(* coherent whatever the summarized ones do. *) + +THEOREM ABS_ReqProgressCorrect == CMPFairSpec => ReqProgress +THEOREM ABS_DirProgressCorrect == CMPFairSpec => DirProgress +THEOREM ABS_UniProgressCorrect == CMPFairSpec => UniProgress +THEOREM ABS_InvProgressCorrect == CMPFairSpec => InvProgress +THEOREM ABS_RpProgressCorrect == CMPFairSpec => RpProgress +THEOREM ABS_WbProgressCorrect == CMPFairSpec => WbProgress +THEOREM ABS_ShWbProgressCorrect == CMPFairSpec => ShWbProgress +THEOREM ABS_NakcProgressCorrect == CMPFairSpec => NakcProgress + +THEOREM ABS_CacheStateCorrect == CMPSpec => []CacheStateProp +THEOREM ABS_CacheDataCorrect == CMPSpec => []CacheDataProp +THEOREM ABS_MemDataCorrect == CMPSpec => []MemDataProp + +THEOREM ABS_Lemma_1_Correct == CMPSpec => []Lemma_1 +THEOREM ABS_Lemma_2_Correct == CMPSpec => []Lemma_2 +THEOREM ABS_Lemma_3_Correct == CMPSpec => []Lemma_3 +THEOREM ABS_Lemma_4_Correct == CMPSpec => []Lemma_4 +THEOREM ABS_Lemma_5_Correct == CMPSpec => []Lemma_5 + +=============================================================================== diff --git a/specifications/FlashProtocol/MCFlashWithMutex.cfg b/specifications/FlashProtocol/MCFlashWithMutex.cfg index 1da87bf8..0352d62f 100644 --- a/specifications/FlashProtocol/MCFlashWithMutex.cfg +++ b/specifications/FlashProtocol/MCFlashWithMutex.cfg @@ -1,7 +1,6 @@ CONSTANTS NODE = {n1, n2} DATA = {d1, d2} - Other = Other Undefined = Undefined SYMMETRY Symmetry diff --git a/specifications/FlashProtocol/MCFlashWithMutex.tla b/specifications/FlashProtocol/MCFlashWithMutex.tla index fde41d52..270b714c 100644 --- a/specifications/FlashProtocol/MCFlashWithMutex.tla +++ b/specifications/FlashProtocol/MCFlashWithMutex.tla @@ -1,8 +1,8 @@ ------------------------- MODULE MCFlashWithMutex ------------------------- EXTENDS FlashWithMutex, TLC -\* Nodes and data values are independently interchangeable. The Other and -\* Undefined sentinels are fixed because they are outside these sets. +\* Nodes and data values are independently interchangeable. The Undefined +\* sentinel is fixed because it is outside these sets. Symmetry == Permutations(NODE) \union Permutations(DATA) ============================================================================== diff --git a/specifications/FlashProtocol/MCFlashWithMutexLive.cfg b/specifications/FlashProtocol/MCFlashWithMutexLive.cfg index d85fb8c4..305fa79b 100644 --- a/specifications/FlashProtocol/MCFlashWithMutexLive.cfg +++ b/specifications/FlashProtocol/MCFlashWithMutexLive.cfg @@ -1,7 +1,6 @@ CONSTANTS NODE = {n1, n2} DATA = {d1, d2} - Other = Other Undefined = Undefined SPECIFICATION FairSpec diff --git a/specifications/FlashProtocol/manifest.json b/specifications/FlashProtocol/manifest.json index a8afa32c..be4a0bd3 100644 --- a/specifications/FlashProtocol/manifest.json +++ b/specifications/FlashProtocol/manifest.json @@ -14,13 +14,18 @@ "features": [], "models": [] }, + { + "path": "specifications/FlashProtocol/FlashWithMutexCMP.tla", + "features": [], + "models": [] + }, { "path": "specifications/FlashProtocol/APFlashWithMutex.tla", "features": [], "models": [ { "path": "specifications/FlashProtocol/APFlashWithMutex.cfg", - "runtime": "00:38:09", + "runtime": "00:00:44", "mode": "symbolic", "result": "success" } @@ -32,12 +37,12 @@ "models": [ { "path": "specifications/FlashProtocol/MCFlashWithMutex.cfg", - "runtime": "00:00:04", + "runtime": "00:00:01", "mode": "exhaustive search", "result": "success", - "distinctStates": 32994, - "totalStates": 159216, - "stateDepth": 34 + "distinctStates": 2024, + "totalStates": 7552, + "stateDepth": 21 } ] }, @@ -47,12 +52,12 @@ "models": [ { "path": "specifications/FlashProtocol/MCFlashWithMutexLive.cfg", - "runtime": "00:04:44", + "runtime": "00:00:15", "mode": "exhaustive search", "result": "success", - "distinctStates": 131976, - "totalStates": 636852, - "stateDepth": 34, + "distinctStates": 8096, + "totalStates": 30196, + "stateDepth": 21, "workers": 4 } ]