From e268fd14d35a6817dc734803972172ee77ec909f Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 20 Jul 2026 15:05:21 -0700 Subject: [PATCH 01/17] Add FlashWithMutex specification and configuration files - Introduced a new TLA+ module `FlashWithMutex` that implements a one-action-per-rule translation of the FLASH directory-based cache coherence protocol. - Added a configuration file `MCFlashWithMutex.cfg` defining constants and invariants for the module. - Created a new module `MCFlashWithMutex` that extends `FlashWithMutex`, setting up the environment for multi-core scenarios. Co-authored-by: Claude Opus 4.8 Signed-off-by: Markus Alexander Kuppe --- README.md | 1 + .../FlashProtocol/FlashWithMutex.tla | 915 ++++++++++++++++++ .../FlashProtocol/MCFlashWithMutex.cfg | 13 + .../FlashProtocol/MCFlashWithMutex.tla | 3 + specifications/FlashProtocol/manifest.json | 33 + 5 files changed, 965 insertions(+) create mode 100644 specifications/FlashProtocol/FlashWithMutex.tla create mode 100644 specifications/FlashProtocol/MCFlashWithMutex.cfg create mode 100644 specifications/FlashProtocol/MCFlashWithMutex.tla create mode 100644 specifications/FlashProtocol/manifest.json diff --git a/README.md b/README.md index ac1c1221..cc1f876b 100644 --- a/README.md +++ b/README.md @@ -107,6 +107,7 @@ Here is a list of specs included in this repository which are validated by the C | [Disruptor](specifications/Disruptor) | Nicholas Schultz-Møller | | | | ✔ | ✔ | | [DAG-based Consensus](specifications/dag-consensus) | Giuliano Losa | | | ✔ | ✔ | | | [German Cache-Coherence Protocol](specifications/GermanProtocol) | Markus Kuppe | | | | ✔ | ✔ | +| [FLASH Cache-Coherence Protocol](specifications/FlashProtocol) | Markus Kuppe | | | | ✔ | | ## Other Examples diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla new file mode 100644 index 00000000..c7144d99 --- /dev/null +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -0,0 +1,915 @@ +------------------------------ 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: a single record variable *) +(* Sta (the Murphi `Sta : STATE`) plus the scalar Home. Enum values use *) +(* the identical Murphi spelling ("CACHE_I", "UNI_Get", ...) 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. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +CONSTANTS + NODE, \* scalarset(NODE_NUM) -- concrete 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 UndefNotInNODE == Undefined \notin NODE +ASSUME UndefNotInDATA == Undefined \notin DATA +ASSUME UndefNotOther == Undefined # Other +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"} +INV_CMD == {"INV_None", "INV_Inv", "INV_InvAck"} +RP_CMD == {"RP_None", "RP_Replace"} +WB_CMD == {"WB_None", "WB_Wb"} +SHWB_CMD == {"SHWB_None", "SHWB_ShWb", "SHWB_FAck"} +NAKC_CMD == {"NAKC_None", "NAKC_Nakc"} + +DataU == DATA \cup {Undefined} +NodeU == ABS_NODE \cup {Undefined} +UniU == UNI_CMD \cup {Undefined} + +VARIABLES + Home, + Sta + +vars == <> + +------------------------------------------------------------------------------- + +TypeOK == + /\ Home \in NODE + /\ Sta.Proc \in [NODE -> [ProcCmd : NODE_CMD, InvMarked : BOOLEAN, + CacheState : CACHE_STATE, CacheData : DataU]] + /\ Sta.Dir \in [Pending : BOOLEAN, Local : BOOLEAN, Dirty : BOOLEAN, + HeadVld : BOOLEAN, HeadPtr : NodeU, ShrVld : BOOLEAN, + ShrSet : [NODE -> BOOLEAN], InvSet : [NODE -> BOOLEAN]] + /\ Sta.MemData \in DATA + /\ Sta.UniMsg \in [NODE -> [Cmd : UNI_CMD, Proc : NodeU, Data : DataU]] + /\ Sta.InvMsg \in [NODE -> [Cmd : INV_CMD]] + /\ Sta.RpMsg \in [NODE -> [Cmd : RP_CMD]] + /\ Sta.WbMsg \in [Cmd : WB_CMD, Proc : NodeU, Data : DataU] + /\ Sta.ShWbMsg \in [Cmd : SHWB_CMD, Proc : NodeU, Data : DataU] + /\ Sta.NakcMsg \in [Cmd : NAKC_CMD] + /\ Sta.CurrData \in DATA + /\ Sta.PrevData \in DATA + /\ Sta.LastWrVld \in BOOLEAN + /\ Sta.LastWrPtr \in NodeU + /\ Sta.PendReqSrc \in NodeU + /\ Sta.PendReqCmd \in UniU + /\ Sta.Collecting \in BOOLEAN + /\ Sta.FwdCmd \in UNI_CMD + /\ Sta.FwdSrc \in NodeU + /\ Sta.LastInvAck \in NodeU + /\ Sta.Env_o \in BOOLEAN + +------------------------------------------------------------------------------- + +Init == + \E h \in NODE, d \in DATA : + /\ Home = h + /\ Sta = + [ Proc |-> [i \in NODE |-> [ProcCmd |-> "NODE_None", InvMarked |-> FALSE, + CacheState |-> "CACHE_I", CacheData |-> Undefined]], + Dir |-> [Pending |-> FALSE, Local |-> FALSE, Dirty |-> FALSE, + HeadVld |-> FALSE, HeadPtr |-> Undefined, ShrVld |-> FALSE, + ShrSet |-> [i \in NODE |-> FALSE], InvSet |-> [i \in NODE |-> FALSE]], + MemData |-> d, + UniMsg |-> [i \in NODE |-> [Cmd |-> "UNI_None", Proc |-> Undefined, Data |-> Undefined]], + InvMsg |-> [i \in NODE |-> [Cmd |-> "INV_None"]], + RpMsg |-> [i \in NODE |-> [Cmd |-> "RP_None"]], + WbMsg |-> [Cmd |-> "WB_None", Proc |-> Undefined, Data |-> Undefined], + ShWbMsg |-> [Cmd |-> "SHWB_None", Proc |-> Undefined, Data |-> Undefined], + NakcMsg |-> [Cmd |-> "NAKC_None"], + CurrData |-> d, + PrevData |-> d, + LastWrVld |-> FALSE, + LastWrPtr |-> Undefined, + PendReqSrc |-> Undefined, + PendReqCmd |-> Undefined, + Collecting |-> FALSE, + FwdCmd |-> "UNI_None", + FwdSrc |-> Undefined, + LastInvAck |-> Undefined, + Env_o |-> TRUE ] + +------------------------------------------------------------------------------- +(* Concrete (non-ABS) rules *) +------------------------------------------------------------------------------- + +Store(src, data) == + /\ Sta.Proc[src].CacheState = "CACHE_E" + /\ Sta' = [Sta EXCEPT !.Proc[src].CacheData = data, + !.CurrData = data, + !.LastWrVld = TRUE, + !.LastWrPtr = src] + /\ UNCHANGED Home + +PI_Remote_Get(src) == + /\ src # Home + /\ Sta.Proc[src].ProcCmd = "NODE_None" + /\ Sta.Proc[src].CacheState = "CACHE_I" + /\ Sta' = [Sta EXCEPT !.Proc[src].ProcCmd = "NODE_Get", + !.UniMsg[src].Cmd = "UNI_Get", + !.UniMsg[src].Proc = Home, + !.UniMsg[src].Data = Undefined] + /\ UNCHANGED Home + +PI_Local_Get_Get == + /\ Sta.Proc[Home].ProcCmd = "NODE_None" + /\ Sta.Proc[Home].CacheState = "CACHE_I" + /\ ~Sta.Dir.Pending /\ Sta.Dir.Dirty + /\ Sta' = [Sta EXCEPT !.Proc[Home].ProcCmd = "NODE_Get", + !.Dir.Pending = TRUE, + !.UniMsg[Home].Cmd = "UNI_Get", + !.UniMsg[Home].Proc = Sta.Dir.HeadPtr, + !.UniMsg[Home].Data = Undefined, + !.FwdCmd = IF Sta.Dir.HeadPtr # Home THEN "UNI_Get" ELSE Sta.FwdCmd, + !.PendReqSrc = Home, + !.PendReqCmd = "UNI_Get", + !.Collecting = FALSE] + /\ UNCHANGED Home + +PI_Local_Get_Put == + /\ Sta.Proc[Home].ProcCmd = "NODE_None" + /\ Sta.Proc[Home].CacheState = "CACHE_I" + /\ ~Sta.Dir.Pending /\ ~Sta.Dir.Dirty + /\ Sta' = [Sta EXCEPT !.Dir.Local = TRUE, + !.Proc[Home].ProcCmd = "NODE_None", + !.Proc[Home].InvMarked = FALSE, + !.Proc[Home].CacheState = + IF Sta.Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", + !.Proc[Home].CacheData = + IF Sta.Proc[Home].InvMarked THEN Undefined ELSE Sta.MemData] + /\ UNCHANGED Home + +PI_Remote_GetX(src) == + /\ src # Home + /\ Sta.Proc[src].ProcCmd = "NODE_None" + /\ Sta.Proc[src].CacheState = "CACHE_I" + /\ Sta' = [Sta EXCEPT !.Proc[src].ProcCmd = "NODE_GetX", + !.UniMsg[src].Cmd = "UNI_GetX", + !.UniMsg[src].Proc = Home, + !.UniMsg[src].Data = Undefined] + /\ UNCHANGED Home + +PI_Local_GetX_GetX == + /\ Sta.Proc[Home].ProcCmd = "NODE_None" + /\ Sta.Proc[Home].CacheState \in {"CACHE_I", "CACHE_S"} + /\ ~Sta.Dir.Pending /\ Sta.Dir.Dirty + /\ Sta' = [Sta EXCEPT !.Proc[Home].ProcCmd = "NODE_GetX", + !.Dir.Pending = TRUE, + !.UniMsg[Home].Cmd = "UNI_GetX", + !.UniMsg[Home].Proc = Sta.Dir.HeadPtr, + !.UniMsg[Home].Data = Undefined, + !.FwdCmd = IF Sta.Dir.HeadPtr # Home THEN "UNI_GetX" ELSE Sta.FwdCmd, + !.PendReqSrc = Home, + !.PendReqCmd = "UNI_GetX", + !.Collecting = FALSE] + /\ UNCHANGED Home + +PI_Local_GetX_PutX == + /\ Sta.Proc[Home].ProcCmd = "NODE_None" + /\ Sta.Proc[Home].CacheState \in {"CACHE_I", "CACHE_S"} + /\ ~Sta.Dir.Pending /\ ~Sta.Dir.Dirty + /\ LET InvP(p) == /\ p # Home + /\ \/ (Sta.Dir.ShrVld /\ Sta.Dir.ShrSet[p]) + \/ (Sta.Dir.HeadVld /\ Sta.Dir.HeadPtr = p) + base == [Sta EXCEPT !.Dir.Local = TRUE, !.Dir.Dirty = TRUE] + withHead == + IF Sta.Dir.HeadVld + THEN [base EXCEPT !.Dir.Pending = TRUE, + !.PendReqSrc = Home, + !.Dir.HeadVld = FALSE, + !.Dir.HeadPtr = Undefined, + !.Dir.ShrVld = FALSE, + !.Dir.ShrSet = [p \in NODE |-> FALSE], + !.Dir.InvSet = [p \in NODE |-> InvP(p)], + !.InvMsg = [p \in NODE |-> [Cmd |-> IF InvP(p) THEN "INV_Inv" ELSE "INV_None"]], + !.Collecting = TRUE, + !.PrevData = Sta.CurrData] + ELSE base + IN Sta' = [withHead EXCEPT !.Proc[Home].ProcCmd = "NODE_None", + !.Proc[Home].InvMarked = FALSE, + !.Proc[Home].CacheState = "CACHE_E", + !.Proc[Home].CacheData = Sta.MemData] + /\ UNCHANGED Home + +PI_Remote_PutX(dst) == + /\ dst # Home + /\ Sta.Proc[dst].ProcCmd = "NODE_None" + /\ Sta.Proc[dst].CacheState = "CACHE_E" + /\ Sta' = [Sta EXCEPT !.Proc[dst].CacheState = "CACHE_I", + !.Proc[dst].CacheData = Undefined, + !.WbMsg.Cmd = "WB_Wb", + !.WbMsg.Proc = dst, + !.WbMsg.Data = Sta.Proc[dst].CacheData] + /\ UNCHANGED Home + +PI_Local_PutX == + /\ Sta.Proc[Home].ProcCmd = "NODE_None" + /\ Sta.Proc[Home].CacheState = "CACHE_E" + /\ Sta' = [Sta EXCEPT !.Proc[Home].CacheState = "CACHE_I", + !.Proc[Home].CacheData = Undefined, + !.Dir.Dirty = FALSE, + !.MemData = Sta.Proc[Home].CacheData, + !.Dir.Local = IF Sta.Dir.Pending THEN Sta.Dir.Local ELSE FALSE] + /\ UNCHANGED Home + +PI_Remote_Replace(src) == + /\ src # Home + /\ Sta.Proc[src].ProcCmd = "NODE_None" + /\ Sta.Proc[src].CacheState = "CACHE_S" + /\ Sta' = [Sta EXCEPT !.Proc[src].CacheState = "CACHE_I", + !.Proc[src].CacheData = Undefined, + !.RpMsg[src].Cmd = "RP_Replace"] + /\ UNCHANGED Home + +PI_Local_Replace == + /\ Sta.Proc[Home].ProcCmd = "NODE_None" + /\ Sta.Proc[Home].CacheState = "CACHE_S" + /\ Sta' = [Sta EXCEPT !.Dir.Local = FALSE, + !.Proc[Home].CacheState = "CACHE_I", + !.Proc[Home].CacheData = Undefined] + /\ UNCHANGED Home + +NI_Nak(dst) == + /\ Sta.UniMsg[dst].Cmd = "UNI_Nak" + /\ Sta' = [Sta EXCEPT !.UniMsg[dst].Cmd = "UNI_None", + !.UniMsg[dst].Proc = Undefined, + !.UniMsg[dst].Data = Undefined, + !.Proc[dst].ProcCmd = "NODE_None", + !.Proc[dst].InvMarked = FALSE] + /\ UNCHANGED Home + +NI_Nak_Clear == + /\ Sta.NakcMsg.Cmd = "NAKC_Nakc" + /\ Sta' = [Sta EXCEPT !.NakcMsg.Cmd = "NAKC_None", !.Dir.Pending = FALSE] + /\ UNCHANGED Home + +NI_Local_Get_Nak(src) == + /\ src # Home + /\ Sta.UniMsg[src].Cmd = "UNI_Get" + /\ Sta.UniMsg[src].Proc = Home + /\ Sta.RpMsg[src].Cmd # "RP_Replace" + /\ \/ Sta.Dir.Pending + \/ (Sta.Dir.Dirty /\ Sta.Dir.Local /\ Sta.Proc[Home].CacheState # "CACHE_E") + \/ (Sta.Dir.Dirty /\ ~Sta.Dir.Local /\ Sta.Dir.HeadPtr = src) + /\ Sta' = [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_Nak", + !.UniMsg[src].Proc = Home, + !.UniMsg[src].Data = Undefined] + /\ UNCHANGED Home + +NI_Local_Get_Get(src) == + /\ src # Home + /\ Sta.UniMsg[src].Cmd = "UNI_Get" + /\ Sta.UniMsg[src].Proc = Home + /\ Sta.RpMsg[src].Cmd # "RP_Replace" + /\ ~Sta.Dir.Pending /\ Sta.Dir.Dirty /\ ~Sta.Dir.Local /\ Sta.Dir.HeadPtr # src + /\ Sta' = [Sta EXCEPT !.Dir.Pending = TRUE, + !.UniMsg[src].Cmd = "UNI_Get", + !.UniMsg[src].Proc = Sta.Dir.HeadPtr, + !.UniMsg[src].Data = Undefined, + !.FwdCmd = IF Sta.Dir.HeadPtr # Home THEN "UNI_Get" ELSE Sta.FwdCmd, + !.PendReqSrc = src, + !.PendReqCmd = "UNI_Get", + !.Collecting = FALSE] + /\ UNCHANGED Home + +NI_Local_Get_Put(src) == + /\ src # Home + /\ Sta.UniMsg[src].Cmd = "UNI_Get" + /\ Sta.UniMsg[src].Proc = Home + /\ Sta.RpMsg[src].Cmd # "RP_Replace" + /\ ~Sta.Dir.Pending + /\ (Sta.Dir.Dirty => (Sta.Dir.Local /\ Sta.Proc[Home].CacheState = "CACHE_E")) + /\ Sta' = + IF Sta.Dir.Dirty + THEN [Sta EXCEPT !.Dir.Dirty = FALSE, !.Dir.HeadVld = TRUE, !.Dir.HeadPtr = src, + !.MemData = Sta.Proc[Home].CacheData, !.Proc[Home].CacheState = "CACHE_S", + !.UniMsg[src].Cmd = "UNI_Put", !.UniMsg[src].Proc = Home, + !.UniMsg[src].Data = Sta.Proc[Home].CacheData] + ELSE LET s1 == IF Sta.Dir.HeadVld + THEN [Sta EXCEPT !.Dir.ShrVld = TRUE, !.Dir.ShrSet[src] = TRUE, + !.Dir.InvSet = [p \in NODE |-> (p = src) \/ Sta.Dir.ShrSet[p]]] + ELSE [Sta EXCEPT !.Dir.HeadVld = TRUE, !.Dir.HeadPtr = src] + IN [s1 EXCEPT !.UniMsg[src].Cmd = "UNI_Put", !.UniMsg[src].Proc = Home, + !.UniMsg[src].Data = Sta.MemData] + /\ UNCHANGED Home + +NI_Remote_Get_Nak(src, dst) == + /\ src # dst /\ dst # Home + /\ Sta.UniMsg[src].Cmd = "UNI_Get" + /\ Sta.UniMsg[src].Proc = dst + /\ Sta.Proc[dst].CacheState # "CACHE_E" + /\ Sta' = [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_Nak", + !.UniMsg[src].Proc = dst, + !.UniMsg[src].Data = Undefined, + !.NakcMsg.Cmd = "NAKC_Nakc", + !.FwdCmd = "UNI_None", + !.FwdSrc = src] + /\ UNCHANGED Home + +NI_Remote_Get_Put(src, dst) == + /\ src # dst /\ dst # Home + /\ Sta.UniMsg[src].Cmd = "UNI_Get" + /\ Sta.UniMsg[src].Proc = dst + /\ Sta.Proc[dst].CacheState = "CACHE_E" + /\ LET s1 == [Sta EXCEPT !.Proc[dst].CacheState = "CACHE_S", + !.UniMsg[src].Cmd = "UNI_Put", + !.UniMsg[src].Proc = dst, + !.UniMsg[src].Data = Sta.Proc[dst].CacheData, + !.FwdCmd = "UNI_None", + !.FwdSrc = src] + IN Sta' = IF src # Home + THEN [s1 EXCEPT !.ShWbMsg.Cmd = "SHWB_ShWb", + !.ShWbMsg.Proc = src, + !.ShWbMsg.Data = Sta.Proc[dst].CacheData] + ELSE s1 + /\ UNCHANGED Home + +NI_Local_GetX_Nak(src) == + /\ src # Home + /\ Sta.UniMsg[src].Cmd = "UNI_GetX" + /\ Sta.UniMsg[src].Proc = Home + /\ \/ Sta.Dir.Pending + \/ (Sta.Dir.Dirty /\ Sta.Dir.Local /\ Sta.Proc[Home].CacheState # "CACHE_E") + \/ (Sta.Dir.Dirty /\ ~Sta.Dir.Local /\ Sta.Dir.HeadPtr = src) + /\ Sta' = [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_Nak", + !.UniMsg[src].Proc = Home, + !.UniMsg[src].Data = Undefined] + /\ UNCHANGED Home + +NI_Local_GetX_GetX(src) == + /\ src # Home + /\ Sta.UniMsg[src].Cmd = "UNI_GetX" + /\ Sta.UniMsg[src].Proc = Home + /\ ~Sta.Dir.Pending /\ Sta.Dir.Dirty /\ ~Sta.Dir.Local /\ Sta.Dir.HeadPtr # src + /\ Sta' = [Sta EXCEPT !.Dir.Pending = TRUE, + !.UniMsg[src].Cmd = "UNI_GetX", + !.UniMsg[src].Proc = Sta.Dir.HeadPtr, + !.UniMsg[src].Data = Undefined, + !.FwdCmd = IF Sta.Dir.HeadPtr # Home THEN "UNI_GetX" ELSE Sta.FwdCmd, + !.PendReqSrc = src, + !.PendReqCmd = "UNI_GetX", + !.Collecting = FALSE] + /\ UNCHANGED Home + +NI_Local_GetX_PutX(src) == + /\ src # Home + /\ Sta.UniMsg[src].Cmd = "UNI_GetX" + /\ Sta.UniMsg[src].Proc = Home + /\ ~Sta.Dir.Pending + /\ (Sta.Dir.Dirty => (Sta.Dir.Local /\ Sta.Proc[Home].CacheState = "CACHE_E")) + /\ LET Cond3(p) == /\ p # Home /\ p # src + /\ \/ (Sta.Dir.ShrVld /\ Sta.Dir.ShrSet[p]) + \/ (Sta.Dir.HeadVld /\ Sta.Dir.HeadPtr = p) + localI(st) == + IF Sta.Dir.Local + THEN [st EXCEPT !.Proc[Home].CacheState = "CACHE_I", + !.Proc[Home].CacheData = Undefined, + !.Proc[Home].InvMarked = + IF Sta.Proc[Home].ProcCmd = "NODE_Get" + THEN TRUE ELSE Sta.Proc[Home].InvMarked] + ELSE st + branch1 == + [Sta EXCEPT !.Dir.Local = FALSE, !.Dir.Dirty = TRUE, !.Dir.HeadVld = TRUE, + !.Dir.HeadPtr = src, !.Dir.ShrVld = FALSE, + !.Dir.ShrSet = [p \in NODE |-> FALSE], + !.Dir.InvSet = [p \in NODE |-> FALSE], + !.UniMsg[src].Cmd = "UNI_PutX", !.UniMsg[src].Proc = Home, + !.UniMsg[src].Data = Sta.Proc[Home].CacheData, + !.Proc[Home].CacheState = "CACHE_I", + !.Proc[Home].CacheData = Undefined] + branch2base == + [Sta EXCEPT !.Dir.Local = FALSE, !.Dir.Dirty = TRUE, !.Dir.HeadVld = TRUE, + !.Dir.HeadPtr = src, !.Dir.ShrVld = FALSE, + !.Dir.ShrSet = [p \in NODE |-> FALSE], + !.Dir.InvSet = [p \in NODE |-> FALSE], + !.UniMsg[src].Cmd = "UNI_PutX", !.UniMsg[src].Proc = Home, + !.UniMsg[src].Data = Sta.MemData, + !.Proc[Home].CacheState = "CACHE_I", + !.Proc[Home].CacheData = Undefined] + branch3base == + [Sta EXCEPT !.Dir.Pending = TRUE, !.Dir.Local = FALSE, !.Dir.Dirty = TRUE, + !.Dir.HeadVld = TRUE, !.Dir.HeadPtr = src, !.Dir.ShrVld = FALSE, + !.Dir.ShrSet = [p \in NODE |-> FALSE], + !.Dir.InvSet = [p \in NODE |-> Cond3(p)], + !.InvMsg = [p \in NODE |-> [Cmd |-> IF Cond3(p) THEN "INV_Inv" ELSE "INV_None"]], + !.UniMsg[src].Cmd = "UNI_PutX", !.UniMsg[src].Proc = Home, + !.UniMsg[src].Data = Sta.MemData, + !.PendReqSrc = src, !.PendReqCmd = "UNI_GetX", + !.Collecting = TRUE, !.PrevData = Sta.CurrData] + elsifCond == + Sta.Dir.HeadVld => (Sta.Dir.HeadPtr = src + /\ \A p \in NODE : p # src => ~Sta.Dir.ShrSet[p]) + IN Sta' = IF Sta.Dir.Dirty THEN branch1 + ELSE IF elsifCond THEN localI(branch2base) + ELSE localI(branch3base) + /\ UNCHANGED Home + +NI_Remote_GetX_Nak(src, dst) == + /\ src # dst /\ dst # Home + /\ Sta.UniMsg[src].Cmd = "UNI_GetX" + /\ Sta.UniMsg[src].Proc = dst + /\ Sta.Proc[dst].CacheState # "CACHE_E" + /\ Sta' = [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_Nak", + !.UniMsg[src].Proc = dst, + !.UniMsg[src].Data = Undefined, + !.NakcMsg.Cmd = "NAKC_Nakc", + !.FwdCmd = "UNI_None", + !.FwdSrc = src] + /\ UNCHANGED Home + +NI_Remote_GetX_PutX(src, dst) == + /\ src # dst /\ dst # Home + /\ Sta.UniMsg[src].Cmd = "UNI_GetX" + /\ Sta.UniMsg[src].Proc = dst + /\ Sta.Proc[dst].CacheState = "CACHE_E" + /\ LET s1 == [Sta EXCEPT !.Proc[dst].CacheState = "CACHE_I", + !.Proc[dst].CacheData = Undefined, + !.UniMsg[src].Cmd = "UNI_PutX", + !.UniMsg[src].Proc = dst, + !.UniMsg[src].Data = Sta.Proc[dst].CacheData, + !.FwdCmd = "UNI_None", + !.FwdSrc = src] + IN Sta' = IF src # Home + THEN [s1 EXCEPT !.ShWbMsg.Cmd = "SHWB_FAck", + !.ShWbMsg.Proc = src, + !.ShWbMsg.Data = Undefined] + ELSE s1 + /\ UNCHANGED Home + +NI_Local_Put == + /\ Sta.UniMsg[Home].Cmd = "UNI_Put" + /\ Sta' = [Sta EXCEPT !.UniMsg[Home].Cmd = "UNI_None", + !.UniMsg[Home].Proc = Undefined, + !.UniMsg[Home].Data = Undefined, + !.Dir.Pending = FALSE, + !.Dir.Dirty = FALSE, + !.Dir.Local = TRUE, + !.MemData = Sta.UniMsg[Home].Data, + !.Proc[Home].ProcCmd = "NODE_None", + !.Proc[Home].InvMarked = FALSE, + !.Proc[Home].CacheState = + IF Sta.Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", + !.Proc[Home].CacheData = + IF Sta.Proc[Home].InvMarked THEN Undefined ELSE Sta.UniMsg[Home].Data] + /\ UNCHANGED Home + +NI_Remote_Put(dst) == + /\ dst # Home + /\ Sta.UniMsg[dst].Cmd = "UNI_Put" + /\ Sta' = [Sta EXCEPT !.UniMsg[dst].Cmd = "UNI_None", + !.UniMsg[dst].Proc = Undefined, + !.UniMsg[dst].Data = Undefined, + !.Proc[dst].ProcCmd = "NODE_None", + !.Proc[dst].InvMarked = FALSE, + !.Proc[dst].CacheState = + IF Sta.Proc[dst].InvMarked THEN "CACHE_I" ELSE "CACHE_S", + !.Proc[dst].CacheData = + IF Sta.Proc[dst].InvMarked THEN Undefined ELSE Sta.UniMsg[dst].Data] + /\ UNCHANGED Home + +NI_Local_PutXAcksDone == + /\ Sta.UniMsg[Home].Cmd = "UNI_PutX" + /\ Sta' = [Sta EXCEPT !.UniMsg[Home].Cmd = "UNI_None", + !.UniMsg[Home].Proc = Undefined, + !.UniMsg[Home].Data = Undefined, + !.Dir.Pending = FALSE, + !.Dir.Local = TRUE, + !.Dir.HeadVld = FALSE, + !.Dir.HeadPtr = Undefined, + !.Proc[Home].ProcCmd = "NODE_None", + !.Proc[Home].InvMarked = FALSE, + !.Proc[Home].CacheState = "CACHE_E", + !.Proc[Home].CacheData = Sta.UniMsg[Home].Data] + /\ UNCHANGED Home + +NI_Remote_PutX(dst) == + /\ dst # Home + /\ Sta.UniMsg[dst].Cmd = "UNI_PutX" + /\ Sta.Proc[dst].ProcCmd = "NODE_GetX" + /\ Sta' = [Sta EXCEPT !.UniMsg[dst].Cmd = "UNI_None", + !.UniMsg[dst].Proc = Undefined, + !.UniMsg[dst].Data = Undefined, + !.Proc[dst].ProcCmd = "NODE_None", + !.Proc[dst].InvMarked = FALSE, + !.Proc[dst].CacheState = "CACHE_E", + !.Proc[dst].CacheData = Sta.UniMsg[dst].Data] + /\ UNCHANGED Home + +NI_Inv(dst) == + /\ dst # Home + /\ Sta.InvMsg[dst].Cmd = "INV_Inv" + /\ Sta' = [Sta EXCEPT !.InvMsg[dst].Cmd = "INV_InvAck", + !.Proc[dst].CacheState = "CACHE_I", + !.Proc[dst].CacheData = Undefined, + !.Proc[dst].InvMarked = + IF Sta.Proc[dst].ProcCmd = "NODE_Get" THEN TRUE + ELSE Sta.Proc[dst].InvMarked] + /\ UNCHANGED Home + +NI_InvAck(src) == + /\ src # Home + /\ Sta.InvMsg[src].Cmd = "INV_InvAck" + /\ Sta.Dir.Pending /\ Sta.Dir.InvSet[src] + /\ LET s1 == [Sta EXCEPT !.InvMsg[src].Cmd = "INV_None", !.Dir.InvSet[src] = FALSE] + moreAcks == \E p \in NODE : p # src /\ Sta.Dir.InvSet[p] + IN Sta' = IF moreAcks + THEN [s1 EXCEPT !.LastInvAck = src] + ELSE [s1 EXCEPT !.Dir.Pending = FALSE, + !.Dir.Local = IF Sta.Dir.Local /\ ~Sta.Dir.Dirty + THEN FALSE ELSE Sta.Dir.Local, + !.Collecting = FALSE, + !.LastInvAck = src] + /\ UNCHANGED Home + +NI_Wb == + /\ Sta.WbMsg.Cmd = "WB_Wb" + /\ Sta' = [Sta EXCEPT !.WbMsg.Cmd = "WB_None", + !.WbMsg.Proc = Undefined, + !.WbMsg.Data = Undefined, + !.Dir.Dirty = FALSE, + !.Dir.HeadVld = FALSE, + !.Dir.HeadPtr = Undefined, + !.MemData = Sta.WbMsg.Data] + /\ UNCHANGED Home + +NI_FAck == + /\ Sta.ShWbMsg.Cmd = "SHWB_FAck" + /\ Sta' = [Sta EXCEPT !.ShWbMsg.Cmd = "SHWB_None", + !.ShWbMsg.Proc = Undefined, + !.ShWbMsg.Data = Undefined, + !.Dir.Pending = FALSE, + !.Dir.HeadPtr = IF Sta.Dir.Dirty THEN Sta.ShWbMsg.Proc ELSE Sta.Dir.HeadPtr] + /\ UNCHANGED Home + +NI_ShWb == + /\ Sta.ShWbMsg.Cmd = "SHWB_ShWb" + /\ Sta' = [Sta EXCEPT !.ShWbMsg.Cmd = "SHWB_None", + !.ShWbMsg.Proc = Undefined, + !.ShWbMsg.Data = Undefined, + !.Dir.Pending = FALSE, + !.Dir.Dirty = FALSE, + !.Dir.ShrVld = TRUE, + !.Dir.ShrSet = [p \in NODE |-> (p = Sta.ShWbMsg.Proc) \/ Sta.Dir.ShrSet[p]], + !.Dir.InvSet = [p \in NODE |-> (p = Sta.ShWbMsg.Proc) \/ Sta.Dir.ShrSet[p]], + !.MemData = Sta.ShWbMsg.Data] + /\ UNCHANGED Home + +NI_Replace(src) == + /\ Sta.RpMsg[src].Cmd = "RP_Replace" + /\ Sta' = [Sta EXCEPT !.RpMsg[src].Cmd = "RP_None", + !.Dir.ShrSet[src] = IF Sta.Dir.ShrVld THEN FALSE ELSE Sta.Dir.ShrSet[src], + !.Dir.InvSet[src] = IF Sta.Dir.ShrVld THEN FALSE ELSE Sta.Dir.InvSet[src]] + /\ UNCHANGED Home + +------------------------------------------------------------------------------- +(* 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 == + /\ Sta.Dir.Dirty + /\ Sta.WbMsg.Cmd # "WB_Wb" + /\ Sta.ShWbMsg.Cmd # "SHWB_ShWb" + /\ \A p \in NODE : Sta.Proc[p].CacheState # "CACHE_E" + /\ Sta.UniMsg[Home].Cmd # "UNI_Put" + /\ \A q \in NODE : Sta.UniMsg[q].Cmd # "UNI_PutX" + +ABS_Store(data) == + /\ Sta.Env_o + /\ AbsDirtyClean + /\ Sta' = [Sta EXCEPT !.CurrData = data, !.LastWrVld = TRUE, !.LastWrPtr = Other] + /\ UNCHANGED Home + +ABS_PI_Remote_PutX == + /\ Sta.Env_o + /\ AbsDirtyClean + /\ Sta' = [Sta EXCEPT !.WbMsg.Cmd = "WB_Wb", !.WbMsg.Proc = Other, !.WbMsg.Data = Sta.CurrData] + /\ UNCHANGED Home + +ABS_NI_Local_Get_Get == + /\ Sta.Env_o + /\ ~Sta.Dir.Pending /\ Sta.Dir.Dirty /\ ~Sta.Dir.Local /\ Sta.Dir.HeadPtr # Other + /\ Sta' = [Sta EXCEPT !.Dir.Pending = TRUE, + !.FwdCmd = IF Sta.Dir.HeadPtr # Home THEN "UNI_Get" ELSE Sta.FwdCmd, + !.PendReqSrc = Other, + !.PendReqCmd = "UNI_Get", + !.Collecting = FALSE] + /\ UNCHANGED Home + +ABS_NI_Local_Get_Put == + /\ Sta.Env_o + /\ ~Sta.Dir.Pending + /\ (Sta.Dir.Dirty => (Sta.Dir.Local /\ Sta.Proc[Home].CacheState = "CACHE_E")) + /\ Sta' = + IF Sta.Dir.Dirty + THEN [Sta EXCEPT !.Dir.Dirty = FALSE, !.Dir.HeadVld = TRUE, !.Dir.HeadPtr = Other, + !.MemData = Sta.Proc[Home].CacheData, !.Proc[Home].CacheState = "CACHE_S"] + ELSE IF Sta.Dir.HeadVld + THEN [Sta EXCEPT !.Dir.ShrVld = TRUE, + !.Dir.InvSet = [p \in NODE |-> Sta.Dir.ShrSet[p]]] + ELSE [Sta EXCEPT !.Dir.HeadVld = TRUE, !.Dir.HeadPtr = Other] + /\ UNCHANGED Home + +ABS_NI_Remote_Get_Nak_src(dst) == + /\ Sta.Env_o /\ dst # Home + /\ Sta.Proc[dst].CacheState # "CACHE_E" + /\ Sta.Dir.Pending /\ ~Sta.Dir.Local + /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_Get" + /\ Sta' = [Sta EXCEPT !.NakcMsg.Cmd = "NAKC_Nakc", !.FwdCmd = "UNI_None", !.FwdSrc = Other] + /\ UNCHANGED Home + +ABS_NI_Remote_Get_Nak_dst(src) == + /\ Sta.Env_o + /\ Sta.UniMsg[src].Cmd = "UNI_Get" /\ Sta.UniMsg[src].Proc = Other + /\ Sta.Dir.Pending /\ ~Sta.Dir.Local + /\ Sta.PendReqSrc = src /\ Sta.FwdCmd = "UNI_Get" + /\ Sta' = [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_Nak", + !.UniMsg[src].Proc = Other, + !.UniMsg[src].Data = Undefined, + !.NakcMsg.Cmd = "NAKC_Nakc", + !.FwdCmd = "UNI_None", + !.FwdSrc = src] + /\ UNCHANGED Home + +ABS_NI_Remote_Get_Nak_src_dst == + /\ Sta.Env_o + /\ Sta.Dir.Pending /\ ~Sta.Dir.Local + /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_Get" + /\ Sta' = [Sta EXCEPT !.NakcMsg.Cmd = "NAKC_Nakc", !.FwdCmd = "UNI_None", !.FwdSrc = Other] + /\ UNCHANGED Home + +ABS_NI_Remote_Get_Put_src(dst) == + /\ Sta.Env_o /\ dst # Home + /\ Sta.Proc[dst].CacheState = "CACHE_E" + /\ Sta.Dir.Pending /\ ~Sta.Dir.Local + /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_Get" + /\ Sta' = [Sta EXCEPT !.Proc[dst].CacheState = "CACHE_S", + !.ShWbMsg.Cmd = "SHWB_ShWb", + !.ShWbMsg.Proc = Other, + !.ShWbMsg.Data = Sta.Proc[dst].CacheData, + !.FwdCmd = "UNI_None", + !.FwdSrc = Other] + /\ UNCHANGED Home + +ABS_NI_Remote_Get_Put_dst(src) == + /\ Sta.Env_o + /\ Sta.UniMsg[src].Cmd = "UNI_Get" /\ Sta.UniMsg[src].Proc = Other + /\ AbsDirtyClean + /\ Sta.Dir.Pending /\ ~Sta.Dir.Local + /\ Sta.PendReqSrc = src /\ Sta.FwdCmd = "UNI_Get" + /\ LET s1 == [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_Put", + !.UniMsg[src].Proc = Other, + !.UniMsg[src].Data = Sta.CurrData, + !.FwdCmd = "UNI_None", + !.FwdSrc = src] + IN Sta' = IF src # Home + THEN [s1 EXCEPT !.ShWbMsg.Cmd = "SHWB_ShWb", + !.ShWbMsg.Proc = src, + !.ShWbMsg.Data = Sta.CurrData] + ELSE s1 + /\ UNCHANGED Home + +ABS_NI_Remote_Get_Put_src_dst == + /\ Sta.Env_o + /\ AbsDirtyClean + /\ Sta.Dir.Pending /\ ~Sta.Dir.Local + /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_Get" + /\ Sta' = [Sta EXCEPT !.ShWbMsg.Cmd = "SHWB_ShWb", + !.ShWbMsg.Proc = Other, + !.ShWbMsg.Data = Sta.CurrData, + !.FwdCmd = "UNI_None", + !.FwdSrc = Other] + /\ UNCHANGED Home + +ABS_NI_Local_GetX_GetX == + /\ Sta.Env_o + /\ ~Sta.Dir.Pending /\ Sta.Dir.Dirty /\ ~Sta.Dir.Local /\ Sta.Dir.HeadPtr # Other + /\ Sta' = [Sta EXCEPT !.Dir.Pending = TRUE, + !.FwdCmd = IF Sta.Dir.HeadPtr # Home THEN "UNI_GetX" ELSE Sta.FwdCmd, + !.PendReqSrc = Other, + !.PendReqCmd = "UNI_GetX", + !.Collecting = FALSE] + /\ UNCHANGED Home + +ABS_NI_Local_GetX_PutX == + /\ Sta.Env_o + /\ ~Sta.Dir.Pending + /\ (Sta.Dir.Dirty => (Sta.Dir.Local /\ Sta.Proc[Home].CacheState = "CACHE_E")) + /\ LET Cond3(p) == /\ p # Home + /\ \/ (Sta.Dir.ShrVld /\ Sta.Dir.ShrSet[p]) + \/ (Sta.Dir.HeadVld /\ Sta.Dir.HeadPtr = p) + localI(st) == + IF Sta.Dir.Local + THEN [st EXCEPT !.Proc[Home].CacheState = "CACHE_I", + !.Proc[Home].CacheData = Undefined, + !.Proc[Home].InvMarked = + IF Sta.Proc[Home].ProcCmd = "NODE_Get" + THEN TRUE ELSE Sta.Proc[Home].InvMarked] + ELSE st + branch1 == + [Sta EXCEPT !.Dir.Local = FALSE, !.Dir.Dirty = TRUE, !.Dir.HeadVld = TRUE, + !.Dir.HeadPtr = Other, !.Dir.ShrVld = FALSE, + !.Dir.ShrSet = [p \in NODE |-> FALSE], + !.Dir.InvSet = [p \in NODE |-> FALSE], + !.Proc[Home].CacheState = "CACHE_I", + !.Proc[Home].CacheData = Undefined] + branch2base == + [Sta EXCEPT !.Dir.Local = FALSE, !.Dir.Dirty = TRUE, !.Dir.HeadVld = TRUE, + !.Dir.HeadPtr = Other, !.Dir.ShrVld = FALSE, + !.Dir.ShrSet = [p \in NODE |-> FALSE], + !.Dir.InvSet = [p \in NODE |-> FALSE], + !.Proc[Home].CacheState = "CACHE_I", + !.Proc[Home].CacheData = Undefined] + branch3base == + [Sta EXCEPT !.Dir.Pending = TRUE, !.Dir.Local = FALSE, !.Dir.Dirty = TRUE, + !.Dir.HeadVld = TRUE, !.Dir.HeadPtr = Other, !.Dir.ShrVld = FALSE, + !.Dir.ShrSet = [p \in NODE |-> FALSE], + !.Dir.InvSet = [p \in NODE |-> Cond3(p)], + !.InvMsg = [p \in NODE |-> [Cmd |-> IF Cond3(p) THEN "INV_Inv" ELSE "INV_None"]], + !.PendReqSrc = Other, !.PendReqCmd = "UNI_GetX", + !.Collecting = TRUE, !.PrevData = Sta.CurrData] + elsifCond == + Sta.Dir.HeadVld => (Sta.Dir.HeadPtr = Other /\ \A p \in NODE : ~Sta.Dir.ShrSet[p]) + IN Sta' = IF Sta.Dir.Dirty THEN branch1 + ELSE IF elsifCond THEN localI(branch2base) + ELSE localI(branch3base) + /\ UNCHANGED Home + +ABS_NI_Remote_GetX_Nak_src(dst) == + /\ Sta.Env_o /\ dst # Home + /\ Sta.Proc[dst].CacheState # "CACHE_E" + /\ Sta.Dir.Pending /\ ~Sta.Dir.Local + /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_GetX" + /\ Sta' = [Sta EXCEPT !.NakcMsg.Cmd = "NAKC_Nakc", !.FwdCmd = "UNI_None", !.FwdSrc = Other] + /\ UNCHANGED Home + +ABS_NI_Remote_GetX_Nak_dst(src) == + /\ Sta.Env_o + /\ Sta.UniMsg[src].Cmd = "UNI_GetX" /\ Sta.UniMsg[src].Proc = Other + /\ Sta.Dir.Pending /\ ~Sta.Dir.Local + /\ Sta.PendReqSrc = src /\ Sta.FwdCmd = "UNI_GetX" + /\ Sta' = [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_Nak", + !.UniMsg[src].Proc = Other, + !.UniMsg[src].Data = Undefined, + !.NakcMsg.Cmd = "NAKC_Nakc", + !.FwdCmd = "UNI_None", + !.FwdSrc = src] + /\ UNCHANGED Home + +ABS_NI_Remote_GetX_Nak_src_dst == + /\ Sta.Env_o + /\ Sta.Dir.Pending /\ ~Sta.Dir.Local + /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_GetX" + /\ Sta' = [Sta EXCEPT !.NakcMsg.Cmd = "NAKC_Nakc", !.FwdCmd = "UNI_None", !.FwdSrc = Other] + /\ UNCHANGED Home + +ABS_NI_Remote_GetX_PutX_src(dst) == + /\ Sta.Env_o /\ dst # Home + /\ Sta.Proc[dst].CacheState = "CACHE_E" + /\ Sta.Dir.Pending /\ ~Sta.Dir.Local + /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_GetX" + /\ Sta' = [Sta EXCEPT !.Proc[dst].CacheState = "CACHE_I", + !.Proc[dst].CacheData = Undefined, + !.ShWbMsg.Cmd = "SHWB_FAck", + !.ShWbMsg.Proc = Other, + !.ShWbMsg.Data = Undefined, + !.FwdCmd = "UNI_None", + !.FwdSrc = Other] + /\ UNCHANGED Home + +ABS_NI_Remote_GetX_PutX_dst(src) == + /\ Sta.Env_o + /\ Sta.UniMsg[src].Cmd = "UNI_GetX" /\ Sta.UniMsg[src].Proc = Other + /\ AbsDirtyClean + /\ Sta.Dir.Pending /\ ~Sta.Dir.Local + /\ Sta.PendReqSrc = src /\ Sta.FwdCmd = "UNI_GetX" + /\ LET s1 == [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_PutX", + !.UniMsg[src].Proc = Other, + !.UniMsg[src].Data = Sta.CurrData, + !.FwdCmd = "UNI_None", + !.FwdSrc = src] + IN Sta' = IF src # Home + THEN [s1 EXCEPT !.ShWbMsg.Cmd = "SHWB_FAck", + !.ShWbMsg.Proc = src, + !.ShWbMsg.Data = Undefined] + ELSE s1 + /\ UNCHANGED Home + +ABS_NI_Remote_GetX_PutX_src_dst == + /\ Sta.Env_o + /\ AbsDirtyClean + /\ Sta.Dir.Pending /\ ~Sta.Dir.Local + /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_GetX" + /\ Sta' = [Sta EXCEPT !.ShWbMsg.Cmd = "SHWB_FAck", + !.ShWbMsg.Proc = Other, + !.ShWbMsg.Data = Undefined, + !.FwdCmd = "UNI_None", + !.FwdSrc = Other] + /\ UNCHANGED Home + +ABS_NI_InvAck == + /\ Sta.Env_o + /\ Sta.Dir.Pending /\ Sta.Collecting + /\ Sta.NakcMsg.Cmd = "NAKC_None" /\ Sta.ShWbMsg.Cmd = "SHWB_None" + /\ \A q \in NODE : + /\ ((Sta.UniMsg[q].Cmd = "UNI_Get" \/ Sta.UniMsg[q].Cmd = "UNI_GetX") + => Sta.UniMsg[q].Proc = Home) + /\ (Sta.UniMsg[q].Cmd = "UNI_PutX" + => (Sta.UniMsg[q].Proc = Home /\ Sta.PendReqSrc = q)) + /\ LET moreAcks == \E p \in NODE : Sta.Dir.InvSet[p] + IN Sta' = IF moreAcks + THEN [Sta EXCEPT !.LastInvAck = Other] + ELSE [Sta EXCEPT !.Dir.Pending = FALSE, + !.Dir.Local = IF Sta.Dir.Local /\ ~Sta.Dir.Dirty + THEN FALSE ELSE Sta.Dir.Local, + !.Collecting = FALSE, + !.LastInvAck = Other] + /\ UNCHANGED Home + +ABS_NI_ShWb == + /\ Sta.Env_o + /\ Sta.ShWbMsg.Cmd = "SHWB_ShWb" /\ Sta.ShWbMsg.Proc = Other + /\ Sta' = [Sta EXCEPT !.ShWbMsg.Cmd = "SHWB_None", + !.ShWbMsg.Proc = Undefined, + !.ShWbMsg.Data = Undefined, + !.Dir.Pending = FALSE, + !.Dir.Dirty = FALSE, + !.Dir.ShrVld = TRUE, + !.Dir.InvSet = [p \in NODE |-> Sta.Dir.ShrSet[p]], + !.MemData = Sta.ShWbMsg.Data] + /\ UNCHANGED Home + +------------------------------------------------------------------------------- + +Next == + \/ \E src \in NODE, data \in DATA : Store(src, data) + \/ \E data \in DATA : ABS_Store(data) + \/ \E src \in NODE : + \/ PI_Remote_Get(src) \/ PI_Remote_GetX(src) + \/ PI_Remote_Replace(src) + \/ NI_Local_Get_Nak(src) \/ NI_Local_Get_Get(src) \/ NI_Local_Get_Put(src) + \/ NI_Local_GetX_Nak(src) \/ NI_Local_GetX_GetX(src) \/ NI_Local_GetX_PutX(src) + \/ NI_InvAck(src) \/ NI_Replace(src) + \/ ABS_NI_Remote_Get_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_src(src) \/ ABS_NI_Remote_GetX_Nak_dst(src) + \/ ABS_NI_Remote_GetX_PutX_src(src) \/ ABS_NI_Remote_GetX_PutX_dst(src) + \/ \E dst \in NODE : + \/ PI_Remote_PutX(dst) + \/ NI_Nak(dst) \/ NI_Remote_Put(dst) \/ NI_Remote_PutX(dst) \/ NI_Inv(dst) + \/ \E src \in NODE, dst \in NODE : + \/ NI_Remote_Get_Nak(src, dst) \/ NI_Remote_Get_Put(src, dst) + \/ NI_Remote_GetX_Nak(src, dst) \/ NI_Remote_GetX_PutX(src, dst) + \/ PI_Local_Get_Get \/ PI_Local_Get_Put + \/ PI_Local_GetX_GetX \/ PI_Local_GetX_PutX + \/ PI_Local_PutX \/ PI_Local_Replace + \/ NI_Nak_Clear \/ NI_Local_Put \/ NI_Local_PutXAcksDone + \/ NI_Wb \/ NI_FAck \/ NI_ShWb + \/ ABS_PI_Remote_PutX + \/ ABS_NI_Local_Get_Get \/ ABS_NI_Local_Get_Put + \/ ABS_NI_Remote_Get_Nak_src_dst \/ ABS_NI_Remote_Get_Put_src_dst + \/ ABS_NI_Local_GetX_GetX \/ ABS_NI_Local_GetX_PutX + \/ ABS_NI_Remote_GetX_Nak_src_dst \/ ABS_NI_Remote_GetX_PutX_src_dst + \/ ABS_NI_InvAck \/ ABS_NI_ShWb + +Spec == Init /\ [][Next]_vars + +------------------------------------------------------------------------------- +(* Safety properties translated from the Murphi `invariant`s (for indep. *) +(* cross-checking; not part of the bisimulation). *) + +CacheStateProp == + \A p, q \in NODE : + p # q => ~(Sta.Proc[p].CacheState = "CACHE_E" /\ Sta.Proc[q].CacheState = "CACHE_E") + +CacheDataProp == + \A p \in NODE : + /\ (Sta.Proc[p].CacheState = "CACHE_E" => Sta.Proc[p].CacheData = Sta.CurrData) + /\ (Sta.Proc[p].CacheState = "CACHE_S" => + /\ (Sta.Collecting => Sta.Proc[p].CacheData = Sta.PrevData) + /\ (~Sta.Collecting => Sta.Proc[p].CacheData = Sta.CurrData)) + +MemDataProp == + ~Sta.Dir.Dirty => Sta.MemData = Sta.CurrData +============================================================================= diff --git a/specifications/FlashProtocol/MCFlashWithMutex.cfg b/specifications/FlashProtocol/MCFlashWithMutex.cfg new file mode 100644 index 00000000..8433adbb --- /dev/null +++ b/specifications/FlashProtocol/MCFlashWithMutex.cfg @@ -0,0 +1,13 @@ +CONSTANTS + NODE = {n1} + DATA = {d1} + Other = Other + Undefined = Undefined + +SPECIFICATION Spec + +INVARIANT + TypeOK + CacheStateProp + CacheDataProp + MemDataProp diff --git a/specifications/FlashProtocol/MCFlashWithMutex.tla b/specifications/FlashProtocol/MCFlashWithMutex.tla new file mode 100644 index 00000000..8691242e --- /dev/null +++ b/specifications/FlashProtocol/MCFlashWithMutex.tla @@ -0,0 +1,3 @@ +------------------------- MODULE MCFlashWithMutex ------------------------- +EXTENDS FlashWithMutex +============================================================================== diff --git a/specifications/FlashProtocol/manifest.json b/specifications/FlashProtocol/manifest.json new file mode 100644 index 00000000..33a61802 --- /dev/null +++ b/specifications/FlashProtocol/manifest.json @@ -0,0 +1,33 @@ +{ + "sources": [ + "https://github.com/dsethi/ProtocolDeadlockFiles/", + "Divjyot Sethi, Muralidhar Talupur, and Sharad Malik, \"Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom,\" ATVA 2014, LNCS 8837, pp. 330-347.", + "Ching-Tsun Chou, Phanindra K. Mannava, and Seungjoon Park, \"A Simple Method for Parameterized Verification of Cache Coherence Protocols,\" FMCAD 2004, LNCS 3312, pp. 382-398." + ], + "authors": [ + "Markus Kuppe" + ], + "tags": [], + "modules": [ + { + "path": "specifications/FlashProtocol/FlashWithMutex.tla", + "features": [], + "models": [] + }, + { + "path": "specifications/FlashProtocol/MCFlashWithMutex.tla", + "features": [], + "models": [ + { + "path": "specifications/FlashProtocol/MCFlashWithMutex.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 414, + "totalStates": 1231, + "stateDepth": 13 + } + ] + } + ] +} From 5f020ed2a08e54ada8ab8ad659cbccb32ba8f399 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 21 Jul 2026 11:46:50 -0700 Subject: [PATCH 02/17] FlashProtocol: refactor FlashWithMutex toward idiomatic TLA+ Rework the FLASH translation from a rule-by-rule transcription into idiomatic TLA+, and note where the TLA+ model departs conceptually from the CMurphi original: - Imperative rule bodies (sequential assignments, undefine, for-loops) become a single declarative next-state relation on primed variables; each Murphi state field maps to one Sta record field, updated with EXCEPT rather than mutated in place. - Enumerated rulesets over a scalarset collapse into parameterised actions quantified with \E over the constant sets. In particular the shared/exclusive (Get/GetX) rule pairs merge into single actions (PI_Remote, NI_Remote_Nak, ABS_NI_Remote_Nak_src, ABS_NI_Remote_Nak_src_dst), as GermanWithMutex does for SendReq. - Murphi's undefined values / abstract node become explicit TLA+ sentinels (Undefined, Other) as model values. - The scalarset-order-dependent ghost LastOtherInvAck (a pure history variable) is dropped rather than modelled. Equivalence between the idiomatic model and its rule-by-rule origin is proved with TLAPS: each merged action is shown (by definitional unfolding) equal to the disjunction of the two actions it replaced, which combine to give Next <=> NextOld. The model remains strongly bisimilar to the CMurphi specification (EQUIVALENT at NODE/DATA = 1x1, 1x2, 2x1). Co-authored-by: Claude Opus 4.8 Signed-off-by: Markus Alexander Kuppe --- .../FlashProtocol/FlashWithMutex.tla | 80 ++++++------------- 1 file changed, 26 insertions(+), 54 deletions(-) diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla index c7144d99..d1cc8f63 100644 --- a/specifications/FlashProtocol/FlashWithMutex.tla +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -40,6 +40,7 @@ RP_CMD == {"RP_None", "RP_Replace"} WB_CMD == {"WB_None", "WB_Wb"} SHWB_CMD == {"SHWB_None", "SHWB_ShWb", "SHWB_FAck"} NAKC_CMD == {"NAKC_None", "NAKC_Nakc"} +ReqCmd == {"Get", "GetX"} \* shared vs. exclusive request flavour DataU == DATA \cup {Undefined} NodeU == ABS_NODE \cup {Undefined} @@ -121,12 +122,14 @@ Store(src, data) == !.LastWrPtr = src] /\ UNCHANGED Home -PI_Remote_Get(src) == +\* Shared/exclusive request from a remote processor (merges the former +\* PI_Remote_Get / PI_Remote_GetX; see FlashWithMutexEquiv.tla). +PI_Remote(src, c) == /\ src # Home /\ Sta.Proc[src].ProcCmd = "NODE_None" /\ Sta.Proc[src].CacheState = "CACHE_I" - /\ Sta' = [Sta EXCEPT !.Proc[src].ProcCmd = "NODE_Get", - !.UniMsg[src].Cmd = "UNI_Get", + /\ Sta' = [Sta EXCEPT !.Proc[src].ProcCmd = IF c = "Get" THEN "NODE_Get" ELSE "NODE_GetX", + !.UniMsg[src].Cmd = IF c = "Get" THEN "UNI_Get" ELSE "UNI_GetX", !.UniMsg[src].Proc = Home, !.UniMsg[src].Data = Undefined] /\ UNCHANGED Home @@ -159,16 +162,6 @@ PI_Local_Get_Put == IF Sta.Proc[Home].InvMarked THEN Undefined ELSE Sta.MemData] /\ UNCHANGED Home -PI_Remote_GetX(src) == - /\ src # Home - /\ Sta.Proc[src].ProcCmd = "NODE_None" - /\ Sta.Proc[src].CacheState = "CACHE_I" - /\ Sta' = [Sta EXCEPT !.Proc[src].ProcCmd = "NODE_GetX", - !.UniMsg[src].Cmd = "UNI_GetX", - !.UniMsg[src].Proc = Home, - !.UniMsg[src].Data = Undefined] - /\ UNCHANGED Home - PI_Local_GetX_GetX == /\ Sta.Proc[Home].ProcCmd = "NODE_None" /\ Sta.Proc[Home].CacheState \in {"CACHE_I", "CACHE_S"} @@ -313,9 +306,11 @@ NI_Local_Get_Put(src) == !.UniMsg[src].Data = Sta.MemData] /\ UNCHANGED Home -NI_Remote_Get_Nak(src, dst) == +\* Remote NAK of a shared/exclusive request (merges the former +\* NI_Remote_Get_Nak / NI_Remote_GetX_Nak; see FlashWithMutexEquiv.tla). +NI_Remote_Nak(src, dst) == /\ src # dst /\ dst # Home - /\ Sta.UniMsg[src].Cmd = "UNI_Get" + /\ Sta.UniMsg[src].Cmd \in {"UNI_Get", "UNI_GetX"} /\ Sta.UniMsg[src].Proc = dst /\ Sta.Proc[dst].CacheState # "CACHE_E" /\ Sta' = [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_Nak", @@ -424,19 +419,6 @@ NI_Local_GetX_PutX(src) == ELSE localI(branch3base) /\ UNCHANGED Home -NI_Remote_GetX_Nak(src, dst) == - /\ src # dst /\ dst # Home - /\ Sta.UniMsg[src].Cmd = "UNI_GetX" - /\ Sta.UniMsg[src].Proc = dst - /\ Sta.Proc[dst].CacheState # "CACHE_E" - /\ Sta' = [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_Nak", - !.UniMsg[src].Proc = dst, - !.UniMsg[src].Data = Undefined, - !.NakcMsg.Cmd = "NAKC_Nakc", - !.FwdCmd = "UNI_None", - !.FwdSrc = src] - /\ UNCHANGED Home - NI_Remote_GetX_PutX(src, dst) == /\ src # dst /\ dst # Home /\ Sta.UniMsg[src].Cmd = "UNI_GetX" @@ -631,11 +613,13 @@ ABS_NI_Local_Get_Put == ELSE [Sta EXCEPT !.Dir.HeadVld = TRUE, !.Dir.HeadPtr = Other] /\ UNCHANGED Home -ABS_NI_Remote_Get_Nak_src(dst) == +\* Abstract remote NAK, source side (merges the former ABS_NI_Remote_Get_Nak_src +\* / ABS_NI_Remote_GetX_Nak_src; see FlashWithMutexEquiv.tla). +ABS_NI_Remote_Nak_src(dst) == /\ Sta.Env_o /\ dst # Home /\ Sta.Proc[dst].CacheState # "CACHE_E" /\ Sta.Dir.Pending /\ ~Sta.Dir.Local - /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_Get" + /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd \in {"UNI_Get", "UNI_GetX"} /\ Sta' = [Sta EXCEPT !.NakcMsg.Cmd = "NAKC_Nakc", !.FwdCmd = "UNI_None", !.FwdSrc = Other] /\ UNCHANGED Home @@ -652,10 +636,12 @@ ABS_NI_Remote_Get_Nak_dst(src) == !.FwdSrc = src] /\ UNCHANGED Home -ABS_NI_Remote_Get_Nak_src_dst == +\* 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 == /\ Sta.Env_o /\ Sta.Dir.Pending /\ ~Sta.Dir.Local - /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_Get" + /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd \in {"UNI_Get", "UNI_GetX"} /\ Sta' = [Sta EXCEPT !.NakcMsg.Cmd = "NAKC_Nakc", !.FwdCmd = "UNI_None", !.FwdSrc = Other] /\ UNCHANGED Home @@ -756,14 +742,6 @@ ABS_NI_Local_GetX_PutX == ELSE localI(branch3base) /\ UNCHANGED Home -ABS_NI_Remote_GetX_Nak_src(dst) == - /\ Sta.Env_o /\ dst # Home - /\ Sta.Proc[dst].CacheState # "CACHE_E" - /\ Sta.Dir.Pending /\ ~Sta.Dir.Local - /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_GetX" - /\ Sta' = [Sta EXCEPT !.NakcMsg.Cmd = "NAKC_Nakc", !.FwdCmd = "UNI_None", !.FwdSrc = Other] - /\ UNCHANGED Home - ABS_NI_Remote_GetX_Nak_dst(src) == /\ Sta.Env_o /\ Sta.UniMsg[src].Cmd = "UNI_GetX" /\ Sta.UniMsg[src].Proc = Other @@ -777,13 +755,6 @@ ABS_NI_Remote_GetX_Nak_dst(src) == !.FwdSrc = src] /\ UNCHANGED Home -ABS_NI_Remote_GetX_Nak_src_dst == - /\ Sta.Env_o - /\ Sta.Dir.Pending /\ ~Sta.Dir.Local - /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_GetX" - /\ Sta' = [Sta EXCEPT !.NakcMsg.Cmd = "NAKC_Nakc", !.FwdCmd = "UNI_None", !.FwdSrc = Other] - /\ UNCHANGED Home - ABS_NI_Remote_GetX_PutX_src(dst) == /\ Sta.Env_o /\ dst # Home /\ Sta.Proc[dst].CacheState = "CACHE_E" @@ -866,21 +837,22 @@ Next == \/ \E src \in NODE, data \in DATA : Store(src, data) \/ \E data \in DATA : ABS_Store(data) \/ \E src \in NODE : - \/ PI_Remote_Get(src) \/ PI_Remote_GetX(src) + \/ \E c \in ReqCmd : PI_Remote(src, c) \/ PI_Remote_Replace(src) \/ NI_Local_Get_Nak(src) \/ NI_Local_Get_Get(src) \/ NI_Local_Get_Put(src) \/ NI_Local_GetX_Nak(src) \/ NI_Local_GetX_GetX(src) \/ NI_Local_GetX_PutX(src) \/ NI_InvAck(src) \/ NI_Replace(src) - \/ ABS_NI_Remote_Get_Nak_src(src) \/ ABS_NI_Remote_Get_Nak_dst(src) + \/ 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_src(src) \/ ABS_NI_Remote_GetX_Nak_dst(src) + \/ ABS_NI_Remote_GetX_Nak_dst(src) \/ ABS_NI_Remote_GetX_PutX_src(src) \/ ABS_NI_Remote_GetX_PutX_dst(src) \/ \E dst \in NODE : \/ PI_Remote_PutX(dst) \/ NI_Nak(dst) \/ NI_Remote_Put(dst) \/ NI_Remote_PutX(dst) \/ NI_Inv(dst) \/ \E src \in NODE, dst \in NODE : - \/ NI_Remote_Get_Nak(src, dst) \/ NI_Remote_Get_Put(src, dst) - \/ NI_Remote_GetX_Nak(src, dst) \/ NI_Remote_GetX_PutX(src, dst) + \/ NI_Remote_Nak(src, dst) \/ NI_Remote_Get_Put(src, dst) + \/ NI_Remote_GetX_PutX(src, dst) \/ PI_Local_Get_Get \/ PI_Local_Get_Put \/ PI_Local_GetX_GetX \/ PI_Local_GetX_PutX \/ PI_Local_PutX \/ PI_Local_Replace @@ -888,9 +860,9 @@ Next == \/ NI_Wb \/ NI_FAck \/ NI_ShWb \/ ABS_PI_Remote_PutX \/ ABS_NI_Local_Get_Get \/ ABS_NI_Local_Get_Put - \/ ABS_NI_Remote_Get_Nak_src_dst \/ ABS_NI_Remote_Get_Put_src_dst + \/ 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_Nak_src_dst \/ ABS_NI_Remote_GetX_PutX_src_dst + \/ ABS_NI_Remote_GetX_PutX_src_dst \/ ABS_NI_InvAck \/ ABS_NI_ShWb Spec == Init /\ [][Next]_vars From 4cbb0966800e62e8c4f09f44110c27ee25410899 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 21 Jul 2026 15:08:28 -0700 Subject: [PATCH 03/17] Refactor FlashWithMutex specification to separate system and environment steps - Introduced a new `System` definition to encapsulate concrete protocol steps. - Added an `Environment` definition to summarize abstract environment interactions. Prepares the spec for a direct parameterized TLAPS proof by isolating System actions from Environment actions. This refactoring was proved correct with TLAPS; the proof was carried out by Opus 4.8. Co-authored-by: Claude Opus 4.8 Signed-off-by: Markus Alexander Kuppe --- .../FlashProtocol/FlashWithMutex.tla | 22 +++++++++++++------ 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla index d1cc8f63..45401664 100644 --- a/specifications/FlashProtocol/FlashWithMutex.tla +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -833,20 +833,15 @@ ABS_NI_ShWb == ------------------------------------------------------------------------------- -Next == +(* Concrete protocol steps (the modelled nodes and directory). *) +System == \/ \E src \in NODE, data \in DATA : Store(src, data) - \/ \E data \in DATA : ABS_Store(data) \/ \E src \in NODE : \/ \E c \in ReqCmd : PI_Remote(src, c) \/ PI_Remote_Replace(src) \/ NI_Local_Get_Nak(src) \/ NI_Local_Get_Get(src) \/ NI_Local_Get_Put(src) \/ NI_Local_GetX_Nak(src) \/ NI_Local_GetX_GetX(src) \/ NI_Local_GetX_PutX(src) \/ NI_InvAck(src) \/ NI_Replace(src) - \/ 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) \/ \E dst \in NODE : \/ PI_Remote_PutX(dst) \/ NI_Nak(dst) \/ NI_Remote_Put(dst) \/ NI_Remote_PutX(dst) \/ NI_Inv(dst) @@ -858,6 +853,17 @@ Next == \/ PI_Local_PutX \/ PI_Local_Replace \/ 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 Sta.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 @@ -865,6 +871,8 @@ Next == \/ ABS_NI_Remote_GetX_PutX_src_dst \/ ABS_NI_InvAck \/ ABS_NI_ShWb +Next == System \/ Environment + Spec == Init /\ [][Next]_vars ------------------------------------------------------------------------------- From 232961b86a082d4c468978c55ccbb9a2a1a9c990 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 22 Jul 2026 07:49:09 -0700 Subject: [PATCH 04/17] Flatten the monolithic `Sta` state record into top-level variables The translation originally mirrored CMurphi's `Sta : STATE` as a single record variable, updated field-by-field through nested EXCEPT. Decompose it into one top-level variable per field (Proc, Dir, MemData, ...). This is more idiomatic TLA+: each action reads and updates only the variables it touches, UNCHANGED and the type invariant become per-variable, and the state is easier to inspect in traces and tooling. Unlike the preceding System/Environment refactoring, this change was not proved correct with TLAPS. Co-authored-by: Claude Opus 4.8 Signed-off-by: Markus Alexander Kuppe --- .../FlashProtocol/FlashWithMutex.tla | 1265 ++++++++--------- 1 file changed, 624 insertions(+), 641 deletions(-) diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla index 45401664..4c05fe1d 100644 --- a/specifications/FlashProtocol/FlashWithMutex.tla +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -4,10 +4,11 @@ (* 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: a single record variable *) -(* Sta (the Murphi `Sta : STATE`) plus the scalar Home. Enum values use *) -(* the identical Murphi spelling ("CACHE_I", "UNI_Get", ...) and record *) -(* field names are identical, so the equivalence mapping is tiny. *) +(* 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 *) @@ -47,521 +48,504 @@ NodeU == ABS_NODE \cup {Undefined} UniU == UNI_CMD \cup {Undefined} VARIABLES - Home, - Sta + Home, Proc, Dir, MemData, UniMsg, InvMsg, RpMsg, WbMsg, ShWbMsg, NakcMsg, + CurrData, PrevData, LastWrVld, LastWrPtr, PendReqSrc, PendReqCmd, + Collecting, FwdCmd, FwdSrc, LastInvAck, Env_o -vars == <> +vars == <> ------------------------------------------------------------------------------- TypeOK == /\ Home \in NODE - /\ Sta.Proc \in [NODE -> [ProcCmd : NODE_CMD, InvMarked : BOOLEAN, - CacheState : CACHE_STATE, CacheData : DataU]] - /\ Sta.Dir \in [Pending : BOOLEAN, Local : BOOLEAN, Dirty : BOOLEAN, - HeadVld : BOOLEAN, HeadPtr : NodeU, ShrVld : BOOLEAN, - ShrSet : [NODE -> BOOLEAN], InvSet : [NODE -> BOOLEAN]] - /\ Sta.MemData \in DATA - /\ Sta.UniMsg \in [NODE -> [Cmd : UNI_CMD, Proc : NodeU, Data : DataU]] - /\ Sta.InvMsg \in [NODE -> [Cmd : INV_CMD]] - /\ Sta.RpMsg \in [NODE -> [Cmd : RP_CMD]] - /\ Sta.WbMsg \in [Cmd : WB_CMD, Proc : NodeU, Data : DataU] - /\ Sta.ShWbMsg \in [Cmd : SHWB_CMD, Proc : NodeU, Data : DataU] - /\ Sta.NakcMsg \in [Cmd : NAKC_CMD] - /\ Sta.CurrData \in DATA - /\ Sta.PrevData \in DATA - /\ Sta.LastWrVld \in BOOLEAN - /\ Sta.LastWrPtr \in NodeU - /\ Sta.PendReqSrc \in NodeU - /\ Sta.PendReqCmd \in UniU - /\ Sta.Collecting \in BOOLEAN - /\ Sta.FwdCmd \in UNI_CMD - /\ Sta.FwdSrc \in NodeU - /\ Sta.LastInvAck \in NodeU - /\ Sta.Env_o \in BOOLEAN + /\ Proc \in [NODE -> [ProcCmd : NODE_CMD, InvMarked : BOOLEAN, + CacheState : CACHE_STATE, CacheData : DataU]] + /\ Dir \in [Pending : BOOLEAN, Local : BOOLEAN, Dirty : BOOLEAN, + HeadVld : BOOLEAN, HeadPtr : NodeU, ShrVld : BOOLEAN, + ShrSet : [NODE -> BOOLEAN], InvSet : [NODE -> BOOLEAN]] + /\ MemData \in DATA + /\ UniMsg \in [NODE -> [Cmd : UNI_CMD, Proc : NodeU, Data : DataU]] + /\ InvMsg \in [NODE -> [Cmd : INV_CMD]] + /\ RpMsg \in [NODE -> [Cmd : RP_CMD]] + /\ WbMsg \in [Cmd : WB_CMD, Proc : NodeU, Data : DataU] + /\ ShWbMsg \in [Cmd : SHWB_CMD, Proc : NodeU, Data : DataU] + /\ NakcMsg \in [Cmd : NAKC_CMD] + /\ CurrData \in DATA + /\ PrevData \in DATA + /\ LastWrVld \in BOOLEAN + /\ LastWrPtr \in NodeU + /\ PendReqSrc \in NodeU + /\ PendReqCmd \in UniU + /\ Collecting \in BOOLEAN + /\ FwdCmd \in UNI_CMD + /\ FwdSrc \in NodeU + /\ LastInvAck \in NodeU + /\ Env_o \in BOOLEAN ------------------------------------------------------------------------------- Init == \E h \in NODE, d \in DATA : /\ Home = h - /\ Sta = - [ Proc |-> [i \in NODE |-> [ProcCmd |-> "NODE_None", InvMarked |-> FALSE, - CacheState |-> "CACHE_I", CacheData |-> Undefined]], - Dir |-> [Pending |-> FALSE, Local |-> FALSE, Dirty |-> FALSE, - HeadVld |-> FALSE, HeadPtr |-> Undefined, ShrVld |-> FALSE, - ShrSet |-> [i \in NODE |-> FALSE], InvSet |-> [i \in NODE |-> FALSE]], - MemData |-> d, - UniMsg |-> [i \in NODE |-> [Cmd |-> "UNI_None", Proc |-> Undefined, Data |-> Undefined]], - InvMsg |-> [i \in NODE |-> [Cmd |-> "INV_None"]], - RpMsg |-> [i \in NODE |-> [Cmd |-> "RP_None"]], - WbMsg |-> [Cmd |-> "WB_None", Proc |-> Undefined, Data |-> Undefined], - ShWbMsg |-> [Cmd |-> "SHWB_None", Proc |-> Undefined, Data |-> Undefined], - NakcMsg |-> [Cmd |-> "NAKC_None"], - CurrData |-> d, - PrevData |-> d, - LastWrVld |-> FALSE, - LastWrPtr |-> Undefined, - PendReqSrc |-> Undefined, - PendReqCmd |-> Undefined, - Collecting |-> FALSE, - FwdCmd |-> "UNI_None", - FwdSrc |-> Undefined, - LastInvAck |-> Undefined, - Env_o |-> TRUE ] + /\ Proc = [i \in NODE |-> [ProcCmd |-> "NODE_None", InvMarked |-> FALSE, + CacheState |-> "CACHE_I", CacheData |-> Undefined]] + /\ Dir = [Pending |-> FALSE, Local |-> FALSE, Dirty |-> FALSE, + HeadVld |-> FALSE, HeadPtr |-> Undefined, ShrVld |-> FALSE, + ShrSet |-> [i \in NODE |-> FALSE], InvSet |-> [i \in NODE |-> FALSE]] + /\ MemData = d + /\ UniMsg = [i \in NODE |-> [Cmd |-> "UNI_None", Proc |-> Undefined, Data |-> Undefined]] + /\ InvMsg = [i \in NODE |-> [Cmd |-> "INV_None"]] + /\ RpMsg = [i \in NODE |-> [Cmd |-> "RP_None"]] + /\ WbMsg = [Cmd |-> "WB_None", Proc |-> Undefined, Data |-> Undefined] + /\ ShWbMsg = [Cmd |-> "SHWB_None", Proc |-> Undefined, Data |-> Undefined] + /\ NakcMsg = [Cmd |-> "NAKC_None"] + /\ CurrData = d + /\ PrevData = d + /\ LastWrVld = FALSE + /\ LastWrPtr = Undefined + /\ PendReqSrc = Undefined + /\ PendReqCmd = Undefined + /\ Collecting = FALSE + /\ FwdCmd = "UNI_None" + /\ FwdSrc = Undefined + /\ LastInvAck = Undefined + /\ Env_o = TRUE ------------------------------------------------------------------------------- (* Concrete (non-ABS) rules *) ------------------------------------------------------------------------------- Store(src, data) == - /\ Sta.Proc[src].CacheState = "CACHE_E" - /\ Sta' = [Sta EXCEPT !.Proc[src].CacheData = data, - !.CurrData = data, - !.LastWrVld = TRUE, - !.LastWrPtr = src] - /\ UNCHANGED Home + /\ Proc[src].CacheState = "CACHE_E" + /\ Proc' = [Proc EXCEPT ![src].CacheData = data] + /\ CurrData' = data + /\ LastWrVld' = TRUE + /\ LastWrPtr' = src + /\ UNCHANGED <> \* Shared/exclusive request from a remote processor (merges the former -\* PI_Remote_Get / PI_Remote_GetX; see FlashWithMutexEquiv.tla). +\* PI_Remote_Get / PI_Remote_GetX). PI_Remote(src, c) == /\ src # Home - /\ Sta.Proc[src].ProcCmd = "NODE_None" - /\ Sta.Proc[src].CacheState = "CACHE_I" - /\ Sta' = [Sta EXCEPT !.Proc[src].ProcCmd = IF c = "Get" THEN "NODE_Get" ELSE "NODE_GetX", - !.UniMsg[src].Cmd = IF c = "Get" THEN "UNI_Get" ELSE "UNI_GetX", - !.UniMsg[src].Proc = Home, - !.UniMsg[src].Data = Undefined] - /\ UNCHANGED Home + /\ Proc[src].ProcCmd = "NODE_None" + /\ Proc[src].CacheState = "CACHE_I" + /\ Proc' = [Proc EXCEPT ![src].ProcCmd = IF c = "Get" THEN "NODE_Get" ELSE "NODE_GetX"] + /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = IF c = "Get" THEN "UNI_Get" ELSE "UNI_GetX", + ![src].Proc = Home, + ![src].Data = Undefined] + /\ UNCHANGED <> PI_Local_Get_Get == - /\ Sta.Proc[Home].ProcCmd = "NODE_None" - /\ Sta.Proc[Home].CacheState = "CACHE_I" - /\ ~Sta.Dir.Pending /\ Sta.Dir.Dirty - /\ Sta' = [Sta EXCEPT !.Proc[Home].ProcCmd = "NODE_Get", - !.Dir.Pending = TRUE, - !.UniMsg[Home].Cmd = "UNI_Get", - !.UniMsg[Home].Proc = Sta.Dir.HeadPtr, - !.UniMsg[Home].Data = Undefined, - !.FwdCmd = IF Sta.Dir.HeadPtr # Home THEN "UNI_Get" ELSE Sta.FwdCmd, - !.PendReqSrc = Home, - !.PendReqCmd = "UNI_Get", - !.Collecting = FALSE] - /\ UNCHANGED Home + /\ Proc[Home].ProcCmd = "NODE_None" + /\ Proc[Home].CacheState = "CACHE_I" + /\ ~Dir.Pending /\ Dir.Dirty + /\ Proc' = [Proc EXCEPT ![Home].ProcCmd = "NODE_Get"] + /\ Dir' = [Dir EXCEPT !.Pending = TRUE] + /\ UniMsg' = [UniMsg EXCEPT ![Home].Cmd = "UNI_Get", ![Home].Proc = Dir.HeadPtr, + ![Home].Data = Undefined] + /\ FwdCmd' = IF Dir.HeadPtr # Home THEN "UNI_Get" ELSE FwdCmd + /\ PendReqSrc' = Home + /\ PendReqCmd' = "UNI_Get" + /\ Collecting' = FALSE + /\ UNCHANGED <> PI_Local_Get_Put == - /\ Sta.Proc[Home].ProcCmd = "NODE_None" - /\ Sta.Proc[Home].CacheState = "CACHE_I" - /\ ~Sta.Dir.Pending /\ ~Sta.Dir.Dirty - /\ Sta' = [Sta EXCEPT !.Dir.Local = TRUE, - !.Proc[Home].ProcCmd = "NODE_None", - !.Proc[Home].InvMarked = FALSE, - !.Proc[Home].CacheState = - IF Sta.Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", - !.Proc[Home].CacheData = - IF Sta.Proc[Home].InvMarked THEN Undefined ELSE Sta.MemData] - /\ UNCHANGED Home + /\ Proc[Home].ProcCmd = "NODE_None" + /\ Proc[Home].CacheState = "CACHE_I" + /\ ~Dir.Pending /\ ~Dir.Dirty + /\ Dir' = [Dir EXCEPT !.Local = TRUE] + /\ Proc' = [Proc EXCEPT ![Home].ProcCmd = "NODE_None", + ![Home].InvMarked = FALSE, + ![Home].CacheState = IF Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", + ![Home].CacheData = IF Proc[Home].InvMarked THEN Undefined ELSE MemData] + /\ UNCHANGED <> PI_Local_GetX_GetX == - /\ Sta.Proc[Home].ProcCmd = "NODE_None" - /\ Sta.Proc[Home].CacheState \in {"CACHE_I", "CACHE_S"} - /\ ~Sta.Dir.Pending /\ Sta.Dir.Dirty - /\ Sta' = [Sta EXCEPT !.Proc[Home].ProcCmd = "NODE_GetX", - !.Dir.Pending = TRUE, - !.UniMsg[Home].Cmd = "UNI_GetX", - !.UniMsg[Home].Proc = Sta.Dir.HeadPtr, - !.UniMsg[Home].Data = Undefined, - !.FwdCmd = IF Sta.Dir.HeadPtr # Home THEN "UNI_GetX" ELSE Sta.FwdCmd, - !.PendReqSrc = Home, - !.PendReqCmd = "UNI_GetX", - !.Collecting = FALSE] - /\ UNCHANGED Home + /\ Proc[Home].ProcCmd = "NODE_None" + /\ Proc[Home].CacheState \in {"CACHE_I", "CACHE_S"} + /\ ~Dir.Pending /\ Dir.Dirty + /\ Proc' = [Proc EXCEPT ![Home].ProcCmd = "NODE_GetX"] + /\ Dir' = [Dir EXCEPT !.Pending = TRUE] + /\ UniMsg' = [UniMsg EXCEPT ![Home].Cmd = "UNI_GetX", ![Home].Proc = Dir.HeadPtr, + ![Home].Data = Undefined] + /\ FwdCmd' = IF Dir.HeadPtr # Home THEN "UNI_GetX" ELSE FwdCmd + /\ PendReqSrc' = Home + /\ PendReqCmd' = "UNI_GetX" + /\ Collecting' = FALSE + /\ UNCHANGED <> PI_Local_GetX_PutX == - /\ Sta.Proc[Home].ProcCmd = "NODE_None" - /\ Sta.Proc[Home].CacheState \in {"CACHE_I", "CACHE_S"} - /\ ~Sta.Dir.Pending /\ ~Sta.Dir.Dirty + /\ Proc[Home].ProcCmd = "NODE_None" + /\ Proc[Home].CacheState \in {"CACHE_I", "CACHE_S"} + /\ ~Dir.Pending /\ ~Dir.Dirty /\ LET InvP(p) == /\ p # Home - /\ \/ (Sta.Dir.ShrVld /\ Sta.Dir.ShrSet[p]) - \/ (Sta.Dir.HeadVld /\ Sta.Dir.HeadPtr = p) - base == [Sta EXCEPT !.Dir.Local = TRUE, !.Dir.Dirty = TRUE] - withHead == - IF Sta.Dir.HeadVld - THEN [base EXCEPT !.Dir.Pending = TRUE, - !.PendReqSrc = Home, - !.Dir.HeadVld = FALSE, - !.Dir.HeadPtr = Undefined, - !.Dir.ShrVld = FALSE, - !.Dir.ShrSet = [p \in NODE |-> FALSE], - !.Dir.InvSet = [p \in NODE |-> InvP(p)], - !.InvMsg = [p \in NODE |-> [Cmd |-> IF InvP(p) THEN "INV_Inv" ELSE "INV_None"]], - !.Collecting = TRUE, - !.PrevData = Sta.CurrData] - ELSE base - IN Sta' = [withHead EXCEPT !.Proc[Home].ProcCmd = "NODE_None", - !.Proc[Home].InvMarked = FALSE, - !.Proc[Home].CacheState = "CACHE_E", - !.Proc[Home].CacheData = Sta.MemData] - /\ UNCHANGED Home + /\ \/ (Dir.ShrVld /\ Dir.ShrSet[p]) + \/ (Dir.HeadVld /\ Dir.HeadPtr = p) + IN /\ Dir' = IF Dir.HeadVld + THEN [Dir EXCEPT !.Local = TRUE, !.Dirty = TRUE, !.Pending = TRUE, + !.HeadVld = FALSE, !.HeadPtr = Undefined, !.ShrVld = FALSE, + !.ShrSet = [p \in NODE |-> FALSE], + !.InvSet = [p \in NODE |-> InvP(p)]] + ELSE [Dir EXCEPT !.Local = TRUE, !.Dirty = TRUE] + /\ InvMsg' = IF Dir.HeadVld + THEN [p \in NODE |-> [Cmd |-> IF InvP(p) THEN "INV_Inv" ELSE "INV_None"]] + ELSE InvMsg + /\ PendReqSrc' = IF Dir.HeadVld THEN Home ELSE PendReqSrc + /\ Collecting' = IF Dir.HeadVld THEN TRUE ELSE Collecting + /\ PrevData' = IF Dir.HeadVld THEN CurrData ELSE PrevData + /\ Proc' = [Proc EXCEPT ![Home].ProcCmd = "NODE_None", + ![Home].InvMarked = FALSE, + ![Home].CacheState = "CACHE_E", + ![Home].CacheData = MemData] + /\ UNCHANGED <> PI_Remote_PutX(dst) == /\ dst # Home - /\ Sta.Proc[dst].ProcCmd = "NODE_None" - /\ Sta.Proc[dst].CacheState = "CACHE_E" - /\ Sta' = [Sta EXCEPT !.Proc[dst].CacheState = "CACHE_I", - !.Proc[dst].CacheData = Undefined, - !.WbMsg.Cmd = "WB_Wb", - !.WbMsg.Proc = dst, - !.WbMsg.Data = Sta.Proc[dst].CacheData] - /\ UNCHANGED Home + /\ Proc[dst].ProcCmd = "NODE_None" + /\ Proc[dst].CacheState = "CACHE_E" + /\ Proc' = [Proc EXCEPT ![dst].CacheState = "CACHE_I", ![dst].CacheData = Undefined] + /\ WbMsg' = [WbMsg EXCEPT !.Cmd = "WB_Wb", !.Proc = dst, !.Data = Proc[dst].CacheData] + /\ UNCHANGED <> PI_Local_PutX == - /\ Sta.Proc[Home].ProcCmd = "NODE_None" - /\ Sta.Proc[Home].CacheState = "CACHE_E" - /\ Sta' = [Sta EXCEPT !.Proc[Home].CacheState = "CACHE_I", - !.Proc[Home].CacheData = Undefined, - !.Dir.Dirty = FALSE, - !.MemData = Sta.Proc[Home].CacheData, - !.Dir.Local = IF Sta.Dir.Pending THEN Sta.Dir.Local ELSE FALSE] - /\ UNCHANGED Home + /\ Proc[Home].ProcCmd = "NODE_None" + /\ Proc[Home].CacheState = "CACHE_E" + /\ Proc' = [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] + /\ Dir' = [Dir EXCEPT !.Dirty = FALSE, !.Local = IF Dir.Pending THEN Dir.Local ELSE FALSE] + /\ MemData' = Proc[Home].CacheData + /\ UNCHANGED <> PI_Remote_Replace(src) == /\ src # Home - /\ Sta.Proc[src].ProcCmd = "NODE_None" - /\ Sta.Proc[src].CacheState = "CACHE_S" - /\ Sta' = [Sta EXCEPT !.Proc[src].CacheState = "CACHE_I", - !.Proc[src].CacheData = Undefined, - !.RpMsg[src].Cmd = "RP_Replace"] - /\ UNCHANGED Home + /\ Proc[src].ProcCmd = "NODE_None" + /\ Proc[src].CacheState = "CACHE_S" + /\ Proc' = [Proc EXCEPT ![src].CacheState = "CACHE_I", ![src].CacheData = Undefined] + /\ RpMsg' = [RpMsg EXCEPT ![src].Cmd = "RP_Replace"] + /\ UNCHANGED <> PI_Local_Replace == - /\ Sta.Proc[Home].ProcCmd = "NODE_None" - /\ Sta.Proc[Home].CacheState = "CACHE_S" - /\ Sta' = [Sta EXCEPT !.Dir.Local = FALSE, - !.Proc[Home].CacheState = "CACHE_I", - !.Proc[Home].CacheData = Undefined] - /\ UNCHANGED Home + /\ Proc[Home].ProcCmd = "NODE_None" + /\ Proc[Home].CacheState = "CACHE_S" + /\ Dir' = [Dir EXCEPT !.Local = FALSE] + /\ Proc' = [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] + /\ UNCHANGED <> NI_Nak(dst) == - /\ Sta.UniMsg[dst].Cmd = "UNI_Nak" - /\ Sta' = [Sta EXCEPT !.UniMsg[dst].Cmd = "UNI_None", - !.UniMsg[dst].Proc = Undefined, - !.UniMsg[dst].Data = Undefined, - !.Proc[dst].ProcCmd = "NODE_None", - !.Proc[dst].InvMarked = FALSE] - /\ UNCHANGED Home + /\ UniMsg[dst].Cmd = "UNI_Nak" + /\ UniMsg' = [UniMsg EXCEPT ![dst].Cmd = "UNI_None", ![dst].Proc = Undefined, ![dst].Data = Undefined] + /\ Proc' = [Proc EXCEPT ![dst].ProcCmd = "NODE_None", ![dst].InvMarked = FALSE] + /\ UNCHANGED <> NI_Nak_Clear == - /\ Sta.NakcMsg.Cmd = "NAKC_Nakc" - /\ Sta' = [Sta EXCEPT !.NakcMsg.Cmd = "NAKC_None", !.Dir.Pending = FALSE] - /\ UNCHANGED Home + /\ NakcMsg.Cmd = "NAKC_Nakc" + /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_None"] + /\ Dir' = [Dir EXCEPT !.Pending = FALSE] + /\ UNCHANGED <> NI_Local_Get_Nak(src) == /\ src # Home - /\ Sta.UniMsg[src].Cmd = "UNI_Get" - /\ Sta.UniMsg[src].Proc = Home - /\ Sta.RpMsg[src].Cmd # "RP_Replace" - /\ \/ Sta.Dir.Pending - \/ (Sta.Dir.Dirty /\ Sta.Dir.Local /\ Sta.Proc[Home].CacheState # "CACHE_E") - \/ (Sta.Dir.Dirty /\ ~Sta.Dir.Local /\ Sta.Dir.HeadPtr = src) - /\ Sta' = [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_Nak", - !.UniMsg[src].Proc = Home, - !.UniMsg[src].Data = Undefined] - /\ UNCHANGED Home + /\ UniMsg[src].Cmd = "UNI_Get" + /\ UniMsg[src].Proc = Home + /\ RpMsg[src].Cmd # "RP_Replace" + /\ \/ Dir.Pending + \/ (Dir.Dirty /\ Dir.Local /\ Proc[Home].CacheState # "CACHE_E") + \/ (Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr = src) + /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_Nak", ![src].Proc = Home, ![src].Data = Undefined] + /\ UNCHANGED <> NI_Local_Get_Get(src) == /\ src # Home - /\ Sta.UniMsg[src].Cmd = "UNI_Get" - /\ Sta.UniMsg[src].Proc = Home - /\ Sta.RpMsg[src].Cmd # "RP_Replace" - /\ ~Sta.Dir.Pending /\ Sta.Dir.Dirty /\ ~Sta.Dir.Local /\ Sta.Dir.HeadPtr # src - /\ Sta' = [Sta EXCEPT !.Dir.Pending = TRUE, - !.UniMsg[src].Cmd = "UNI_Get", - !.UniMsg[src].Proc = Sta.Dir.HeadPtr, - !.UniMsg[src].Data = Undefined, - !.FwdCmd = IF Sta.Dir.HeadPtr # Home THEN "UNI_Get" ELSE Sta.FwdCmd, - !.PendReqSrc = src, - !.PendReqCmd = "UNI_Get", - !.Collecting = FALSE] - /\ UNCHANGED Home + /\ UniMsg[src].Cmd = "UNI_Get" + /\ UniMsg[src].Proc = Home + /\ RpMsg[src].Cmd # "RP_Replace" + /\ ~Dir.Pending /\ Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr # src + /\ Dir' = [Dir EXCEPT !.Pending = TRUE] + /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_Get", ![src].Proc = Dir.HeadPtr, ![src].Data = Undefined] + /\ FwdCmd' = IF Dir.HeadPtr # Home THEN "UNI_Get" ELSE FwdCmd + /\ PendReqSrc' = src + /\ PendReqCmd' = "UNI_Get" + /\ Collecting' = FALSE + /\ UNCHANGED <> NI_Local_Get_Put(src) == /\ src # Home - /\ Sta.UniMsg[src].Cmd = "UNI_Get" - /\ Sta.UniMsg[src].Proc = Home - /\ Sta.RpMsg[src].Cmd # "RP_Replace" - /\ ~Sta.Dir.Pending - /\ (Sta.Dir.Dirty => (Sta.Dir.Local /\ Sta.Proc[Home].CacheState = "CACHE_E")) - /\ Sta' = - IF Sta.Dir.Dirty - THEN [Sta EXCEPT !.Dir.Dirty = FALSE, !.Dir.HeadVld = TRUE, !.Dir.HeadPtr = src, - !.MemData = Sta.Proc[Home].CacheData, !.Proc[Home].CacheState = "CACHE_S", - !.UniMsg[src].Cmd = "UNI_Put", !.UniMsg[src].Proc = Home, - !.UniMsg[src].Data = Sta.Proc[Home].CacheData] - ELSE LET s1 == IF Sta.Dir.HeadVld - THEN [Sta EXCEPT !.Dir.ShrVld = TRUE, !.Dir.ShrSet[src] = TRUE, - !.Dir.InvSet = [p \in NODE |-> (p = src) \/ Sta.Dir.ShrSet[p]]] - ELSE [Sta EXCEPT !.Dir.HeadVld = TRUE, !.Dir.HeadPtr = src] - IN [s1 EXCEPT !.UniMsg[src].Cmd = "UNI_Put", !.UniMsg[src].Proc = Home, - !.UniMsg[src].Data = Sta.MemData] - /\ UNCHANGED Home + /\ UniMsg[src].Cmd = "UNI_Get" + /\ UniMsg[src].Proc = Home + /\ RpMsg[src].Cmd # "RP_Replace" + /\ ~Dir.Pending + /\ (Dir.Dirty => (Dir.Local /\ Proc[Home].CacheState = "CACHE_E")) + /\ Dir' = IF Dir.Dirty + THEN [Dir EXCEPT !.Dirty = FALSE, !.HeadVld = TRUE, !.HeadPtr = src] + ELSE IF Dir.HeadVld + THEN [Dir EXCEPT !.ShrVld = TRUE, !.ShrSet[src] = TRUE, + !.InvSet = [p \in NODE |-> (p = src) \/ Dir.ShrSet[p]]] + ELSE [Dir EXCEPT !.HeadVld = TRUE, !.HeadPtr = src] + /\ MemData' = IF Dir.Dirty THEN Proc[Home].CacheData ELSE MemData + /\ Proc' = IF Dir.Dirty THEN [Proc EXCEPT ![Home].CacheState = "CACHE_S"] ELSE Proc + /\ UniMsg' = IF Dir.Dirty + THEN [UniMsg EXCEPT ![src].Cmd = "UNI_Put", ![src].Proc = Home, + ![src].Data = Proc[Home].CacheData] + ELSE [UniMsg EXCEPT ![src].Cmd = "UNI_Put", ![src].Proc = Home, + ![src].Data = MemData] + /\ UNCHANGED <> \* Remote NAK of a shared/exclusive request (merges the former -\* NI_Remote_Get_Nak / NI_Remote_GetX_Nak; see FlashWithMutexEquiv.tla). +\* NI_Remote_Get_Nak / NI_Remote_GetX_Nak). NI_Remote_Nak(src, dst) == /\ src # dst /\ dst # Home - /\ Sta.UniMsg[src].Cmd \in {"UNI_Get", "UNI_GetX"} - /\ Sta.UniMsg[src].Proc = dst - /\ Sta.Proc[dst].CacheState # "CACHE_E" - /\ Sta' = [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_Nak", - !.UniMsg[src].Proc = dst, - !.UniMsg[src].Data = Undefined, - !.NakcMsg.Cmd = "NAKC_Nakc", - !.FwdCmd = "UNI_None", - !.FwdSrc = src] - /\ UNCHANGED Home + /\ UniMsg[src].Cmd \in {"UNI_Get", "UNI_GetX"} + /\ UniMsg[src].Proc = dst + /\ Proc[dst].CacheState # "CACHE_E" + /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_Nak", ![src].Proc = dst, ![src].Data = Undefined] + /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_Nakc"] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = src + /\ UNCHANGED <> NI_Remote_Get_Put(src, dst) == /\ src # dst /\ dst # Home - /\ Sta.UniMsg[src].Cmd = "UNI_Get" - /\ Sta.UniMsg[src].Proc = dst - /\ Sta.Proc[dst].CacheState = "CACHE_E" - /\ LET s1 == [Sta EXCEPT !.Proc[dst].CacheState = "CACHE_S", - !.UniMsg[src].Cmd = "UNI_Put", - !.UniMsg[src].Proc = dst, - !.UniMsg[src].Data = Sta.Proc[dst].CacheData, - !.FwdCmd = "UNI_None", - !.FwdSrc = src] - IN Sta' = IF src # Home - THEN [s1 EXCEPT !.ShWbMsg.Cmd = "SHWB_ShWb", - !.ShWbMsg.Proc = src, - !.ShWbMsg.Data = Sta.Proc[dst].CacheData] - ELSE s1 - /\ UNCHANGED Home + /\ UniMsg[src].Cmd = "UNI_Get" + /\ UniMsg[src].Proc = dst + /\ Proc[dst].CacheState = "CACHE_E" + /\ Proc' = [Proc EXCEPT ![dst].CacheState = "CACHE_S"] + /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_Put", ![src].Proc = dst, + ![src].Data = Proc[dst].CacheData] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = src + /\ ShWbMsg' = IF src # Home + THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_ShWb", !.Proc = src, !.Data = Proc[dst].CacheData] + ELSE ShWbMsg + /\ UNCHANGED <> NI_Local_GetX_Nak(src) == /\ src # Home - /\ Sta.UniMsg[src].Cmd = "UNI_GetX" - /\ Sta.UniMsg[src].Proc = Home - /\ \/ Sta.Dir.Pending - \/ (Sta.Dir.Dirty /\ Sta.Dir.Local /\ Sta.Proc[Home].CacheState # "CACHE_E") - \/ (Sta.Dir.Dirty /\ ~Sta.Dir.Local /\ Sta.Dir.HeadPtr = src) - /\ Sta' = [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_Nak", - !.UniMsg[src].Proc = Home, - !.UniMsg[src].Data = Undefined] - /\ UNCHANGED Home + /\ UniMsg[src].Cmd = "UNI_GetX" + /\ UniMsg[src].Proc = Home + /\ \/ Dir.Pending + \/ (Dir.Dirty /\ Dir.Local /\ Proc[Home].CacheState # "CACHE_E") + \/ (Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr = src) + /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_Nak", ![src].Proc = Home, ![src].Data = Undefined] + /\ UNCHANGED <> NI_Local_GetX_GetX(src) == /\ src # Home - /\ Sta.UniMsg[src].Cmd = "UNI_GetX" - /\ Sta.UniMsg[src].Proc = Home - /\ ~Sta.Dir.Pending /\ Sta.Dir.Dirty /\ ~Sta.Dir.Local /\ Sta.Dir.HeadPtr # src - /\ Sta' = [Sta EXCEPT !.Dir.Pending = TRUE, - !.UniMsg[src].Cmd = "UNI_GetX", - !.UniMsg[src].Proc = Sta.Dir.HeadPtr, - !.UniMsg[src].Data = Undefined, - !.FwdCmd = IF Sta.Dir.HeadPtr # Home THEN "UNI_GetX" ELSE Sta.FwdCmd, - !.PendReqSrc = src, - !.PendReqCmd = "UNI_GetX", - !.Collecting = FALSE] - /\ UNCHANGED Home + /\ UniMsg[src].Cmd = "UNI_GetX" + /\ UniMsg[src].Proc = Home + /\ ~Dir.Pending /\ Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr # src + /\ Dir' = [Dir EXCEPT !.Pending = TRUE] + /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_GetX", ![src].Proc = Dir.HeadPtr, ![src].Data = Undefined] + /\ FwdCmd' = IF Dir.HeadPtr # Home THEN "UNI_GetX" ELSE FwdCmd + /\ PendReqSrc' = src + /\ PendReqCmd' = "UNI_GetX" + /\ Collecting' = FALSE + /\ UNCHANGED <> NI_Local_GetX_PutX(src) == /\ src # Home - /\ Sta.UniMsg[src].Cmd = "UNI_GetX" - /\ Sta.UniMsg[src].Proc = Home - /\ ~Sta.Dir.Pending - /\ (Sta.Dir.Dirty => (Sta.Dir.Local /\ Sta.Proc[Home].CacheState = "CACHE_E")) + /\ UniMsg[src].Cmd = "UNI_GetX" + /\ UniMsg[src].Proc = Home + /\ ~Dir.Pending + /\ (Dir.Dirty => (Dir.Local /\ Proc[Home].CacheState = "CACHE_E")) /\ LET Cond3(p) == /\ p # Home /\ p # src - /\ \/ (Sta.Dir.ShrVld /\ Sta.Dir.ShrSet[p]) - \/ (Sta.Dir.HeadVld /\ Sta.Dir.HeadPtr = p) - localI(st) == - IF Sta.Dir.Local - THEN [st EXCEPT !.Proc[Home].CacheState = "CACHE_I", - !.Proc[Home].CacheData = Undefined, - !.Proc[Home].InvMarked = - IF Sta.Proc[Home].ProcCmd = "NODE_Get" - THEN TRUE ELSE Sta.Proc[Home].InvMarked] - ELSE st - branch1 == - [Sta EXCEPT !.Dir.Local = FALSE, !.Dir.Dirty = TRUE, !.Dir.HeadVld = TRUE, - !.Dir.HeadPtr = src, !.Dir.ShrVld = FALSE, - !.Dir.ShrSet = [p \in NODE |-> FALSE], - !.Dir.InvSet = [p \in NODE |-> FALSE], - !.UniMsg[src].Cmd = "UNI_PutX", !.UniMsg[src].Proc = Home, - !.UniMsg[src].Data = Sta.Proc[Home].CacheData, - !.Proc[Home].CacheState = "CACHE_I", - !.Proc[Home].CacheData = Undefined] - branch2base == - [Sta EXCEPT !.Dir.Local = FALSE, !.Dir.Dirty = TRUE, !.Dir.HeadVld = TRUE, - !.Dir.HeadPtr = src, !.Dir.ShrVld = FALSE, - !.Dir.ShrSet = [p \in NODE |-> FALSE], - !.Dir.InvSet = [p \in NODE |-> FALSE], - !.UniMsg[src].Cmd = "UNI_PutX", !.UniMsg[src].Proc = Home, - !.UniMsg[src].Data = Sta.MemData, - !.Proc[Home].CacheState = "CACHE_I", - !.Proc[Home].CacheData = Undefined] - branch3base == - [Sta EXCEPT !.Dir.Pending = TRUE, !.Dir.Local = FALSE, !.Dir.Dirty = TRUE, - !.Dir.HeadVld = TRUE, !.Dir.HeadPtr = src, !.Dir.ShrVld = FALSE, - !.Dir.ShrSet = [p \in NODE |-> FALSE], - !.Dir.InvSet = [p \in NODE |-> Cond3(p)], - !.InvMsg = [p \in NODE |-> [Cmd |-> IF Cond3(p) THEN "INV_Inv" ELSE "INV_None"]], - !.UniMsg[src].Cmd = "UNI_PutX", !.UniMsg[src].Proc = Home, - !.UniMsg[src].Data = Sta.MemData, - !.PendReqSrc = src, !.PendReqCmd = "UNI_GetX", - !.Collecting = TRUE, !.PrevData = Sta.CurrData] - elsifCond == - Sta.Dir.HeadVld => (Sta.Dir.HeadPtr = src - /\ \A p \in NODE : p # src => ~Sta.Dir.ShrSet[p]) - IN Sta' = IF Sta.Dir.Dirty THEN branch1 - ELSE IF elsifCond THEN localI(branch2base) - ELSE localI(branch3base) - /\ UNCHANGED Home + /\ \/ (Dir.ShrVld /\ Dir.ShrSet[p]) + \/ (Dir.HeadVld /\ Dir.HeadPtr = p) + elsifCond == Dir.HeadVld => (Dir.HeadPtr = src + /\ \A p \in NODE : p # src => ~Dir.ShrSet[p]) + ProcLocalI == [Proc EXCEPT ![Home].CacheState = "CACHE_I", + ![Home].CacheData = Undefined, + ![Home].InvMarked = + IF Proc[Home].ProcCmd = "NODE_Get" + THEN TRUE ELSE Proc[Home].InvMarked] + commonDir == [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, + !.HeadPtr = src, !.ShrVld = FALSE, + !.ShrSet = [p \in NODE |-> FALSE], + !.InvSet = [p \in NODE |-> FALSE]] + branch3Dir == [Dir EXCEPT !.Pending = TRUE, !.Local = FALSE, !.Dirty = TRUE, + !.HeadVld = TRUE, !.HeadPtr = src, !.ShrVld = FALSE, + !.ShrSet = [p \in NODE |-> FALSE], + !.InvSet = [p \in NODE |-> Cond3(p)]] + IN /\ Dir' = IF Dir.Dirty \/ elsifCond THEN commonDir ELSE branch3Dir + /\ Proc' = IF Dir.Dirty + THEN [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] + ELSE IF Dir.Local THEN ProcLocalI ELSE Proc + /\ UniMsg' = IF Dir.Dirty + THEN [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = Home, + ![src].Data = Proc[Home].CacheData] + ELSE [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = Home, + ![src].Data = MemData] + /\ InvMsg' = IF Dir.Dirty \/ elsifCond THEN InvMsg + ELSE [p \in NODE |-> [Cmd |-> IF Cond3(p) THEN "INV_Inv" ELSE "INV_None"]] + /\ PendReqSrc' = IF Dir.Dirty \/ elsifCond THEN PendReqSrc ELSE src + /\ PendReqCmd' = IF Dir.Dirty \/ elsifCond THEN PendReqCmd ELSE "UNI_GetX" + /\ Collecting' = IF Dir.Dirty \/ elsifCond THEN Collecting ELSE TRUE + /\ PrevData' = IF Dir.Dirty \/ elsifCond THEN PrevData ELSE CurrData + /\ UNCHANGED <> NI_Remote_GetX_PutX(src, dst) == /\ src # dst /\ dst # Home - /\ Sta.UniMsg[src].Cmd = "UNI_GetX" - /\ Sta.UniMsg[src].Proc = dst - /\ Sta.Proc[dst].CacheState = "CACHE_E" - /\ LET s1 == [Sta EXCEPT !.Proc[dst].CacheState = "CACHE_I", - !.Proc[dst].CacheData = Undefined, - !.UniMsg[src].Cmd = "UNI_PutX", - !.UniMsg[src].Proc = dst, - !.UniMsg[src].Data = Sta.Proc[dst].CacheData, - !.FwdCmd = "UNI_None", - !.FwdSrc = src] - IN Sta' = IF src # Home - THEN [s1 EXCEPT !.ShWbMsg.Cmd = "SHWB_FAck", - !.ShWbMsg.Proc = src, - !.ShWbMsg.Data = Undefined] - ELSE s1 - /\ UNCHANGED Home + /\ UniMsg[src].Cmd = "UNI_GetX" + /\ UniMsg[src].Proc = dst + /\ Proc[dst].CacheState = "CACHE_E" + /\ Proc' = [Proc EXCEPT ![dst].CacheState = "CACHE_I", ![dst].CacheData = Undefined] + /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = dst, + ![src].Data = Proc[dst].CacheData] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = src + /\ ShWbMsg' = IF src # Home + THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_FAck", !.Proc = src, !.Data = Undefined] + ELSE ShWbMsg + /\ UNCHANGED <> NI_Local_Put == - /\ Sta.UniMsg[Home].Cmd = "UNI_Put" - /\ Sta' = [Sta EXCEPT !.UniMsg[Home].Cmd = "UNI_None", - !.UniMsg[Home].Proc = Undefined, - !.UniMsg[Home].Data = Undefined, - !.Dir.Pending = FALSE, - !.Dir.Dirty = FALSE, - !.Dir.Local = TRUE, - !.MemData = Sta.UniMsg[Home].Data, - !.Proc[Home].ProcCmd = "NODE_None", - !.Proc[Home].InvMarked = FALSE, - !.Proc[Home].CacheState = - IF Sta.Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", - !.Proc[Home].CacheData = - IF Sta.Proc[Home].InvMarked THEN Undefined ELSE Sta.UniMsg[Home].Data] - /\ UNCHANGED Home + /\ UniMsg[Home].Cmd = "UNI_Put" + /\ UniMsg' = [UniMsg EXCEPT ![Home].Cmd = "UNI_None", ![Home].Proc = Undefined, ![Home].Data = Undefined] + /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.Dirty = FALSE, !.Local = TRUE] + /\ MemData' = UniMsg[Home].Data + /\ Proc' = [Proc EXCEPT ![Home].ProcCmd = "NODE_None", + ![Home].InvMarked = FALSE, + ![Home].CacheState = IF Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", + ![Home].CacheData = IF Proc[Home].InvMarked THEN Undefined ELSE UniMsg[Home].Data] + /\ UNCHANGED <> NI_Remote_Put(dst) == /\ dst # Home - /\ Sta.UniMsg[dst].Cmd = "UNI_Put" - /\ Sta' = [Sta EXCEPT !.UniMsg[dst].Cmd = "UNI_None", - !.UniMsg[dst].Proc = Undefined, - !.UniMsg[dst].Data = Undefined, - !.Proc[dst].ProcCmd = "NODE_None", - !.Proc[dst].InvMarked = FALSE, - !.Proc[dst].CacheState = - IF Sta.Proc[dst].InvMarked THEN "CACHE_I" ELSE "CACHE_S", - !.Proc[dst].CacheData = - IF Sta.Proc[dst].InvMarked THEN Undefined ELSE Sta.UniMsg[dst].Data] - /\ UNCHANGED Home + /\ UniMsg[dst].Cmd = "UNI_Put" + /\ UniMsg' = [UniMsg EXCEPT ![dst].Cmd = "UNI_None", ![dst].Proc = Undefined, ![dst].Data = Undefined] + /\ Proc' = [Proc EXCEPT ![dst].ProcCmd = "NODE_None", + ![dst].InvMarked = FALSE, + ![dst].CacheState = IF Proc[dst].InvMarked THEN "CACHE_I" ELSE "CACHE_S", + ![dst].CacheData = IF Proc[dst].InvMarked THEN Undefined ELSE UniMsg[dst].Data] + /\ UNCHANGED <> NI_Local_PutXAcksDone == - /\ Sta.UniMsg[Home].Cmd = "UNI_PutX" - /\ Sta' = [Sta EXCEPT !.UniMsg[Home].Cmd = "UNI_None", - !.UniMsg[Home].Proc = Undefined, - !.UniMsg[Home].Data = Undefined, - !.Dir.Pending = FALSE, - !.Dir.Local = TRUE, - !.Dir.HeadVld = FALSE, - !.Dir.HeadPtr = Undefined, - !.Proc[Home].ProcCmd = "NODE_None", - !.Proc[Home].InvMarked = FALSE, - !.Proc[Home].CacheState = "CACHE_E", - !.Proc[Home].CacheData = Sta.UniMsg[Home].Data] - /\ UNCHANGED Home + /\ UniMsg[Home].Cmd = "UNI_PutX" + /\ UniMsg' = [UniMsg EXCEPT ![Home].Cmd = "UNI_None", ![Home].Proc = Undefined, ![Home].Data = Undefined] + /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.Local = TRUE, !.HeadVld = FALSE, !.HeadPtr = Undefined] + /\ Proc' = [Proc EXCEPT ![Home].ProcCmd = "NODE_None", + ![Home].InvMarked = FALSE, + ![Home].CacheState = "CACHE_E", + ![Home].CacheData = UniMsg[Home].Data] + /\ UNCHANGED <> NI_Remote_PutX(dst) == /\ dst # Home - /\ Sta.UniMsg[dst].Cmd = "UNI_PutX" - /\ Sta.Proc[dst].ProcCmd = "NODE_GetX" - /\ Sta' = [Sta EXCEPT !.UniMsg[dst].Cmd = "UNI_None", - !.UniMsg[dst].Proc = Undefined, - !.UniMsg[dst].Data = Undefined, - !.Proc[dst].ProcCmd = "NODE_None", - !.Proc[dst].InvMarked = FALSE, - !.Proc[dst].CacheState = "CACHE_E", - !.Proc[dst].CacheData = Sta.UniMsg[dst].Data] - /\ UNCHANGED Home + /\ UniMsg[dst].Cmd = "UNI_PutX" + /\ Proc[dst].ProcCmd = "NODE_GetX" + /\ UniMsg' = [UniMsg EXCEPT ![dst].Cmd = "UNI_None", ![dst].Proc = Undefined, ![dst].Data = Undefined] + /\ Proc' = [Proc EXCEPT ![dst].ProcCmd = "NODE_None", + ![dst].InvMarked = FALSE, + ![dst].CacheState = "CACHE_E", + ![dst].CacheData = UniMsg[dst].Data] + /\ UNCHANGED <> NI_Inv(dst) == /\ dst # Home - /\ Sta.InvMsg[dst].Cmd = "INV_Inv" - /\ Sta' = [Sta EXCEPT !.InvMsg[dst].Cmd = "INV_InvAck", - !.Proc[dst].CacheState = "CACHE_I", - !.Proc[dst].CacheData = Undefined, - !.Proc[dst].InvMarked = - IF Sta.Proc[dst].ProcCmd = "NODE_Get" THEN TRUE - ELSE Sta.Proc[dst].InvMarked] - /\ UNCHANGED Home + /\ InvMsg[dst].Cmd = "INV_Inv" + /\ InvMsg' = [InvMsg EXCEPT ![dst].Cmd = "INV_InvAck"] + /\ Proc' = [Proc EXCEPT ![dst].CacheState = "CACHE_I", + ![dst].CacheData = Undefined, + ![dst].InvMarked = IF Proc[dst].ProcCmd = "NODE_Get" THEN TRUE + ELSE Proc[dst].InvMarked] + /\ UNCHANGED <> NI_InvAck(src) == /\ src # Home - /\ Sta.InvMsg[src].Cmd = "INV_InvAck" - /\ Sta.Dir.Pending /\ Sta.Dir.InvSet[src] - /\ LET s1 == [Sta EXCEPT !.InvMsg[src].Cmd = "INV_None", !.Dir.InvSet[src] = FALSE] - moreAcks == \E p \in NODE : p # src /\ Sta.Dir.InvSet[p] - IN Sta' = IF moreAcks - THEN [s1 EXCEPT !.LastInvAck = src] - ELSE [s1 EXCEPT !.Dir.Pending = FALSE, - !.Dir.Local = IF Sta.Dir.Local /\ ~Sta.Dir.Dirty - THEN FALSE ELSE Sta.Dir.Local, - !.Collecting = FALSE, - !.LastInvAck = src] - /\ UNCHANGED Home + /\ InvMsg[src].Cmd = "INV_InvAck" + /\ Dir.Pending /\ Dir.InvSet[src] + /\ LET moreAcks == \E p \in NODE : p # src /\ Dir.InvSet[p] + IN /\ InvMsg' = [InvMsg EXCEPT ![src].Cmd = "INV_None"] + /\ Dir' = IF moreAcks + THEN [Dir EXCEPT !.InvSet[src] = FALSE] + ELSE [Dir EXCEPT !.InvSet[src] = FALSE, !.Pending = FALSE, + !.Local = IF Dir.Local /\ ~Dir.Dirty THEN FALSE ELSE Dir.Local] + /\ Collecting' = IF moreAcks THEN Collecting ELSE FALSE + /\ LastInvAck' = src + /\ UNCHANGED <> NI_Wb == - /\ Sta.WbMsg.Cmd = "WB_Wb" - /\ Sta' = [Sta EXCEPT !.WbMsg.Cmd = "WB_None", - !.WbMsg.Proc = Undefined, - !.WbMsg.Data = Undefined, - !.Dir.Dirty = FALSE, - !.Dir.HeadVld = FALSE, - !.Dir.HeadPtr = Undefined, - !.MemData = Sta.WbMsg.Data] - /\ UNCHANGED Home + /\ WbMsg.Cmd = "WB_Wb" + /\ WbMsg' = [WbMsg EXCEPT !.Cmd = "WB_None", !.Proc = Undefined, !.Data = Undefined] + /\ Dir' = [Dir EXCEPT !.Dirty = FALSE, !.HeadVld = FALSE, !.HeadPtr = Undefined] + /\ MemData' = WbMsg.Data + /\ UNCHANGED <> NI_FAck == - /\ Sta.ShWbMsg.Cmd = "SHWB_FAck" - /\ Sta' = [Sta EXCEPT !.ShWbMsg.Cmd = "SHWB_None", - !.ShWbMsg.Proc = Undefined, - !.ShWbMsg.Data = Undefined, - !.Dir.Pending = FALSE, - !.Dir.HeadPtr = IF Sta.Dir.Dirty THEN Sta.ShWbMsg.Proc ELSE Sta.Dir.HeadPtr] - /\ UNCHANGED Home + /\ ShWbMsg.Cmd = "SHWB_FAck" + /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_None", !.Proc = Undefined, !.Data = Undefined] + /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.HeadPtr = IF Dir.Dirty THEN ShWbMsg.Proc ELSE Dir.HeadPtr] + /\ UNCHANGED <> NI_ShWb == - /\ Sta.ShWbMsg.Cmd = "SHWB_ShWb" - /\ Sta' = [Sta EXCEPT !.ShWbMsg.Cmd = "SHWB_None", - !.ShWbMsg.Proc = Undefined, - !.ShWbMsg.Data = Undefined, - !.Dir.Pending = FALSE, - !.Dir.Dirty = FALSE, - !.Dir.ShrVld = TRUE, - !.Dir.ShrSet = [p \in NODE |-> (p = Sta.ShWbMsg.Proc) \/ Sta.Dir.ShrSet[p]], - !.Dir.InvSet = [p \in NODE |-> (p = Sta.ShWbMsg.Proc) \/ Sta.Dir.ShrSet[p]], - !.MemData = Sta.ShWbMsg.Data] - /\ UNCHANGED Home + /\ ShWbMsg.Cmd = "SHWB_ShWb" + /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_None", !.Proc = Undefined, !.Data = Undefined] + /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.Dirty = FALSE, !.ShrVld = TRUE, + !.ShrSet = [p \in NODE |-> (p = ShWbMsg.Proc) \/ Dir.ShrSet[p]], + !.InvSet = [p \in NODE |-> (p = ShWbMsg.Proc) \/ Dir.ShrSet[p]]] + /\ MemData' = ShWbMsg.Data + /\ UNCHANGED <> NI_Replace(src) == - /\ Sta.RpMsg[src].Cmd = "RP_Replace" - /\ Sta' = [Sta EXCEPT !.RpMsg[src].Cmd = "RP_None", - !.Dir.ShrSet[src] = IF Sta.Dir.ShrVld THEN FALSE ELSE Sta.Dir.ShrSet[src], - !.Dir.InvSet[src] = IF Sta.Dir.ShrVld THEN FALSE ELSE Sta.Dir.InvSet[src]] - /\ UNCHANGED Home + /\ RpMsg[src].Cmd = "RP_Replace" + /\ RpMsg' = [RpMsg EXCEPT ![src].Cmd = "RP_None"] + /\ Dir' = [Dir EXCEPT !.ShrSet[src] = IF Dir.ShrVld THEN FALSE ELSE Dir.ShrSet[src], + !.InvSet[src] = IF Dir.ShrVld THEN FALSE ELSE Dir.InvSet[src]] + /\ UNCHANGED <> ------------------------------------------------------------------------------- (* ABS_* abstract-environment rules *) @@ -570,266 +554,265 @@ NI_Replace(src) == (* a writeback from the abstract node (Lemma_1 side condition). *) AbsDirtyClean == - /\ Sta.Dir.Dirty - /\ Sta.WbMsg.Cmd # "WB_Wb" - /\ Sta.ShWbMsg.Cmd # "SHWB_ShWb" - /\ \A p \in NODE : Sta.Proc[p].CacheState # "CACHE_E" - /\ Sta.UniMsg[Home].Cmd # "UNI_Put" - /\ \A q \in NODE : Sta.UniMsg[q].Cmd # "UNI_PutX" + /\ 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) == - /\ Sta.Env_o + /\ Env_o /\ AbsDirtyClean - /\ Sta' = [Sta EXCEPT !.CurrData = data, !.LastWrVld = TRUE, !.LastWrPtr = Other] - /\ UNCHANGED Home + /\ CurrData' = data + /\ LastWrVld' = TRUE + /\ LastWrPtr' = Other + /\ UNCHANGED <> ABS_PI_Remote_PutX == - /\ Sta.Env_o + /\ Env_o /\ AbsDirtyClean - /\ Sta' = [Sta EXCEPT !.WbMsg.Cmd = "WB_Wb", !.WbMsg.Proc = Other, !.WbMsg.Data = Sta.CurrData] - /\ UNCHANGED Home + /\ WbMsg' = [WbMsg EXCEPT !.Cmd = "WB_Wb", !.Proc = Other, !.Data = CurrData] + /\ UNCHANGED <> ABS_NI_Local_Get_Get == - /\ Sta.Env_o - /\ ~Sta.Dir.Pending /\ Sta.Dir.Dirty /\ ~Sta.Dir.Local /\ Sta.Dir.HeadPtr # Other - /\ Sta' = [Sta EXCEPT !.Dir.Pending = TRUE, - !.FwdCmd = IF Sta.Dir.HeadPtr # Home THEN "UNI_Get" ELSE Sta.FwdCmd, - !.PendReqSrc = Other, - !.PendReqCmd = "UNI_Get", - !.Collecting = FALSE] - /\ UNCHANGED Home + /\ 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 == - /\ Sta.Env_o - /\ ~Sta.Dir.Pending - /\ (Sta.Dir.Dirty => (Sta.Dir.Local /\ Sta.Proc[Home].CacheState = "CACHE_E")) - /\ Sta' = - IF Sta.Dir.Dirty - THEN [Sta EXCEPT !.Dir.Dirty = FALSE, !.Dir.HeadVld = TRUE, !.Dir.HeadPtr = Other, - !.MemData = Sta.Proc[Home].CacheData, !.Proc[Home].CacheState = "CACHE_S"] - ELSE IF Sta.Dir.HeadVld - THEN [Sta EXCEPT !.Dir.ShrVld = TRUE, - !.Dir.InvSet = [p \in NODE |-> Sta.Dir.ShrSet[p]]] - ELSE [Sta EXCEPT !.Dir.HeadVld = TRUE, !.Dir.HeadPtr = Other] - /\ UNCHANGED Home + /\ 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 = [p \in NODE |-> Dir.ShrSet[p]]] + 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; see FlashWithMutexEquiv.tla). +\* / ABS_NI_Remote_GetX_Nak_src). ABS_NI_Remote_Nak_src(dst) == - /\ Sta.Env_o /\ dst # Home - /\ Sta.Proc[dst].CacheState # "CACHE_E" - /\ Sta.Dir.Pending /\ ~Sta.Dir.Local - /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd \in {"UNI_Get", "UNI_GetX"} - /\ Sta' = [Sta EXCEPT !.NakcMsg.Cmd = "NAKC_Nakc", !.FwdCmd = "UNI_None", !.FwdSrc = Other] - /\ UNCHANGED Home + /\ Env_o /\ dst # Home + /\ Proc[dst].CacheState # "CACHE_E" + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = Other /\ FwdCmd \in {"UNI_Get", "UNI_GetX"} + /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_Nakc"] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = Other + /\ UNCHANGED <> ABS_NI_Remote_Get_Nak_dst(src) == - /\ Sta.Env_o - /\ Sta.UniMsg[src].Cmd = "UNI_Get" /\ Sta.UniMsg[src].Proc = Other - /\ Sta.Dir.Pending /\ ~Sta.Dir.Local - /\ Sta.PendReqSrc = src /\ Sta.FwdCmd = "UNI_Get" - /\ Sta' = [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_Nak", - !.UniMsg[src].Proc = Other, - !.UniMsg[src].Data = Undefined, - !.NakcMsg.Cmd = "NAKC_Nakc", - !.FwdCmd = "UNI_None", - !.FwdSrc = src] - /\ UNCHANGED Home + /\ 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", ![src].Proc = Other, ![src].Data = Undefined] + /\ NakcMsg' = [NakcMsg EXCEPT !.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 == - /\ Sta.Env_o - /\ Sta.Dir.Pending /\ ~Sta.Dir.Local - /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd \in {"UNI_Get", "UNI_GetX"} - /\ Sta' = [Sta EXCEPT !.NakcMsg.Cmd = "NAKC_Nakc", !.FwdCmd = "UNI_None", !.FwdSrc = Other] - /\ UNCHANGED Home + /\ Env_o + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = Other /\ FwdCmd \in {"UNI_Get", "UNI_GetX"} + /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_Nakc"] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = Other + /\ UNCHANGED <> ABS_NI_Remote_Get_Put_src(dst) == - /\ Sta.Env_o /\ dst # Home - /\ Sta.Proc[dst].CacheState = "CACHE_E" - /\ Sta.Dir.Pending /\ ~Sta.Dir.Local - /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_Get" - /\ Sta' = [Sta EXCEPT !.Proc[dst].CacheState = "CACHE_S", - !.ShWbMsg.Cmd = "SHWB_ShWb", - !.ShWbMsg.Proc = Other, - !.ShWbMsg.Data = Sta.Proc[dst].CacheData, - !.FwdCmd = "UNI_None", - !.FwdSrc = Other] - /\ UNCHANGED Home + /\ 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' = [ShWbMsg EXCEPT !.Cmd = "SHWB_ShWb", !.Proc = Other, !.Data = Proc[dst].CacheData] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = Other + /\ UNCHANGED <> ABS_NI_Remote_Get_Put_dst(src) == - /\ Sta.Env_o - /\ Sta.UniMsg[src].Cmd = "UNI_Get" /\ Sta.UniMsg[src].Proc = Other + /\ Env_o + /\ UniMsg[src].Cmd = "UNI_Get" /\ UniMsg[src].Proc = Other /\ AbsDirtyClean - /\ Sta.Dir.Pending /\ ~Sta.Dir.Local - /\ Sta.PendReqSrc = src /\ Sta.FwdCmd = "UNI_Get" - /\ LET s1 == [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_Put", - !.UniMsg[src].Proc = Other, - !.UniMsg[src].Data = Sta.CurrData, - !.FwdCmd = "UNI_None", - !.FwdSrc = src] - IN Sta' = IF src # Home - THEN [s1 EXCEPT !.ShWbMsg.Cmd = "SHWB_ShWb", - !.ShWbMsg.Proc = src, - !.ShWbMsg.Data = Sta.CurrData] - ELSE s1 - /\ UNCHANGED Home + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = src /\ FwdCmd = "UNI_Get" + /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_Put", ![src].Proc = Other, ![src].Data = CurrData] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = src + /\ ShWbMsg' = IF src # Home + THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_ShWb", !.Proc = src, !.Data = CurrData] + ELSE ShWbMsg + /\ UNCHANGED <> ABS_NI_Remote_Get_Put_src_dst == - /\ Sta.Env_o + /\ Env_o /\ AbsDirtyClean - /\ Sta.Dir.Pending /\ ~Sta.Dir.Local - /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_Get" - /\ Sta' = [Sta EXCEPT !.ShWbMsg.Cmd = "SHWB_ShWb", - !.ShWbMsg.Proc = Other, - !.ShWbMsg.Data = Sta.CurrData, - !.FwdCmd = "UNI_None", - !.FwdSrc = Other] - /\ UNCHANGED Home + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = Other /\ FwdCmd = "UNI_Get" + /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_ShWb", !.Proc = Other, !.Data = CurrData] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = Other + /\ UNCHANGED <> ABS_NI_Local_GetX_GetX == - /\ Sta.Env_o - /\ ~Sta.Dir.Pending /\ Sta.Dir.Dirty /\ ~Sta.Dir.Local /\ Sta.Dir.HeadPtr # Other - /\ Sta' = [Sta EXCEPT !.Dir.Pending = TRUE, - !.FwdCmd = IF Sta.Dir.HeadPtr # Home THEN "UNI_GetX" ELSE Sta.FwdCmd, - !.PendReqSrc = Other, - !.PendReqCmd = "UNI_GetX", - !.Collecting = FALSE] - /\ UNCHANGED Home + /\ 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 <> ABS_NI_Local_GetX_PutX == - /\ Sta.Env_o - /\ ~Sta.Dir.Pending - /\ (Sta.Dir.Dirty => (Sta.Dir.Local /\ Sta.Proc[Home].CacheState = "CACHE_E")) + /\ Env_o + /\ ~Dir.Pending + /\ (Dir.Dirty => (Dir.Local /\ Proc[Home].CacheState = "CACHE_E")) /\ LET Cond3(p) == /\ p # Home - /\ \/ (Sta.Dir.ShrVld /\ Sta.Dir.ShrSet[p]) - \/ (Sta.Dir.HeadVld /\ Sta.Dir.HeadPtr = p) - localI(st) == - IF Sta.Dir.Local - THEN [st EXCEPT !.Proc[Home].CacheState = "CACHE_I", - !.Proc[Home].CacheData = Undefined, - !.Proc[Home].InvMarked = - IF Sta.Proc[Home].ProcCmd = "NODE_Get" - THEN TRUE ELSE Sta.Proc[Home].InvMarked] - ELSE st - branch1 == - [Sta EXCEPT !.Dir.Local = FALSE, !.Dir.Dirty = TRUE, !.Dir.HeadVld = TRUE, - !.Dir.HeadPtr = Other, !.Dir.ShrVld = FALSE, - !.Dir.ShrSet = [p \in NODE |-> FALSE], - !.Dir.InvSet = [p \in NODE |-> FALSE], - !.Proc[Home].CacheState = "CACHE_I", - !.Proc[Home].CacheData = Undefined] - branch2base == - [Sta EXCEPT !.Dir.Local = FALSE, !.Dir.Dirty = TRUE, !.Dir.HeadVld = TRUE, - !.Dir.HeadPtr = Other, !.Dir.ShrVld = FALSE, - !.Dir.ShrSet = [p \in NODE |-> FALSE], - !.Dir.InvSet = [p \in NODE |-> FALSE], - !.Proc[Home].CacheState = "CACHE_I", - !.Proc[Home].CacheData = Undefined] - branch3base == - [Sta EXCEPT !.Dir.Pending = TRUE, !.Dir.Local = FALSE, !.Dir.Dirty = TRUE, - !.Dir.HeadVld = TRUE, !.Dir.HeadPtr = Other, !.Dir.ShrVld = FALSE, - !.Dir.ShrSet = [p \in NODE |-> FALSE], - !.Dir.InvSet = [p \in NODE |-> Cond3(p)], - !.InvMsg = [p \in NODE |-> [Cmd |-> IF Cond3(p) THEN "INV_Inv" ELSE "INV_None"]], - !.PendReqSrc = Other, !.PendReqCmd = "UNI_GetX", - !.Collecting = TRUE, !.PrevData = Sta.CurrData] - elsifCond == - Sta.Dir.HeadVld => (Sta.Dir.HeadPtr = Other /\ \A p \in NODE : ~Sta.Dir.ShrSet[p]) - IN Sta' = IF Sta.Dir.Dirty THEN branch1 - ELSE IF elsifCond THEN localI(branch2base) - ELSE localI(branch3base) - /\ UNCHANGED Home + /\ \/ (Dir.ShrVld /\ Dir.ShrSet[p]) + \/ (Dir.HeadVld /\ Dir.HeadPtr = p) + elsifCond == Dir.HeadVld => (Dir.HeadPtr = Other /\ \A p \in NODE : ~Dir.ShrSet[p]) + ProcLocalI == [Proc EXCEPT ![Home].CacheState = "CACHE_I", + ![Home].CacheData = Undefined, + ![Home].InvMarked = + IF Proc[Home].ProcCmd = "NODE_Get" + THEN TRUE ELSE Proc[Home].InvMarked] + ProcII == [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] + commonDir == [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, + !.HeadPtr = Other, !.ShrVld = FALSE, + !.ShrSet = [p \in NODE |-> FALSE], + !.InvSet = [p \in NODE |-> FALSE]] + branch3Dir == [Dir EXCEPT !.Pending = TRUE, !.Local = FALSE, !.Dirty = TRUE, + !.HeadVld = TRUE, !.HeadPtr = Other, !.ShrVld = FALSE, + !.ShrSet = [p \in NODE |-> FALSE], + !.InvSet = [p \in NODE |-> Cond3(p)]] + IN /\ Dir' = IF Dir.Dirty \/ elsifCond THEN commonDir ELSE branch3Dir + /\ Proc' = IF Dir.Dirty THEN ProcII + ELSE IF Dir.Local THEN ProcLocalI + ELSE IF elsifCond THEN ProcII ELSE Proc + /\ InvMsg' = IF Dir.Dirty \/ elsifCond THEN InvMsg + ELSE [p \in NODE |-> [Cmd |-> IF Cond3(p) THEN "INV_Inv" ELSE "INV_None"]] + /\ PendReqSrc' = IF Dir.Dirty \/ elsifCond THEN PendReqSrc ELSE Other + /\ PendReqCmd' = IF Dir.Dirty \/ elsifCond THEN PendReqCmd ELSE "UNI_GetX" + /\ Collecting' = IF Dir.Dirty \/ elsifCond THEN Collecting ELSE TRUE + /\ PrevData' = IF Dir.Dirty \/ elsifCond THEN PrevData ELSE CurrData + /\ UNCHANGED <> ABS_NI_Remote_GetX_Nak_dst(src) == - /\ Sta.Env_o - /\ Sta.UniMsg[src].Cmd = "UNI_GetX" /\ Sta.UniMsg[src].Proc = Other - /\ Sta.Dir.Pending /\ ~Sta.Dir.Local - /\ Sta.PendReqSrc = src /\ Sta.FwdCmd = "UNI_GetX" - /\ Sta' = [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_Nak", - !.UniMsg[src].Proc = Other, - !.UniMsg[src].Data = Undefined, - !.NakcMsg.Cmd = "NAKC_Nakc", - !.FwdCmd = "UNI_None", - !.FwdSrc = src] - /\ UNCHANGED Home + /\ 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", ![src].Proc = Other, ![src].Data = Undefined] + /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_Nakc"] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = src + /\ UNCHANGED <> ABS_NI_Remote_GetX_PutX_src(dst) == - /\ Sta.Env_o /\ dst # Home - /\ Sta.Proc[dst].CacheState = "CACHE_E" - /\ Sta.Dir.Pending /\ ~Sta.Dir.Local - /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_GetX" - /\ Sta' = [Sta EXCEPT !.Proc[dst].CacheState = "CACHE_I", - !.Proc[dst].CacheData = Undefined, - !.ShWbMsg.Cmd = "SHWB_FAck", - !.ShWbMsg.Proc = Other, - !.ShWbMsg.Data = Undefined, - !.FwdCmd = "UNI_None", - !.FwdSrc = Other] - /\ UNCHANGED Home + /\ 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' = [ShWbMsg EXCEPT !.Cmd = "SHWB_FAck", !.Proc = Other, !.Data = Undefined] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = Other + /\ UNCHANGED <> ABS_NI_Remote_GetX_PutX_dst(src) == - /\ Sta.Env_o - /\ Sta.UniMsg[src].Cmd = "UNI_GetX" /\ Sta.UniMsg[src].Proc = Other + /\ Env_o + /\ UniMsg[src].Cmd = "UNI_GetX" /\ UniMsg[src].Proc = Other /\ AbsDirtyClean - /\ Sta.Dir.Pending /\ ~Sta.Dir.Local - /\ Sta.PendReqSrc = src /\ Sta.FwdCmd = "UNI_GetX" - /\ LET s1 == [Sta EXCEPT !.UniMsg[src].Cmd = "UNI_PutX", - !.UniMsg[src].Proc = Other, - !.UniMsg[src].Data = Sta.CurrData, - !.FwdCmd = "UNI_None", - !.FwdSrc = src] - IN Sta' = IF src # Home - THEN [s1 EXCEPT !.ShWbMsg.Cmd = "SHWB_FAck", - !.ShWbMsg.Proc = src, - !.ShWbMsg.Data = Undefined] - ELSE s1 - /\ UNCHANGED Home + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = src /\ FwdCmd = "UNI_GetX" + /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = Other, ![src].Data = CurrData] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = src + /\ ShWbMsg' = IF src # Home + THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_FAck", !.Proc = src, !.Data = Undefined] + ELSE ShWbMsg + /\ UNCHANGED <> ABS_NI_Remote_GetX_PutX_src_dst == - /\ Sta.Env_o + /\ Env_o /\ AbsDirtyClean - /\ Sta.Dir.Pending /\ ~Sta.Dir.Local - /\ Sta.PendReqSrc = Other /\ Sta.FwdCmd = "UNI_GetX" - /\ Sta' = [Sta EXCEPT !.ShWbMsg.Cmd = "SHWB_FAck", - !.ShWbMsg.Proc = Other, - !.ShWbMsg.Data = Undefined, - !.FwdCmd = "UNI_None", - !.FwdSrc = Other] - /\ UNCHANGED Home + /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = Other /\ FwdCmd = "UNI_GetX" + /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_FAck", !.Proc = Other, !.Data = Undefined] + /\ FwdCmd' = "UNI_None" + /\ FwdSrc' = Other + /\ UNCHANGED <> ABS_NI_InvAck == - /\ Sta.Env_o - /\ Sta.Dir.Pending /\ Sta.Collecting - /\ Sta.NakcMsg.Cmd = "NAKC_None" /\ Sta.ShWbMsg.Cmd = "SHWB_None" + /\ Env_o + /\ Dir.Pending /\ Collecting + /\ NakcMsg.Cmd = "NAKC_None" /\ ShWbMsg.Cmd = "SHWB_None" /\ \A q \in NODE : - /\ ((Sta.UniMsg[q].Cmd = "UNI_Get" \/ Sta.UniMsg[q].Cmd = "UNI_GetX") - => Sta.UniMsg[q].Proc = Home) - /\ (Sta.UniMsg[q].Cmd = "UNI_PutX" - => (Sta.UniMsg[q].Proc = Home /\ Sta.PendReqSrc = q)) - /\ LET moreAcks == \E p \in NODE : Sta.Dir.InvSet[p] - IN Sta' = IF moreAcks - THEN [Sta EXCEPT !.LastInvAck = Other] - ELSE [Sta EXCEPT !.Dir.Pending = FALSE, - !.Dir.Local = IF Sta.Dir.Local /\ ~Sta.Dir.Dirty - THEN FALSE ELSE Sta.Dir.Local, - !.Collecting = FALSE, - !.LastInvAck = Other] - /\ UNCHANGED Home + /\ ((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)) + /\ LET moreAcks == \E p \in NODE : Dir.InvSet[p] + IN /\ Dir' = IF moreAcks THEN Dir + ELSE [Dir EXCEPT !.Pending = FALSE, + !.Local = IF Dir.Local /\ ~Dir.Dirty THEN FALSE ELSE Dir.Local] + /\ Collecting' = IF moreAcks THEN Collecting ELSE FALSE + /\ LastInvAck' = Other + /\ UNCHANGED <> ABS_NI_ShWb == - /\ Sta.Env_o - /\ Sta.ShWbMsg.Cmd = "SHWB_ShWb" /\ Sta.ShWbMsg.Proc = Other - /\ Sta' = [Sta EXCEPT !.ShWbMsg.Cmd = "SHWB_None", - !.ShWbMsg.Proc = Undefined, - !.ShWbMsg.Data = Undefined, - !.Dir.Pending = FALSE, - !.Dir.Dirty = FALSE, - !.Dir.ShrVld = TRUE, - !.Dir.InvSet = [p \in NODE |-> Sta.Dir.ShrSet[p]], - !.MemData = Sta.ShWbMsg.Data] - /\ UNCHANGED Home + /\ Env_o + /\ ShWbMsg.Cmd = "SHWB_ShWb" /\ ShWbMsg.Proc = Other + /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_None", !.Proc = Undefined, !.Data = Undefined] + /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.Dirty = FALSE, !.ShrVld = TRUE, + !.InvSet = [p \in NODE |-> Dir.ShrSet[p]]] + /\ MemData' = ShWbMsg.Data + /\ UNCHANGED <> ------------------------------------------------------------------------------- @@ -855,7 +838,7 @@ System == \/ NI_Wb \/ NI_FAck \/ NI_ShWb (* Abstract environment steps: the CMP `Other`-node interactions summarised *) -(* by the ABS_* rules (all guarded by Sta.Env_o). *) +(* by the ABS_* rules (all guarded by Env_o). *) Environment == \/ \E data \in DATA : ABS_Store(data) \/ \E src \in NODE : @@ -881,15 +864,15 @@ Spec == Init /\ [][Next]_vars CacheStateProp == \A p, q \in NODE : - p # q => ~(Sta.Proc[p].CacheState = "CACHE_E" /\ Sta.Proc[q].CacheState = "CACHE_E") + p # q => ~(Proc[p].CacheState = "CACHE_E" /\ Proc[q].CacheState = "CACHE_E") CacheDataProp == \A p \in NODE : - /\ (Sta.Proc[p].CacheState = "CACHE_E" => Sta.Proc[p].CacheData = Sta.CurrData) - /\ (Sta.Proc[p].CacheState = "CACHE_S" => - /\ (Sta.Collecting => Sta.Proc[p].CacheData = Sta.PrevData) - /\ (~Sta.Collecting => Sta.Proc[p].CacheData = Sta.CurrData)) + /\ (Proc[p].CacheState = "CACHE_E" => Proc[p].CacheData = CurrData) + /\ (Proc[p].CacheState = "CACHE_S" => + /\ (Collecting => Proc[p].CacheData = PrevData) + /\ (~Collecting => Proc[p].CacheData = CurrData)) MemDataProp == - ~Sta.Dir.Dirty => Sta.MemData = Sta.CurrData + ~Dir.Dirty => MemData = CurrData ============================================================================= From 2ee9b05bfe449d3f2751abb943bcf4cda67cfdfe Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 22 Jul 2026 11:00:12 -0700 Subject: [PATCH 05/17] Fix NI_Local_GetX_PutX to invalidate Proc[Home] when not Dir.Local In the PutX branch reached with ~Dir.Dirty /\ elsifCond /\ ~Dir.Local the flat spec left Proc unchanged, whereas the record-based baseline specification invalidates the home cache line (CacheState = "CACHE_I", CacheData = Undefined). Mirror the record behavior so the flat and record encodings agree. This divergence was found by proving per-action equivalence between the flat and record specs with a patched TLAPS. Model checking with TLC did not surface the difference: no reachable state or invariant distinguished the two encodings. Co-authored-by: Claude Opus 4.8 Signed-off-by: Markus Alexander Kuppe --- specifications/FlashProtocol/FlashWithMutex.tla | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla index 4c05fe1d..4b80ba98 100644 --- a/specifications/FlashProtocol/FlashWithMutex.tla +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -401,7 +401,10 @@ NI_Local_GetX_PutX(src) == IN /\ Dir' = IF Dir.Dirty \/ elsifCond THEN commonDir ELSE branch3Dir /\ Proc' = IF Dir.Dirty THEN [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] - ELSE IF Dir.Local THEN ProcLocalI ELSE Proc + ELSE IF Dir.Local THEN ProcLocalI + ELSE IF elsifCond + THEN [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] + ELSE Proc /\ UniMsg' = IF Dir.Dirty THEN [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = Home, ![src].Data = Proc[Home].CacheData] From bc4f2ed27652538932dd8fc08e591ffe02dda14d Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Sat, 25 Jul 2026 22:25:00 -0700 Subject: [PATCH 06/17] Encode the directory's ShrSet and InvSet as sets of nodes Both fields transcribed Murphi's `array [NODE] of boolean` as characteristic functions in [NODE -> BOOLEAN]: membership read as Dir.ShrSet[p], insertion and removal went through EXCEPT on a nested index, and emptiness tests were quantifications over NODE. Make them subsets of NODE instead, so membership is p \in Dir.ShrSet, the updates are \cup and \, and the guards become Dir.ShrSet = {}, Dir.ShrSet \subseteq {src} and Dir.InvSet \ {src} # {}. NI_ShWb needs care: ShWbMsg.Proc ranges over ABS_NODE, and the NODE-indexed array silently dropped it when it was Other. The set version therefore adds {ShWbMsg.Proc} \cap NODE, keeping ShrSet a subset of NODE. Proved behaviour-preserving with TLAPS: per action, Next and Init are equivalent to those of the previous, array-based encoding, under the gluing that maps each set to its characteristic function. Unlike the record flattening this changes the state space rather than re-bundling it, so the equivalence is relative to the Dir conjunct of TypeOK -- the encoding is a bijection on well-typed directories only. TLC is unchanged at 1231/414 states for NODE/DATA = 1/1 and 4,533,240/929,572 at 2/2. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- .../FlashProtocol/FlashWithMutex.tla | 62 ++++++++++--------- 1 file changed, 32 insertions(+), 30 deletions(-) diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla index 4b80ba98..cad0aaa0 100644 --- a/specifications/FlashProtocol/FlashWithMutex.tla +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -64,7 +64,7 @@ TypeOK == CacheState : CACHE_STATE, CacheData : DataU]] /\ Dir \in [Pending : BOOLEAN, Local : BOOLEAN, Dirty : BOOLEAN, HeadVld : BOOLEAN, HeadPtr : NodeU, ShrVld : BOOLEAN, - ShrSet : [NODE -> BOOLEAN], InvSet : [NODE -> BOOLEAN]] + ShrSet : SUBSET NODE, InvSet : SUBSET NODE] /\ MemData \in DATA /\ UniMsg \in [NODE -> [Cmd : UNI_CMD, Proc : NodeU, Data : DataU]] /\ InvMsg \in [NODE -> [Cmd : INV_CMD]] @@ -93,7 +93,7 @@ Init == CacheState |-> "CACHE_I", CacheData |-> Undefined]] /\ Dir = [Pending |-> FALSE, Local |-> FALSE, Dirty |-> FALSE, HeadVld |-> FALSE, HeadPtr |-> Undefined, ShrVld |-> FALSE, - ShrSet |-> [i \in NODE |-> FALSE], InvSet |-> [i \in NODE |-> FALSE]] + ShrSet |-> {}, InvSet |-> {}] /\ MemData = d /\ UniMsg = [i \in NODE |-> [Cmd |-> "UNI_None", Proc |-> Undefined, Data |-> Undefined]] /\ InvMsg = [i \in NODE |-> [Cmd |-> "INV_None"]] @@ -188,13 +188,13 @@ PI_Local_GetX_PutX == /\ Proc[Home].CacheState \in {"CACHE_I", "CACHE_S"} /\ ~Dir.Pending /\ ~Dir.Dirty /\ LET InvP(p) == /\ p # Home - /\ \/ (Dir.ShrVld /\ Dir.ShrSet[p]) + /\ \/ (Dir.ShrVld /\ p \in Dir.ShrSet) \/ (Dir.HeadVld /\ Dir.HeadPtr = p) IN /\ Dir' = IF Dir.HeadVld THEN [Dir EXCEPT !.Local = TRUE, !.Dirty = TRUE, !.Pending = TRUE, !.HeadVld = FALSE, !.HeadPtr = Undefined, !.ShrVld = FALSE, - !.ShrSet = [p \in NODE |-> FALSE], - !.InvSet = [p \in NODE |-> InvP(p)]] + !.ShrSet = {}, + !.InvSet = {p \in NODE : InvP(p)}] ELSE [Dir EXCEPT !.Local = TRUE, !.Dirty = TRUE] /\ InvMsg' = IF Dir.HeadVld THEN [p \in NODE |-> [Cmd |-> IF InvP(p) THEN "INV_Inv" ELSE "INV_None"]] @@ -302,8 +302,8 @@ NI_Local_Get_Put(src) == /\ Dir' = IF Dir.Dirty THEN [Dir EXCEPT !.Dirty = FALSE, !.HeadVld = TRUE, !.HeadPtr = src] ELSE IF Dir.HeadVld - THEN [Dir EXCEPT !.ShrVld = TRUE, !.ShrSet[src] = TRUE, - !.InvSet = [p \in NODE |-> (p = src) \/ Dir.ShrSet[p]]] + THEN [Dir EXCEPT !.ShrVld = TRUE, !.ShrSet = Dir.ShrSet \cup {src}, + !.InvSet = Dir.ShrSet \cup {src}] ELSE [Dir EXCEPT !.HeadVld = TRUE, !.HeadPtr = src] /\ MemData' = IF Dir.Dirty THEN Proc[Home].CacheData ELSE MemData /\ Proc' = IF Dir.Dirty THEN [Proc EXCEPT ![Home].CacheState = "CACHE_S"] ELSE Proc @@ -381,10 +381,10 @@ NI_Local_GetX_PutX(src) == /\ ~Dir.Pending /\ (Dir.Dirty => (Dir.Local /\ Proc[Home].CacheState = "CACHE_E")) /\ LET Cond3(p) == /\ p # Home /\ p # src - /\ \/ (Dir.ShrVld /\ Dir.ShrSet[p]) + /\ \/ (Dir.ShrVld /\ p \in Dir.ShrSet) \/ (Dir.HeadVld /\ Dir.HeadPtr = p) elsifCond == Dir.HeadVld => (Dir.HeadPtr = src - /\ \A p \in NODE : p # src => ~Dir.ShrSet[p]) + /\ Dir.ShrSet \subseteq {src}) ProcLocalI == [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined, ![Home].InvMarked = @@ -392,12 +392,12 @@ NI_Local_GetX_PutX(src) == THEN TRUE ELSE Proc[Home].InvMarked] commonDir == [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, !.HeadPtr = src, !.ShrVld = FALSE, - !.ShrSet = [p \in NODE |-> FALSE], - !.InvSet = [p \in NODE |-> FALSE]] + !.ShrSet = {}, + !.InvSet = {}] branch3Dir == [Dir EXCEPT !.Pending = TRUE, !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, !.HeadPtr = src, !.ShrVld = FALSE, - !.ShrSet = [p \in NODE |-> FALSE], - !.InvSet = [p \in NODE |-> Cond3(p)]] + !.ShrSet = {}, + !.InvSet = {p \in NODE : Cond3(p)}] IN /\ Dir' = IF Dir.Dirty \/ elsifCond THEN commonDir ELSE branch3Dir /\ Proc' = IF Dir.Dirty THEN [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] @@ -501,12 +501,12 @@ NI_Inv(dst) == NI_InvAck(src) == /\ src # Home /\ InvMsg[src].Cmd = "INV_InvAck" - /\ Dir.Pending /\ Dir.InvSet[src] - /\ LET moreAcks == \E p \in NODE : p # src /\ Dir.InvSet[p] + /\ Dir.Pending /\ src \in Dir.InvSet + /\ LET moreAcks == Dir.InvSet \ {src} # {} IN /\ InvMsg' = [InvMsg EXCEPT ![src].Cmd = "INV_None"] /\ Dir' = IF moreAcks - THEN [Dir EXCEPT !.InvSet[src] = FALSE] - ELSE [Dir EXCEPT !.InvSet[src] = FALSE, !.Pending = FALSE, + THEN [Dir EXCEPT !.InvSet = Dir.InvSet \ {src}] + ELSE [Dir EXCEPT !.InvSet = Dir.InvSet \ {src}, !.Pending = FALSE, !.Local = IF Dir.Local /\ ~Dir.Dirty THEN FALSE ELSE Dir.Local] /\ Collecting' = IF moreAcks THEN Collecting ELSE FALSE /\ LastInvAck' = src @@ -533,9 +533,11 @@ NI_FAck == NI_ShWb == /\ ShWbMsg.Cmd = "SHWB_ShWb" /\ ShWbMsg' = [ShWbMsg EXCEPT !.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 = [p \in NODE |-> (p = ShWbMsg.Proc) \/ Dir.ShrSet[p]], - !.InvSet = [p \in NODE |-> (p = ShWbMsg.Proc) \/ Dir.ShrSet[p]]] + !.ShrSet = Dir.ShrSet \cup ({ShWbMsg.Proc} \cap NODE), + !.InvSet = Dir.ShrSet \cup ({ShWbMsg.Proc} \cap NODE)] /\ MemData' = ShWbMsg.Data /\ UNCHANGED <> @@ -599,7 +601,7 @@ ABS_NI_Local_Get_Put == /\ Dir' = IF Dir.Dirty THEN [Dir EXCEPT !.Dirty = FALSE, !.HeadVld = TRUE, !.HeadPtr = Other] ELSE IF Dir.HeadVld - THEN [Dir EXCEPT !.ShrVld = TRUE, !.InvSet = [p \in NODE |-> Dir.ShrSet[p]]] + 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 @@ -704,9 +706,9 @@ ABS_NI_Local_GetX_PutX == /\ ~Dir.Pending /\ (Dir.Dirty => (Dir.Local /\ Proc[Home].CacheState = "CACHE_E")) /\ LET Cond3(p) == /\ p # Home - /\ \/ (Dir.ShrVld /\ Dir.ShrSet[p]) + /\ \/ (Dir.ShrVld /\ p \in Dir.ShrSet) \/ (Dir.HeadVld /\ Dir.HeadPtr = p) - elsifCond == Dir.HeadVld => (Dir.HeadPtr = Other /\ \A p \in NODE : ~Dir.ShrSet[p]) + elsifCond == Dir.HeadVld => (Dir.HeadPtr = Other /\ Dir.ShrSet = {}) ProcLocalI == [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined, ![Home].InvMarked = @@ -715,12 +717,12 @@ ABS_NI_Local_GetX_PutX == ProcII == [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] commonDir == [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, !.HeadPtr = Other, !.ShrVld = FALSE, - !.ShrSet = [p \in NODE |-> FALSE], - !.InvSet = [p \in NODE |-> FALSE]] + !.ShrSet = {}, + !.InvSet = {}] branch3Dir == [Dir EXCEPT !.Pending = TRUE, !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, !.HeadPtr = Other, !.ShrVld = FALSE, - !.ShrSet = [p \in NODE |-> FALSE], - !.InvSet = [p \in NODE |-> Cond3(p)]] + !.ShrSet = {}, + !.InvSet = {p \in NODE : Cond3(p)}] IN /\ Dir' = IF Dir.Dirty \/ elsifCond THEN commonDir ELSE branch3Dir /\ Proc' = IF Dir.Dirty THEN ProcII ELSE IF Dir.Local THEN ProcLocalI @@ -797,7 +799,7 @@ ABS_NI_InvAck == => UniMsg[q].Proc = Home) /\ (UniMsg[q].Cmd = "UNI_PutX" => (UniMsg[q].Proc = Home /\ PendReqSrc = q)) - /\ LET moreAcks == \E p \in NODE : Dir.InvSet[p] + /\ LET moreAcks == Dir.InvSet # {} IN /\ Dir' = IF moreAcks THEN Dir ELSE [Dir EXCEPT !.Pending = FALSE, !.Local = IF Dir.Local /\ ~Dir.Dirty THEN FALSE ELSE Dir.Local] @@ -811,7 +813,7 @@ ABS_NI_ShWb == /\ ShWbMsg.Cmd = "SHWB_ShWb" /\ ShWbMsg.Proc = Other /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_None", !.Proc = Undefined, !.Data = Undefined] /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.Dirty = FALSE, !.ShrVld = TRUE, - !.InvSet = [p \in NODE |-> Dir.ShrSet[p]]] + !.InvSet = Dir.ShrSet] /\ MemData' = ShWbMsg.Data /\ UNCHANGED < Date: Sun, 26 Jul 2026 06:46:40 -0700 Subject: [PATCH 07/17] Split the multi-branch actions into disjoint guarded sub-actions Five actions -- PI_Local_GetX_PutX, NI_Local_GetX_PutX, NI_InvAck and the ABS_ flavours of the latter two -- transcribed Murphi's if/elsif/else as a LET binding each branch's next-state values and an IF chain that repeated the branch condition once per updated variable, so a single branch was spread across a dozen conjuncts. Restate each action as a disjunction of sub-actions that carry their own guard: every branch is now a straight-line list of assignments and each condition appears once. The LET-bound InvP and Cond3 were the same predicate in three actions; hoist it to InvNodes(exclude), the nodes to invalidate less Home and the requester. Likewise NoOtherSharers(req) for the elsif guard, shared by the concrete and abstract flavours, and ProcHomeInvalid resp. ProcHomeInvalidMarked for Home's dropped line. IF survives only where it picks a field value rather than a branch. Proved behaviour-preserving with TLAPS: per action, Next and Init are equivalent to those of the previous form, which stated the branches as IF chains over LET-bound helpers. Both forms have the same variables, so the restructuring is purely propositional and needs no gluing; the only hypothesis is the Dir conjunct of TypeOK, since rewriting IF c THEN a ELSE b as guarded disjuncts requires c \in BOOLEAN and every branch condition is a Boolean Dir field. TLC is unchanged at 1231/414 states for NODE/DATA = 1/1 and 4,533,240/929,572 at 2/2. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- .../FlashProtocol/FlashWithMutex.tla | 258 +++++++++++------- 1 file changed, 161 insertions(+), 97 deletions(-) diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla index cad0aaa0..0d3689b1 100644 --- a/specifications/FlashProtocol/FlashWithMutex.tla +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -113,6 +113,32 @@ Init == /\ LastInvAck = Undefined /\ Env_o = TRUE +------------------------------------------------------------------------------- +(* Shared fragments of the *_GetX_PutX actions, which grant a line *) +(* exclusively and so have to revoke it from everyone else first. *) + +\* The nodes that must be invalidated before the line can be granted: the +\* sharers and the head, less Home and the requester themselves. +InvNodes(exclude) == + {p \in NODE \ exclude : \/ (Dir.ShrVld /\ p \in Dir.ShrSet) + \/ (Dir.HeadVld /\ Dir.HeadPtr = p)} + +\* Nobody has to be invalidated: either there is no head pointer, or req is +\* already the head and the only sharer. +NoOtherSharers(req) == + Dir.HeadVld => (Dir.HeadPtr = req /\ Dir.ShrSet \subseteq {req}) + +\* Home's line dropped, because the GetX takes it away. +ProcHomeInvalid == + [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] + +\* As ProcHomeInvalid, but a Get of Home's that is still in flight is marked, so +\* that its reply is not mistaken for a fresh grant. +ProcHomeInvalidMarked == + [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined, + ![Home].InvMarked = IF Proc[Home].ProcCmd = "NODE_Get" + THEN TRUE ELSE Proc[Home].InvMarked] + ------------------------------------------------------------------------------- (* Concrete (non-ABS) rules *) ------------------------------------------------------------------------------- @@ -183,29 +209,35 @@ PI_Local_GetX_GetX == /\ UNCHANGED <> +\* The line is shared: the sharers and the head are invalidated first, so +\* Home's own request goes pending. +PI_Local_GetX_PutX_Inv == + /\ Dir.HeadVld + /\ Dir' = [Dir EXCEPT !.Local = TRUE, !.Dirty = TRUE, !.Pending = TRUE, + !.HeadVld = FALSE, !.HeadPtr = Undefined, !.ShrVld = FALSE, + !.ShrSet = {}, !.InvSet = InvNodes({Home})] + /\ InvMsg' = [p \in NODE |-> [Cmd |-> IF p \in InvNodes({Home}) + THEN "INV_Inv" ELSE "INV_None"]] + /\ PendReqSrc' = Home + /\ Collecting' = TRUE + /\ PrevData' = CurrData + +\* Nobody holds the line, so it is granted right away. +PI_Local_GetX_PutX_Grant == + /\ ~Dir.HeadVld + /\ Dir' = [Dir EXCEPT !.Local = TRUE, !.Dirty = TRUE] + /\ UNCHANGED <> + PI_Local_GetX_PutX == /\ Proc[Home].ProcCmd = "NODE_None" /\ Proc[Home].CacheState \in {"CACHE_I", "CACHE_S"} /\ ~Dir.Pending /\ ~Dir.Dirty - /\ LET InvP(p) == /\ p # Home - /\ \/ (Dir.ShrVld /\ p \in Dir.ShrSet) - \/ (Dir.HeadVld /\ Dir.HeadPtr = p) - IN /\ Dir' = IF Dir.HeadVld - THEN [Dir EXCEPT !.Local = TRUE, !.Dirty = TRUE, !.Pending = TRUE, - !.HeadVld = FALSE, !.HeadPtr = Undefined, !.ShrVld = FALSE, - !.ShrSet = {}, - !.InvSet = {p \in NODE : InvP(p)}] - ELSE [Dir EXCEPT !.Local = TRUE, !.Dirty = TRUE] - /\ InvMsg' = IF Dir.HeadVld - THEN [p \in NODE |-> [Cmd |-> IF InvP(p) THEN "INV_Inv" ELSE "INV_None"]] - ELSE InvMsg - /\ PendReqSrc' = IF Dir.HeadVld THEN Home ELSE PendReqSrc - /\ Collecting' = IF Dir.HeadVld THEN TRUE ELSE Collecting - /\ PrevData' = IF Dir.HeadVld THEN CurrData ELSE PrevData - /\ Proc' = [Proc EXCEPT ![Home].ProcCmd = "NODE_None", - ![Home].InvMarked = FALSE, - ![Home].CacheState = "CACHE_E", - ![Home].CacheData = MemData] + /\ Proc' = [Proc EXCEPT ![Home].ProcCmd = "NODE_None", + ![Home].InvMarked = FALSE, + ![Home].CacheState = "CACHE_E", + ![Home].CacheData = MemData] + /\ \/ PI_Local_GetX_PutX_Inv + \/ PI_Local_GetX_PutX_Grant /\ UNCHANGED <> @@ -374,48 +406,55 @@ NI_Local_GetX_GetX(src) == /\ UNCHANGED <> +\* Home holds the line exclusively, so it can be handed to src directly. +NI_Local_GetX_PutX_Dirty(src) == + /\ Dir.Dirty + /\ Dir' = [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, + !.HeadPtr = src, !.ShrVld = FALSE, !.ShrSet = {}, !.InvSet = {}] + /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = Home, + ![src].Data = Proc[Home].CacheData] + /\ Proc' = ProcHomeInvalid + /\ UNCHANGED <> + +\* src is already the head and the only sharer, so nobody has to be invalidated +\* and memory's copy is handed over. +NI_Local_GetX_PutX_Grant(src) == + /\ ~Dir.Dirty + /\ NoOtherSharers(src) + /\ Dir' = [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, + !.HeadPtr = src, !.ShrVld = FALSE, !.ShrSet = {}, !.InvSet = {}] + /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = Home, + ![src].Data = MemData] + /\ Proc' = IF Dir.Local THEN ProcHomeInvalidMarked ELSE ProcHomeInvalid + /\ UNCHANGED <> + +\* Others share the line: they are invalidated first and the request goes +\* pending until their acks come back. +NI_Local_GetX_PutX_Inv(src) == + /\ ~Dir.Dirty + /\ ~NoOtherSharers(src) + /\ Dir' = [Dir EXCEPT !.Pending = TRUE, !.Local = FALSE, !.Dirty = TRUE, + !.HeadVld = TRUE, !.HeadPtr = src, !.ShrVld = FALSE, + !.ShrSet = {}, !.InvSet = InvNodes({Home, src})] + /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = Home, + ![src].Data = MemData] + /\ Proc' = IF Dir.Local THEN ProcHomeInvalidMarked ELSE Proc + /\ InvMsg' = [p \in NODE |-> [Cmd |-> IF p \in InvNodes({Home, src}) + THEN "INV_Inv" ELSE "INV_None"]] + /\ PendReqSrc' = src + /\ PendReqCmd' = "UNI_GetX" + /\ Collecting' = TRUE + /\ PrevData' = CurrData + NI_Local_GetX_PutX(src) == /\ src # Home /\ UniMsg[src].Cmd = "UNI_GetX" /\ UniMsg[src].Proc = Home /\ ~Dir.Pending /\ (Dir.Dirty => (Dir.Local /\ Proc[Home].CacheState = "CACHE_E")) - /\ LET Cond3(p) == /\ p # Home /\ p # src - /\ \/ (Dir.ShrVld /\ p \in Dir.ShrSet) - \/ (Dir.HeadVld /\ Dir.HeadPtr = p) - elsifCond == Dir.HeadVld => (Dir.HeadPtr = src - /\ Dir.ShrSet \subseteq {src}) - ProcLocalI == [Proc EXCEPT ![Home].CacheState = "CACHE_I", - ![Home].CacheData = Undefined, - ![Home].InvMarked = - IF Proc[Home].ProcCmd = "NODE_Get" - THEN TRUE ELSE Proc[Home].InvMarked] - commonDir == [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, - !.HeadPtr = src, !.ShrVld = FALSE, - !.ShrSet = {}, - !.InvSet = {}] - branch3Dir == [Dir EXCEPT !.Pending = TRUE, !.Local = FALSE, !.Dirty = TRUE, - !.HeadVld = TRUE, !.HeadPtr = src, !.ShrVld = FALSE, - !.ShrSet = {}, - !.InvSet = {p \in NODE : Cond3(p)}] - IN /\ Dir' = IF Dir.Dirty \/ elsifCond THEN commonDir ELSE branch3Dir - /\ Proc' = IF Dir.Dirty - THEN [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] - ELSE IF Dir.Local THEN ProcLocalI - ELSE IF elsifCond - THEN [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] - ELSE Proc - /\ UniMsg' = IF Dir.Dirty - THEN [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = Home, - ![src].Data = Proc[Home].CacheData] - ELSE [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = Home, - ![src].Data = MemData] - /\ InvMsg' = IF Dir.Dirty \/ elsifCond THEN InvMsg - ELSE [p \in NODE |-> [Cmd |-> IF Cond3(p) THEN "INV_Inv" ELSE "INV_None"]] - /\ PendReqSrc' = IF Dir.Dirty \/ elsifCond THEN PendReqSrc ELSE src - /\ PendReqCmd' = IF Dir.Dirty \/ elsifCond THEN PendReqCmd ELSE "UNI_GetX" - /\ Collecting' = IF Dir.Dirty \/ elsifCond THEN Collecting ELSE TRUE - /\ PrevData' = IF Dir.Dirty \/ elsifCond THEN PrevData ELSE CurrData + /\ \/ NI_Local_GetX_PutX_Dirty(src) + \/ NI_Local_GetX_PutX_Grant(src) + \/ NI_Local_GetX_PutX_Inv(src) /\ UNCHANGED <> @@ -498,18 +537,27 @@ NI_Inv(dst) == PrevData, LastWrVld, LastWrPtr, PendReqSrc, PendReqCmd, Collecting, FwdCmd, FwdSrc, LastInvAck, Env_o>> +\* Acks are still outstanding: only this one is recorded. +NI_InvAck_More(src) == + /\ Dir.InvSet \ {src} # {} + /\ Dir' = [Dir EXCEPT !.InvSet = Dir.InvSet \ {src}] + /\ UNCHANGED Collecting + +\* The last ack: the invalidation round is complete and the request retires. +NI_InvAck_Last(src) == + /\ Dir.InvSet \ {src} = {} + /\ Dir' = [Dir EXCEPT !.InvSet = Dir.InvSet \ {src}, !.Pending = FALSE, + !.Local = IF Dir.Local /\ ~Dir.Dirty THEN FALSE ELSE Dir.Local] + /\ Collecting' = FALSE + NI_InvAck(src) == /\ src # Home /\ InvMsg[src].Cmd = "INV_InvAck" /\ Dir.Pending /\ src \in Dir.InvSet - /\ LET moreAcks == Dir.InvSet \ {src} # {} - IN /\ InvMsg' = [InvMsg EXCEPT ![src].Cmd = "INV_None"] - /\ Dir' = IF moreAcks - THEN [Dir EXCEPT !.InvSet = Dir.InvSet \ {src}] - ELSE [Dir EXCEPT !.InvSet = Dir.InvSet \ {src}, !.Pending = FALSE, - !.Local = IF Dir.Local /\ ~Dir.Dirty THEN FALSE ELSE Dir.Local] - /\ Collecting' = IF moreAcks THEN Collecting ELSE FALSE - /\ LastInvAck' = src + /\ InvMsg' = [InvMsg EXCEPT ![src].Cmd = "INV_None"] + /\ LastInvAck' = src + /\ \/ NI_InvAck_More(src) + \/ NI_InvAck_Last(src) /\ UNCHANGED <> @@ -701,38 +749,45 @@ ABS_NI_Local_GetX_GetX == /\ 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' = [Dir EXCEPT !.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")) - /\ LET Cond3(p) == /\ p # Home - /\ \/ (Dir.ShrVld /\ p \in Dir.ShrSet) - \/ (Dir.HeadVld /\ Dir.HeadPtr = p) - elsifCond == Dir.HeadVld => (Dir.HeadPtr = Other /\ Dir.ShrSet = {}) - ProcLocalI == [Proc EXCEPT ![Home].CacheState = "CACHE_I", - ![Home].CacheData = Undefined, - ![Home].InvMarked = - IF Proc[Home].ProcCmd = "NODE_Get" - THEN TRUE ELSE Proc[Home].InvMarked] - ProcII == [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] - commonDir == [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, - !.HeadPtr = Other, !.ShrVld = FALSE, - !.ShrSet = {}, - !.InvSet = {}] - branch3Dir == [Dir EXCEPT !.Pending = TRUE, !.Local = FALSE, !.Dirty = TRUE, - !.HeadVld = TRUE, !.HeadPtr = Other, !.ShrVld = FALSE, - !.ShrSet = {}, - !.InvSet = {p \in NODE : Cond3(p)}] - IN /\ Dir' = IF Dir.Dirty \/ elsifCond THEN commonDir ELSE branch3Dir - /\ Proc' = IF Dir.Dirty THEN ProcII - ELSE IF Dir.Local THEN ProcLocalI - ELSE IF elsifCond THEN ProcII ELSE Proc - /\ InvMsg' = IF Dir.Dirty \/ elsifCond THEN InvMsg - ELSE [p \in NODE |-> [Cmd |-> IF Cond3(p) THEN "INV_Inv" ELSE "INV_None"]] - /\ PendReqSrc' = IF Dir.Dirty \/ elsifCond THEN PendReqSrc ELSE Other - /\ PendReqCmd' = IF Dir.Dirty \/ elsifCond THEN PendReqCmd ELSE "UNI_GetX" - /\ Collecting' = IF Dir.Dirty \/ elsifCond THEN Collecting ELSE TRUE - /\ PrevData' = IF Dir.Dirty \/ elsifCond THEN PrevData ELSE CurrData + /\ \/ ABS_NI_Local_GetX_PutX_Dirty + \/ ABS_NI_Local_GetX_PutX_Grant + \/ ABS_NI_Local_GetX_PutX_Inv /\ UNCHANGED <> @@ -790,6 +845,18 @@ ABS_NI_Remote_GetX_PutX_src_dst == PrevData, LastWrVld, LastWrPtr, PendReqSrc, PendReqCmd, Collecting, LastInvAck, Env_o>> +\* Concrete nodes have not acked yet, so the round stays open. +ABS_NI_InvAck_More == + /\ Dir.InvSet # {} + /\ UNCHANGED <> + +\* All concrete nodes have acked: the round closes and the request retires. +ABS_NI_InvAck_Last == + /\ Dir.InvSet = {} + /\ Dir' = [Dir EXCEPT !.Pending = FALSE, + !.Local = IF Dir.Local /\ ~Dir.Dirty THEN FALSE ELSE Dir.Local] + /\ Collecting' = FALSE + ABS_NI_InvAck == /\ Env_o /\ Dir.Pending /\ Collecting @@ -799,12 +866,9 @@ ABS_NI_InvAck == => UniMsg[q].Proc = Home) /\ (UniMsg[q].Cmd = "UNI_PutX" => (UniMsg[q].Proc = Home /\ PendReqSrc = q)) - /\ LET moreAcks == Dir.InvSet # {} - IN /\ Dir' = IF moreAcks THEN Dir - ELSE [Dir EXCEPT !.Pending = FALSE, - !.Local = IF Dir.Local /\ ~Dir.Dirty THEN FALSE ELSE Dir.Local] - /\ Collecting' = IF moreAcks THEN Collecting ELSE FALSE - /\ LastInvAck' = Other + /\ LastInvAck' = Other + /\ \/ ABS_NI_InvAck_More + \/ ABS_NI_InvAck_Last /\ UNCHANGED <> From a57548ae4bc26c21e64979f7cc1568d6063f1188 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Sun, 26 Jul 2026 06:57:14 -0700 Subject: [PATCH 08/17] Name the three groups of variables that share a frame condition Every action spelled its frame condition out as a tuple of up to 20 individual variables, so a one-line update carried three lines of UNCHANGED and adding a variable meant touching all 56 definitions. Group the variables that no action ever changes on its own and name the groups: lastWrVars for the write-tracking ghosts CurrData, LastWrVld and LastWrPtr, pendVars for the pending request's PendReqSrc, PendReqCmd and Collecting, and fwdVars for FwdCmd and FwdSrc. An action that does change one member spells that group's other members out, so no precision is lost; the lists shrink from 881 names to 673. The groups are not chosen by eye: lastWrVars is exactly a class of the partition of the variables by the set of actions whose frame mentions them, so it costs nothing, and pendVars and fwdVars are usable in 42 resp. 30 of the 56 definitions. A netVars for the six message variables was rejected -- it would apply to only 9, since the actions change messages one at a time. Proved behaviour-preserving with TLAPS: per action, Next and Init are equivalent to those of the previous form, which listed the group members individually. The two forms share their variables and every guard and update is the same formula, so unlike the set encoding and the disjunct split this equivalence needs no hypothesis whatever: it reduces to UNCHANGED of a tuple holding a group being UNCHANGED of the tuple with the group spliced in. TLC is unchanged at 1231/414 states for NODE/DATA = 1/1 and 4,533,240/929,572 at 2/2. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- .../FlashProtocol/FlashWithMutex.tla | 255 ++++++++---------- 1 file changed, 117 insertions(+), 138 deletions(-) diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla index 0d3689b1..570558c1 100644 --- a/specifications/FlashProtocol/FlashWithMutex.tla +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -56,6 +56,21 @@ vars == <> +\* 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 +\* action that does change one member spells the group's others out. + +\* Who last wrote the line and what they wrote: read only by the data +\* properties, never by a guard. +lastWrVars == <> + +\* The request Home is currently working on, and whether it is still waiting +\* for invalidation acks. +pendVars == <> + +\* The request Home forwarded to the dirty node. +fwdVars == <> + ------------------------------------------------------------------------------- TypeOK == @@ -150,7 +165,7 @@ Store(src, data) == /\ LastWrVld' = TRUE /\ LastWrPtr' = src /\ UNCHANGED <> + PrevData, pendVars, fwdVars, LastInvAck, Env_o>> \* Shared/exclusive request from a remote processor (merges the former \* PI_Remote_Get / PI_Remote_GetX). @@ -162,9 +177,8 @@ PI_Remote(src, c) == /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = IF c = "Get" THEN "UNI_Get" ELSE "UNI_GetX", ![src].Proc = Home, ![src].Data = Undefined] - /\ UNCHANGED <> + /\ UNCHANGED <> PI_Local_Get_Get == /\ Proc[Home].ProcCmd = "NODE_None" @@ -178,8 +192,8 @@ PI_Local_Get_Get == /\ PendReqSrc' = Home /\ PendReqCmd' = "UNI_Get" /\ Collecting' = FALSE - /\ UNCHANGED <> + /\ UNCHANGED <> PI_Local_Get_Put == /\ Proc[Home].ProcCmd = "NODE_None" @@ -190,9 +204,8 @@ PI_Local_Get_Put == ![Home].InvMarked = FALSE, ![Home].CacheState = IF Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", ![Home].CacheData = IF Proc[Home].InvMarked THEN Undefined ELSE MemData] - /\ UNCHANGED <> + /\ UNCHANGED <> PI_Local_GetX_GetX == /\ Proc[Home].ProcCmd = "NODE_None" @@ -206,8 +219,8 @@ PI_Local_GetX_GetX == /\ PendReqSrc' = Home /\ PendReqCmd' = "UNI_GetX" /\ Collecting' = FALSE - /\ UNCHANGED <> + /\ UNCHANGED <> \* The line is shared: the sharers and the head are invalidated first, so \* Home's own request goes pending. @@ -226,7 +239,7 @@ PI_Local_GetX_PutX_Inv == PI_Local_GetX_PutX_Grant == /\ ~Dir.HeadVld /\ Dir' = [Dir EXCEPT !.Local = TRUE, !.Dirty = TRUE] - /\ UNCHANGED <> + /\ UNCHANGED <> PI_Local_GetX_PutX == /\ Proc[Home].ProcCmd = "NODE_None" @@ -238,8 +251,8 @@ PI_Local_GetX_PutX == ![Home].CacheData = MemData] /\ \/ PI_Local_GetX_PutX_Inv \/ PI_Local_GetX_PutX_Grant - /\ UNCHANGED <> + /\ UNCHANGED <> PI_Remote_PutX(dst) == /\ dst # Home @@ -247,9 +260,8 @@ PI_Remote_PutX(dst) == /\ Proc[dst].CacheState = "CACHE_E" /\ Proc' = [Proc EXCEPT ![dst].CacheState = "CACHE_I", ![dst].CacheData = Undefined] /\ WbMsg' = [WbMsg EXCEPT !.Cmd = "WB_Wb", !.Proc = dst, !.Data = Proc[dst].CacheData] - /\ UNCHANGED <> + /\ UNCHANGED <> PI_Local_PutX == /\ Proc[Home].ProcCmd = "NODE_None" @@ -257,9 +269,8 @@ PI_Local_PutX == /\ Proc' = [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] /\ Dir' = [Dir EXCEPT !.Dirty = FALSE, !.Local = IF Dir.Pending THEN Dir.Local ELSE FALSE] /\ MemData' = Proc[Home].CacheData - /\ UNCHANGED <> + /\ UNCHANGED <> PI_Remote_Replace(src) == /\ src # Home @@ -267,34 +278,30 @@ PI_Remote_Replace(src) == /\ Proc[src].CacheState = "CACHE_S" /\ Proc' = [Proc EXCEPT ![src].CacheState = "CACHE_I", ![src].CacheData = Undefined] /\ RpMsg' = [RpMsg EXCEPT ![src].Cmd = "RP_Replace"] - /\ UNCHANGED <> + /\ UNCHANGED <> PI_Local_Replace == /\ Proc[Home].ProcCmd = "NODE_None" /\ Proc[Home].CacheState = "CACHE_S" /\ Dir' = [Dir EXCEPT !.Local = FALSE] /\ Proc' = [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Nak(dst) == /\ UniMsg[dst].Cmd = "UNI_Nak" /\ UniMsg' = [UniMsg EXCEPT ![dst].Cmd = "UNI_None", ![dst].Proc = Undefined, ![dst].Data = Undefined] /\ Proc' = [Proc EXCEPT ![dst].ProcCmd = "NODE_None", ![dst].InvMarked = FALSE] - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Nak_Clear == /\ NakcMsg.Cmd = "NAKC_Nakc" /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_None"] /\ Dir' = [Dir EXCEPT !.Pending = FALSE] - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Local_Get_Nak(src) == /\ src # Home @@ -305,9 +312,8 @@ NI_Local_Get_Nak(src) == \/ (Dir.Dirty /\ Dir.Local /\ Proc[Home].CacheState # "CACHE_E") \/ (Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr = src) /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_Nak", ![src].Proc = Home, ![src].Data = Undefined] - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Local_Get_Get(src) == /\ src # Home @@ -321,8 +327,8 @@ NI_Local_Get_Get(src) == /\ PendReqSrc' = src /\ PendReqCmd' = "UNI_Get" /\ Collecting' = FALSE - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Local_Get_Put(src) == /\ src # Home @@ -344,9 +350,8 @@ NI_Local_Get_Put(src) == ![src].Data = Proc[Home].CacheData] ELSE [UniMsg EXCEPT ![src].Cmd = "UNI_Put", ![src].Proc = Home, ![src].Data = MemData] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Remote NAK of a shared/exclusive request (merges the former \* NI_Remote_Get_Nak / NI_Remote_GetX_Nak). @@ -359,9 +364,8 @@ NI_Remote_Nak(src, dst) == /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_Nakc"] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = src - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Remote_Get_Put(src, dst) == /\ src # dst /\ dst # Home @@ -376,9 +380,8 @@ NI_Remote_Get_Put(src, dst) == /\ ShWbMsg' = IF src # Home THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_ShWb", !.Proc = src, !.Data = Proc[dst].CacheData] ELSE ShWbMsg - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Local_GetX_Nak(src) == /\ src # Home @@ -388,9 +391,8 @@ NI_Local_GetX_Nak(src) == \/ (Dir.Dirty /\ Dir.Local /\ Proc[Home].CacheState # "CACHE_E") \/ (Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr = src) /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_Nak", ![src].Proc = Home, ![src].Data = Undefined] - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Local_GetX_GetX(src) == /\ src # Home @@ -403,8 +405,8 @@ NI_Local_GetX_GetX(src) == /\ PendReqSrc' = src /\ PendReqCmd' = "UNI_GetX" /\ Collecting' = FALSE - /\ UNCHANGED <> + /\ UNCHANGED <> \* Home holds the line exclusively, so it can be handed to src directly. NI_Local_GetX_PutX_Dirty(src) == @@ -414,7 +416,7 @@ NI_Local_GetX_PutX_Dirty(src) == /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = Home, ![src].Data = Proc[Home].CacheData] /\ Proc' = ProcHomeInvalid - /\ UNCHANGED <> + /\ UNCHANGED <> \* src is already the head and the only sharer, so nobody has to be invalidated \* and memory's copy is handed over. @@ -426,7 +428,7 @@ NI_Local_GetX_PutX_Grant(src) == /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = Home, ![src].Data = MemData] /\ Proc' = IF Dir.Local THEN ProcHomeInvalidMarked ELSE ProcHomeInvalid - /\ UNCHANGED <> + /\ UNCHANGED <> \* Others share the line: they are invalidated first and the request goes \* pending until their acks come back. @@ -455,8 +457,8 @@ 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 @@ -471,9 +473,8 @@ NI_Remote_GetX_PutX(src, dst) == /\ ShWbMsg' = IF src # Home THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_FAck", !.Proc = src, !.Data = Undefined] ELSE ShWbMsg - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Local_Put == /\ UniMsg[Home].Cmd = "UNI_Put" @@ -484,9 +485,8 @@ NI_Local_Put == ![Home].InvMarked = FALSE, ![Home].CacheState = IF Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", ![Home].CacheData = IF Proc[Home].InvMarked THEN Undefined ELSE UniMsg[Home].Data] - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Remote_Put(dst) == /\ dst # Home @@ -496,9 +496,8 @@ NI_Remote_Put(dst) == ![dst].InvMarked = FALSE, ![dst].CacheState = IF Proc[dst].InvMarked THEN "CACHE_I" ELSE "CACHE_S", ![dst].CacheData = IF Proc[dst].InvMarked THEN Undefined ELSE UniMsg[dst].Data] - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Local_PutXAcksDone == /\ UniMsg[Home].Cmd = "UNI_PutX" @@ -508,9 +507,8 @@ NI_Local_PutXAcksDone == ![Home].InvMarked = FALSE, ![Home].CacheState = "CACHE_E", ![Home].CacheData = UniMsg[Home].Data] - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Remote_PutX(dst) == /\ dst # Home @@ -521,9 +519,8 @@ NI_Remote_PutX(dst) == ![dst].InvMarked = FALSE, ![dst].CacheState = "CACHE_E", ![dst].CacheData = UniMsg[dst].Data] - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Inv(dst) == /\ dst # Home @@ -533,9 +530,8 @@ NI_Inv(dst) == ![dst].CacheData = Undefined, ![dst].InvMarked = IF Proc[dst].ProcCmd = "NODE_Get" THEN TRUE ELSE Proc[dst].InvMarked] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Acks are still outstanding: only this one is recorded. NI_InvAck_More(src) == @@ -558,25 +554,23 @@ NI_InvAck(src) == /\ LastInvAck' = src /\ \/ NI_InvAck_More(src) \/ NI_InvAck_Last(src) - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Wb == /\ WbMsg.Cmd = "WB_Wb" /\ WbMsg' = [WbMsg EXCEPT !.Cmd = "WB_None", !.Proc = Undefined, !.Data = Undefined] /\ Dir' = [Dir EXCEPT !.Dirty = FALSE, !.HeadVld = FALSE, !.HeadPtr = Undefined] /\ MemData' = WbMsg.Data - /\ UNCHANGED <> + /\ UNCHANGED <> NI_FAck == /\ ShWbMsg.Cmd = "SHWB_FAck" /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_None", !.Proc = Undefined, !.Data = Undefined] /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.HeadPtr = IF Dir.Dirty THEN ShWbMsg.Proc ELSE Dir.HeadPtr] - /\ UNCHANGED <> + /\ UNCHANGED <> NI_ShWb == /\ ShWbMsg.Cmd = "SHWB_ShWb" @@ -587,18 +581,16 @@ NI_ShWb == !.ShrSet = Dir.ShrSet \cup ({ShWbMsg.Proc} \cap NODE), !.InvSet = Dir.ShrSet \cup ({ShWbMsg.Proc} \cap NODE)] /\ MemData' = ShWbMsg.Data - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Replace(src) == /\ RpMsg[src].Cmd = "RP_Replace" /\ RpMsg' = [RpMsg EXCEPT ![src].Cmd = "RP_None"] /\ 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 <> + /\ UNCHANGED <> ------------------------------------------------------------------------------- (* ABS_* abstract-environment rules *) @@ -620,16 +612,15 @@ ABS_Store(data) == /\ CurrData' = data /\ LastWrVld' = TRUE /\ LastWrPtr' = Other - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_PI_Remote_PutX == /\ Env_o /\ AbsDirtyClean /\ WbMsg' = [WbMsg EXCEPT !.Cmd = "WB_Wb", !.Proc = Other, !.Data = CurrData] - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Local_Get_Get == /\ Env_o @@ -639,8 +630,8 @@ ABS_NI_Local_Get_Get == /\ PendReqSrc' = Other /\ PendReqCmd' = "UNI_Get" /\ Collecting' = FALSE - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Local_Get_Put == /\ Env_o @@ -653,9 +644,8 @@ ABS_NI_Local_Get_Put == 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 <> + /\ UNCHANGED <> \* Abstract remote NAK, source side (merges the former ABS_NI_Remote_Get_Nak_src \* / ABS_NI_Remote_GetX_Nak_src). @@ -667,9 +657,8 @@ ABS_NI_Remote_Nak_src(dst) == /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_Nakc"] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Remote_Get_Nak_dst(src) == /\ Env_o @@ -680,9 +669,8 @@ ABS_NI_Remote_Get_Nak_dst(src) == /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_Nakc"] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = src - /\ UNCHANGED <> + /\ UNCHANGED <> \* Abstract remote NAK, both sides abstract (merges the former \* ABS_NI_Remote_Get_Nak_src_dst / ABS_NI_Remote_GetX_Nak_src_dst). @@ -693,9 +681,8 @@ ABS_NI_Remote_Nak_src_dst == /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_Nakc"] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Remote_Get_Put_src(dst) == /\ Env_o /\ dst # Home @@ -706,9 +693,8 @@ ABS_NI_Remote_Get_Put_src(dst) == /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_ShWb", !.Proc = Other, !.Data = Proc[dst].CacheData] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Remote_Get_Put_dst(src) == /\ Env_o @@ -722,9 +708,8 @@ ABS_NI_Remote_Get_Put_dst(src) == /\ ShWbMsg' = IF src # Home THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_ShWb", !.Proc = src, !.Data = CurrData] ELSE ShWbMsg - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Remote_Get_Put_src_dst == /\ Env_o @@ -734,9 +719,8 @@ ABS_NI_Remote_Get_Put_src_dst == /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_ShWb", !.Proc = Other, !.Data = CurrData] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Local_GetX_GetX == /\ Env_o @@ -746,8 +730,8 @@ ABS_NI_Local_GetX_GetX == /\ PendReqSrc' = Other /\ PendReqCmd' = "UNI_GetX" /\ Collecting' = FALSE - /\ UNCHANGED <> + /\ UNCHANGED <> \* Home holds the line exclusively; the abstract node takes it over. ABS_NI_Local_GetX_PutX_Dirty == @@ -755,7 +739,7 @@ ABS_NI_Local_GetX_PutX_Dirty == /\ Dir' = [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, !.HeadPtr = Other, !.ShrVld = FALSE, !.ShrSet = {}, !.InvSet = {}] /\ Proc' = ProcHomeInvalid - /\ UNCHANGED <> + /\ UNCHANGED <> \* The abstract node is already the head and no concrete node shares the line. ABS_NI_Local_GetX_PutX_Grant == @@ -764,7 +748,7 @@ ABS_NI_Local_GetX_PutX_Grant == /\ Dir' = [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, !.HeadPtr = Other, !.ShrVld = FALSE, !.ShrSet = {}, !.InvSet = {}] /\ Proc' = IF Dir.Local THEN ProcHomeInvalidMarked ELSE ProcHomeInvalid - /\ UNCHANGED <> + /\ UNCHANGED <> \* Concrete nodes share the line: they are invalidated first. ABS_NI_Local_GetX_PutX_Inv == @@ -788,8 +772,8 @@ ABS_NI_Local_GetX_PutX == /\ \/ ABS_NI_Local_GetX_PutX_Dirty \/ ABS_NI_Local_GetX_PutX_Grant \/ ABS_NI_Local_GetX_PutX_Inv - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Remote_GetX_Nak_dst(src) == /\ Env_o @@ -800,9 +784,8 @@ ABS_NI_Remote_GetX_Nak_dst(src) == /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_Nakc"] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = src - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Remote_GetX_PutX_src(dst) == /\ Env_o /\ dst # Home @@ -813,9 +796,8 @@ ABS_NI_Remote_GetX_PutX_src(dst) == /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_FAck", !.Proc = Other, !.Data = Undefined] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Remote_GetX_PutX_dst(src) == /\ Env_o @@ -829,9 +811,8 @@ ABS_NI_Remote_GetX_PutX_dst(src) == /\ ShWbMsg' = IF src # Home THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_FAck", !.Proc = src, !.Data = Undefined] ELSE ShWbMsg - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Remote_GetX_PutX_src_dst == /\ Env_o @@ -841,9 +822,8 @@ ABS_NI_Remote_GetX_PutX_src_dst == /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_FAck", !.Proc = Other, !.Data = Undefined] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other - /\ UNCHANGED <> + /\ UNCHANGED <> \* Concrete nodes have not acked yet, so the round stays open. ABS_NI_InvAck_More == @@ -869,8 +849,8 @@ ABS_NI_InvAck == /\ LastInvAck' = Other /\ \/ ABS_NI_InvAck_More \/ ABS_NI_InvAck_Last - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_ShWb == /\ Env_o @@ -879,9 +859,8 @@ ABS_NI_ShWb == /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.Dirty = FALSE, !.ShrVld = TRUE, !.InvSet = Dir.ShrSet] /\ MemData' = ShWbMsg.Data - /\ UNCHANGED <> + /\ UNCHANGED <> ------------------------------------------------------------------------------- From 5a0560140ba8c75373d92fbaccb211ca4e6b3a61 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Sun, 26 Jul 2026 20:17:21 -0700 Subject: [PATCH 09/17] Drop the write-only ghosts LastWrVld, LastWrPtr and LastInvAck The three record who wrote and who acked last: LastWrVld whether any write has happened, LastWrPtr the writing node, LastInvAck the node whose ack closed the last invalidation round. Nothing reads them. No guard, no other variable's update and no invariant mentions them, in flashWithMutex.m either, where they are equally vestigial -- CacheStateProp, CacheDataProp, MemDataProp, Lemma_1 to Lemma_5 and the Progress1_* invariants all ignore them. They are written by Store, ABS_Store, NI_InvAck and ABS_NI_InvAck and by nothing else. Delete them, together with their TypeOK and Init conjuncts; lastWrVars keeps only CurrData and so dissolves back into that variable. The data properties do rest on history, but on CurrData and PrevData, which record what was written rather than by whom and are kept: CacheDataProp reads both and MemDataProp reads CurrData. Dropping LastInvAck empties a branch of ABS_NI_InvAck. Murphi's rule branches on whether concrete invalidation acks are still outstanding, and that branch assigns only LastInvAck and LastOtherInvAck, both of which this translation omits, so ABS_NI_InvAck_More was left holding every one of the 18 variables unchanged. It was an explicit stuttering step, which a TLA+ spec never needs: Spec uses [Next]_vars and is stuttering-invariant by construction. With only the closing branch left there is nothing to disjoin, so ABS_NI_InvAck_Last is inlined and its guard joins the other guards. Next keeps all 49 actions; only the two sub-action definitions go. Since the three refine the state without constraining it, deleting them quotients the reachable graph rather than preserving it: TLC goes from 414 to 78 distinct states for NODE/DATA = 1/1 and from 929,572 to 131,976 at 2/2, generated states from 4,533,240 to 636,852. The projection onto the surviving 18 variables, and with it every invariant, is unchanged. Of that drop in generated states, 13,384 are the ABS_NI_InvAck self-loops that were computed and then discarded. Proved with TLAPS against the previous form, which carried the three. The variable set shrinks, so the two Next relations cannot be equivalent; what is proved per action is that the old action is the new one conjoined with its constraint on the three, and that every old step is a new step. That constraint never appears in a guard, so it cannot affect whether the action is enabled, and it is a conjunction of equalities fixing all three from the unprimed state, so the old step matching a new one exists and is unique -- the forgetful map is a functional bisimulation, not merely a projection. For 45 of the 49 actions the three are simply left unchanged. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- .../FlashProtocol/FlashWithMutex.tla | 185 ++++++++---------- specifications/FlashProtocol/manifest.json | 6 +- 2 files changed, 84 insertions(+), 107 deletions(-) diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla index 570558c1..52690e60 100644 --- a/specifications/FlashProtocol/FlashWithMutex.tla +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -49,21 +49,16 @@ UniU == UNI_CMD \cup {Undefined} VARIABLES Home, Proc, Dir, MemData, UniMsg, InvMsg, RpMsg, WbMsg, ShWbMsg, NakcMsg, - CurrData, PrevData, LastWrVld, LastWrPtr, PendReqSrc, PendReqCmd, - Collecting, FwdCmd, FwdSrc, LastInvAck, Env_o + CurrData, PrevData, PendReqSrc, PendReqCmd, Collecting, FwdCmd, FwdSrc, Env_o vars == <> + CurrData, PrevData, PendReqSrc, PendReqCmd, Collecting, FwdCmd, FwdSrc, + Env_o>> \* 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 \* action that does change one member spells the group's others out. -\* Who last wrote the line and what they wrote: read only by the data -\* properties, never by a guard. -lastWrVars == <> - \* The request Home is currently working on, and whether it is still waiting \* for invalidation acks. pendVars == <> @@ -89,14 +84,11 @@ TypeOK == /\ NakcMsg \in [Cmd : NAKC_CMD] /\ CurrData \in DATA /\ PrevData \in DATA - /\ LastWrVld \in BOOLEAN - /\ LastWrPtr \in NodeU /\ PendReqSrc \in NodeU /\ PendReqCmd \in UniU /\ Collecting \in BOOLEAN /\ FwdCmd \in UNI_CMD /\ FwdSrc \in NodeU - /\ LastInvAck \in NodeU /\ Env_o \in BOOLEAN ------------------------------------------------------------------------------- @@ -118,14 +110,11 @@ Init == /\ NakcMsg = [Cmd |-> "NAKC_None"] /\ CurrData = d /\ PrevData = d - /\ LastWrVld = FALSE - /\ LastWrPtr = Undefined /\ PendReqSrc = Undefined /\ PendReqCmd = Undefined /\ Collecting = FALSE /\ FwdCmd = "UNI_None" /\ FwdSrc = Undefined - /\ LastInvAck = Undefined /\ Env_o = TRUE ------------------------------------------------------------------------------- @@ -162,10 +151,8 @@ Store(src, data) == /\ Proc[src].CacheState = "CACHE_E" /\ Proc' = [Proc EXCEPT ![src].CacheData = data] /\ CurrData' = data - /\ LastWrVld' = TRUE - /\ LastWrPtr' = src /\ UNCHANGED <> + PrevData, pendVars, fwdVars, Env_o>> \* Shared/exclusive request from a remote processor (merges the former \* PI_Remote_Get / PI_Remote_GetX). @@ -178,7 +165,7 @@ PI_Remote(src, c) == ![src].Proc = Home, ![src].Data = Undefined] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars, Env_o>> PI_Local_Get_Get == /\ Proc[Home].ProcCmd = "NODE_None" @@ -192,8 +179,8 @@ PI_Local_Get_Get == /\ PendReqSrc' = Home /\ PendReqCmd' = "UNI_Get" /\ Collecting' = FALSE - /\ UNCHANGED <> + /\ UNCHANGED <> PI_Local_Get_Put == /\ Proc[Home].ProcCmd = "NODE_None" @@ -205,7 +192,7 @@ PI_Local_Get_Put == ![Home].CacheState = IF Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", ![Home].CacheData = IF Proc[Home].InvMarked THEN Undefined ELSE MemData] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars, Env_o>> PI_Local_GetX_GetX == /\ Proc[Home].ProcCmd = "NODE_None" @@ -219,8 +206,8 @@ PI_Local_GetX_GetX == /\ PendReqSrc' = Home /\ PendReqCmd' = "UNI_GetX" /\ Collecting' = FALSE - /\ UNCHANGED <> + /\ UNCHANGED <> \* The line is shared: the sharers and the head are invalidated first, so \* Home's own request goes pending. @@ -251,8 +238,8 @@ PI_Local_GetX_PutX == ![Home].CacheData = MemData] /\ \/ PI_Local_GetX_PutX_Inv \/ PI_Local_GetX_PutX_Grant - /\ UNCHANGED <> + /\ UNCHANGED <> PI_Remote_PutX(dst) == /\ dst # Home @@ -261,7 +248,7 @@ PI_Remote_PutX(dst) == /\ Proc' = [Proc EXCEPT ![dst].CacheState = "CACHE_I", ![dst].CacheData = Undefined] /\ WbMsg' = [WbMsg EXCEPT !.Cmd = "WB_Wb", !.Proc = dst, !.Data = Proc[dst].CacheData] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars, Env_o>> PI_Local_PutX == /\ Proc[Home].ProcCmd = "NODE_None" @@ -269,8 +256,8 @@ PI_Local_PutX == /\ Proc' = [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] /\ Dir' = [Dir EXCEPT !.Dirty = FALSE, !.Local = IF Dir.Pending THEN Dir.Local ELSE FALSE] /\ MemData' = Proc[Home].CacheData - /\ UNCHANGED <> + /\ UNCHANGED <> PI_Remote_Replace(src) == /\ src # Home @@ -279,7 +266,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, Env_o>> PI_Local_Replace == /\ Proc[Home].ProcCmd = "NODE_None" @@ -287,21 +274,21 @@ PI_Local_Replace == /\ Dir' = [Dir EXCEPT !.Local = FALSE] /\ Proc' = [Proc EXCEPT ![Home].CacheState = "CACHE_I", ![Home].CacheData = Undefined] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars, Env_o>> NI_Nak(dst) == /\ UniMsg[dst].Cmd = "UNI_Nak" /\ UniMsg' = [UniMsg EXCEPT ![dst].Cmd = "UNI_None", ![dst].Proc = Undefined, ![dst].Data = Undefined] /\ Proc' = [Proc EXCEPT ![dst].ProcCmd = "NODE_None", ![dst].InvMarked = FALSE] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars, Env_o>> NI_Nak_Clear == /\ NakcMsg.Cmd = "NAKC_Nakc" /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_None"] /\ Dir' = [Dir EXCEPT !.Pending = FALSE] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars, Env_o>> NI_Local_Get_Nak(src) == /\ src # Home @@ -313,7 +300,7 @@ NI_Local_Get_Nak(src) == \/ (Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr = src) /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_Nak", ![src].Proc = Home, ![src].Data = Undefined] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars, Env_o>> NI_Local_Get_Get(src) == /\ src # Home @@ -328,7 +315,7 @@ NI_Local_Get_Get(src) == /\ PendReqCmd' = "UNI_Get" /\ Collecting' = FALSE /\ UNCHANGED <> + CurrData, PrevData, FwdSrc, Env_o>> NI_Local_Get_Put(src) == /\ src # Home @@ -350,8 +337,8 @@ NI_Local_Get_Put(src) == ![src].Data = Proc[Home].CacheData] ELSE [UniMsg EXCEPT ![src].Cmd = "UNI_Put", ![src].Proc = Home, ![src].Data = MemData] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Remote NAK of a shared/exclusive request (merges the former \* NI_Remote_Get_Nak / NI_Remote_GetX_Nak). @@ -364,8 +351,8 @@ NI_Remote_Nak(src, dst) == /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_Nakc"] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = src - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Remote_Get_Put(src, dst) == /\ src # dst /\ dst # Home @@ -380,8 +367,8 @@ NI_Remote_Get_Put(src, dst) == /\ ShWbMsg' = IF src # Home THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_ShWb", !.Proc = src, !.Data = Proc[dst].CacheData] ELSE ShWbMsg - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Local_GetX_Nak(src) == /\ src # Home @@ -392,7 +379,7 @@ NI_Local_GetX_Nak(src) == \/ (Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr = src) /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_Nak", ![src].Proc = Home, ![src].Data = Undefined] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars, Env_o>> NI_Local_GetX_GetX(src) == /\ src # Home @@ -406,7 +393,7 @@ NI_Local_GetX_GetX(src) == /\ PendReqCmd' = "UNI_GetX" /\ Collecting' = FALSE /\ UNCHANGED <> + CurrData, PrevData, FwdSrc, Env_o>> \* Home holds the line exclusively, so it can be handed to src directly. NI_Local_GetX_PutX_Dirty(src) == @@ -457,8 +444,8 @@ 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 @@ -473,8 +460,8 @@ NI_Remote_GetX_PutX(src, dst) == /\ ShWbMsg' = IF src # Home THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_FAck", !.Proc = src, !.Data = Undefined] ELSE ShWbMsg - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Local_Put == /\ UniMsg[Home].Cmd = "UNI_Put" @@ -485,8 +472,8 @@ NI_Local_Put == ![Home].InvMarked = FALSE, ![Home].CacheState = IF Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", ![Home].CacheData = IF Proc[Home].InvMarked THEN Undefined ELSE UniMsg[Home].Data] - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Remote_Put(dst) == /\ dst # Home @@ -497,7 +484,7 @@ NI_Remote_Put(dst) == ![dst].CacheState = IF Proc[dst].InvMarked THEN "CACHE_I" ELSE "CACHE_S", ![dst].CacheData = IF Proc[dst].InvMarked THEN Undefined ELSE UniMsg[dst].Data] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars, Env_o>> NI_Local_PutXAcksDone == /\ UniMsg[Home].Cmd = "UNI_PutX" @@ -507,8 +494,8 @@ NI_Local_PutXAcksDone == ![Home].InvMarked = FALSE, ![Home].CacheState = "CACHE_E", ![Home].CacheData = UniMsg[Home].Data] - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Remote_PutX(dst) == /\ dst # Home @@ -520,7 +507,7 @@ NI_Remote_PutX(dst) == ![dst].CacheState = "CACHE_E", ![dst].CacheData = UniMsg[dst].Data] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars, Env_o>> NI_Inv(dst) == /\ dst # Home @@ -531,7 +518,7 @@ NI_Inv(dst) == ![dst].InvMarked = IF Proc[dst].ProcCmd = "NODE_Get" THEN TRUE ELSE Proc[dst].InvMarked] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars, Env_o>> \* Acks are still outstanding: only this one is recorded. NI_InvAck_More(src) == @@ -551,26 +538,25 @@ NI_InvAck(src) == /\ InvMsg[src].Cmd = "INV_InvAck" /\ Dir.Pending /\ src \in Dir.InvSet /\ InvMsg' = [InvMsg EXCEPT ![src].Cmd = "INV_None"] - /\ LastInvAck' = src /\ \/ NI_InvAck_More(src) \/ NI_InvAck_Last(src) /\ UNCHANGED <> + CurrData, PrevData, PendReqSrc, PendReqCmd, fwdVars, Env_o>> NI_Wb == /\ WbMsg.Cmd = "WB_Wb" /\ WbMsg' = [WbMsg EXCEPT !.Cmd = "WB_None", !.Proc = Undefined, !.Data = Undefined] /\ Dir' = [Dir EXCEPT !.Dirty = FALSE, !.HeadVld = FALSE, !.HeadPtr = Undefined] /\ MemData' = WbMsg.Data - /\ UNCHANGED <> + /\ UNCHANGED <> NI_FAck == /\ ShWbMsg.Cmd = "SHWB_FAck" /\ ShWbMsg' = [ShWbMsg EXCEPT !.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, Env_o>> NI_ShWb == /\ ShWbMsg.Cmd = "SHWB_ShWb" @@ -581,8 +567,8 @@ NI_ShWb == !.ShrSet = Dir.ShrSet \cup ({ShWbMsg.Proc} \cap NODE), !.InvSet = Dir.ShrSet \cup ({ShWbMsg.Proc} \cap NODE)] /\ MemData' = ShWbMsg.Data - /\ UNCHANGED <> + /\ UNCHANGED <> NI_Replace(src) == /\ RpMsg[src].Cmd = "RP_Replace" @@ -590,7 +576,7 @@ 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 <> + CurrData, PrevData, pendVars, fwdVars, Env_o>> ------------------------------------------------------------------------------- (* ABS_* abstract-environment rules *) @@ -610,17 +596,15 @@ ABS_Store(data) == /\ Env_o /\ AbsDirtyClean /\ CurrData' = data - /\ LastWrVld' = TRUE - /\ LastWrPtr' = Other /\ UNCHANGED <> + NakcMsg, PrevData, pendVars, fwdVars, Env_o>> ABS_PI_Remote_PutX == /\ Env_o /\ AbsDirtyClean /\ WbMsg' = [WbMsg EXCEPT !.Cmd = "WB_Wb", !.Proc = Other, !.Data = CurrData] /\ UNCHANGED <> + CurrData, PrevData, pendVars, fwdVars, Env_o>> ABS_NI_Local_Get_Get == /\ Env_o @@ -631,7 +615,7 @@ ABS_NI_Local_Get_Get == /\ PendReqCmd' = "UNI_Get" /\ Collecting' = FALSE /\ UNCHANGED <> + CurrData, PrevData, FwdSrc, Env_o>> ABS_NI_Local_Get_Put == /\ Env_o @@ -644,8 +628,8 @@ ABS_NI_Local_Get_Put == 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 <> + /\ UNCHANGED <> \* Abstract remote NAK, source side (merges the former ABS_NI_Remote_Get_Nak_src \* / ABS_NI_Remote_GetX_Nak_src). @@ -658,7 +642,7 @@ ABS_NI_Remote_Nak_src(dst) == /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other /\ UNCHANGED <> + CurrData, PrevData, pendVars, Env_o>> ABS_NI_Remote_Get_Nak_dst(src) == /\ Env_o @@ -669,8 +653,8 @@ ABS_NI_Remote_Get_Nak_dst(src) == /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_Nakc"] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = src - /\ UNCHANGED <> + /\ UNCHANGED <> \* Abstract remote NAK, both sides abstract (merges the former \* ABS_NI_Remote_Get_Nak_src_dst / ABS_NI_Remote_GetX_Nak_src_dst). @@ -682,7 +666,7 @@ ABS_NI_Remote_Nak_src_dst == /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other /\ UNCHANGED <> + CurrData, PrevData, pendVars, Env_o>> ABS_NI_Remote_Get_Put_src(dst) == /\ Env_o /\ dst # Home @@ -693,8 +677,8 @@ ABS_NI_Remote_Get_Put_src(dst) == /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_ShWb", !.Proc = Other, !.Data = Proc[dst].CacheData] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Remote_Get_Put_dst(src) == /\ Env_o @@ -708,8 +692,8 @@ ABS_NI_Remote_Get_Put_dst(src) == /\ ShWbMsg' = IF src # Home THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_ShWb", !.Proc = src, !.Data = CurrData] ELSE ShWbMsg - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Remote_Get_Put_src_dst == /\ Env_o @@ -720,7 +704,7 @@ ABS_NI_Remote_Get_Put_src_dst == /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other /\ UNCHANGED <> + CurrData, PrevData, pendVars, Env_o>> ABS_NI_Local_GetX_GetX == /\ Env_o @@ -731,7 +715,7 @@ ABS_NI_Local_GetX_GetX == /\ PendReqCmd' = "UNI_GetX" /\ Collecting' = FALSE /\ UNCHANGED <> + CurrData, PrevData, FwdSrc, Env_o>> \* Home holds the line exclusively; the abstract node takes it over. ABS_NI_Local_GetX_PutX_Dirty == @@ -772,8 +756,8 @@ ABS_NI_Local_GetX_PutX == /\ \/ ABS_NI_Local_GetX_PutX_Dirty \/ ABS_NI_Local_GetX_PutX_Grant \/ ABS_NI_Local_GetX_PutX_Inv - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Remote_GetX_Nak_dst(src) == /\ Env_o @@ -784,8 +768,8 @@ ABS_NI_Remote_GetX_Nak_dst(src) == /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_Nakc"] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = src - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Remote_GetX_PutX_src(dst) == /\ Env_o /\ dst # Home @@ -796,8 +780,8 @@ ABS_NI_Remote_GetX_PutX_src(dst) == /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_FAck", !.Proc = Other, !.Data = Undefined] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Remote_GetX_PutX_dst(src) == /\ Env_o @@ -811,8 +795,8 @@ ABS_NI_Remote_GetX_PutX_dst(src) == /\ ShWbMsg' = IF src # Home THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_FAck", !.Proc = src, !.Data = Undefined] ELSE ShWbMsg - /\ UNCHANGED <> + /\ UNCHANGED <> ABS_NI_Remote_GetX_PutX_src_dst == /\ Env_o @@ -823,34 +807,27 @@ ABS_NI_Remote_GetX_PutX_src_dst == /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other /\ UNCHANGED <> - -\* Concrete nodes have not acked yet, so the round stays open. -ABS_NI_InvAck_More == - /\ Dir.InvSet # {} - /\ UNCHANGED <> + CurrData, PrevData, pendVars, Env_o>> \* All concrete nodes have acked: the round closes and the request retires. -ABS_NI_InvAck_Last == - /\ Dir.InvSet = {} - /\ Dir' = [Dir EXCEPT !.Pending = FALSE, - !.Local = IF Dir.Local /\ ~Dir.Dirty THEN FALSE ELSE Dir.Local] - /\ Collecting' = FALSE - +\* 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)) - /\ LastInvAck' = Other - /\ \/ ABS_NI_InvAck_More - \/ ABS_NI_InvAck_Last + /\ Dir' = [Dir EXCEPT !.Pending = FALSE, + !.Local = IF Dir.Local /\ ~Dir.Dirty THEN FALSE ELSE Dir.Local] + /\ Collecting' = FALSE /\ UNCHANGED <> + CurrData, PrevData, PendReqSrc, PendReqCmd, fwdVars, Env_o>> ABS_NI_ShWb == /\ Env_o @@ -859,8 +836,8 @@ ABS_NI_ShWb == /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.Dirty = FALSE, !.ShrVld = TRUE, !.InvSet = Dir.ShrSet] /\ MemData' = ShWbMsg.Data - /\ UNCHANGED <> + /\ UNCHANGED <> ------------------------------------------------------------------------------- diff --git a/specifications/FlashProtocol/manifest.json b/specifications/FlashProtocol/manifest.json index 33a61802..09533ad2 100644 --- a/specifications/FlashProtocol/manifest.json +++ b/specifications/FlashProtocol/manifest.json @@ -23,9 +23,9 @@ "runtime": "00:00:01", "mode": "exhaustive search", "result": "success", - "distinctStates": 414, - "totalStates": 1231, - "stateDepth": 13 + "distinctStates": 78, + "totalStates": 241, + "stateDepth": 9 } ] } From c434377fd62d1a4646cf8aab1ae370cd0b0e95a9 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Sun, 26 Jul 2026 20:20:35 -0700 Subject: [PATCH 10/17] Document the history variables CurrData and PrevData are what is left of the model's history variables now that the write-only ghosts are gone, and neither is self-explanatory at its declaration: CurrData is read by the ABS_* actions as well as by the data properties, so it is not merely auxiliary, while PrevData is read by nothing but CacheDataProp's Collecting case. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- specifications/FlashProtocol/FlashWithMutex.tla | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla index 52690e60..6b8441ba 100644 --- a/specifications/FlashProtocol/FlashWithMutex.tla +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -55,6 +55,12 @@ vars == <> +\* 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. + \* 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 \* action that does change one member spells the group's others out. From 8db8885448ddc5a332baa76f59fbb9005e44e5b8 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 27 Jul 2026 09:58:05 -0700 Subject: [PATCH 11/17] Assign whole records where an action writes all of their fields Every update of UniMsg, InvMsg, RpMsg, WbMsg, ShWbMsg and NakcMsg assigns all of the record's fields, as do six of the Proc updates and three of the Dir ones. Written as a field-wise EXCEPT, such an update preserves the record type only by inheritance from the old value, and a forgotten field silently keeps whatever was there before -- a stale .Data on a UNI_Nak, say. Replace those 57 updates by record literals: the function-valued ones become [UniMsg EXCEPT ![src] = [Cmd |-> ..., Proc |-> ..., Data |-> ...]], and since WbMsg, ShWbMsg and NakcMsg are plain records, their 20 updates drop the EXCEPT altogether. Fields follow TypeOK's order. Partial updates of Proc and Dir keep their EXCEPT, where carrying the other fields over is the point. Proved behaviour-preserving with TLAPS: per action, Next and Init are equivalent to the previous field-wise form. The equivalence needs TypeOK, and needs it only of the record being updated -- [r EXCEPT !.a = x, !.b = y] and [a |-> x, b |-> y] agree exactly when r has the fields a and b and no others. One bridge lemma per record shape discharges that; the values written need no hypothesis, which is the point of the change. TLC is unchanged at 241/78 states for NODE/DATA = 1/1 and 650,236/131,976 at 2/2. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- .../FlashProtocol/FlashWithMutex.tla | 175 +++++++++--------- 1 file changed, 83 insertions(+), 92 deletions(-) diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla index 6b8441ba..ed48ceec 100644 --- a/specifications/FlashProtocol/FlashWithMutex.tla +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -167,9 +167,8 @@ PI_Remote(src, c) == /\ Proc[src].ProcCmd = "NODE_None" /\ Proc[src].CacheState = "CACHE_I" /\ Proc' = [Proc EXCEPT ![src].ProcCmd = IF c = "Get" THEN "NODE_Get" ELSE "NODE_GetX"] - /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = IF c = "Get" THEN "UNI_Get" ELSE "UNI_GetX", - ![src].Proc = Home, - ![src].Data = Undefined] + /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> IF c = "Get" THEN "UNI_Get" ELSE "UNI_GetX", + Proc |-> Home, Data |-> Undefined]] /\ UNCHANGED <> @@ -179,8 +178,8 @@ PI_Local_Get_Get == /\ ~Dir.Pending /\ Dir.Dirty /\ Proc' = [Proc EXCEPT ![Home].ProcCmd = "NODE_Get"] /\ Dir' = [Dir EXCEPT !.Pending = TRUE] - /\ UniMsg' = [UniMsg EXCEPT ![Home].Cmd = "UNI_Get", ![Home].Proc = Dir.HeadPtr, - ![Home].Data = Undefined] + /\ UniMsg' = [UniMsg EXCEPT ![Home] = [Cmd |-> "UNI_Get", Proc |-> Dir.HeadPtr, + Data |-> Undefined]] /\ FwdCmd' = IF Dir.HeadPtr # Home THEN "UNI_Get" ELSE FwdCmd /\ PendReqSrc' = Home /\ PendReqCmd' = "UNI_Get" @@ -193,10 +192,9 @@ PI_Local_Get_Put == /\ Proc[Home].CacheState = "CACHE_I" /\ ~Dir.Pending /\ ~Dir.Dirty /\ Dir' = [Dir EXCEPT !.Local = TRUE] - /\ Proc' = [Proc EXCEPT ![Home].ProcCmd = "NODE_None", - ![Home].InvMarked = FALSE, - ![Home].CacheState = IF Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", - ![Home].CacheData = IF Proc[Home].InvMarked THEN Undefined ELSE MemData] + /\ Proc' = [Proc EXCEPT ![Home] = [ProcCmd |-> "NODE_None", InvMarked |-> FALSE, + CacheState |-> IF Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", + CacheData |-> IF Proc[Home].InvMarked THEN Undefined ELSE MemData]] /\ UNCHANGED <> @@ -206,8 +204,8 @@ PI_Local_GetX_GetX == /\ ~Dir.Pending /\ Dir.Dirty /\ Proc' = [Proc EXCEPT ![Home].ProcCmd = "NODE_GetX"] /\ Dir' = [Dir EXCEPT !.Pending = TRUE] - /\ UniMsg' = [UniMsg EXCEPT ![Home].Cmd = "UNI_GetX", ![Home].Proc = Dir.HeadPtr, - ![Home].Data = Undefined] + /\ UniMsg' = [UniMsg EXCEPT ![Home] = [Cmd |-> "UNI_GetX", Proc |-> Dir.HeadPtr, + Data |-> Undefined]] /\ FwdCmd' = IF Dir.HeadPtr # Home THEN "UNI_GetX" ELSE FwdCmd /\ PendReqSrc' = Home /\ PendReqCmd' = "UNI_GetX" @@ -219,9 +217,8 @@ PI_Local_GetX_GetX == \* Home's own request goes pending. PI_Local_GetX_PutX_Inv == /\ Dir.HeadVld - /\ Dir' = [Dir EXCEPT !.Local = TRUE, !.Dirty = TRUE, !.Pending = TRUE, - !.HeadVld = FALSE, !.HeadPtr = Undefined, !.ShrVld = FALSE, - !.ShrSet = {}, !.InvSet = InvNodes({Home})] + /\ Dir' = [Pending |-> TRUE, Local |-> TRUE, Dirty |-> TRUE, HeadVld |-> FALSE, + HeadPtr |-> Undefined, ShrVld |-> FALSE, ShrSet |-> {}, InvSet |-> InvNodes({Home})] /\ InvMsg' = [p \in NODE |-> [Cmd |-> IF p \in InvNodes({Home}) THEN "INV_Inv" ELSE "INV_None"]] /\ PendReqSrc' = Home @@ -238,10 +235,8 @@ PI_Local_GetX_PutX == /\ Proc[Home].ProcCmd = "NODE_None" /\ Proc[Home].CacheState \in {"CACHE_I", "CACHE_S"} /\ ~Dir.Pending /\ ~Dir.Dirty - /\ Proc' = [Proc EXCEPT ![Home].ProcCmd = "NODE_None", - ![Home].InvMarked = FALSE, - ![Home].CacheState = "CACHE_E", - ![Home].CacheData = MemData] + /\ Proc' = [Proc EXCEPT ![Home] = [ProcCmd |-> "NODE_None", InvMarked |-> FALSE, + CacheState |-> "CACHE_E", CacheData |-> MemData]] /\ \/ PI_Local_GetX_PutX_Inv \/ PI_Local_GetX_PutX_Grant /\ UNCHANGED < "WB_Wb", Proc |-> dst, Data |-> Proc[dst].CacheData] /\ UNCHANGED <> @@ -270,7 +265,7 @@ PI_Remote_Replace(src) == /\ Proc[src].ProcCmd = "NODE_None" /\ Proc[src].CacheState = "CACHE_S" /\ Proc' = [Proc EXCEPT ![src].CacheState = "CACHE_I", ![src].CacheData = Undefined] - /\ RpMsg' = [RpMsg EXCEPT ![src].Cmd = "RP_Replace"] + /\ RpMsg' = [RpMsg EXCEPT ![src] = [Cmd |-> "RP_Replace"]] /\ UNCHANGED <> @@ -284,14 +279,15 @@ PI_Local_Replace == NI_Nak(dst) == /\ UniMsg[dst].Cmd = "UNI_Nak" - /\ UniMsg' = [UniMsg EXCEPT ![dst].Cmd = "UNI_None", ![dst].Proc = Undefined, ![dst].Data = Undefined] + /\ UniMsg' = [UniMsg EXCEPT ![dst] = [Cmd |-> "UNI_None", Proc |-> Undefined, + Data |-> Undefined]] /\ Proc' = [Proc EXCEPT ![dst].ProcCmd = "NODE_None", ![dst].InvMarked = FALSE] /\ UNCHANGED <> NI_Nak_Clear == /\ NakcMsg.Cmd = "NAKC_Nakc" - /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_None"] + /\ NakcMsg' = [Cmd |-> "NAKC_None"] /\ Dir' = [Dir EXCEPT !.Pending = FALSE] /\ UNCHANGED <> @@ -304,7 +300,7 @@ NI_Local_Get_Nak(src) == /\ \/ Dir.Pending \/ (Dir.Dirty /\ Dir.Local /\ Proc[Home].CacheState # "CACHE_E") \/ (Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr = src) - /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_Nak", ![src].Proc = Home, ![src].Data = Undefined] + /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Nak", Proc |-> Home, Data |-> Undefined]] /\ UNCHANGED <> @@ -315,7 +311,8 @@ NI_Local_Get_Get(src) == /\ RpMsg[src].Cmd # "RP_Replace" /\ ~Dir.Pending /\ Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr # src /\ Dir' = [Dir EXCEPT !.Pending = TRUE] - /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_Get", ![src].Proc = Dir.HeadPtr, ![src].Data = Undefined] + /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Get", Proc |-> Dir.HeadPtr, + Data |-> Undefined]] /\ FwdCmd' = IF Dir.HeadPtr # Home THEN "UNI_Get" ELSE FwdCmd /\ PendReqSrc' = src /\ PendReqCmd' = "UNI_Get" @@ -339,10 +336,9 @@ NI_Local_Get_Put(src) == /\ MemData' = IF Dir.Dirty THEN Proc[Home].CacheData ELSE MemData /\ Proc' = IF Dir.Dirty THEN [Proc EXCEPT ![Home].CacheState = "CACHE_S"] ELSE Proc /\ UniMsg' = IF Dir.Dirty - THEN [UniMsg EXCEPT ![src].Cmd = "UNI_Put", ![src].Proc = Home, - ![src].Data = Proc[Home].CacheData] - ELSE [UniMsg EXCEPT ![src].Cmd = "UNI_Put", ![src].Proc = Home, - ![src].Data = MemData] + THEN [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Put", Proc |-> Home, + Data |-> Proc[Home].CacheData]] + ELSE [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Put", Proc |-> Home, Data |-> MemData]] /\ UNCHANGED <> @@ -353,8 +349,8 @@ NI_Remote_Nak(src, dst) == /\ UniMsg[src].Cmd \in {"UNI_Get", "UNI_GetX"} /\ UniMsg[src].Proc = dst /\ Proc[dst].CacheState # "CACHE_E" - /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_Nak", ![src].Proc = dst, ![src].Data = Undefined] - /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_Nakc"] + /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Nak", Proc |-> dst, Data |-> Undefined]] + /\ NakcMsg' = [Cmd |-> "NAKC_Nakc"] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = src /\ UNCHANGED < "UNI_Put", Proc |-> dst, + Data |-> Proc[dst].CacheData]] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = src /\ ShWbMsg' = IF src # Home - THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_ShWb", !.Proc = src, !.Data = Proc[dst].CacheData] + THEN [Cmd |-> "SHWB_ShWb", Proc |-> src, Data |-> Proc[dst].CacheData] ELSE ShWbMsg /\ UNCHANGED <> @@ -383,7 +379,7 @@ NI_Local_GetX_Nak(src) == /\ \/ Dir.Pending \/ (Dir.Dirty /\ Dir.Local /\ Proc[Home].CacheState # "CACHE_E") \/ (Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr = src) - /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_Nak", ![src].Proc = Home, ![src].Data = Undefined] + /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Nak", Proc |-> Home, Data |-> Undefined]] /\ UNCHANGED <> @@ -393,7 +389,8 @@ NI_Local_GetX_GetX(src) == /\ UniMsg[src].Proc = Home /\ ~Dir.Pending /\ Dir.Dirty /\ ~Dir.Local /\ Dir.HeadPtr # src /\ Dir' = [Dir EXCEPT !.Pending = TRUE] - /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_GetX", ![src].Proc = Dir.HeadPtr, ![src].Data = Undefined] + /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_GetX", Proc |-> Dir.HeadPtr, + Data |-> Undefined]] /\ FwdCmd' = IF Dir.HeadPtr # Home THEN "UNI_GetX" ELSE FwdCmd /\ PendReqSrc' = src /\ PendReqCmd' = "UNI_GetX" @@ -406,8 +403,8 @@ NI_Local_GetX_PutX_Dirty(src) == /\ Dir.Dirty /\ Dir' = [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, !.HeadPtr = src, !.ShrVld = FALSE, !.ShrSet = {}, !.InvSet = {}] - /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = Home, - ![src].Data = Proc[Home].CacheData] + /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_PutX", Proc |-> Home, + Data |-> Proc[Home].CacheData]] /\ Proc' = ProcHomeInvalid /\ UNCHANGED <> @@ -418,8 +415,7 @@ NI_Local_GetX_PutX_Grant(src) == /\ NoOtherSharers(src) /\ Dir' = [Dir EXCEPT !.Local = FALSE, !.Dirty = TRUE, !.HeadVld = TRUE, !.HeadPtr = src, !.ShrVld = FALSE, !.ShrSet = {}, !.InvSet = {}] - /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = Home, - ![src].Data = MemData] + /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_PutX", Proc |-> Home, Data |-> MemData]] /\ Proc' = IF Dir.Local THEN ProcHomeInvalidMarked ELSE ProcHomeInvalid /\ UNCHANGED <> @@ -428,11 +424,9 @@ NI_Local_GetX_PutX_Grant(src) == NI_Local_GetX_PutX_Inv(src) == /\ ~Dir.Dirty /\ ~NoOtherSharers(src) - /\ Dir' = [Dir EXCEPT !.Pending = TRUE, !.Local = FALSE, !.Dirty = TRUE, - !.HeadVld = TRUE, !.HeadPtr = src, !.ShrVld = FALSE, - !.ShrSet = {}, !.InvSet = InvNodes({Home, src})] - /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = Home, - ![src].Data = MemData] + /\ Dir' = [Pending |-> TRUE, Local |-> FALSE, Dirty |-> TRUE, HeadVld |-> TRUE, HeadPtr |-> src, + ShrVld |-> FALSE, ShrSet |-> {}, InvSet |-> InvNodes({Home, src})] + /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_PutX", Proc |-> Home, Data |-> MemData]] /\ Proc' = IF Dir.Local THEN ProcHomeInvalidMarked ELSE Proc /\ InvMsg' = [p \in NODE |-> [Cmd |-> IF p \in InvNodes({Home, src}) THEN "INV_Inv" ELSE "INV_None"]] @@ -459,47 +453,46 @@ NI_Remote_GetX_PutX(src, dst) == /\ UniMsg[src].Proc = dst /\ Proc[dst].CacheState = "CACHE_E" /\ Proc' = [Proc EXCEPT ![dst].CacheState = "CACHE_I", ![dst].CacheData = Undefined] - /\ UniMsg' = [UniMsg EXCEPT ![src].Cmd = "UNI_PutX", ![src].Proc = dst, - ![src].Data = Proc[dst].CacheData] + /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_PutX", Proc |-> dst, + Data |-> Proc[dst].CacheData]] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = src /\ ShWbMsg' = IF src # Home - THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_FAck", !.Proc = src, !.Data = Undefined] + THEN [Cmd |-> "SHWB_FAck", Proc |-> src, Data |-> Undefined] ELSE ShWbMsg /\ UNCHANGED <> NI_Local_Put == /\ UniMsg[Home].Cmd = "UNI_Put" - /\ UniMsg' = [UniMsg EXCEPT ![Home].Cmd = "UNI_None", ![Home].Proc = Undefined, ![Home].Data = Undefined] + /\ UniMsg' = [UniMsg EXCEPT ![Home] = [Cmd |-> "UNI_None", Proc |-> Undefined, + Data |-> Undefined]] /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.Dirty = FALSE, !.Local = TRUE] /\ MemData' = UniMsg[Home].Data - /\ Proc' = [Proc EXCEPT ![Home].ProcCmd = "NODE_None", - ![Home].InvMarked = FALSE, - ![Home].CacheState = IF Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", - ![Home].CacheData = IF Proc[Home].InvMarked THEN Undefined ELSE UniMsg[Home].Data] + /\ Proc' = [Proc EXCEPT ![Home] = [ProcCmd |-> "NODE_None", InvMarked |-> FALSE, + CacheState |-> IF Proc[Home].InvMarked THEN "CACHE_I" ELSE "CACHE_S", + CacheData |-> IF Proc[Home].InvMarked THEN Undefined ELSE UniMsg[Home].Data]] /\ UNCHANGED <> NI_Remote_Put(dst) == /\ dst # Home /\ UniMsg[dst].Cmd = "UNI_Put" - /\ UniMsg' = [UniMsg EXCEPT ![dst].Cmd = "UNI_None", ![dst].Proc = Undefined, ![dst].Data = Undefined] - /\ Proc' = [Proc EXCEPT ![dst].ProcCmd = "NODE_None", - ![dst].InvMarked = FALSE, - ![dst].CacheState = IF Proc[dst].InvMarked THEN "CACHE_I" ELSE "CACHE_S", - ![dst].CacheData = IF Proc[dst].InvMarked THEN Undefined ELSE UniMsg[dst].Data] + /\ UniMsg' = [UniMsg EXCEPT ![dst] = [Cmd |-> "UNI_None", Proc |-> Undefined, + Data |-> Undefined]] + /\ Proc' = [Proc EXCEPT ![dst] = [ProcCmd |-> "NODE_None", InvMarked |-> FALSE, + CacheState |-> IF Proc[dst].InvMarked THEN "CACHE_I" ELSE "CACHE_S", + CacheData |-> IF Proc[dst].InvMarked THEN Undefined ELSE UniMsg[dst].Data]] /\ UNCHANGED <> NI_Local_PutXAcksDone == /\ UniMsg[Home].Cmd = "UNI_PutX" - /\ UniMsg' = [UniMsg EXCEPT ![Home].Cmd = "UNI_None", ![Home].Proc = Undefined, ![Home].Data = Undefined] + /\ UniMsg' = [UniMsg EXCEPT ![Home] = [Cmd |-> "UNI_None", Proc |-> Undefined, + Data |-> Undefined]] /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.Local = TRUE, !.HeadVld = FALSE, !.HeadPtr = Undefined] - /\ Proc' = [Proc EXCEPT ![Home].ProcCmd = "NODE_None", - ![Home].InvMarked = FALSE, - ![Home].CacheState = "CACHE_E", - ![Home].CacheData = UniMsg[Home].Data] + /\ Proc' = [Proc EXCEPT ![Home] = [ProcCmd |-> "NODE_None", InvMarked |-> FALSE, + CacheState |-> "CACHE_E", CacheData |-> UniMsg[Home].Data]] /\ UNCHANGED <> @@ -507,18 +500,17 @@ NI_Remote_PutX(dst) == /\ dst # Home /\ UniMsg[dst].Cmd = "UNI_PutX" /\ Proc[dst].ProcCmd = "NODE_GetX" - /\ UniMsg' = [UniMsg EXCEPT ![dst].Cmd = "UNI_None", ![dst].Proc = Undefined, ![dst].Data = Undefined] - /\ Proc' = [Proc EXCEPT ![dst].ProcCmd = "NODE_None", - ![dst].InvMarked = FALSE, - ![dst].CacheState = "CACHE_E", - ![dst].CacheData = UniMsg[dst].Data] + /\ UniMsg' = [UniMsg EXCEPT ![dst] = [Cmd |-> "UNI_None", Proc |-> Undefined, + Data |-> Undefined]] + /\ Proc' = [Proc EXCEPT ![dst] = [ProcCmd |-> "NODE_None", InvMarked |-> FALSE, + CacheState |-> "CACHE_E", CacheData |-> UniMsg[dst].Data]] /\ UNCHANGED <> NI_Inv(dst) == /\ dst # Home /\ InvMsg[dst].Cmd = "INV_Inv" - /\ InvMsg' = [InvMsg EXCEPT ![dst].Cmd = "INV_InvAck"] + /\ InvMsg' = [InvMsg EXCEPT ![dst] = [Cmd |-> "INV_InvAck"]] /\ Proc' = [Proc EXCEPT ![dst].CacheState = "CACHE_I", ![dst].CacheData = Undefined, ![dst].InvMarked = IF Proc[dst].ProcCmd = "NODE_Get" THEN TRUE @@ -543,7 +535,7 @@ NI_InvAck(src) == /\ src # Home /\ InvMsg[src].Cmd = "INV_InvAck" /\ Dir.Pending /\ src \in Dir.InvSet - /\ InvMsg' = [InvMsg EXCEPT ![src].Cmd = "INV_None"] + /\ InvMsg' = [InvMsg EXCEPT ![src] = [Cmd |-> "INV_None"]] /\ \/ NI_InvAck_More(src) \/ NI_InvAck_Last(src) /\ UNCHANGED < "WB_None", Proc |-> Undefined, Data |-> Undefined] /\ Dir' = [Dir EXCEPT !.Dirty = FALSE, !.HeadVld = FALSE, !.HeadPtr = Undefined] /\ MemData' = WbMsg.Data /\ UNCHANGED < "SHWB_None", Proc |-> Undefined, Data |-> Undefined] /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.HeadPtr = IF Dir.Dirty THEN ShWbMsg.Proc ELSE Dir.HeadPtr] /\ UNCHANGED <> NI_ShWb == /\ ShWbMsg.Cmd = "SHWB_ShWb" - /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_None", !.Proc = Undefined, !.Data = Undefined] + /\ 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, @@ -578,7 +570,7 @@ NI_ShWb == NI_Replace(src) == /\ RpMsg[src].Cmd = "RP_Replace" - /\ RpMsg' = [RpMsg EXCEPT ![src].Cmd = "RP_None"] + /\ RpMsg' = [RpMsg EXCEPT ![src] = [Cmd |-> "RP_None"]] /\ 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 < "WB_Wb", Proc |-> Other, Data |-> CurrData] /\ UNCHANGED <> @@ -644,7 +636,7 @@ ABS_NI_Remote_Nak_src(dst) == /\ Proc[dst].CacheState # "CACHE_E" /\ Dir.Pending /\ ~Dir.Local /\ PendReqSrc = Other /\ FwdCmd \in {"UNI_Get", "UNI_GetX"} - /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_Nakc"] + /\ NakcMsg' = [Cmd |-> "NAKC_Nakc"] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other /\ UNCHANGED < "UNI_Nak", Proc |-> Other, Data |-> Undefined]] + /\ NakcMsg' = [Cmd |-> "NAKC_Nakc"] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = src /\ UNCHANGED < "NAKC_Nakc"] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other /\ UNCHANGED < "SHWB_ShWb", Proc |-> Other, Data |-> Proc[dst].CacheData] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other /\ UNCHANGED < "UNI_Put", Proc |-> Other, Data |-> CurrData]] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = src /\ ShWbMsg' = IF src # Home - THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_ShWb", !.Proc = src, !.Data = CurrData] + THEN [Cmd |-> "SHWB_ShWb", Proc |-> src, Data |-> CurrData] ELSE ShWbMsg /\ UNCHANGED <> @@ -706,7 +698,7 @@ ABS_NI_Remote_Get_Put_src_dst == /\ AbsDirtyClean /\ Dir.Pending /\ ~Dir.Local /\ PendReqSrc = Other /\ FwdCmd = "UNI_Get" - /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_ShWb", !.Proc = Other, !.Data = CurrData] + /\ ShWbMsg' = [Cmd |-> "SHWB_ShWb", Proc |-> Other, Data |-> CurrData] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other /\ UNCHANGED < 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"]] @@ -770,8 +761,8 @@ 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", ![src].Proc = Other, ![src].Data = Undefined] - /\ NakcMsg' = [NakcMsg EXCEPT !.Cmd = "NAKC_Nakc"] + /\ UniMsg' = [UniMsg EXCEPT ![src] = [Cmd |-> "UNI_Nak", Proc |-> Other, Data |-> Undefined]] + /\ NakcMsg' = [Cmd |-> "NAKC_Nakc"] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = src /\ UNCHANGED < "SHWB_FAck", Proc |-> Other, Data |-> Undefined] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other /\ UNCHANGED < "UNI_PutX", Proc |-> Other, Data |-> CurrData]] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = src /\ ShWbMsg' = IF src # Home - THEN [ShWbMsg EXCEPT !.Cmd = "SHWB_FAck", !.Proc = src, !.Data = Undefined] + THEN [Cmd |-> "SHWB_FAck", Proc |-> src, Data |-> Undefined] ELSE ShWbMsg /\ UNCHANGED <> @@ -809,7 +800,7 @@ ABS_NI_Remote_GetX_PutX_src_dst == /\ AbsDirtyClean /\ Dir.Pending /\ ~Dir.Local /\ PendReqSrc = Other /\ FwdCmd = "UNI_GetX" - /\ ShWbMsg' = [ShWbMsg EXCEPT !.Cmd = "SHWB_FAck", !.Proc = Other, !.Data = Undefined] + /\ ShWbMsg' = [Cmd |-> "SHWB_FAck", Proc |-> Other, Data |-> Undefined] /\ FwdCmd' = "UNI_None" /\ FwdSrc' = Other /\ UNCHANGED < "SHWB_None", Proc |-> Undefined, Data |-> Undefined] /\ Dir' = [Dir EXCEPT !.Pending = FALSE, !.Dirty = FALSE, !.ShrVld = TRUE, !.InvSet = Dir.ShrSet] /\ MemData' = ShWbMsg.Data From 0a94831859c82e4afe78c6aeb773da4144fbf2c6 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 27 Jul 2026 10:15:14 -0700 Subject: [PATCH 12/17] Check the two-node, two-datum configuration At NODE/DATA = 1/1 the invariants say almost nothing. CacheStateProp quantifies over pairs p, q in NODE with p # q and there is no such pair, so it is vacuous. MemDataProp compares MemData with CurrData, which TypeOK confines to a singleton DATA, so it holds in every state. CacheDataProp degenerates into a definedness check, since the only way a cached copy can differ from CurrData is by being Undefined. Home is moreover the only node, so every action guarded by src # Home, dst # Home or src # dst is disabled and the concrete remote paths are exercised only through the Other abstraction. Widen MCFlashWithMutex.cfg to two nodes and two data values, where the pairs exist and a stale datum is distinguishable: 650,236 states, 131,976 distinct, depth 34, 9s. That stays well inside the 30s budget below which CI checks a model exhaustively. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- specifications/FlashProtocol/MCFlashWithMutex.cfg | 4 ++-- specifications/FlashProtocol/manifest.json | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/specifications/FlashProtocol/MCFlashWithMutex.cfg b/specifications/FlashProtocol/MCFlashWithMutex.cfg index 8433adbb..93004f7d 100644 --- a/specifications/FlashProtocol/MCFlashWithMutex.cfg +++ b/specifications/FlashProtocol/MCFlashWithMutex.cfg @@ -1,6 +1,6 @@ CONSTANTS - NODE = {n1} - DATA = {d1} + NODE = {n1, n2} + DATA = {d1, d2} Other = Other Undefined = Undefined diff --git a/specifications/FlashProtocol/manifest.json b/specifications/FlashProtocol/manifest.json index 09533ad2..f0ae592c 100644 --- a/specifications/FlashProtocol/manifest.json +++ b/specifications/FlashProtocol/manifest.json @@ -20,12 +20,12 @@ "models": [ { "path": "specifications/FlashProtocol/MCFlashWithMutex.cfg", - "runtime": "00:00:01", + "runtime": "00:00:09", "mode": "exhaustive search", "result": "success", - "distinctStates": 78, - "totalStates": 241, - "stateDepth": 9 + "distinctStates": 131976, + "totalStates": 650236, + "stateDepth": 34 } ] } From 8546705820c22965d6707b6780a864c9c36eb373 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 27 Jul 2026 10:52:41 -0700 Subject: [PATCH 13/17] Type-check and symbolically check the spec with Apalache Add APFlashWithMutex.tla, a wrapper that INSTANCEs FlashWithMutex with annotated CONSTANTS and VARIABLES, leaving the spec itself free of tool-specific annotations. Undefined stands for a missing node, a missing datum and a missing command alike, so NodeU, DataU and UniU force NODE, DATA and the command enums into a single Apalache type. Str is the only one that also covers the command spellings, which rules out uninterpreted types for nodes and data. fwdVars == <> pairs two equally typed components, which Snowcat cannot tell apart from a two-element sequence. The group is shadowed in the wrapper by an annotated copy of the same body; SANY warns about the duplicate definition, as it does for the same trick in APDisruptor_SPMC. APFlashWithMutex.cfg checks the four safety properties of MCFlashWithMutex.cfg at NODE/DATA = 2/2. Apalache 0.58.3 reports no error up to computation length 5 in 3m36s, past the 30s budget, so CI smoke-tests the model instead of running it to completion. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- README.md | 2 +- .../FlashProtocol/APFlashWithMutex.cfg | 13 +++ .../FlashProtocol/APFlashWithMutex.tla | 82 +++++++++++++++++++ specifications/FlashProtocol/manifest.json | 12 +++ 4 files changed, 108 insertions(+), 1 deletion(-) create mode 100644 specifications/FlashProtocol/APFlashWithMutex.cfg create mode 100644 specifications/FlashProtocol/APFlashWithMutex.tla diff --git a/README.md b/README.md index cc1f876b..0e4a22cb 100644 --- a/README.md +++ b/README.md @@ -107,7 +107,7 @@ Here is a list of specs included in this repository which are validated by the C | [Disruptor](specifications/Disruptor) | Nicholas Schultz-Møller | | | | ✔ | ✔ | | [DAG-based Consensus](specifications/dag-consensus) | Giuliano Losa | | | ✔ | ✔ | | | [German Cache-Coherence Protocol](specifications/GermanProtocol) | Markus Kuppe | | | | ✔ | ✔ | -| [FLASH Cache-Coherence Protocol](specifications/FlashProtocol) | Markus Kuppe | | | | ✔ | | +| [FLASH Cache-Coherence Protocol](specifications/FlashProtocol) | Markus Kuppe | | | | ✔ | ✔ | ## Other Examples diff --git a/specifications/FlashProtocol/APFlashWithMutex.cfg b/specifications/FlashProtocol/APFlashWithMutex.cfg new file mode 100644 index 00000000..8acdafed --- /dev/null +++ b/specifications/FlashProtocol/APFlashWithMutex.cfg @@ -0,0 +1,13 @@ +CONSTANT + NODE <- NodeVal + DATA <- DataVal + Other <- OtherVal + Undefined <- UndefinedVal + +INVARIANT + TypeOK + CacheStateProp + CacheDataProp + MemDataProp + +SPECIFICATION Spec diff --git a/specifications/FlashProtocol/APFlashWithMutex.tla b/specifications/FlashProtocol/APFlashWithMutex.tla new file mode 100644 index 00000000..e0baf4a2 --- /dev/null +++ b/specifications/FlashProtocol/APFlashWithMutex.tla @@ -0,0 +1,82 @@ +------------------------- MODULE APFlashWithMutex ------------------------- +(* Apalache type annotations for FlashWithMutex.tla, applied via INSTANCE so + the original spec remains free of tool-specific idiosyncrasies. + + Undefined is the sentinel of node-, data-, and command-valued variables + alike, so NODE, DATA, and the command enums all have to share one type. + Str is the only candidate, which rules out modelling nodes and data as + uninterpreted Apalache types. + + Run bounded model checking for executions of at most 5 Next steps with: + apalache-mc check --length=5 --config=APFlashWithMutex.cfg APFlashWithMutex.tla + This completes in about 4 minutes on a 2021 M1 MacBook. +*) + +CONSTANTS + \* @type: Set(Str); + NODE, + \* @type: Set(Str); + DATA, + \* @type: Str; + Other, + \* @type: Str; + Undefined + +VARIABLES + \* @type: Str; + Home, + \* @type: Str -> { ProcCmd: Str, InvMarked: Bool, CacheState: Str, CacheData: Str }; + Proc, + \* @type: { Pending: Bool, Local: Bool, Dirty: Bool, HeadVld: Bool, HeadPtr: Str, ShrVld: Bool, ShrSet: Set(Str), InvSet: Set(Str) }; + Dir, + \* @type: Str; + MemData, + \* @type: Str -> { Cmd: Str, Proc: Str, Data: Str }; + UniMsg, + \* @type: Str -> { Cmd: Str }; + InvMsg, + \* @type: Str -> { Cmd: Str }; + RpMsg, + \* @type: { Cmd: Str, Proc: Str, Data: Str }; + WbMsg, + \* @type: { Cmd: Str, Proc: Str, Data: Str }; + ShWbMsg, + \* @type: { Cmd: Str }; + NakcMsg, + \* @type: Str; + CurrData, + \* @type: Str; + PrevData, + \* @type: Str; + PendReqSrc, + \* @type: Str; + PendReqCmd, + \* @type: Bool; + Collecting, + \* @type: Str; + FwdCmd, + \* @type: Str; + FwdSrc, + \* @type: Bool; + Env_o + +\* 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 +\* with an annotated but otherwise identical body. +\* +\* Brittle: this trick relies on SANY tolerating a duplicate definition only +\* when the body is identical to the one in `FlashWithMutex`. Any change to +\* the body below turns the warning into a hard "Multiple declarations" +\* error. +\* @type: <>; +fwdVars == <> + +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/manifest.json b/specifications/FlashProtocol/manifest.json index f0ae592c..941fe1f3 100644 --- a/specifications/FlashProtocol/manifest.json +++ b/specifications/FlashProtocol/manifest.json @@ -14,6 +14,18 @@ "features": [], "models": [] }, + { + "path": "specifications/FlashProtocol/APFlashWithMutex.tla", + "features": [], + "models": [ + { + "path": "specifications/FlashProtocol/APFlashWithMutex.cfg", + "runtime": "00:03:36", + "mode": "symbolic", + "result": "success" + } + ] + }, { "path": "specifications/FlashProtocol/MCFlashWithMutex.tla", "features": [], From 7a35009d35b5ed6cf817b70a299c726b34113e20 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 27 Jul 2026 13:53:08 -0700 Subject: [PATCH 14/17] Quotient the FLASH model by the scalarset symmetry NODE and DATA translate Murphi scalarsets. A scalarset is not merely a set whose elements happen to be interchangeable; interchangeability is the type's defining property, and Murphi acts on it by canonicalizing every state before hashing it. The model was declaring the model values but not the symmetry, so TLC was exploring the full graph while Murphi explored the quotient. That is the one thing EQUIV-MANUAL 7.5 tells translators not to do: SYMMETRY must union all scalarset types, "matching Murphi's symmetry exactly, or the reachable-state counts (and the checker's quotient) will differ". Declaring it brings the model into conformance rather than trading fidelity for speed. Symmetry is sound here: Spec and each checked invariant are preserved by every permutation in the symmetry set. Home is a variable rather than a distinguished constant, so it permutes with the remaining state, and the new assumptions Other \notin DATA and NODE \cap DATA = {} ensure that no permutation moves Other or Undefined. Only invariants are checked, so the usual restriction on SYMMETRY with temporal properties does not apply. The assumptions matter because violating them fails silently. With one model value shared between NODE and DATA, TLC reports no error: without SYMMETRY it finds the same 131,976 distinct states at depth 34; with SYMMETRY it finds 109,447 distinct states, three distinct initial states instead of one, and depth 42. Symmetry reduction cannot increase the depth of the state graph. The quotient is exactly the one Murphi computes. Under NODE/DATA = 2/2 the group is S2 x S2, of order four, and both tools divide by four on the nose: TLC goes from 131,976 distinct states to 32,994, and Murphi from 1,205,832 to 301,458 under exhaustive canonicalization (-sym1). Neither ratio is approximate and neither has fixpoints, which is the evidence that the Permutations set declared here is Murphi's symmetry group and not some coarser or finer relation. Depth is unchanged at 34 and runtime drops from nine seconds to four. The manifest's totalStates moves further than the quotient alone accounts for, from 650,236 to 159,216. The recorded figure was stale: dropping the ABS_NI_InvAck stuttering branch took the pre-symmetry generated count to 636,852 without the manifest being updated. Only distinctStates divides by the group order exactly; generated counts depend on the exploration order, which canonicalization perturbs. The absolute counts still differ between the two tools, and are meant to. Murphi's state carries the write-only ghosts LastWrVld, LastWrPtr, LastInvAck and LastOtherInvAck; this translation drops the first three and the comparator projects LastOtherInvAck away through ignorePaths. So the count to compare across tools is the quotient factor, not the state total. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- specifications/FlashProtocol/FlashWithMutex.tla | 2 ++ specifications/FlashProtocol/MCFlashWithMutex.cfg | 2 ++ specifications/FlashProtocol/MCFlashWithMutex.tla | 7 ++++++- specifications/FlashProtocol/manifest.json | 6 +++--- 4 files changed, 13 insertions(+), 4 deletions(-) diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla index ed48ceec..a7b3c223 100644 --- a/specifications/FlashProtocol/FlashWithMutex.tla +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -24,9 +24,11 @@ CONSTANTS 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) diff --git a/specifications/FlashProtocol/MCFlashWithMutex.cfg b/specifications/FlashProtocol/MCFlashWithMutex.cfg index 93004f7d..f8f9f6f6 100644 --- a/specifications/FlashProtocol/MCFlashWithMutex.cfg +++ b/specifications/FlashProtocol/MCFlashWithMutex.cfg @@ -4,6 +4,8 @@ CONSTANTS Other = Other Undefined = Undefined +SYMMETRY Symmetry + SPECIFICATION Spec INVARIANT diff --git a/specifications/FlashProtocol/MCFlashWithMutex.tla b/specifications/FlashProtocol/MCFlashWithMutex.tla index 8691242e..fde41d52 100644 --- a/specifications/FlashProtocol/MCFlashWithMutex.tla +++ b/specifications/FlashProtocol/MCFlashWithMutex.tla @@ -1,3 +1,8 @@ ------------------------- MODULE MCFlashWithMutex ------------------------- -EXTENDS FlashWithMutex +EXTENDS FlashWithMutex, TLC + +\* Nodes and data values are independently interchangeable. The Other and +\* Undefined sentinels are fixed because they are outside these sets. +Symmetry == Permutations(NODE) \union Permutations(DATA) + ============================================================================== diff --git a/specifications/FlashProtocol/manifest.json b/specifications/FlashProtocol/manifest.json index 941fe1f3..99283a68 100644 --- a/specifications/FlashProtocol/manifest.json +++ b/specifications/FlashProtocol/manifest.json @@ -32,11 +32,11 @@ "models": [ { "path": "specifications/FlashProtocol/MCFlashWithMutex.cfg", - "runtime": "00:00:09", + "runtime": "00:00:04", "mode": "exhaustive search", "result": "success", - "distinctStates": 131976, - "totalStates": 650236, + "distinctStates": 32994, + "totalStates": 159216, "stateDepth": 34 } ] From 5d09f629373cdb77e1dd6b77fb42845e1b1254ea Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 27 Jul 2026 14:30:37 -0700 Subject: [PATCH 15/17] Check the Murphi Lemma_1 through Lemma_5 invariants The Murphi rules cite five lemmas by name to justify their guards: these are the side conditions that make the `Other`-node abstraction sound, not properties a user cares about. The translation carried the rules but not the lemmas, leaving the citations as unchecked claims. Each Murphi lemma reads `forall h : NODE do h = Home -> ...` and so instantiates h only to Home, which the translations write directly. All five hold, under TLC at NODE/DATA = 2/2 and under Apalache up to computation length 5. They also strengthen the suite: mutants that stall the protocol or loosen a guard slip past the three data properties but violate the lemmas. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- .../FlashProtocol/APFlashWithMutex.cfg | 5 ++ .../FlashProtocol/APFlashWithMutex.tla | 3 +- .../FlashProtocol/FlashWithMutex.tla | 62 +++++++++++++++++++ .../FlashProtocol/MCFlashWithMutex.cfg | 5 ++ specifications/FlashProtocol/manifest.json | 2 +- 5 files changed, 75 insertions(+), 2 deletions(-) diff --git a/specifications/FlashProtocol/APFlashWithMutex.cfg b/specifications/FlashProtocol/APFlashWithMutex.cfg index 8acdafed..4c790ba3 100644 --- a/specifications/FlashProtocol/APFlashWithMutex.cfg +++ b/specifications/FlashProtocol/APFlashWithMutex.cfg @@ -9,5 +9,10 @@ INVARIANT CacheStateProp CacheDataProp MemDataProp + Lemma_1 + Lemma_2 + Lemma_3 + Lemma_4 + Lemma_5 SPECIFICATION Spec diff --git a/specifications/FlashProtocol/APFlashWithMutex.tla b/specifications/FlashProtocol/APFlashWithMutex.tla index e0baf4a2..ebf85a3e 100644 --- a/specifications/FlashProtocol/APFlashWithMutex.tla +++ b/specifications/FlashProtocol/APFlashWithMutex.tla @@ -9,7 +9,8 @@ Run bounded model checking for executions of at most 5 Next steps with: apalache-mc check --length=5 --config=APFlashWithMutex.cfg APFlashWithMutex.tla - This completes in about 4 minutes on a 2021 M1 MacBook. + Runtime depends on the hardware and on the invariant list; manifest.json + records the current measurement. *) CONSTANTS diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla index a7b3c223..5aa9da81 100644 --- a/specifications/FlashProtocol/FlashWithMutex.tla +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -899,4 +899,66 @@ CacheDataProp == MemDataProp == ~Dir.Dirty => MemData = CurrData + +------------------------------------------------------------------------------- +(* 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. *) +(* *) +(* 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". +Lemma_1 == + \A dst \in NODE : + Proc[dst].CacheState = "CACHE_E" => + /\ Dir.Dirty + /\ WbMsg.Cmd # "WB_Wb" + /\ ShWbMsg.Cmd # "SHWB_ShWb" + /\ \A p \in NODE : p # dst => Proc[p].CacheState # "CACHE_E" + /\ UniMsg[Home].Cmd # "UNI_Put" + /\ \A q \in NODE : UniMsg[q].Cmd # "UNI_PutX" + +\* 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. +Lemma_2 == + \A src, dst \in NODE : + (/\ src # dst /\ dst # Home + /\ UniMsg[src].Cmd = "UNI_Get" /\ UniMsg[src].Proc = dst) + => /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = src /\ FwdCmd = "UNI_Get" + +\* Lemma_2 for the exclusive flavour. +Lemma_3 == + \A src, dst \in NODE : + (/\ src # dst /\ dst # Home + /\ UniMsg[src].Cmd = "UNI_GetX" /\ UniMsg[src].Proc = dst) + => /\ Dir.Pending /\ ~Dir.Local + /\ PendReqSrc = src /\ FwdCmd = "UNI_GetX" + +\* 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. +Lemma_4 == + \A p \in NODE : + (p # Home /\ InvMsg[p].Cmd = "INV_InvAck") => + /\ Dir.Pending /\ Collecting + /\ NakcMsg.Cmd = "NAKC_None" /\ ShWbMsg.Cmd = "SHWB_None" + /\ \A q \in NODE : + /\ (UniMsg[q].Cmd \in {"UNI_Get", "UNI_GetX"} => UniMsg[q].Proc = Home) + /\ (UniMsg[q].Cmd = "UNI_PutX" => (UniMsg[q].Proc = Home /\ PendReqSrc = q)) + +\* 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. +Lemma_5 == + \A p \in NODE : Proc[p].CacheState = "CACHE_E" => Proc[p].CacheData = CurrData ============================================================================= diff --git a/specifications/FlashProtocol/MCFlashWithMutex.cfg b/specifications/FlashProtocol/MCFlashWithMutex.cfg index f8f9f6f6..1da87bf8 100644 --- a/specifications/FlashProtocol/MCFlashWithMutex.cfg +++ b/specifications/FlashProtocol/MCFlashWithMutex.cfg @@ -13,3 +13,8 @@ INVARIANT CacheStateProp CacheDataProp MemDataProp + Lemma_1 + Lemma_2 + Lemma_3 + Lemma_4 + Lemma_5 diff --git a/specifications/FlashProtocol/manifest.json b/specifications/FlashProtocol/manifest.json index 99283a68..b17ec646 100644 --- a/specifications/FlashProtocol/manifest.json +++ b/specifications/FlashProtocol/manifest.json @@ -20,7 +20,7 @@ "models": [ { "path": "specifications/FlashProtocol/APFlashWithMutex.cfg", - "runtime": "00:03:36", + "runtime": "00:38:09", "mode": "symbolic", "result": "success" } From 2ee38a5ecf54cc68cd83bc3c38b1650f787e5595 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 29 Jul 2026 05:48:21 -0700 Subject: [PATCH 16/17] Check progress as liveness instead of as an enabledness invariant Murphi has no temporal-property language, so the source model encodes its deadlock argument as the state invariants Progress1_it11/it21/it22: in a pending state, some rule that continues the transaction is enabled. That encoding has to name the agent whose progress is at stake, which is what the auxiliary LastOtherInvAck is for, and it enumerates the continuation guards by hand in the guardXXX/progress_XXX functions. A leads-to formula needs neither device, which is why neither has a counterpart here: the ghost stays dropped and the guard functions are not translated. The two encodings are not equivalent. An enabledness invariant is a one-step non-blocking check, so it cannot separate deadlock from starvation. ReqSuccess is defined but deliberately not checked, to mark that boundary: TLC returns a lasso in which n2 issues a Get, the abstract node takes the line, Home issues a Get and is served, n2 is NAKed and reissues, and the cycle repeats. Every state of that cycle has a continuation rule enabled, so Progress1_it11/it21/it22 hold throughout a behaviour in which n2 never obtains the line. Fairness is asserted per message slot rather than per action. Which handler applies to a waiting message depends on directory state that other actions change while the message waits, so no single handler need be continuously enabled, but some member of the slot's group always is: WF_vars of HandleUni(n), HandleInv(n), NI_Replace(n), AbsRespond(n), HandleShWb, ABS_NI_InvAck, NI_Nak_Clear, NI_Wb and AbsRespondSrcDst, thirteen conjuncts at NODE = 2. Per-action SF_vars was the first attempt: it assumes more than the protocol needs, and TLC rejects its sixty-one conjuncts outright with "the temporal formula exceeds the maximum supported size in disjunctive normal form". That ceiling is the cross product taken when the fairness conjuncts are put into DNF, which is exponential in their number; it is not the cost of the tableau or of the behaviour graph, either of which would have absorbed them. Lifting it is https://github.com/tlaplus/tlaplus/issues/1251. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- .../FlashProtocol/FlashWithMutex.tla | 90 +++++++++++++++++++ .../FlashProtocol/MCFlashWithMutexLive.cfg | 17 ++++ .../FlashProtocol/MCFlashWithMutexLive.tla | 9 ++ specifications/FlashProtocol/manifest.json | 16 ++++ 4 files changed, 132 insertions(+) create mode 100644 specifications/FlashProtocol/MCFlashWithMutexLive.cfg create mode 100644 specifications/FlashProtocol/MCFlashWithMutexLive.tla diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla index 5aa9da81..8d4e4674 100644 --- a/specifications/FlashProtocol/FlashWithMutex.tla +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -882,6 +882,96 @@ Next == System \/ Environment Spec == Init /\ [][Next]_vars +------------------------------------------------------------------------------- +(* Progress, stated as liveness. *) +(* *) +(* Fairness is asserted per *message slot* rather than per action. Which *) +(* handler applies to a waiting message depends on the directory state, which *) +(* 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. *) + +\* Everything that can consume or rewrite the unicast message in slot n. +HandleUni(n) == + \/ NI_Nak(n) + \/ NI_Local_Get_Nak(n) \/ NI_Local_Get_Get(n) \/ NI_Local_Get_Put(n) + \/ NI_Local_GetX_Nak(n) \/ NI_Local_GetX_GetX(n) \/ NI_Local_GetX_PutX(n) + \/ NI_Remote_Put(n) \/ NI_Remote_PutX(n) + \/ (n = Home /\ (NI_Local_Put \/ NI_Local_PutXAcksDone)) + \/ \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 + +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 + +\* No request stays outstanding forever. This is deadlock freedom, not a claim +\* that requests succeed: a request also retires by being NAKed, so a request +\* that is endlessly NAKed and reissued satisfies it. +ReqProgress == + \A n \in NODE : (Proc[n].ProcCmd # "NODE_None") ~> (Proc[n].ProcCmd = "NODE_None") + +\* The directory does not stay busy forever. Of everything here this is the +\* closest counterpart to Progress1_it11. +DirProgress == Dir.Pending ~> ~Dir.Pending + +\* No message is stranded in the network. +UniProgress == + \A n \in NODE : (UniMsg[n].Cmd # "UNI_None") ~> (UniMsg[n].Cmd = "UNI_None") +InvProgress == + \A n \in NODE : (InvMsg[n].Cmd # "INV_None") ~> (InvMsg[n].Cmd = "INV_None") +RpProgress == + \A n \in NODE : (RpMsg[n].Cmd = "RP_Replace") ~> (RpMsg[n].Cmd = "RP_None") +WbProgress == (WbMsg.Cmd = "WB_Wb") ~> (WbMsg.Cmd = "WB_None") +ShWbProgress == (ShWbMsg.Cmd # "SHWB_None") ~> (ShWbMsg.Cmd = "SHWB_None") +NakcProgress == (NakcMsg.Cmd = "NAKC_Nakc") ~> (NakcMsg.Cmd = "NAKC_None") + +\* 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 +\* 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 +\* can. Ruling the cycle out needs an arbitration assumption the protocol does +\* not make. +ReqSuccess == + \A n \in NODE : (Proc[n].ProcCmd = "NODE_Get") ~> (Proc[n].CacheState # "CACHE_I") + ------------------------------------------------------------------------------- (* Safety properties translated from the Murphi `invariant`s (for indep. *) (* cross-checking; not part of the bisimulation). *) diff --git a/specifications/FlashProtocol/MCFlashWithMutexLive.cfg b/specifications/FlashProtocol/MCFlashWithMutexLive.cfg new file mode 100644 index 00000000..d85fb8c4 --- /dev/null +++ b/specifications/FlashProtocol/MCFlashWithMutexLive.cfg @@ -0,0 +1,17 @@ +CONSTANTS + NODE = {n1, n2} + DATA = {d1, d2} + Other = Other + Undefined = Undefined + +SPECIFICATION FairSpec + +PROPERTIES + ReqProgress + DirProgress + UniProgress + InvProgress + RpProgress + WbProgress + ShWbProgress + NakcProgress diff --git a/specifications/FlashProtocol/MCFlashWithMutexLive.tla b/specifications/FlashProtocol/MCFlashWithMutexLive.tla new file mode 100644 index 00000000..95e263e7 --- /dev/null +++ b/specifications/FlashProtocol/MCFlashWithMutexLive.tla @@ -0,0 +1,9 @@ +----------------------- MODULE MCFlashWithMutexLive ----------------------- +EXTENDS FlashWithMutex + +\* Deliberately no Symmetry definition: TLC's symmetry reduction can miss +\* liveness violations, so the liveness model explores the unreduced graph. +\* Safety and the Murphi Lemma_* invariants are checked, with symmetry, by +\* MCFlashWithMutex.cfg instead. + +============================================================================== diff --git a/specifications/FlashProtocol/manifest.json b/specifications/FlashProtocol/manifest.json index b17ec646..a8afa32c 100644 --- a/specifications/FlashProtocol/manifest.json +++ b/specifications/FlashProtocol/manifest.json @@ -40,6 +40,22 @@ "stateDepth": 34 } ] + }, + { + "path": "specifications/FlashProtocol/MCFlashWithMutexLive.tla", + "features": [], + "models": [ + { + "path": "specifications/FlashProtocol/MCFlashWithMutexLive.cfg", + "runtime": "00:04:44", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 131976, + "totalStates": 636852, + "stateDepth": 34, + "workers": 4 + } + ] } ] } From fa2397a3e1e47ef2d9c12563341f6bdce058bca0 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 29 Jul 2026 05:57:51 -0700 Subject: [PATCH 17/17] State the checked properties as theorems Every property now carries a theorem naming the specification it was checked against, written next to the definition rather than collected at the bottom of the module, so a reader who scrolls to a property sees what is claimed of it. TypeOK, CacheStateProp, CacheDataProp, MemDataProp and Lemma_1 through Lemma_5 are asserted of Spec. MCFlashWithMutex.cfg checks them at NODE = DATA = 2 and quotients by the scalarset symmetry, which is sound because all nine are invariants: 32,994 distinct states. The eight progress properties are asserted of FairSpec. MCFlashWithMutexLive.cfg checks them at the same size without symmetry, because TLC's symmetry reduction can hide liveness violations: 131,976 distinct states. Depth 34 either way. These are model-checking results at one configuration, not proofs. Nothing is discharged for arbitrary NODE or DATA, and TLC ignores THEOREM, so the theorems add no work to either run. ReqSuccess gets no theorem because it does not hold; the lasso that refutes it stays recorded in the comment above it. TypeCorrect sits after Spec rather than after TypeOK, which is defined up with the variables, because a theorem cannot mention Spec before Spec is defined. Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- .../FlashProtocol/FlashWithMutex.tla | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/specifications/FlashProtocol/FlashWithMutex.tla b/specifications/FlashProtocol/FlashWithMutex.tla index 8d4e4674..4104630f 100644 --- a/specifications/FlashProtocol/FlashWithMutex.tla +++ b/specifications/FlashProtocol/FlashWithMutex.tla @@ -882,6 +882,9 @@ Next == System \/ Environment Spec == Init /\ [][Next]_vars +\* TypeOK is defined up with the variables; its theorem has to wait for Spec. +THEOREM TypeCorrect == Spec => []TypeOK + ------------------------------------------------------------------------------- (* Progress, stated as liveness. *) (* *) @@ -945,21 +948,34 @@ FairSpec == Init /\ [][Next]_vars /\ Fairness \* that is endlessly NAKed and reissued satisfies it. ReqProgress == \A n \in NODE : (Proc[n].ProcCmd # "NODE_None") ~> (Proc[n].ProcCmd = "NODE_None") +THEOREM ReqProgressCorrect == FairSpec => ReqProgress \* The directory does not stay busy forever. Of everything here this is the \* closest counterpart to Progress1_it11. DirProgress == Dir.Pending ~> ~Dir.Pending +THEOREM DirProgressCorrect == FairSpec => DirProgress \* No message is stranded in the network. UniProgress == \A n \in NODE : (UniMsg[n].Cmd # "UNI_None") ~> (UniMsg[n].Cmd = "UNI_None") +THEOREM UniProgressCorrect == FairSpec => UniProgress + InvProgress == \A n \in NODE : (InvMsg[n].Cmd # "INV_None") ~> (InvMsg[n].Cmd = "INV_None") +THEOREM InvProgressCorrect == FairSpec => InvProgress + RpProgress == \A n \in NODE : (RpMsg[n].Cmd = "RP_Replace") ~> (RpMsg[n].Cmd = "RP_None") +THEOREM RpProgressCorrect == FairSpec => RpProgress + WbProgress == (WbMsg.Cmd = "WB_Wb") ~> (WbMsg.Cmd = "WB_None") +THEOREM WbProgressCorrect == FairSpec => WbProgress + ShWbProgress == (ShWbMsg.Cmd # "SHWB_None") ~> (ShWbMsg.Cmd = "SHWB_None") +THEOREM ShWbProgressCorrect == FairSpec => ShWbProgress + NakcProgress == (NakcMsg.Cmd = "NAKC_Nakc") ~> (NakcMsg.Cmd = "NAKC_None") +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 @@ -979,6 +995,7 @@ ReqSuccess == CacheStateProp == \A p, q \in NODE : p # q => ~(Proc[p].CacheState = "CACHE_E" /\ Proc[q].CacheState = "CACHE_E") +THEOREM CacheStateCorrect == Spec => []CacheStateProp CacheDataProp == \A p \in NODE : @@ -986,9 +1003,11 @@ CacheDataProp == /\ (Proc[p].CacheState = "CACHE_S" => /\ (Collecting => Proc[p].CacheData = PrevData) /\ (~Collecting => Proc[p].CacheData = CurrData)) +THEOREM CacheDataCorrect == Spec => []CacheDataProp MemDataProp == ~Dir.Dirty => MemData = CurrData +THEOREM MemDataCorrect == Spec => []MemDataProp ------------------------------------------------------------------------------- (* The Murphi `Lemma_*` invariants. Unlike the three properties above these *) @@ -1015,6 +1034,7 @@ Lemma_1 == /\ \A p \in NODE : p # dst => Proc[p].CacheState # "CACHE_E" /\ UniMsg[Home].Cmd # "UNI_Put" /\ \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. @@ -1024,6 +1044,7 @@ Lemma_2 == /\ UniMsg[src].Cmd = "UNI_Get" /\ UniMsg[src].Proc = dst) => /\ Dir.Pending /\ ~Dir.Local /\ PendReqSrc = src /\ FwdCmd = "UNI_Get" +THEOREM Lemma_2_Correct == Spec => []Lemma_2 \* Lemma_2 for the exclusive flavour. Lemma_3 == @@ -1032,6 +1053,7 @@ Lemma_3 == /\ UniMsg[src].Cmd = "UNI_GetX" /\ UniMsg[src].Proc = dst) => /\ Dir.Pending /\ ~Dir.Local /\ 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 @@ -1044,6 +1066,7 @@ Lemma_4 == /\ \A q \in NODE : /\ (UniMsg[q].Cmd \in {"UNI_Get", "UNI_GetX"} => UniMsg[q].Proc = Home) /\ (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 @@ -1051,4 +1074,5 @@ Lemma_4 == \* 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 =============================================================================