From 4115b7d02a81b8c2b5beaaa9874591674f9f16ca Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 18 Jun 2026 11:18:24 -0700 Subject: [PATCH 01/12] Add German cache-coherence protocol example with TLC and Apalache models A new specifications/GermanProtocol directory translating the German directory-based cache-coherence protocol from the Murphi sources in Divjyot Sethi's ProtocolDeadlockFiles repository (provenance: German -> Chou/Mannava/Park FMCAD 2004 -> Sethi/Talupur/Malik ATVA 2014). The TLA+ was synthesized by Opus 4.8 under supervision; see the directory README.md for the full attribution chain. Three levels of refinement, each a standalone module: - GermanCoherence: control-only model, coherence/mutual exclusion only. - German: the CMP-style parameterized abstraction (concrete nodes plus a single abstract "Other" environment node and the ABS_* rules). - GermanWithMutex: the data-carrying refinement, adding data-integrity (DataProp), the structural well-formedness invariants, and the Lemma_1/Lemma_2 noninterference lemmas, plus liveness under fairness. Tooling added for each spec, following the conventions already used in the repo (INSTANCE-based Apalache wrappers; MC* TLC drivers): - AP{GermanCoherence,German,GermanWithMutex}.tla/.cfg apply Apalache type annotations via INSTANCE so the specs stay tool-agnostic; nodes and data are uninterpreted types so the NODE \cup {Other, NoNode} unions type-check. Safety invariants only (no liveness). - MC{GermanCoherence,German,GermanWithMutex}.tla/.cfg use the smallest meaningful constants -- two nodes (the minimum for non-vacuous mutual exclusion) and, for GermanWithMutex, two data values (so writes are distinguishable) -- with Permutations symmetry reduction. Co-authored-by: Claude Opus 4.8 Signed-off-by: Markus Alexander Kuppe --- README.md | 1 + specifications/GermanProtocol/APGerman.cfg | 11 + specifications/GermanProtocol/APGerman.tla | 44 +++ .../GermanProtocol/APGermanCoherence.cfg | 9 + .../GermanProtocol/APGermanCoherence.tla | 41 +++ .../GermanProtocol/APGermanWithMutex.cfg | 17 ++ .../GermanProtocol/APGermanWithMutex.tla | 52 ++++ specifications/GermanProtocol/German.tla | 213 ++++++++++++++ .../GermanProtocol/GermanCoherence.tla | 160 ++++++++++ .../GermanProtocol/GermanWithMutex.tla | 276 ++++++++++++++++++ specifications/GermanProtocol/MCGerman.cfg | 16 + specifications/GermanProtocol/MCGerman.tla | 8 + .../GermanProtocol/MCGermanCoherence.cfg | 13 + .../GermanProtocol/MCGermanCoherence.tla | 7 + .../GermanProtocol/MCGermanWithMutex.cfg | 26 ++ .../GermanProtocol/MCGermanWithMutex.tla | 4 + specifications/GermanProtocol/README.md | 113 +++++++ specifications/GermanProtocol/manifest.json | 110 +++++++ 18 files changed, 1121 insertions(+) create mode 100644 specifications/GermanProtocol/APGerman.cfg create mode 100644 specifications/GermanProtocol/APGerman.tla create mode 100644 specifications/GermanProtocol/APGermanCoherence.cfg create mode 100644 specifications/GermanProtocol/APGermanCoherence.tla create mode 100644 specifications/GermanProtocol/APGermanWithMutex.cfg create mode 100644 specifications/GermanProtocol/APGermanWithMutex.tla create mode 100644 specifications/GermanProtocol/German.tla create mode 100644 specifications/GermanProtocol/GermanCoherence.tla create mode 100644 specifications/GermanProtocol/GermanWithMutex.tla create mode 100644 specifications/GermanProtocol/MCGerman.cfg create mode 100644 specifications/GermanProtocol/MCGerman.tla create mode 100644 specifications/GermanProtocol/MCGermanCoherence.cfg create mode 100644 specifications/GermanProtocol/MCGermanCoherence.tla create mode 100644 specifications/GermanProtocol/MCGermanWithMutex.cfg create mode 100644 specifications/GermanProtocol/MCGermanWithMutex.tla create mode 100644 specifications/GermanProtocol/README.md create mode 100644 specifications/GermanProtocol/manifest.json diff --git a/README.md b/README.md index 04d47257..ac1c1221 100644 --- a/README.md +++ b/README.md @@ -106,6 +106,7 @@ Here is a list of specs included in this repository which are validated by the C | [Buffered Random Access File](specifications/braf) | Calvin Loncaric | | | | ✔ | | | [Disruptor](specifications/Disruptor) | Nicholas Schultz-Møller | | | | ✔ | ✔ | | [DAG-based Consensus](specifications/dag-consensus) | Giuliano Losa | | | ✔ | ✔ | | +| [German Cache-Coherence Protocol](specifications/GermanProtocol) | Markus Kuppe | | | | ✔ | ✔ | ## Other Examples diff --git a/specifications/GermanProtocol/APGerman.cfg b/specifications/GermanProtocol/APGerman.cfg new file mode 100644 index 00000000..a655b707 --- /dev/null +++ b/specifications/GermanProtocol/APGerman.cfg @@ -0,0 +1,11 @@ +CONSTANT + NODE <- NodeVal + Other <- OtherVal + NoNode <- NoNodeVal + +INVARIANT + TypeOK + Coherence + Lemma_1 + +SPECIFICATION Spec diff --git a/specifications/GermanProtocol/APGerman.tla b/specifications/GermanProtocol/APGerman.tla new file mode 100644 index 00000000..fda49d49 --- /dev/null +++ b/specifications/GermanProtocol/APGerman.tla @@ -0,0 +1,44 @@ +----------------------------- MODULE APGerman ----------------------------- +(* Apalache type annotations for German.tla, applied via INSTANCE so the + original spec remains free of tool-specific idiosyncrasies. + + Nodes are modelled as an uninterpreted Apalache type (NODE); the abstract + environment node Other and the NoNode sentinel share that type so that + `curPtr \in NODE \cup {Other, NoNode}` is well typed. *) + +CONSTANTS + \* @type: Set(NODE); + NODE, + \* @type: NODE; + Other, + \* @type: NODE; + NoNode + +VARIABLES + \* @type: NODE -> Str; + cache, + \* @type: NODE -> Str; + chan1, + \* @type: NODE -> Str; + chan2, + \* @type: NODE -> Str; + chan3, + \* @type: NODE -> Bool; + invSet, + \* @type: NODE -> Bool; + shrSet, + \* @type: Bool; + exGntd, + \* @type: Str; + curCmd, + \* @type: NODE; + curPtr + +INSTANCE German + +\* Concrete values for the constants used by APGerman.cfg. +NodeVal == { "n1_OF_NODE", "n2_OF_NODE" } +OtherVal == "other_OF_NODE" +NoNodeVal == "noNode_OF_NODE" + +============================================================================== diff --git a/specifications/GermanProtocol/APGermanCoherence.cfg b/specifications/GermanProtocol/APGermanCoherence.cfg new file mode 100644 index 00000000..400dfd0e --- /dev/null +++ b/specifications/GermanProtocol/APGermanCoherence.cfg @@ -0,0 +1,9 @@ +CONSTANT + NODE <- NodeVal + NoNode <- NoNodeVal + +INVARIANT + TypeOK + Coherence + +SPECIFICATION Spec diff --git a/specifications/GermanProtocol/APGermanCoherence.tla b/specifications/GermanProtocol/APGermanCoherence.tla new file mode 100644 index 00000000..59e20c9f --- /dev/null +++ b/specifications/GermanProtocol/APGermanCoherence.tla @@ -0,0 +1,41 @@ +------------------------- MODULE APGermanCoherence ------------------------- +(* Apalache type annotations for GermanCoherence.tla, applied via INSTANCE so + the original spec remains free of tool-specific idiosyncrasies. + + Nodes are modelled as an uninterpreted Apalache type (NODE); the NoNode + sentinel shares that type so that `curPtr \in NODE \cup {NoNode}` is well + typed. *) + +CONSTANTS + \* @type: Set(NODE); + NODE, + \* @type: NODE; + NoNode + +VARIABLES + \* @type: NODE -> Str; + cache, + \* @type: NODE -> Str; + chan1, + \* @type: NODE -> Str; + chan2, + \* @type: NODE -> Str; + chan3, + \* @type: NODE -> Bool; + invSet, + \* @type: NODE -> Bool; + shrSet, + \* @type: Bool; + exGntd, + \* @type: Str; + curCmd, + \* @type: NODE; + curPtr + +INSTANCE GermanCoherence + +\* Concrete values for the constants used by APGermanCoherence.cfg. +NodeVal == { "n1_OF_NODE", "n2_OF_NODE" } +NoNodeVal == "noNode_OF_NODE" + +============================================================================== diff --git a/specifications/GermanProtocol/APGermanWithMutex.cfg b/specifications/GermanProtocol/APGermanWithMutex.cfg new file mode 100644 index 00000000..3eab6f17 --- /dev/null +++ b/specifications/GermanProtocol/APGermanWithMutex.cfg @@ -0,0 +1,17 @@ +CONSTANT + NODE <- NodeVal + DATA <- DataVal + NoData <- NoDataVal + NoNode <- NoNodeVal + +INVARIANT + TypeOK + Coherence + DataProp + ChannelWellFormed + TransactionConsistency + DirectoryAccurate + ExclusiveIsolation + WritebackCarriesLatest + +SPECIFICATION Spec diff --git a/specifications/GermanProtocol/APGermanWithMutex.tla b/specifications/GermanProtocol/APGermanWithMutex.tla new file mode 100644 index 00000000..ccfafe71 --- /dev/null +++ b/specifications/GermanProtocol/APGermanWithMutex.tla @@ -0,0 +1,52 @@ +------------------------- MODULE APGermanWithMutex ------------------------- +(* Apalache type annotations for GermanWithMutex.tla, applied via INSTANCE so + the original spec remains free of tool-specific idiosyncrasies. + + Nodes and data values are modelled as uninterpreted Apalache types (NODE, + DATA). The NoNode / NoData sentinels share those types so that the union + sets in TypeOK are well typed. Only the safety invariants are checked; + Apalache does not verify the liveness properties (FairSpec) of the spec. *) + +CONSTANTS + \* @type: Set(NODE); + NODE, + \* @type: Set(DATA); + DATA, + \* @type: DATA; + NoData, + \* @type: NODE; + NoNode + +VARIABLES + \* @type: NODE -> { state: Str, data: DATA }; + cache, + \* @type: NODE -> { cmd: Str, data: DATA }; + chan1, + \* @type: NODE -> { cmd: Str, data: DATA }; + chan2, + \* @type: NODE -> { cmd: Str, data: DATA }; + chan3, + \* @type: NODE -> Bool; + invSet, + \* @type: NODE -> Bool; + shrSet, + \* @type: Bool; + exGntd, + \* @type: Str; + curCmd, + \* @type: NODE; + curPtr, + \* @type: DATA; + memData, + \* @type: DATA; + auxData + +INSTANCE GermanWithMutex + +\* Concrete values for the constants used by APGermanWithMutex.cfg. +NodeVal == { "n1_OF_NODE", "n2_OF_NODE" } +DataVal == { "d1_OF_DATA", "d2_OF_DATA" } +NoDataVal == "noData_OF_DATA" +NoNodeVal == "noNode_OF_NODE" + +============================================================================== diff --git a/specifications/GermanProtocol/German.tla b/specifications/GermanProtocol/German.tla new file mode 100644 index 00000000..e873a046 --- /dev/null +++ b/specifications/GermanProtocol/German.tla @@ -0,0 +1,213 @@ +-------------------------------- MODULE German -------------------------------- +CONSTANTS + NODE, + Other, + NoNode + +ASSUME Other \notin NODE +ASSUME NoNode \notin NODE /\ NoNode # Other + +CacheState == {"I", "S", "E"} +MsgCmd == {"Empty", "ReqS", "ReqE", "Inv", "InvAck", "GntS", "GntE"} + +VARIABLES + cache, chan1, chan2, chan3, invSet, shrSet, exGntd, curCmd, curPtr + +vars == <> + +------------------------------------------------------------------------------- + +TypeOK == + /\ cache \in [NODE -> CacheState] + /\ chan1 \in [NODE -> MsgCmd] + /\ chan2 \in [NODE -> MsgCmd] + /\ chan3 \in [NODE -> MsgCmd] + /\ invSet \in [NODE -> BOOLEAN] + /\ shrSet \in [NODE -> BOOLEAN] + /\ exGntd \in BOOLEAN + /\ curCmd \in MsgCmd + /\ curPtr \in NODE \cup {Other, NoNode} + +Init == + /\ cache = [i \in NODE |-> "I"] + /\ chan1 = [i \in NODE |-> "Empty"] + /\ chan2 = [i \in NODE |-> "Empty"] + /\ chan3 = [i \in NODE |-> "Empty"] + /\ invSet = [i \in NODE |-> FALSE] + /\ shrSet = [i \in NODE |-> FALSE] + /\ exGntd = FALSE + /\ curCmd = "Empty" + /\ curPtr = NoNode + +------------------------------------------------------------------------------- + +SendReqS(i) == + /\ chan1[i] = "Empty" + /\ cache[i] = "I" + /\ chan1' = [chan1 EXCEPT ![i] = "ReqS"] + /\ UNCHANGED <> + +SendReqE(i) == + /\ chan1[i] = "Empty" + /\ cache[i] \in {"I", "S"} + /\ chan1' = [chan1 EXCEPT ![i] = "ReqE"] + /\ UNCHANGED <> + +RecvReqS(i) == + /\ curCmd = "Empty" + /\ chan1[i] = "ReqS" + /\ curCmd' = "ReqS" + /\ curPtr' = i + /\ chan1' = [chan1 EXCEPT ![i] = "Empty"] + /\ invSet' = shrSet + /\ UNCHANGED <> + +RecvReqE(i) == + /\ curCmd = "Empty" + /\ chan1[i] = "ReqE" + /\ curCmd' = "ReqE" + /\ curPtr' = i + /\ chan1' = [chan1 EXCEPT ![i] = "Empty"] + /\ invSet' = shrSet + /\ UNCHANGED <> + +SendInv(i) == + /\ chan2[i] = "Empty" + /\ invSet[i] = TRUE + /\ (curCmd = "ReqE" \/ (curCmd = "ReqS" /\ exGntd = TRUE)) + /\ chan2' = [chan2 EXCEPT ![i] = "Inv"] + /\ invSet' = [invSet EXCEPT ![i] = FALSE] + /\ UNCHANGED <> + +SendInvAck(i) == + /\ chan2[i] = "Inv" + /\ chan3[i] = "Empty" + /\ chan2' = [chan2 EXCEPT ![i] = "Empty"] + /\ chan3' = [chan3 EXCEPT ![i] = "InvAck"] + /\ cache' = [cache EXCEPT ![i] = "I"] + /\ UNCHANGED <> + +RecvInvAck(i) == + /\ chan3[i] = "InvAck" + /\ curCmd # "Empty" + /\ chan3' = [chan3 EXCEPT ![i] = "Empty"] + /\ shrSet' = [shrSet EXCEPT ![i] = FALSE] + /\ exGntd' = IF exGntd = TRUE THEN FALSE ELSE exGntd + /\ UNCHANGED <> + +SendGntS(i) == + /\ curCmd = "ReqS" + /\ curPtr = i + /\ chan2[i] = "Empty" + /\ exGntd = FALSE + /\ chan2' = [chan2 EXCEPT ![i] = "GntS"] + /\ shrSet' = [shrSet EXCEPT ![i] = TRUE] + /\ curCmd' = "Empty" + /\ curPtr' = NoNode + /\ UNCHANGED <> + +SendGntE(i) == + /\ curCmd = "ReqE" + /\ curPtr = i + /\ chan2[i] = "Empty" + /\ exGntd = FALSE + /\ \A j \in NODE : shrSet[j] = FALSE + /\ chan2' = [chan2 EXCEPT ![i] = "GntE"] + /\ shrSet' = [shrSet EXCEPT ![i] = TRUE] + /\ exGntd' = TRUE + /\ curCmd' = "Empty" + /\ curPtr' = NoNode + /\ UNCHANGED <> + +RecvGntS(i) == + /\ chan2[i] = "GntS" + /\ cache' = [cache EXCEPT ![i] = "S"] + /\ chan2' = [chan2 EXCEPT ![i] = "Empty"] + /\ UNCHANGED <> + +RecvGntE(i) == + /\ chan2[i] = "GntE" + /\ cache' = [cache EXCEPT ![i] = "E"] + /\ chan2' = [chan2 EXCEPT ![i] = "Empty"] + /\ UNCHANGED <> + +------------------------------------------------------------------------------- + +ABS_RecvReqS == + /\ curCmd = "Empty" + /\ curCmd' = "ReqS" + /\ curPtr' = Other + /\ invSet' = shrSet + /\ UNCHANGED <> + +ABS_RecvReqE == + /\ curCmd = "Empty" + /\ curCmd' = "ReqE" + /\ curPtr' = Other + /\ invSet' = shrSet + /\ UNCHANGED <> + +ABS_SendGntS == + /\ curCmd = "ReqS" + /\ curPtr = Other + /\ exGntd = FALSE + /\ curCmd' = "Empty" + /\ curPtr' = NoNode + /\ UNCHANGED <> + +ABS_SendGntE == + /\ curCmd = "ReqE" + /\ curPtr = Other + /\ exGntd = FALSE + /\ \A j \in NODE : shrSet[j] = FALSE + /\ exGntd' = TRUE + /\ curCmd' = "Empty" + /\ curPtr' = NoNode + /\ UNCHANGED <> + +\* Other acknowledges relinquishing its exclusive copy. Guarded (as in +\* german.m) so it only fires when no concrete node is exclusive / mid-grant / +\* mid-ack -- the noninterference condition that keeps the abstraction sound. +ABS_RecvInvAck == + /\ curCmd # "Empty" + /\ exGntd = TRUE + /\ \A j \in NODE : + /\ cache[j] # "E" + /\ chan2[j] # "GntE" + /\ chan3[j] # "InvAck" + /\ exGntd' = FALSE + /\ UNCHANGED <> + +------------------------------------------------------------------------------- + +Next == + \/ \E i \in NODE : + \/ SendReqS(i) \/ SendReqE(i) + \/ RecvReqS(i) \/ RecvReqE(i) + \/ SendInv(i) \/ SendInvAck(i) \/ RecvInvAck(i) + \/ SendGntS(i) \/ SendGntE(i) + \/ RecvGntS(i) \/ RecvGntE(i) + \/ ABS_RecvReqS \/ ABS_RecvReqE + \/ ABS_SendGntS \/ ABS_SendGntE + \/ ABS_RecvInvAck + +Spec == Init /\ [][Next]_vars + +------------------------------------------------------------------------------- + +Coherence == + \A i, j \in NODE : + i # j => + /\ (cache[i] = "E" => cache[j] = "I") + /\ (cache[i] = "S" => cache[j] \in {"I", "S"}) + +Lemma_1 == + \A i \in NODE : + (chan3[i] = "InvAck" /\ curCmd # "Empty" /\ exGntd = TRUE) => + \A j \in NODE : + j # i => + /\ cache[j] # "E" + /\ chan2[j] # "GntE" + /\ chan3[j] # "InvAck" + +============================================================================= diff --git a/specifications/GermanProtocol/GermanCoherence.tla b/specifications/GermanProtocol/GermanCoherence.tla new file mode 100644 index 00000000..f88435c9 --- /dev/null +++ b/specifications/GermanProtocol/GermanCoherence.tla @@ -0,0 +1,160 @@ +---------------------------- MODULE GermanCoherence ---------------------------- +CONSTANTS + NODE, + NoNode + +ASSUME NoNodeNotInNODE == NoNode \notin NODE + +CacheState == {"I", "S", "E"} +MsgCmd == {"Empty", "ReqS", "ReqE", "Inv", "InvAck", "GntS", "GntE"} + +VARIABLES + cache, + chan1, + chan2, + chan3, + invSet, + shrSet, + exGntd, + curCmd, + curPtr + +vars == <> + +------------------------------------------------------------------------------- + +TypeOK == + /\ cache \in [NODE -> CacheState] + /\ chan1 \in [NODE -> MsgCmd] + /\ chan2 \in [NODE -> MsgCmd] + /\ chan3 \in [NODE -> MsgCmd] + /\ invSet \in [NODE -> BOOLEAN] + /\ shrSet \in [NODE -> BOOLEAN] + /\ exGntd \in BOOLEAN + /\ curCmd \in MsgCmd + /\ curPtr \in NODE \cup {NoNode} + +Init == + /\ cache = [i \in NODE |-> "I"] + /\ chan1 = [i \in NODE |-> "Empty"] + /\ chan2 = [i \in NODE |-> "Empty"] + /\ chan3 = [i \in NODE |-> "Empty"] + /\ invSet = [i \in NODE |-> FALSE] + /\ shrSet = [i \in NODE |-> FALSE] + /\ exGntd = FALSE + /\ curCmd = "Empty" + /\ curPtr = NoNode + +------------------------------------------------------------------------------- + +SendReqS(i) == + /\ chan1[i] = "Empty" + /\ cache[i] = "I" + /\ chan1' = [chan1 EXCEPT ![i] = "ReqS"] + /\ UNCHANGED <> + +SendReqE(i) == + /\ chan1[i] = "Empty" + /\ cache[i] \in {"I", "S"} + /\ chan1' = [chan1 EXCEPT ![i] = "ReqE"] + /\ UNCHANGED <> + +RecvReqS(i) == + /\ curCmd = "Empty" + /\ chan1[i] = "ReqS" + /\ curCmd' = "ReqS" + /\ curPtr' = i + /\ chan1' = [chan1 EXCEPT ![i] = "Empty"] + /\ invSet' = shrSet + /\ UNCHANGED <> + +RecvReqE(i) == + /\ curCmd = "Empty" + /\ chan1[i] = "ReqE" + /\ curCmd' = "ReqE" + /\ curPtr' = i + /\ chan1' = [chan1 EXCEPT ![i] = "Empty"] + /\ invSet' = shrSet + /\ UNCHANGED <> + +SendInv(i) == + /\ chan2[i] = "Empty" + /\ invSet[i] = TRUE + /\ (curCmd = "ReqE" \/ (curCmd = "ReqS" /\ exGntd = TRUE)) + /\ chan2' = [chan2 EXCEPT ![i] = "Inv"] + /\ invSet' = [invSet EXCEPT ![i] = FALSE] + /\ UNCHANGED <> + +SendInvAck(i) == + /\ chan2[i] = "Inv" + /\ chan3[i] = "Empty" + /\ chan2' = [chan2 EXCEPT ![i] = "Empty"] + /\ chan3' = [chan3 EXCEPT ![i] = "InvAck"] + /\ cache' = [cache EXCEPT ![i] = "I"] + /\ UNCHANGED <> + +RecvInvAck(i) == + /\ chan3[i] = "InvAck" + /\ curCmd # "Empty" + /\ chan3' = [chan3 EXCEPT ![i] = "Empty"] + /\ shrSet' = [shrSet EXCEPT ![i] = FALSE] + /\ exGntd' = IF exGntd = TRUE THEN FALSE ELSE exGntd + /\ UNCHANGED <> + +SendGntS(i) == + /\ curCmd = "ReqS" + /\ curPtr = i + /\ chan2[i] = "Empty" + /\ exGntd = FALSE + /\ chan2' = [chan2 EXCEPT ![i] = "GntS"] + /\ shrSet' = [shrSet EXCEPT ![i] = TRUE] + /\ curCmd' = "Empty" + /\ curPtr' = NoNode + /\ UNCHANGED <> + +SendGntE(i) == + /\ curCmd = "ReqE" + /\ curPtr = i + /\ chan2[i] = "Empty" + /\ exGntd = FALSE + /\ \A j \in NODE : shrSet[j] = FALSE + /\ chan2' = [chan2 EXCEPT ![i] = "GntE"] + /\ shrSet' = [shrSet EXCEPT ![i] = TRUE] + /\ exGntd' = TRUE + /\ curCmd' = "Empty" + /\ curPtr' = NoNode + /\ UNCHANGED <> + +RecvGntS(i) == + /\ chan2[i] = "GntS" + /\ cache' = [cache EXCEPT ![i] = "S"] + /\ chan2' = [chan2 EXCEPT ![i] = "Empty"] + /\ UNCHANGED <> + +RecvGntE(i) == + /\ chan2[i] = "GntE" + /\ cache' = [cache EXCEPT ![i] = "E"] + /\ chan2' = [chan2 EXCEPT ![i] = "Empty"] + /\ UNCHANGED <> + +------------------------------------------------------------------------------- + +Next == + \E i \in NODE : + \/ SendReqS(i) \/ SendReqE(i) + \/ RecvReqS(i) \/ RecvReqE(i) + \/ SendInv(i) \/ SendInvAck(i) \/ RecvInvAck(i) + \/ SendGntS(i) \/ SendGntE(i) + \/ RecvGntS(i) \/ RecvGntE(i) + +Spec == Init /\ [][Next]_vars + +------------------------------------------------------------------------------- + +Coherence == + \A i, j \in NODE : + i # j => + /\ (cache[i] = "E" => cache[j] = "I") + /\ (cache[i] = "S" => cache[j] \in {"I", "S"}) + +============================================================================= diff --git a/specifications/GermanProtocol/GermanWithMutex.tla b/specifications/GermanProtocol/GermanWithMutex.tla new file mode 100644 index 00000000..d26bb973 --- /dev/null +++ b/specifications/GermanProtocol/GermanWithMutex.tla @@ -0,0 +1,276 @@ +----------------------------- MODULE GermanWithMutex ----------------------------- +EXTENDS Naturals, FiniteSets + +CONSTANTS + NODE, + DATA, + NoData, + NoNode + +ASSUME NoDataNotInDATA == NoData \notin DATA +ASSUME NoNodeNotInNODE == NoNode \notin NODE + +CacheState == {"I", "S", "E"} +MsgCmd == {"Empty", "ReqS", "ReqE", "Inv", "InvAck", "GntS", "GntE"} + +Payload == DATA \cup {NoData} + +VARIABLES + cache, + chan1, + chan2, + chan3, + invSet, + shrSet, + exGntd, + curCmd, + curPtr, + memData, + auxData + +vars == <> + +------------------------------------------------------------------------------- + +TypeOK == + /\ cache \in [NODE -> [state : CacheState, data : Payload]] + /\ chan1 \in [NODE -> [cmd : MsgCmd, data : Payload]] + /\ chan2 \in [NODE -> [cmd : MsgCmd, data : Payload]] + /\ chan3 \in [NODE -> [cmd : MsgCmd, data : Payload]] + /\ invSet \in [NODE -> BOOLEAN] + /\ shrSet \in [NODE -> BOOLEAN] + /\ exGntd \in BOOLEAN + /\ curCmd \in MsgCmd + /\ curPtr \in NODE \cup {NoNode} + /\ memData \in DATA + /\ auxData \in DATA + +Init == + \E d \in DATA : + /\ cache = [i \in NODE |-> [state |-> "I", data |-> NoData]] + /\ chan1 = [i \in NODE |-> [cmd |-> "Empty", data |-> NoData]] + /\ chan2 = [i \in NODE |-> [cmd |-> "Empty", data |-> NoData]] + /\ chan3 = [i \in NODE |-> [cmd |-> "Empty", data |-> NoData]] + /\ invSet = [i \in NODE |-> FALSE] + /\ shrSet = [i \in NODE |-> FALSE] + /\ exGntd = FALSE + /\ curCmd = "Empty" + /\ curPtr = NoNode + /\ memData = d + /\ auxData = d + +------------------------------------------------------------------------------- + +Store(i, d) == + /\ cache[i].state = "E" + /\ cache' = [cache EXCEPT ![i].data = d] + /\ auxData' = d + /\ UNCHANGED <> + +SendReqS(i) == + /\ chan1[i].cmd = "Empty" + /\ cache[i].state = "I" + /\ chan1' = [chan1 EXCEPT ![i].cmd = "ReqS"] + /\ UNCHANGED <> + +SendReqE(i) == + /\ chan1[i].cmd = "Empty" + /\ cache[i].state \in {"I", "S"} + /\ chan1' = [chan1 EXCEPT ![i].cmd = "ReqE"] + /\ UNCHANGED <> + +RecvGntS(i) == + /\ chan2[i].cmd = "GntS" + /\ cache' = [cache EXCEPT ![i].state = "S", ![i].data = chan2[i].data] + /\ chan2' = [chan2 EXCEPT ![i].cmd = "Empty", ![i].data = NoData] + /\ UNCHANGED <> + +RecvGntE(i) == + /\ chan2[i].cmd = "GntE" + /\ cache' = [cache EXCEPT ![i].state = "E", ![i].data = chan2[i].data] + /\ chan2' = [chan2 EXCEPT ![i].cmd = "Empty", ![i].data = NoData] + /\ UNCHANGED <> + +SendInvAck(i) == + /\ chan2[i].cmd = "Inv" + /\ chan3[i].cmd = "Empty" + /\ chan2' = [chan2 EXCEPT ![i].cmd = "Empty", ![i].data = NoData] + /\ chan3' = [chan3 EXCEPT ![i].cmd = "InvAck", + ![i].data = IF cache[i].state = "E" + THEN cache[i].data + ELSE NoData] + /\ cache' = [cache EXCEPT ![i].state = "I", ![i].data = NoData] + /\ UNCHANGED <> + +------------------------------------------------------------------------------- + +RecvReqS(i) == + /\ curCmd = "Empty" + /\ chan1[i].cmd = "ReqS" + /\ curCmd' = "ReqS" + /\ curPtr' = i + /\ chan1' = [chan1 EXCEPT ![i].cmd = "Empty"] + /\ invSet' = shrSet + /\ UNCHANGED <> + +RecvReqE(i) == + /\ curCmd = "Empty" + /\ chan1[i].cmd = "ReqE" + /\ curCmd' = "ReqE" + /\ curPtr' = i + /\ chan1' = [chan1 EXCEPT ![i].cmd = "Empty"] + /\ invSet' = shrSet + /\ UNCHANGED <> + +SendInv(i) == + /\ chan2[i].cmd = "Empty" + /\ invSet[i] = TRUE + /\ (curCmd = "ReqE" \/ (curCmd = "ReqS" /\ exGntd = TRUE)) + /\ chan2' = [chan2 EXCEPT ![i].cmd = "Inv"] + /\ invSet' = [invSet EXCEPT ![i] = FALSE] + /\ UNCHANGED <> + +RecvInvAck(i) == + /\ chan3[i].cmd = "InvAck" + /\ curCmd # "Empty" + /\ shrSet' = [shrSet EXCEPT ![i] = FALSE] + /\ IF exGntd = TRUE + THEN /\ exGntd' = FALSE + /\ memData' = chan3[i].data + /\ chan3' = [chan3 EXCEPT ![i].cmd = "Empty", ![i].data = NoData] + ELSE /\ chan3' = [chan3 EXCEPT ![i].cmd = "Empty"] + /\ UNCHANGED <> + /\ UNCHANGED <> + +SendGntS(i) == + /\ curCmd = "ReqS" + /\ curPtr = i + /\ chan2[i].cmd = "Empty" + /\ exGntd = FALSE + /\ chan2' = [chan2 EXCEPT ![i].cmd = "GntS", ![i].data = memData] + /\ shrSet' = [shrSet EXCEPT ![i] = TRUE] + /\ curCmd' = "Empty" + /\ curPtr' = NoNode + /\ UNCHANGED <> + +SendGntE(i) == + /\ curCmd = "ReqE" + /\ curPtr = i + /\ chan2[i].cmd = "Empty" + /\ exGntd = FALSE + /\ \A j \in NODE : shrSet[j] = FALSE + /\ chan2' = [chan2 EXCEPT ![i].cmd = "GntE", ![i].data = memData] + /\ shrSet' = [shrSet EXCEPT ![i] = TRUE] + /\ exGntd' = TRUE + /\ curCmd' = "Empty" + /\ curPtr' = NoNode + /\ UNCHANGED <> + +------------------------------------------------------------------------------- + +Next == + \/ \E i \in NODE, d \in DATA : Store(i, d) + \/ \E i \in NODE : + \/ SendReqS(i) \/ SendReqE(i) + \/ RecvReqS(i) \/ RecvReqE(i) + \/ SendInv(i) \/ SendInvAck(i) \/ RecvInvAck(i) + \/ SendGntS(i) \/ SendGntE(i) + \/ RecvGntS(i) \/ RecvGntE(i) + +Spec == Init /\ [][Next]_vars + +------------------------------------------------------------------------------- + +Abstract == INSTANCE GermanCoherence WITH + cache <- [i \in NODE |-> cache[i].state], + chan1 <- [i \in NODE |-> chan1[i].cmd], + chan2 <- [i \in NODE |-> chan2[i].cmd], + chan3 <- [i \in NODE |-> chan3[i].cmd] + +Refinement == Abstract!Spec + +------------------------------------------------------------------------------- + +Coherence == + \A i, j \in NODE : + i # j => + /\ (cache[i].state = "E" => cache[j].state = "I") + /\ (cache[i].state = "S" => cache[j].state \in {"I", "S"}) + +DataProp == + /\ (exGntd = FALSE => memData = auxData) + /\ \A i \in NODE : cache[i].state # "I" => cache[i].data = auxData + +------------------------------------------------------------------------------- + +ChannelWellFormed == + \A i \in NODE : + /\ chan1[i].cmd \in {"Empty", "ReqS", "ReqE"} + /\ chan2[i].cmd \in {"Empty", "Inv", "GntS", "GntE"} + /\ chan3[i].cmd \in {"Empty", "InvAck"} + +TransactionConsistency == + (curCmd = "Empty") <=> (curPtr = NoNode) + +DirectoryAccurate == + \A i \in NODE : cache[i].state \in {"S", "E"} => shrSet[i] = TRUE + +ExclusiveIsolation == + \A i \in NODE : + cache[i].state = "E" => + /\ exGntd = TRUE + /\ \A j \in NODE : + j # i => + /\ cache[j].state = "I" + /\ chan2[j].cmd \notin {"GntS", "GntE"} + /\ chan3[j].cmd # "InvAck" + +WritebackCarriesLatest == + \A i \in NODE : + (chan3[i].cmd = "InvAck" /\ curCmd # "Empty" /\ exGntd = TRUE) => + /\ chan3[i].data = auxData + /\ \A j \in NODE : + j # i => + /\ cache[j].state # "E" + /\ chan2[j].cmd # "GntE" + /\ chan3[j].cmd # "InvAck" + +------------------------------------------------------------------------------- + +Fairness == + \A i \in NODE : + /\ SF_vars(RecvReqS(i)) + /\ SF_vars(RecvReqE(i)) + /\ WF_vars(SendInv(i)) + /\ WF_vars(SendInvAck(i)) + /\ WF_vars(RecvInvAck(i)) + /\ WF_vars(SendGntS(i)) + /\ WF_vars(SendGntE(i)) + /\ WF_vars(RecvGntS(i)) + /\ WF_vars(RecvGntE(i)) + +FairSpec == Spec /\ Fairness + +RequestEventuallyServed == + \A i \in NODE : + (chan1[i].cmd \in {"ReqS", "ReqE"}) ~> (chan1[i].cmd = "Empty") + +SharedRequestEventuallyGranted == + \A i \in NODE : + (chan1[i].cmd = "ReqS") ~> (cache[i].state # "I") + +ExclusiveRequestEventuallyGranted == + \A i \in NODE : + (chan1[i].cmd = "ReqE") ~> (cache[i].state = "E") + +============================================================================= diff --git a/specifications/GermanProtocol/MCGerman.cfg b/specifications/GermanProtocol/MCGerman.cfg new file mode 100644 index 00000000..c7f4e6fb --- /dev/null +++ b/specifications/GermanProtocol/MCGerman.cfg @@ -0,0 +1,16 @@ +\* Smallest meaningful instance of the CMP abstraction: two concrete nodes +\* (needed for Coherence to be non-vacuous) plus the single abstract node Other +\* that summarises all remaining nodes. +CONSTANTS + NODE = {n1, n2} + Other = other + NoNode = noNode + +SYMMETRY Symmetry + +SPECIFICATION Spec + +INVARIANT + TypeOK + Coherence + Lemma_1 diff --git a/specifications/GermanProtocol/MCGerman.tla b/specifications/GermanProtocol/MCGerman.tla new file mode 100644 index 00000000..29a5bcd3 --- /dev/null +++ b/specifications/GermanProtocol/MCGerman.tla @@ -0,0 +1,8 @@ +----------------------------- MODULE MCGerman ----------------------------- +EXTENDS German, TLC + +\* The concrete nodes are interchangeable, so collapse permutations of NODE. +\* Other and NoNode are fixed sentinels and are not permuted. +Symmetry == Permutations(NODE) + +============================================================================== diff --git a/specifications/GermanProtocol/MCGermanCoherence.cfg b/specifications/GermanProtocol/MCGermanCoherence.cfg new file mode 100644 index 00000000..01dbecb2 --- /dev/null +++ b/specifications/GermanProtocol/MCGermanCoherence.cfg @@ -0,0 +1,13 @@ +\* Smallest meaningful instance: two nodes are required for the mutual-exclusion +\* property Coherence (i # j) to be non-vacuous. +CONSTANTS + NODE = {n1, n2} + NoNode = noNode + +SYMMETRY Symmetry + +SPECIFICATION Spec + +INVARIANT + TypeOK + Coherence diff --git a/specifications/GermanProtocol/MCGermanCoherence.tla b/specifications/GermanProtocol/MCGermanCoherence.tla new file mode 100644 index 00000000..1f3cbb5e --- /dev/null +++ b/specifications/GermanProtocol/MCGermanCoherence.tla @@ -0,0 +1,7 @@ +------------------------- MODULE MCGermanCoherence ------------------------- +EXTENDS GermanCoherence, TLC + +\* Nodes are interchangeable, so collapse permutations of NODE. +Symmetry == Permutations(NODE) + +============================================================================== diff --git a/specifications/GermanProtocol/MCGermanWithMutex.cfg b/specifications/GermanProtocol/MCGermanWithMutex.cfg new file mode 100644 index 00000000..d4ac815d --- /dev/null +++ b/specifications/GermanProtocol/MCGermanWithMutex.cfg @@ -0,0 +1,26 @@ +\* Smallest meaningful instance: two nodes (Coherence needs i # j) and two +\* distinct data values, so that writes are distinguishable and the data-integrity +\* property DataProp is exercised non-vacuously. +\* +\* Besides the safety invariants this model also checks the refinement +\* Spec => Abstract!Spec (the data-forgetting projection onto GermanCoherence, +\* defined in GermanWithMutex.tla). +CONSTANTS + NODE = {n1, n2} + DATA = {d1, d2} + NoData = noData + NoNode = noNode + +SPECIFICATION Spec + +INVARIANT + TypeOK + Coherence + DataProp + ChannelWellFormed + TransactionConsistency + DirectoryAccurate + ExclusiveIsolation + WritebackCarriesLatest + +PROPERTY Refinement diff --git a/specifications/GermanProtocol/MCGermanWithMutex.tla b/specifications/GermanProtocol/MCGermanWithMutex.tla new file mode 100644 index 00000000..da3d8857 --- /dev/null +++ b/specifications/GermanProtocol/MCGermanWithMutex.tla @@ -0,0 +1,4 @@ +------------------------- MODULE MCGermanWithMutex ------------------------- +EXTENDS GermanWithMutex + +============================================================================== diff --git a/specifications/GermanProtocol/README.md b/specifications/GermanProtocol/README.md new file mode 100644 index 00000000..bd1489c9 --- /dev/null +++ b/specifications/GermanProtocol/README.md @@ -0,0 +1,113 @@ +# German Protocol Deadlock Example + +The TLA+ specifications in this directory are **agentic translations** — produced +by an AI coding agent — and adaptations of the Murphi German cache-coherence +protocol (see *Provenance* below). Each TLA+ specification is checked to +describe the *same* system as its Murphi counterpart — not just that they satisfy +the same properties, but that they exhibit exactly the same behavior, step for +step. + +## What "equivalent" means here + +Murphi and TLA+ share essentially the same underlying semantics: each defines a +system as a set of behaviors — sequences of states generated by +nondeterministically firing guarded transitions (Murphi rules, TLA+ actions) from +a set of initial states. This common operational semantics is what renders the +two specifications comparable, and it permits each to be interpreted as the same +kind of structure — a labeled transition system (LTS): a set of states (each a +valuation of the model's variables), a set of initial states, and transitions +between states, every transition labeled by the action that produced it. + +The two models are declared equivalent iff their LTSs are **strongly +bisimilar** — i.e. there exists a relation pairing states of one side with states +of the other such that: + +- every initial state on each side is paired with an initial state on the other; +- paired states agree on their observable variable valuations; and +- for every labeled transition one side can take, the other can take a + transition with the *same* label into an again-paired state. + +When no bisimulation exists, the check produces a counterexample rather than +a bare yes/no. + +## How the tools fit together + +Neither model checker checks any properties or decides equivalence. Each only +exhaustively explores its own model and emits its LTS; an independent comparator +then decides bisimilarity. + +- CMurphi: exhaustively explores the Murphi model's reachable state space — a + breadth-first search with the symmetry/multiset reductions turned off — and + uses its built-in graph export to emit an LTS of every reachable state and + every fired transition. +- TLC: exhaustively enumerates the TLA+ model's reachable states and uses its + state-graph dump hook to emit an LTS of the states and their labeled + transitions. +- The comparator (a Python program) reads both LTSs (converted into one + shared format), aligns them into the shared vocabulary, decides whether they + are strongly bisimilar, and reports the verdict. + +## Limitations + +Only finite models can be exported and compared (the usual model-checking +constraint). Bisimilarity requires the action granularity to align — each +Murphi rule must correspond to a TLA+ action — and paired states must share the +same observable valuation, so the result is a state-respecting strong +bisimulation. Tractability is bounded by state-space explosion: both sides' +complete reachable graphs must be enumerated, exported, and compared, so the +models must stay small enough for each full graph to be materialized. Finally, +this approach compares only the behavior of the two models; it does not check +that their correctness properties (invariants) are themselves equivalent. + +## Provenance + +The TLA+ specification in this directory was created by translating and adapting one or more of the Murphi specifications from: + +> Divjyot Sethi, `ProtocolDeadlockFiles`, GitHub repository. +> https://github.com/dsethi/ProtocolDeadlockFiles/ + +That repository was published as supplementary Murphi source code for: + +> Divjyot Sethi, Muralidhar Talupur, and Sharad Malik, +> “Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom,” +> *Automated Technology for Verification and Analysis (ATVA 2014)*, LNCS 8837, pp. 330–347. +> DOI: `10.1007/978-3-319-11936-6_24` + +The Murphi files in that repository include variants such as `germanNoMutex.m`, `germanWithMutex.m`, and `germanBuggy.m`. These variants are used in the [ATVA 2014 work](https://arxiv.org/pdf/1407.7468) to study deadlock freedom, including a deliberately buggy version that demonstrates a deadlock. + +The underlying German protocol model is older than the Sethi–Talupur–Malik artifact. The ATVA 2014 paper identifies its German protocol code as being based on the Murphi model from: + +> Ching-Tsun Chou, Phanindra K. Mannava, and Seungjoon Park, +> “A Simple Method for Parameterized Verification of Cache Coherence Protocols,” +> *Formal Methods in Computer-Aided Design (FMCAD 2004)*, LNCS 3312, pp. 382–398. +> DOI: `10.1007/978-3-540-30494-4_27` + +That paper attributes the protocol itself to Steven M. German by personal communication. +Steven German's own tutorial on the protocol is available here: + +> Steven German, "Tutorial on the German Cache Coherence Protocol." +> https://users.cs.utah.edu/~ganesh/presentations/fmcad04_tutorial2/german/steven-tutorial.pdf + +In summary, the provenance of this TLA+ example is: + +```text +Steven M. German protocol benchmark + -> Chou, Mannava, and Park Murphi model, FMCAD 2004 + -> Sethi, Talupur, and Malik Murphi deadlock examples, ATVA 2014 + -> this TLA+ translation/adaptation +``` + +## Attribution + +Please cite the original Murphi artifact and the related publications when reusing this example in research, teaching, or derivative artifacts: + +1. Divjyot Sethi, Muralidhar Talupur, and Sharad Malik, “Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom,” ATVA 2014. +2. Ching-Tsun Chou, Phanindra K. Mannava, and Seungjoon Park, “A Simple Method for Parameterized Verification of Cache Coherence Protocols,” FMCAD 2004. +3. Divjyot Sethi’s `ProtocolDeadlockFiles` repository: https://github.com/dsethi/ProtocolDeadlockFiles/ +4. Steven German, “Tutorial on the German Cache Coherence Protocol”: https://users.cs.utah.edu/~ganesh/presentations/fmcad04_tutorial2/german/steven-tutorial.pdf + +## Licensing + +The TLA+ files in this directory should be distributed under the license used by `examples.tlapl.us`, unless otherwise stated. + +Because this example was derived from Murphi source code in an external repository, users should also review the licensing and attribution requirements of the upstream artifact before redistributing modified versions. diff --git a/specifications/GermanProtocol/manifest.json b/specifications/GermanProtocol/manifest.json new file mode 100644 index 00000000..c62a29a1 --- /dev/null +++ b/specifications/GermanProtocol/manifest.json @@ -0,0 +1,110 @@ +{ + "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.", + "Steven German, \"Tutorial on the German Cache Coherence Protocol,\" https://users.cs.utah.edu/~ganesh/presentations/fmcad04_tutorial2/german/steven-tutorial.pdf" + ], + "authors": [ + "Markus Kuppe" + ], + "tags": [], + "modules": [ + { + "path": "specifications/GermanProtocol/APGerman.tla", + "features": [], + "models": [ + { + "path": "specifications/GermanProtocol/APGerman.cfg", + "runtime": "00:00:20", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "path": "specifications/GermanProtocol/APGermanCoherence.tla", + "features": [], + "models": [ + { + "path": "specifications/GermanProtocol/APGermanCoherence.cfg", + "runtime": "00:00:08", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "path": "specifications/GermanProtocol/APGermanWithMutex.tla", + "features": [], + "models": [ + { + "path": "specifications/GermanProtocol/APGermanWithMutex.cfg", + "runtime": "00:00:39", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "path": "specifications/GermanProtocol/German.tla", + "features": [], + "models": [] + }, + { + "path": "specifications/GermanProtocol/GermanCoherence.tla", + "features": [], + "models": [] + }, + { + "path": "specifications/GermanProtocol/GermanWithMutex.tla", + "features": [], + "models": [] + }, + { + "path": "specifications/GermanProtocol/MCGerman.tla", + "features": [], + "models": [ + { + "path": "specifications/GermanProtocol/MCGerman.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 1107, + "totalStates": 3281, + "stateDepth": 19 + } + ] + }, + { + "path": "specifications/GermanProtocol/MCGermanCoherence.tla", + "features": [], + "models": [ + { + "path": "specifications/GermanProtocol/MCGermanCoherence.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 735, + "totalStates": 1946, + "stateDepth": 19 + } + ] + }, + { + "path": "specifications/GermanProtocol/MCGermanWithMutex.tla", + "features": [], + "models": [ + { + "path": "specifications/GermanProtocol/MCGermanWithMutex.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 3390, + "totalStates": 9914, + "stateDepth": 19 + } + ] + } + ] +} From af48e035ee641603e542446b37bec7d8cc5eae40 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 15 Jul 2026 07:38:41 -0700 Subject: [PATCH 02/12] Document ABS_RecvInvAck's noninterference conjunct Explain that the \A j conjunct in the ABS_RecvInvAck action's enabling condition is the operational mutual-exclusion noninterference lemma (Chou/Mannava/Park FMCAD 2004; Sethi/Talupur/Malik arXiv:1407.7468): germanWithMutex.m conjoins it, germanNoMutex.m deliberately omits it. Co-authored-by: Claude Opus 4.8 Signed-off-by: Markus Alexander Kuppe --- specifications/GermanProtocol/German.tla | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/specifications/GermanProtocol/German.tla b/specifications/GermanProtocol/German.tla index e873a046..57511e39 100644 --- a/specifications/GermanProtocol/German.tla +++ b/specifications/GermanProtocol/German.tla @@ -171,6 +171,14 @@ ABS_SendGntE == ABS_RecvInvAck == /\ curCmd # "Empty" /\ exGntd = TRUE + \* Operational form of the mutual-exclusion noninterference lemma ("Lemma_1" + \* of Chou, Mannava & Park, FMCAD 2004 = ref [11] of Sethi, Talupur & Malik, + \* arXiv:1407.7468, whose online models these are). germanWithMutex.m is the + \* CMP-strengthened abstraction that conjoins this guard onto absRecvInvAck; + \* germanNoMutex.m omits it on purpose -- the deadlock-study model that needs + \* no noninterference lemma -- so it admits the spurious "bogus InvAck from + \* Other" counterexample to mutual exclusion. Dropping this one conjunct makes + \* German.tla bisimilar to germanNoMutex.m. /\ \A j \in NODE : /\ cache[j] # "E" /\ chan2[j] # "GntE" From 1244293aa7ce7764d67449b32fd291b5e06c99e4 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 13 Jul 2026 15:57:37 -0700 Subject: [PATCH 03/12] Towards idiomatic TLA+: Merge shared/exclusive action pairs. These specs were translated from Murphi, whose rules cannot express intra-action nondeterminism, so a single nondeterministic choice must be split across separate rules. TLA+ expresses that choice directly with existential quantification and disjunction, so collapse each flavour-split pair into one action. This removes the duplication the Murphi encoding forced without changing the specs' behaviors. Verified equivalence-preserving with TLAPS: an auxiliary module per spec keeps the old split actions as _o operators, and TLAPS proves Next <=> Next_o (one BY DEF biconditional lemma per merged action). ```tla (* Per-action equivalences (divide and conquer). *) LEMMA SendReqEquiv == ASSUME NEW i \in NODE PROVE SendReq(i) <=> (SendReqS_o(i) \/ SendReqE_o(i)) BY DEF SendReq, SendReqS_o, SendReqE_o LEMMA RecvReqEquiv == ASSUME NEW i \in NODE PROVE RecvReq(i) <=> (RecvReqS_o(i) \/ RecvReqE_o(i)) BY DEF RecvReq, RecvReqS_o, RecvReqE_o LEMMA SendGntEquiv == ASSUME NEW i \in NODE PROVE SendGnt(i) <=> (SendGntS_o(i) \/ SendGntE_o(i)) BY DEF SendGnt, SendGntS_o, SendGntE_o LEMMA RecvGntEquiv == ASSUME NEW i \in NODE PROVE RecvGnt(i) <=> (RecvGntS_o(i) \/ RecvGntE_o(i)) BY DEF RecvGnt, RecvGntS_o, RecvGntE_o ------------------------------------------------------------------------------- (* Coarse-grained equivalence at the level of Next. *) THEOREM NextEquiv == Next <=> Next_o BY SendReqEquiv, RecvReqEquiv, SendGntEquiv, RecvGntEquiv DEF Next, Next_o ``` Co-authored-by: Claude Opus 4.8 Signed-off-by: Markus Alexander Kuppe --- specifications/GermanProtocol/German.tla | 100 +++++------------- .../GermanProtocol/GermanCoherence.tla | 69 ++++-------- .../GermanProtocol/GermanWithMutex.tla | 83 +++++---------- 3 files changed, 70 insertions(+), 182 deletions(-) diff --git a/specifications/GermanProtocol/German.tla b/specifications/GermanProtocol/German.tla index 57511e39..a65e86ae 100644 --- a/specifications/GermanProtocol/German.tla +++ b/specifications/GermanProtocol/German.tla @@ -41,31 +41,17 @@ Init == ------------------------------------------------------------------------------- -SendReqS(i) == +SendReq(i) == /\ chan1[i] = "Empty" - /\ cache[i] = "I" - /\ chan1' = [chan1 EXCEPT ![i] = "ReqS"] + /\ \E c \in {"ReqS", "ReqE"} : + /\ cache[i] \in (IF c = "ReqS" THEN {"I"} ELSE {"I", "S"}) + /\ chan1' = [chan1 EXCEPT ![i] = c] /\ UNCHANGED <> -SendReqE(i) == - /\ chan1[i] = "Empty" - /\ cache[i] \in {"I", "S"} - /\ chan1' = [chan1 EXCEPT ![i] = "ReqE"] - /\ UNCHANGED <> - -RecvReqS(i) == +RecvReq(i) == /\ curCmd = "Empty" - /\ chan1[i] = "ReqS" - /\ curCmd' = "ReqS" - /\ curPtr' = i - /\ chan1' = [chan1 EXCEPT ![i] = "Empty"] - /\ invSet' = shrSet - /\ UNCHANGED <> - -RecvReqE(i) == - /\ curCmd = "Empty" - /\ chan1[i] = "ReqE" - /\ curCmd' = "ReqE" + /\ chan1[i] \in {"ReqS", "ReqE"} + /\ curCmd' = chan1[i] /\ curPtr' = i /\ chan1' = [chan1 EXCEPT ![i] = "Empty"] /\ invSet' = shrSet @@ -95,72 +81,40 @@ RecvInvAck(i) == /\ exGntd' = IF exGntd = TRUE THEN FALSE ELSE exGntd /\ UNCHANGED <> -SendGntS(i) == - /\ curCmd = "ReqS" +SendGnt(i) == + /\ curCmd \in {"ReqS", "ReqE"} /\ curPtr = i /\ chan2[i] = "Empty" /\ exGntd = FALSE - /\ chan2' = [chan2 EXCEPT ![i] = "GntS"] + /\ curCmd = "ReqE" => \A j \in NODE : shrSet[j] = FALSE + /\ chan2' = [chan2 EXCEPT ![i] = IF curCmd = "ReqS" THEN "GntS" ELSE "GntE"] /\ shrSet' = [shrSet EXCEPT ![i] = TRUE] - /\ curCmd' = "Empty" - /\ curPtr' = NoNode - /\ UNCHANGED <> - -SendGntE(i) == - /\ curCmd = "ReqE" - /\ curPtr = i - /\ chan2[i] = "Empty" - /\ exGntd = FALSE - /\ \A j \in NODE : shrSet[j] = FALSE - /\ chan2' = [chan2 EXCEPT ![i] = "GntE"] - /\ shrSet' = [shrSet EXCEPT ![i] = TRUE] - /\ exGntd' = TRUE + /\ exGntd' = (curCmd = "ReqE") /\ curCmd' = "Empty" /\ curPtr' = NoNode /\ UNCHANGED <> -RecvGntS(i) == - /\ chan2[i] = "GntS" - /\ cache' = [cache EXCEPT ![i] = "S"] - /\ chan2' = [chan2 EXCEPT ![i] = "Empty"] - /\ UNCHANGED <> - -RecvGntE(i) == - /\ chan2[i] = "GntE" - /\ cache' = [cache EXCEPT ![i] = "E"] +RecvGnt(i) == + /\ chan2[i] \in {"GntS", "GntE"} + /\ cache' = [cache EXCEPT ![i] = IF chan2[i] = "GntS" THEN "S" ELSE "E"] /\ chan2' = [chan2 EXCEPT ![i] = "Empty"] /\ UNCHANGED <> ------------------------------------------------------------------------------- -ABS_RecvReqS == - /\ curCmd = "Empty" - /\ curCmd' = "ReqS" - /\ curPtr' = Other - /\ invSet' = shrSet - /\ UNCHANGED <> - -ABS_RecvReqE == +ABS_RecvReq == /\ curCmd = "Empty" - /\ curCmd' = "ReqE" + /\ \E c \in {"ReqS", "ReqE"} : curCmd' = c /\ curPtr' = Other /\ invSet' = shrSet /\ UNCHANGED <> -ABS_SendGntS == - /\ curCmd = "ReqS" - /\ curPtr = Other - /\ exGntd = FALSE - /\ curCmd' = "Empty" - /\ curPtr' = NoNode - /\ UNCHANGED <> - -ABS_SendGntE == - /\ curCmd = "ReqE" +ABS_SendGnt == + /\ curCmd \in {"ReqS", "ReqE"} /\ curPtr = Other /\ exGntd = FALSE - /\ \A j \in NODE : shrSet[j] = FALSE - /\ exGntd' = TRUE + /\ curCmd = "ReqE" => \A j \in NODE : shrSet[j] = FALSE + /\ exGntd' = (curCmd = "ReqE") /\ curCmd' = "Empty" /\ curPtr' = NoNode /\ UNCHANGED <> @@ -190,13 +144,13 @@ ABS_RecvInvAck == Next == \/ \E i \in NODE : - \/ SendReqS(i) \/ SendReqE(i) - \/ RecvReqS(i) \/ RecvReqE(i) + \/ SendReq(i) + \/ RecvReq(i) \/ SendInv(i) \/ SendInvAck(i) \/ RecvInvAck(i) - \/ SendGntS(i) \/ SendGntE(i) - \/ RecvGntS(i) \/ RecvGntE(i) - \/ ABS_RecvReqS \/ ABS_RecvReqE - \/ ABS_SendGntS \/ ABS_SendGntE + \/ SendGnt(i) + \/ RecvGnt(i) + \/ ABS_RecvReq + \/ ABS_SendGnt \/ ABS_RecvInvAck Spec == Init /\ [][Next]_vars diff --git a/specifications/GermanProtocol/GermanCoherence.tla b/specifications/GermanProtocol/GermanCoherence.tla index f88435c9..3a1f4661 100644 --- a/specifications/GermanProtocol/GermanCoherence.tla +++ b/specifications/GermanProtocol/GermanCoherence.tla @@ -47,31 +47,17 @@ Init == ------------------------------------------------------------------------------- -SendReqS(i) == +SendReq(i) == /\ chan1[i] = "Empty" - /\ cache[i] = "I" - /\ chan1' = [chan1 EXCEPT ![i] = "ReqS"] + /\ \E c \in {"ReqS", "ReqE"} : + /\ cache[i] \in (IF c = "ReqS" THEN {"I"} ELSE {"I", "S"}) + /\ chan1' = [chan1 EXCEPT ![i] = c] /\ UNCHANGED <> -SendReqE(i) == - /\ chan1[i] = "Empty" - /\ cache[i] \in {"I", "S"} - /\ chan1' = [chan1 EXCEPT ![i] = "ReqE"] - /\ UNCHANGED <> - -RecvReqS(i) == - /\ curCmd = "Empty" - /\ chan1[i] = "ReqS" - /\ curCmd' = "ReqS" - /\ curPtr' = i - /\ chan1' = [chan1 EXCEPT ![i] = "Empty"] - /\ invSet' = shrSet - /\ UNCHANGED <> - -RecvReqE(i) == +RecvReq(i) == /\ curCmd = "Empty" - /\ chan1[i] = "ReqE" - /\ curCmd' = "ReqE" + /\ chan1[i] \in {"ReqS", "ReqE"} + /\ curCmd' = chan1[i] /\ curPtr' = i /\ chan1' = [chan1 EXCEPT ![i] = "Empty"] /\ invSet' = shrSet @@ -101,39 +87,22 @@ RecvInvAck(i) == /\ exGntd' = IF exGntd = TRUE THEN FALSE ELSE exGntd /\ UNCHANGED <> -SendGntS(i) == - /\ curCmd = "ReqS" +SendGnt(i) == + /\ curCmd \in {"ReqS", "ReqE"} /\ curPtr = i /\ chan2[i] = "Empty" /\ exGntd = FALSE - /\ chan2' = [chan2 EXCEPT ![i] = "GntS"] + /\ curCmd = "ReqE" => \A j \in NODE : shrSet[j] = FALSE + /\ chan2' = [chan2 EXCEPT ![i] = IF curCmd = "ReqS" THEN "GntS" ELSE "GntE"] /\ shrSet' = [shrSet EXCEPT ![i] = TRUE] - /\ curCmd' = "Empty" - /\ curPtr' = NoNode - /\ UNCHANGED <> - -SendGntE(i) == - /\ curCmd = "ReqE" - /\ curPtr = i - /\ chan2[i] = "Empty" - /\ exGntd = FALSE - /\ \A j \in NODE : shrSet[j] = FALSE - /\ chan2' = [chan2 EXCEPT ![i] = "GntE"] - /\ shrSet' = [shrSet EXCEPT ![i] = TRUE] - /\ exGntd' = TRUE + /\ exGntd' = (curCmd = "ReqE") /\ curCmd' = "Empty" /\ curPtr' = NoNode /\ UNCHANGED <> -RecvGntS(i) == - /\ chan2[i] = "GntS" - /\ cache' = [cache EXCEPT ![i] = "S"] - /\ chan2' = [chan2 EXCEPT ![i] = "Empty"] - /\ UNCHANGED <> - -RecvGntE(i) == - /\ chan2[i] = "GntE" - /\ cache' = [cache EXCEPT ![i] = "E"] +RecvGnt(i) == + /\ chan2[i] \in {"GntS", "GntE"} + /\ cache' = [cache EXCEPT ![i] = IF chan2[i] = "GntS" THEN "S" ELSE "E"] /\ chan2' = [chan2 EXCEPT ![i] = "Empty"] /\ UNCHANGED <> @@ -141,11 +110,11 @@ RecvGntE(i) == Next == \E i \in NODE : - \/ SendReqS(i) \/ SendReqE(i) - \/ RecvReqS(i) \/ RecvReqE(i) + \/ SendReq(i) + \/ RecvReq(i) \/ SendInv(i) \/ SendInvAck(i) \/ RecvInvAck(i) - \/ SendGntS(i) \/ SendGntE(i) - \/ RecvGntS(i) \/ RecvGntE(i) + \/ SendGnt(i) + \/ RecvGnt(i) Spec == Init /\ [][Next]_vars diff --git a/specifications/GermanProtocol/GermanWithMutex.tla b/specifications/GermanProtocol/GermanWithMutex.tla index d26bb973..f562b087 100644 --- a/specifications/GermanProtocol/GermanWithMutex.tla +++ b/specifications/GermanProtocol/GermanWithMutex.tla @@ -69,30 +69,18 @@ Store(i, d) == /\ UNCHANGED <> -SendReqS(i) == +SendReq(i) == /\ chan1[i].cmd = "Empty" - /\ cache[i].state = "I" - /\ chan1' = [chan1 EXCEPT ![i].cmd = "ReqS"] + /\ \E c \in {"ReqS", "ReqE"} : + /\ cache[i].state \in (IF c = "ReqS" THEN {"I"} ELSE {"I", "S"}) + /\ chan1' = [chan1 EXCEPT ![i].cmd = c] /\ UNCHANGED <> -SendReqE(i) == - /\ chan1[i].cmd = "Empty" - /\ cache[i].state \in {"I", "S"} - /\ chan1' = [chan1 EXCEPT ![i].cmd = "ReqE"] - /\ UNCHANGED <> - -RecvGntS(i) == - /\ chan2[i].cmd = "GntS" - /\ cache' = [cache EXCEPT ![i].state = "S", ![i].data = chan2[i].data] - /\ chan2' = [chan2 EXCEPT ![i].cmd = "Empty", ![i].data = NoData] - /\ UNCHANGED <> - -RecvGntE(i) == - /\ chan2[i].cmd = "GntE" - /\ cache' = [cache EXCEPT ![i].state = "E", ![i].data = chan2[i].data] +RecvGnt(i) == + /\ chan2[i].cmd \in {"GntS", "GntE"} + /\ cache' = [cache EXCEPT ![i].state = IF chan2[i].cmd = "GntS" THEN "S" ELSE "E", + ![i].data = chan2[i].data] /\ chan2' = [chan2 EXCEPT ![i].cmd = "Empty", ![i].data = NoData] /\ UNCHANGED <> @@ -111,20 +99,10 @@ SendInvAck(i) == ------------------------------------------------------------------------------- -RecvReqS(i) == - /\ curCmd = "Empty" - /\ chan1[i].cmd = "ReqS" - /\ curCmd' = "ReqS" - /\ curPtr' = i - /\ chan1' = [chan1 EXCEPT ![i].cmd = "Empty"] - /\ invSet' = shrSet - /\ UNCHANGED <> - -RecvReqE(i) == +RecvReq(i) == /\ curCmd = "Empty" - /\ chan1[i].cmd = "ReqE" - /\ curCmd' = "ReqE" + /\ chan1[i].cmd \in {"ReqS", "ReqE"} + /\ curCmd' = chan1[i].cmd /\ curPtr' = i /\ chan1' = [chan1 EXCEPT ![i].cmd = "Empty"] /\ invSet' = shrSet @@ -152,26 +130,16 @@ RecvInvAck(i) == /\ UNCHANGED <> /\ UNCHANGED <> -SendGntS(i) == - /\ curCmd = "ReqS" - /\ curPtr = i - /\ chan2[i].cmd = "Empty" - /\ exGntd = FALSE - /\ chan2' = [chan2 EXCEPT ![i].cmd = "GntS", ![i].data = memData] - /\ shrSet' = [shrSet EXCEPT ![i] = TRUE] - /\ curCmd' = "Empty" - /\ curPtr' = NoNode - /\ UNCHANGED <> - -SendGntE(i) == - /\ curCmd = "ReqE" +SendGnt(i) == + /\ curCmd \in {"ReqS", "ReqE"} /\ curPtr = i /\ chan2[i].cmd = "Empty" /\ exGntd = FALSE - /\ \A j \in NODE : shrSet[j] = FALSE - /\ chan2' = [chan2 EXCEPT ![i].cmd = "GntE", ![i].data = memData] + /\ curCmd = "ReqE" => \A j \in NODE : shrSet[j] = FALSE + /\ chan2' = [chan2 EXCEPT ![i].cmd = IF curCmd = "ReqS" THEN "GntS" ELSE "GntE", + ![i].data = memData] /\ shrSet' = [shrSet EXCEPT ![i] = TRUE] - /\ exGntd' = TRUE + /\ exGntd' = (curCmd = "ReqE") /\ curCmd' = "Empty" /\ curPtr' = NoNode /\ UNCHANGED <> @@ -181,11 +149,11 @@ SendGntE(i) == Next == \/ \E i \in NODE, d \in DATA : Store(i, d) \/ \E i \in NODE : - \/ SendReqS(i) \/ SendReqE(i) - \/ RecvReqS(i) \/ RecvReqE(i) + \/ SendReq(i) + \/ RecvReq(i) \/ SendInv(i) \/ SendInvAck(i) \/ RecvInvAck(i) - \/ SendGntS(i) \/ SendGntE(i) - \/ RecvGntS(i) \/ RecvGntE(i) + \/ SendGnt(i) + \/ RecvGnt(i) Spec == Init /\ [][Next]_vars @@ -249,15 +217,12 @@ WritebackCarriesLatest == Fairness == \A i \in NODE : - /\ SF_vars(RecvReqS(i)) - /\ SF_vars(RecvReqE(i)) + /\ SF_vars(RecvReq(i)) /\ WF_vars(SendInv(i)) /\ WF_vars(SendInvAck(i)) /\ WF_vars(RecvInvAck(i)) - /\ WF_vars(SendGntS(i)) - /\ WF_vars(SendGntE(i)) - /\ WF_vars(RecvGntS(i)) - /\ WF_vars(RecvGntE(i)) + /\ WF_vars(SendGnt(i)) + /\ WF_vars(RecvGnt(i)) FairSpec == Spec /\ Fairness From c0fad654cc52a967e46a91eb013ccaf2aba1111b Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 20 Jul 2026 13:30:05 -0700 Subject: [PATCH 04/12] Simplify exGntd reset on invalidation acknowledgment Signed-off-by: Markus Alexander Kuppe --- specifications/GermanProtocol/German.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specifications/GermanProtocol/German.tla b/specifications/GermanProtocol/German.tla index a65e86ae..bc78a801 100644 --- a/specifications/GermanProtocol/German.tla +++ b/specifications/GermanProtocol/German.tla @@ -78,7 +78,7 @@ RecvInvAck(i) == /\ curCmd # "Empty" /\ chan3' = [chan3 EXCEPT ![i] = "Empty"] /\ shrSet' = [shrSet EXCEPT ![i] = FALSE] - /\ exGntd' = IF exGntd = TRUE THEN FALSE ELSE exGntd + /\ exGntd' = FALSE /\ UNCHANGED <> SendGnt(i) == From 2a56f7e85289ec2d613be74999bf7f6b598e980a Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 20 Jul 2026 13:30:50 -0700 Subject: [PATCH 05/12] Use set difference for distinct-node quantification Signed-off-by: Markus Alexander Kuppe --- specifications/GermanProtocol/German.tla | 3 +-- specifications/GermanProtocol/GermanWithMutex.tla | 6 ++---- 2 files changed, 3 insertions(+), 6 deletions(-) diff --git a/specifications/GermanProtocol/German.tla b/specifications/GermanProtocol/German.tla index bc78a801..3133794c 100644 --- a/specifications/GermanProtocol/German.tla +++ b/specifications/GermanProtocol/German.tla @@ -166,8 +166,7 @@ Coherence == Lemma_1 == \A i \in NODE : (chan3[i] = "InvAck" /\ curCmd # "Empty" /\ exGntd = TRUE) => - \A j \in NODE : - j # i => + \A j \in NODE \ {i} : /\ cache[j] # "E" /\ chan2[j] # "GntE" /\ chan3[j] # "InvAck" diff --git a/specifications/GermanProtocol/GermanWithMutex.tla b/specifications/GermanProtocol/GermanWithMutex.tla index f562b087..bba8cc38 100644 --- a/specifications/GermanProtocol/GermanWithMutex.tla +++ b/specifications/GermanProtocol/GermanWithMutex.tla @@ -197,8 +197,7 @@ ExclusiveIsolation == \A i \in NODE : cache[i].state = "E" => /\ exGntd = TRUE - /\ \A j \in NODE : - j # i => + /\ \A j \in NODE \ {i} : /\ cache[j].state = "I" /\ chan2[j].cmd \notin {"GntS", "GntE"} /\ chan3[j].cmd # "InvAck" @@ -207,8 +206,7 @@ WritebackCarriesLatest == \A i \in NODE : (chan3[i].cmd = "InvAck" /\ curCmd # "Empty" /\ exGntd = TRUE) => /\ chan3[i].data = auxData - /\ \A j \in NODE : - j # i => + /\ \A j \in NODE \ {i} : /\ cache[j].state # "E" /\ chan2[j].cmd # "GntE" /\ chan3[j].cmd # "InvAck" From 10fcc1faa80de00de63313bc1790cd3f07dd7537 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 20 Jul 2026 13:31:09 -0700 Subject: [PATCH 06/12] Enable node and data symmetry for GermanWithMutex Signed-off-by: Markus Alexander Kuppe --- specifications/GermanProtocol/MCGermanWithMutex.cfg | 2 ++ specifications/GermanProtocol/MCGermanWithMutex.tla | 6 +++++- specifications/GermanProtocol/manifest.json | 4 ++-- 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/specifications/GermanProtocol/MCGermanWithMutex.cfg b/specifications/GermanProtocol/MCGermanWithMutex.cfg index d4ac815d..52d39b06 100644 --- a/specifications/GermanProtocol/MCGermanWithMutex.cfg +++ b/specifications/GermanProtocol/MCGermanWithMutex.cfg @@ -11,6 +11,8 @@ CONSTANTS NoData = noData NoNode = noNode +SYMMETRY Symmetry + SPECIFICATION Spec INVARIANT diff --git a/specifications/GermanProtocol/MCGermanWithMutex.tla b/specifications/GermanProtocol/MCGermanWithMutex.tla index da3d8857..1aaa7006 100644 --- a/specifications/GermanProtocol/MCGermanWithMutex.tla +++ b/specifications/GermanProtocol/MCGermanWithMutex.tla @@ -1,4 +1,8 @@ ------------------------- MODULE MCGermanWithMutex ------------------------- -EXTENDS GermanWithMutex +EXTENDS GermanWithMutex, TLC + +\* Nodes and data values are independently interchangeable. The NoNode and +\* NoData sentinels are fixed because they are outside these sets. +Symmetry == Permutations(NODE) \union Permutations(DATA) ============================================================================== diff --git a/specifications/GermanProtocol/manifest.json b/specifications/GermanProtocol/manifest.json index c62a29a1..83b45247 100644 --- a/specifications/GermanProtocol/manifest.json +++ b/specifications/GermanProtocol/manifest.json @@ -100,8 +100,8 @@ "runtime": "00:00:01", "mode": "exhaustive search", "result": "success", - "distinctStates": 3390, - "totalStates": 9914, + "distinctStates": 852, + "totalStates": 2493, "stateDepth": 19 } ] From 1133ada103f60fa5bd6822880fcdfc746219c225 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 20 Jul 2026 13:31:32 -0700 Subject: [PATCH 07/12] Document Apalache commands, bounds, and runtimes Signed-off-by: Markus Alexander Kuppe --- specifications/GermanProtocol/APGerman.tla | 7 ++++++- specifications/GermanProtocol/APGermanCoherence.tla | 7 ++++++- specifications/GermanProtocol/APGermanWithMutex.tla | 7 ++++++- 3 files changed, 18 insertions(+), 3 deletions(-) diff --git a/specifications/GermanProtocol/APGerman.tla b/specifications/GermanProtocol/APGerman.tla index fda49d49..443c52ea 100644 --- a/specifications/GermanProtocol/APGerman.tla +++ b/specifications/GermanProtocol/APGerman.tla @@ -4,7 +4,12 @@ Nodes are modelled as an uninterpreted Apalache type (NODE); the abstract environment node Other and the NoNode sentinel share that type so that - `curPtr \in NODE \cup {Other, NoNode}` is well typed. *) + `curPtr \in NODE \cup {Other, NoNode}` is well typed. + + Run bounded model checking for executions of at most 20 Next steps with: + apalache-mc check --config=APGerman.cfg --length=20 APGerman.tla + This completes in under 10 minutes on a 2021 M1 MacBook. +*) CONSTANTS \* @type: Set(NODE); diff --git a/specifications/GermanProtocol/APGermanCoherence.tla b/specifications/GermanProtocol/APGermanCoherence.tla index 59e20c9f..a6b56e58 100644 --- a/specifications/GermanProtocol/APGermanCoherence.tla +++ b/specifications/GermanProtocol/APGermanCoherence.tla @@ -4,7 +4,12 @@ Nodes are modelled as an uninterpreted Apalache type (NODE); the NoNode sentinel shares that type so that `curPtr \in NODE \cup {NoNode}` is well - typed. *) + typed. + + Run bounded model checking for executions of at most 20 Next steps with: + apalache-mc check --config=APGermanCoherence.cfg --length=20 APGermanCoherence.tla + This completes in under 10 minutes on a 2021 M1 MacBook. +*) CONSTANTS \* @type: Set(NODE); diff --git a/specifications/GermanProtocol/APGermanWithMutex.tla b/specifications/GermanProtocol/APGermanWithMutex.tla index ccfafe71..fbd32c2b 100644 --- a/specifications/GermanProtocol/APGermanWithMutex.tla +++ b/specifications/GermanProtocol/APGermanWithMutex.tla @@ -5,7 +5,12 @@ Nodes and data values are modelled as uninterpreted Apalache types (NODE, DATA). The NoNode / NoData sentinels share those types so that the union sets in TypeOK are well typed. Only the safety invariants are checked; - Apalache does not verify the liveness properties (FairSpec) of the spec. *) + Apalache does not verify the liveness properties (FairSpec) of the spec. + + Run bounded model checking for executions of at most 10 Next steps with: + apalache-mc check --config=APGermanWithMutex.cfg --length=10 APGermanWithMutex.tla + This completes quickly on a 2021 M1 MacBook; length 20 takes over 1.5 hours. +*) CONSTANTS \* @type: Set(NODE); From 6fef511d9362b404b68aabb1581542935dcffe6b Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 20 Jul 2026 13:32:16 -0700 Subject: [PATCH 08/12] Strengthen command types in German protocol models Fold ChannelWellFormed into TypeOK and restrict each channel and curCmd to reachable command values. Signed-off-by: Markus Alexander Kuppe --- .../GermanProtocol/APGermanWithMutex.cfg | 1 - specifications/GermanProtocol/German.tla | 15 +++++----- .../GermanProtocol/GermanCoherence.tla | 9 +++--- .../GermanProtocol/GermanWithMutex.tla | 29 +++++++------------ .../GermanProtocol/MCGermanWithMutex.cfg | 1 - 5 files changed, 21 insertions(+), 34 deletions(-) diff --git a/specifications/GermanProtocol/APGermanWithMutex.cfg b/specifications/GermanProtocol/APGermanWithMutex.cfg index 3eab6f17..138f50d7 100644 --- a/specifications/GermanProtocol/APGermanWithMutex.cfg +++ b/specifications/GermanProtocol/APGermanWithMutex.cfg @@ -8,7 +8,6 @@ INVARIANT TypeOK Coherence DataProp - ChannelWellFormed TransactionConsistency DirectoryAccurate ExclusiveIsolation diff --git a/specifications/GermanProtocol/German.tla b/specifications/GermanProtocol/German.tla index 3133794c..530e6136 100644 --- a/specifications/GermanProtocol/German.tla +++ b/specifications/GermanProtocol/German.tla @@ -8,7 +8,6 @@ ASSUME Other \notin NODE ASSUME NoNode \notin NODE /\ NoNode # Other CacheState == {"I", "S", "E"} -MsgCmd == {"Empty", "ReqS", "ReqE", "Inv", "InvAck", "GntS", "GntE"} VARIABLES cache, chan1, chan2, chan3, invSet, shrSet, exGntd, curCmd, curPtr @@ -19,13 +18,13 @@ vars == <> TypeOK == /\ cache \in [NODE -> CacheState] - /\ chan1 \in [NODE -> MsgCmd] - /\ chan2 \in [NODE -> MsgCmd] - /\ chan3 \in [NODE -> MsgCmd] + /\ chan1 \in [NODE -> {"Empty", "ReqS", "ReqE"}] + /\ chan2 \in [NODE -> {"Empty", "Inv", "GntS", "GntE"}] + /\ chan3 \in [NODE -> {"Empty", "InvAck"}] /\ invSet \in [NODE -> BOOLEAN] /\ shrSet \in [NODE -> BOOLEAN] /\ exGntd \in BOOLEAN - /\ curCmd \in MsgCmd + /\ curCmd \in {"Empty", "ReqS", "ReqE"} /\ curPtr \in NODE \cup {Other, NoNode} Init == @@ -167,8 +166,8 @@ Lemma_1 == \A i \in NODE : (chan3[i] = "InvAck" /\ curCmd # "Empty" /\ exGntd = TRUE) => \A j \in NODE \ {i} : - /\ cache[j] # "E" - /\ chan2[j] # "GntE" - /\ chan3[j] # "InvAck" + /\ cache[j] # "E" + /\ chan2[j] # "GntE" + /\ chan3[j] # "InvAck" ============================================================================= diff --git a/specifications/GermanProtocol/GermanCoherence.tla b/specifications/GermanProtocol/GermanCoherence.tla index 3a1f4661..8f386dd7 100644 --- a/specifications/GermanProtocol/GermanCoherence.tla +++ b/specifications/GermanProtocol/GermanCoherence.tla @@ -6,7 +6,6 @@ CONSTANTS ASSUME NoNodeNotInNODE == NoNode \notin NODE CacheState == {"I", "S", "E"} -MsgCmd == {"Empty", "ReqS", "ReqE", "Inv", "InvAck", "GntS", "GntE"} VARIABLES cache, @@ -25,13 +24,13 @@ vars == <> TypeOK == /\ cache \in [NODE -> CacheState] - /\ chan1 \in [NODE -> MsgCmd] - /\ chan2 \in [NODE -> MsgCmd] - /\ chan3 \in [NODE -> MsgCmd] + /\ chan1 \in [NODE -> {"Empty", "ReqS", "ReqE"}] + /\ chan2 \in [NODE -> {"Empty", "Inv", "GntS", "GntE"}] + /\ chan3 \in [NODE -> {"Empty", "InvAck"}] /\ invSet \in [NODE -> BOOLEAN] /\ shrSet \in [NODE -> BOOLEAN] /\ exGntd \in BOOLEAN - /\ curCmd \in MsgCmd + /\ curCmd \in {"Empty", "ReqS", "ReqE"} /\ curPtr \in NODE \cup {NoNode} Init == diff --git a/specifications/GermanProtocol/GermanWithMutex.tla b/specifications/GermanProtocol/GermanWithMutex.tla index bba8cc38..db20f4c5 100644 --- a/specifications/GermanProtocol/GermanWithMutex.tla +++ b/specifications/GermanProtocol/GermanWithMutex.tla @@ -11,7 +11,6 @@ ASSUME NoDataNotInDATA == NoData \notin DATA ASSUME NoNodeNotInNODE == NoNode \notin NODE CacheState == {"I", "S", "E"} -MsgCmd == {"Empty", "ReqS", "ReqE", "Inv", "InvAck", "GntS", "GntE"} Payload == DATA \cup {NoData} @@ -35,13 +34,13 @@ vars == < [state : CacheState, data : Payload]] - /\ chan1 \in [NODE -> [cmd : MsgCmd, data : Payload]] - /\ chan2 \in [NODE -> [cmd : MsgCmd, data : Payload]] - /\ chan3 \in [NODE -> [cmd : MsgCmd, data : Payload]] + /\ chan1 \in [NODE -> [cmd : {"Empty", "ReqS", "ReqE"}, data : Payload]] + /\ chan2 \in [NODE -> [cmd : {"Empty", "Inv", "GntS", "GntE"}, data : Payload]] + /\ chan3 \in [NODE -> [cmd : {"Empty", "InvAck"}, data : Payload]] /\ invSet \in [NODE -> BOOLEAN] /\ shrSet \in [NODE -> BOOLEAN] /\ exGntd \in BOOLEAN - /\ curCmd \in MsgCmd + /\ curCmd \in {"Empty", "ReqS", "ReqE"} /\ curPtr \in NODE \cup {NoNode} /\ memData \in DATA /\ auxData \in DATA @@ -179,14 +178,6 @@ DataProp == /\ (exGntd = FALSE => memData = auxData) /\ \A i \in NODE : cache[i].state # "I" => cache[i].data = auxData -------------------------------------------------------------------------------- - -ChannelWellFormed == - \A i \in NODE : - /\ chan1[i].cmd \in {"Empty", "ReqS", "ReqE"} - /\ chan2[i].cmd \in {"Empty", "Inv", "GntS", "GntE"} - /\ chan3[i].cmd \in {"Empty", "InvAck"} - TransactionConsistency == (curCmd = "Empty") <=> (curPtr = NoNode) @@ -198,18 +189,18 @@ ExclusiveIsolation == cache[i].state = "E" => /\ exGntd = TRUE /\ \A j \in NODE \ {i} : - /\ cache[j].state = "I" - /\ chan2[j].cmd \notin {"GntS", "GntE"} - /\ chan3[j].cmd # "InvAck" + /\ cache[j].state = "I" + /\ chan2[j].cmd \notin {"GntS", "GntE"} + /\ chan3[j].cmd # "InvAck" WritebackCarriesLatest == \A i \in NODE : (chan3[i].cmd = "InvAck" /\ curCmd # "Empty" /\ exGntd = TRUE) => /\ chan3[i].data = auxData /\ \A j \in NODE \ {i} : - /\ cache[j].state # "E" - /\ chan2[j].cmd # "GntE" - /\ chan3[j].cmd # "InvAck" + /\ cache[j].state # "E" + /\ chan2[j].cmd # "GntE" + /\ chan3[j].cmd # "InvAck" ------------------------------------------------------------------------------- diff --git a/specifications/GermanProtocol/MCGermanWithMutex.cfg b/specifications/GermanProtocol/MCGermanWithMutex.cfg index 52d39b06..2d406259 100644 --- a/specifications/GermanProtocol/MCGermanWithMutex.cfg +++ b/specifications/GermanProtocol/MCGermanWithMutex.cfg @@ -19,7 +19,6 @@ INVARIANT TypeOK Coherence DataProp - ChannelWellFormed TransactionConsistency DirectoryAccurate ExclusiveIsolation From 4d865afec0c7e3f952b11ed49bc630ebb28c333e Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 20 Jul 2026 13:35:34 -0700 Subject: [PATCH 09/12] Represent German directory membership as sets Signed-off-by: Markus Alexander Kuppe --- specifications/GermanProtocol/APGerman.tla | 4 ++-- .../GermanProtocol/APGermanCoherence.tla | 4 ++-- .../GermanProtocol/APGermanWithMutex.tla | 4 ++-- specifications/GermanProtocol/German.tla | 20 +++++++++---------- .../GermanProtocol/GermanCoherence.tla | 18 ++++++++--------- .../GermanProtocol/GermanWithMutex.tla | 20 +++++++++---------- 6 files changed, 35 insertions(+), 35 deletions(-) diff --git a/specifications/GermanProtocol/APGerman.tla b/specifications/GermanProtocol/APGerman.tla index 443c52ea..2a568432 100644 --- a/specifications/GermanProtocol/APGerman.tla +++ b/specifications/GermanProtocol/APGerman.tla @@ -28,9 +28,9 @@ VARIABLES chan2, \* @type: NODE -> Str; chan3, - \* @type: NODE -> Bool; + \* @type: Set(NODE); invSet, - \* @type: NODE -> Bool; + \* @type: Set(NODE); shrSet, \* @type: Bool; exGntd, diff --git a/specifications/GermanProtocol/APGermanCoherence.tla b/specifications/GermanProtocol/APGermanCoherence.tla index a6b56e58..f8eed60a 100644 --- a/specifications/GermanProtocol/APGermanCoherence.tla +++ b/specifications/GermanProtocol/APGermanCoherence.tla @@ -26,9 +26,9 @@ VARIABLES chan2, \* @type: NODE -> Str; chan3, - \* @type: NODE -> Bool; + \* @type: Set(NODE); invSet, - \* @type: NODE -> Bool; + \* @type: Set(NODE); shrSet, \* @type: Bool; exGntd, diff --git a/specifications/GermanProtocol/APGermanWithMutex.tla b/specifications/GermanProtocol/APGermanWithMutex.tla index fbd32c2b..4a07dac2 100644 --- a/specifications/GermanProtocol/APGermanWithMutex.tla +++ b/specifications/GermanProtocol/APGermanWithMutex.tla @@ -31,9 +31,9 @@ VARIABLES chan2, \* @type: NODE -> { cmd: Str, data: DATA }; chan3, - \* @type: NODE -> Bool; + \* @type: Set(NODE); invSet, - \* @type: NODE -> Bool; + \* @type: Set(NODE); shrSet, \* @type: Bool; exGntd, diff --git a/specifications/GermanProtocol/German.tla b/specifications/GermanProtocol/German.tla index 530e6136..3dd13f63 100644 --- a/specifications/GermanProtocol/German.tla +++ b/specifications/GermanProtocol/German.tla @@ -21,8 +21,8 @@ TypeOK == /\ chan1 \in [NODE -> {"Empty", "ReqS", "ReqE"}] /\ chan2 \in [NODE -> {"Empty", "Inv", "GntS", "GntE"}] /\ chan3 \in [NODE -> {"Empty", "InvAck"}] - /\ invSet \in [NODE -> BOOLEAN] - /\ shrSet \in [NODE -> BOOLEAN] + /\ invSet \subseteq NODE + /\ shrSet \subseteq NODE /\ exGntd \in BOOLEAN /\ curCmd \in {"Empty", "ReqS", "ReqE"} /\ curPtr \in NODE \cup {Other, NoNode} @@ -32,8 +32,8 @@ Init == /\ chan1 = [i \in NODE |-> "Empty"] /\ chan2 = [i \in NODE |-> "Empty"] /\ chan3 = [i \in NODE |-> "Empty"] - /\ invSet = [i \in NODE |-> FALSE] - /\ shrSet = [i \in NODE |-> FALSE] + /\ invSet = {} + /\ shrSet = {} /\ exGntd = FALSE /\ curCmd = "Empty" /\ curPtr = NoNode @@ -58,10 +58,10 @@ RecvReq(i) == SendInv(i) == /\ chan2[i] = "Empty" - /\ invSet[i] = TRUE + /\ i \in invSet /\ (curCmd = "ReqE" \/ (curCmd = "ReqS" /\ exGntd = TRUE)) /\ chan2' = [chan2 EXCEPT ![i] = "Inv"] - /\ invSet' = [invSet EXCEPT ![i] = FALSE] + /\ invSet' = invSet \ {i} /\ UNCHANGED <> SendInvAck(i) == @@ -76,7 +76,7 @@ RecvInvAck(i) == /\ chan3[i] = "InvAck" /\ curCmd # "Empty" /\ chan3' = [chan3 EXCEPT ![i] = "Empty"] - /\ shrSet' = [shrSet EXCEPT ![i] = FALSE] + /\ shrSet' = shrSet \ {i} /\ exGntd' = FALSE /\ UNCHANGED <> @@ -85,9 +85,9 @@ SendGnt(i) == /\ curPtr = i /\ chan2[i] = "Empty" /\ exGntd = FALSE - /\ curCmd = "ReqE" => \A j \in NODE : shrSet[j] = FALSE + /\ curCmd = "ReqE" => shrSet = {} /\ chan2' = [chan2 EXCEPT ![i] = IF curCmd = "ReqS" THEN "GntS" ELSE "GntE"] - /\ shrSet' = [shrSet EXCEPT ![i] = TRUE] + /\ shrSet' = shrSet \cup {i} /\ exGntd' = (curCmd = "ReqE") /\ curCmd' = "Empty" /\ curPtr' = NoNode @@ -112,7 +112,7 @@ ABS_SendGnt == /\ curCmd \in {"ReqS", "ReqE"} /\ curPtr = Other /\ exGntd = FALSE - /\ curCmd = "ReqE" => \A j \in NODE : shrSet[j] = FALSE + /\ curCmd = "ReqE" => shrSet = {} /\ exGntd' = (curCmd = "ReqE") /\ curCmd' = "Empty" /\ curPtr' = NoNode diff --git a/specifications/GermanProtocol/GermanCoherence.tla b/specifications/GermanProtocol/GermanCoherence.tla index 8f386dd7..f3d9120e 100644 --- a/specifications/GermanProtocol/GermanCoherence.tla +++ b/specifications/GermanProtocol/GermanCoherence.tla @@ -27,8 +27,8 @@ TypeOK == /\ chan1 \in [NODE -> {"Empty", "ReqS", "ReqE"}] /\ chan2 \in [NODE -> {"Empty", "Inv", "GntS", "GntE"}] /\ chan3 \in [NODE -> {"Empty", "InvAck"}] - /\ invSet \in [NODE -> BOOLEAN] - /\ shrSet \in [NODE -> BOOLEAN] + /\ invSet \subseteq NODE + /\ shrSet \subseteq NODE /\ exGntd \in BOOLEAN /\ curCmd \in {"Empty", "ReqS", "ReqE"} /\ curPtr \in NODE \cup {NoNode} @@ -38,8 +38,8 @@ Init == /\ chan1 = [i \in NODE |-> "Empty"] /\ chan2 = [i \in NODE |-> "Empty"] /\ chan3 = [i \in NODE |-> "Empty"] - /\ invSet = [i \in NODE |-> FALSE] - /\ shrSet = [i \in NODE |-> FALSE] + /\ invSet = {} + /\ shrSet = {} /\ exGntd = FALSE /\ curCmd = "Empty" /\ curPtr = NoNode @@ -64,10 +64,10 @@ RecvReq(i) == SendInv(i) == /\ chan2[i] = "Empty" - /\ invSet[i] = TRUE + /\ i \in invSet /\ (curCmd = "ReqE" \/ (curCmd = "ReqS" /\ exGntd = TRUE)) /\ chan2' = [chan2 EXCEPT ![i] = "Inv"] - /\ invSet' = [invSet EXCEPT ![i] = FALSE] + /\ invSet' = invSet \ {i} /\ UNCHANGED <> SendInvAck(i) == @@ -82,7 +82,7 @@ RecvInvAck(i) == /\ chan3[i] = "InvAck" /\ curCmd # "Empty" /\ chan3' = [chan3 EXCEPT ![i] = "Empty"] - /\ shrSet' = [shrSet EXCEPT ![i] = FALSE] + /\ shrSet' = shrSet \ {i} /\ exGntd' = IF exGntd = TRUE THEN FALSE ELSE exGntd /\ UNCHANGED <> @@ -91,9 +91,9 @@ SendGnt(i) == /\ curPtr = i /\ chan2[i] = "Empty" /\ exGntd = FALSE - /\ curCmd = "ReqE" => \A j \in NODE : shrSet[j] = FALSE + /\ curCmd = "ReqE" => shrSet = {} /\ chan2' = [chan2 EXCEPT ![i] = IF curCmd = "ReqS" THEN "GntS" ELSE "GntE"] - /\ shrSet' = [shrSet EXCEPT ![i] = TRUE] + /\ shrSet' = shrSet \cup {i} /\ exGntd' = (curCmd = "ReqE") /\ curCmd' = "Empty" /\ curPtr' = NoNode diff --git a/specifications/GermanProtocol/GermanWithMutex.tla b/specifications/GermanProtocol/GermanWithMutex.tla index db20f4c5..05f740fe 100644 --- a/specifications/GermanProtocol/GermanWithMutex.tla +++ b/specifications/GermanProtocol/GermanWithMutex.tla @@ -37,8 +37,8 @@ TypeOK == /\ chan1 \in [NODE -> [cmd : {"Empty", "ReqS", "ReqE"}, data : Payload]] /\ chan2 \in [NODE -> [cmd : {"Empty", "Inv", "GntS", "GntE"}, data : Payload]] /\ chan3 \in [NODE -> [cmd : {"Empty", "InvAck"}, data : Payload]] - /\ invSet \in [NODE -> BOOLEAN] - /\ shrSet \in [NODE -> BOOLEAN] + /\ invSet \subseteq NODE + /\ shrSet \subseteq NODE /\ exGntd \in BOOLEAN /\ curCmd \in {"Empty", "ReqS", "ReqE"} /\ curPtr \in NODE \cup {NoNode} @@ -51,8 +51,8 @@ Init == /\ chan1 = [i \in NODE |-> [cmd |-> "Empty", data |-> NoData]] /\ chan2 = [i \in NODE |-> [cmd |-> "Empty", data |-> NoData]] /\ chan3 = [i \in NODE |-> [cmd |-> "Empty", data |-> NoData]] - /\ invSet = [i \in NODE |-> FALSE] - /\ shrSet = [i \in NODE |-> FALSE] + /\ invSet = {} + /\ shrSet = {} /\ exGntd = FALSE /\ curCmd = "Empty" /\ curPtr = NoNode @@ -110,17 +110,17 @@ RecvReq(i) == SendInv(i) == /\ chan2[i].cmd = "Empty" - /\ invSet[i] = TRUE + /\ i \in invSet /\ (curCmd = "ReqE" \/ (curCmd = "ReqS" /\ exGntd = TRUE)) /\ chan2' = [chan2 EXCEPT ![i].cmd = "Inv"] - /\ invSet' = [invSet EXCEPT ![i] = FALSE] + /\ invSet' = invSet \ {i} /\ UNCHANGED <> RecvInvAck(i) == /\ chan3[i].cmd = "InvAck" /\ curCmd # "Empty" - /\ shrSet' = [shrSet EXCEPT ![i] = FALSE] + /\ shrSet' = shrSet \ {i} /\ IF exGntd = TRUE THEN /\ exGntd' = FALSE /\ memData' = chan3[i].data @@ -134,10 +134,10 @@ SendGnt(i) == /\ curPtr = i /\ chan2[i].cmd = "Empty" /\ exGntd = FALSE - /\ curCmd = "ReqE" => \A j \in NODE : shrSet[j] = FALSE + /\ curCmd = "ReqE" => shrSet = {} /\ chan2' = [chan2 EXCEPT ![i].cmd = IF curCmd = "ReqS" THEN "GntS" ELSE "GntE", ![i].data = memData] - /\ shrSet' = [shrSet EXCEPT ![i] = TRUE] + /\ shrSet' = shrSet \cup {i} /\ exGntd' = (curCmd = "ReqE") /\ curCmd' = "Empty" /\ curPtr' = NoNode @@ -182,7 +182,7 @@ TransactionConsistency == (curCmd = "Empty") <=> (curPtr = NoNode) DirectoryAccurate == - \A i \in NODE : cache[i].state \in {"S", "E"} => shrSet[i] = TRUE + \A i \in NODE : cache[i].state \in {"S", "E"} => i \in shrSet ExclusiveIsolation == \A i \in NODE : From 8f1791c550681331d1d5a5c382b1fc987778cf33 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 20 Jul 2026 13:39:52 -0700 Subject: [PATCH 10/12] Document CMP abstract-environment actions Signed-off-by: Markus Alexander Kuppe --- specifications/GermanProtocol/German.tla | 2 ++ 1 file changed, 2 insertions(+) diff --git a/specifications/GermanProtocol/German.tla b/specifications/GermanProtocol/German.tla index 3dd13f63..d44697a5 100644 --- a/specifications/GermanProtocol/German.tla +++ b/specifications/GermanProtocol/German.tla @@ -101,6 +101,8 @@ RecvGnt(i) == ------------------------------------------------------------------------------- +\* CMP abstraction actions: Other summarizes nodes omitted from NODE, projecting +\* their hidden cache and channel behavior onto visible shared state. ABS_RecvReq == /\ curCmd = "Empty" /\ \E c \in {"ReqS", "ReqE"} : curCmd' = c From e33fca3ccfdae24fc4a27b70639134105ca3e5ec Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 20 Jul 2026 13:43:07 -0700 Subject: [PATCH 11/12] Check GermanCoherence refinement of the CMP abstraction Signed-off-by: Markus Alexander Kuppe --- specifications/GermanProtocol/MCGermanCoherence.cfg | 3 +++ specifications/GermanProtocol/MCGermanCoherence.tla | 9 +++++++++ 2 files changed, 12 insertions(+) diff --git a/specifications/GermanProtocol/MCGermanCoherence.cfg b/specifications/GermanProtocol/MCGermanCoherence.cfg index 01dbecb2..28ecdc1d 100644 --- a/specifications/GermanProtocol/MCGermanCoherence.cfg +++ b/specifications/GermanProtocol/MCGermanCoherence.cfg @@ -3,6 +3,7 @@ CONSTANTS NODE = {n1, n2} NoNode = noNode + Other = other SYMMETRY Symmetry @@ -11,3 +12,5 @@ SPECIFICATION Spec INVARIANT TypeOK Coherence + +PROPERTY Refinement diff --git a/specifications/GermanProtocol/MCGermanCoherence.tla b/specifications/GermanProtocol/MCGermanCoherence.tla index 1f3cbb5e..31cf4cea 100644 --- a/specifications/GermanProtocol/MCGermanCoherence.tla +++ b/specifications/GermanProtocol/MCGermanCoherence.tla @@ -1,6 +1,15 @@ ------------------------- MODULE MCGermanCoherence ------------------------- EXTENDS GermanCoherence, TLC +CONSTANT Other +ASSUME Other \notin NODE /\ Other # NoNode + +\* The concrete finite-node protocol refines the CMP abstraction by the +\* identity mapping; it simply never exercises the abstract node Other. +Abstract == INSTANCE German + +Refinement == Abstract!Spec + \* Nodes are interchangeable, so collapse permutations of NODE. Symmetry == Permutations(NODE) From 475781d0189a07a8b8b6136f439ba20aa5cc46a1 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 20 Jul 2026 14:32:32 -0700 Subject: [PATCH 12/12] Rename German models by abstraction level Use consistent Data, Control, and CMPWithMutex names across the specifications, TLC and Apalache models, manifest, and documentation. Signed-off-by: Markus Alexander Kuppe --- ...{APGerman.cfg => APGermanCMPWithMutex.cfg} | 0 ...{APGerman.tla => APGermanCMPWithMutex.tla} | 12 ++++---- ...ermanCoherence.cfg => APGermanControl.cfg} | 0 ...ermanCoherence.tla => APGermanControl.tla} | 12 ++++---- ...APGermanWithMutex.cfg => APGermanData.cfg} | 0 ...APGermanWithMutex.tla => APGermanData.tla} | 13 ++++---- .../{German.tla => GermanCMPWithMutex.tla} | 4 +-- ...{GermanCoherence.tla => GermanControl.tla} | 2 +- .../{GermanWithMutex.tla => GermanData.tla} | 4 +-- ...{MCGerman.cfg => MCGermanCMPWithMutex.cfg} | 0 ...{MCGerman.tla => MCGermanCMPWithMutex.tla} | 4 +-- ...ermanCoherence.cfg => MCGermanControl.cfg} | 0 ...ermanCoherence.tla => MCGermanControl.tla} | 6 ++-- ...MCGermanWithMutex.cfg => MCGermanData.cfg} | 4 +-- ...MCGermanWithMutex.tla => MCGermanData.tla} | 4 +-- specifications/GermanProtocol/README.md | 19 ++++++++++++ specifications/GermanProtocol/manifest.json | 30 +++++++++---------- 17 files changed, 67 insertions(+), 47 deletions(-) rename specifications/GermanProtocol/{APGerman.cfg => APGermanCMPWithMutex.cfg} (100%) rename specifications/GermanProtocol/{APGerman.tla => APGermanCMPWithMutex.tla} (69%) rename specifications/GermanProtocol/{APGermanCoherence.cfg => APGermanControl.cfg} (100%) rename specifications/GermanProtocol/{APGermanCoherence.tla => APGermanControl.tla} (67%) rename specifications/GermanProtocol/{APGermanWithMutex.cfg => APGermanData.cfg} (100%) rename specifications/GermanProtocol/{APGermanWithMutex.tla => APGermanData.tla} (75%) rename specifications/GermanProtocol/{German.tla => GermanCMPWithMutex.tla} (97%) rename specifications/GermanProtocol/{GermanCoherence.tla => GermanControl.tla} (98%) rename specifications/GermanProtocol/{GermanWithMutex.tla => GermanData.tla} (98%) rename specifications/GermanProtocol/{MCGerman.cfg => MCGermanCMPWithMutex.cfg} (100%) rename specifications/GermanProtocol/{MCGerman.tla => MCGermanCMPWithMutex.tla} (69%) rename specifications/GermanProtocol/{MCGermanCoherence.cfg => MCGermanControl.cfg} (100%) rename specifications/GermanProtocol/{MCGermanCoherence.tla => MCGermanControl.tla} (73%) rename specifications/GermanProtocol/{MCGermanWithMutex.cfg => MCGermanData.cfg} (92%) rename specifications/GermanProtocol/{MCGermanWithMutex.tla => MCGermanData.tla} (72%) diff --git a/specifications/GermanProtocol/APGerman.cfg b/specifications/GermanProtocol/APGermanCMPWithMutex.cfg similarity index 100% rename from specifications/GermanProtocol/APGerman.cfg rename to specifications/GermanProtocol/APGermanCMPWithMutex.cfg diff --git a/specifications/GermanProtocol/APGerman.tla b/specifications/GermanProtocol/APGermanCMPWithMutex.tla similarity index 69% rename from specifications/GermanProtocol/APGerman.tla rename to specifications/GermanProtocol/APGermanCMPWithMutex.tla index 2a568432..e4c4977b 100644 --- a/specifications/GermanProtocol/APGerman.tla +++ b/specifications/GermanProtocol/APGermanCMPWithMutex.tla @@ -1,5 +1,5 @@ ------------------------------ MODULE APGerman ----------------------------- -(* Apalache type annotations for German.tla, applied via INSTANCE so the +------------------------ MODULE APGermanCMPWithMutex ------------------------ +(* Apalache type annotations for GermanCMPWithMutex.tla, applied via INSTANCE so the original spec remains free of tool-specific idiosyncrasies. Nodes are modelled as an uninterpreted Apalache type (NODE); the abstract @@ -7,8 +7,8 @@ `curPtr \in NODE \cup {Other, NoNode}` is well typed. Run bounded model checking for executions of at most 20 Next steps with: - apalache-mc check --config=APGerman.cfg --length=20 APGerman.tla - This completes in under 10 minutes on a 2021 M1 MacBook. + apalache-mc check --config=APGermanCMPWithMutex.cfg --length=20 APGermanCMPWithMutex.tla + This completes in about 20 minutes on a 2021 M1 MacBook. *) CONSTANTS @@ -39,9 +39,9 @@ VARIABLES \* @type: NODE; curPtr -INSTANCE German +INSTANCE GermanCMPWithMutex -\* Concrete values for the constants used by APGerman.cfg. +\* Concrete values for the constants used by APGermanCMPWithMutex.cfg. NodeVal == { "n1_OF_NODE", "n2_OF_NODE" } OtherVal == "other_OF_NODE" NoNodeVal == "noNode_OF_NODE" diff --git a/specifications/GermanProtocol/APGermanCoherence.cfg b/specifications/GermanProtocol/APGermanControl.cfg similarity index 100% rename from specifications/GermanProtocol/APGermanCoherence.cfg rename to specifications/GermanProtocol/APGermanControl.cfg diff --git a/specifications/GermanProtocol/APGermanCoherence.tla b/specifications/GermanProtocol/APGermanControl.tla similarity index 67% rename from specifications/GermanProtocol/APGermanCoherence.tla rename to specifications/GermanProtocol/APGermanControl.tla index f8eed60a..d4118387 100644 --- a/specifications/GermanProtocol/APGermanCoherence.tla +++ b/specifications/GermanProtocol/APGermanControl.tla @@ -1,5 +1,5 @@ -------------------------- MODULE APGermanCoherence ------------------------- -(* Apalache type annotations for GermanCoherence.tla, applied via INSTANCE so +--------------------------- MODULE APGermanControl --------------------------- +(* Apalache type annotations for GermanControl.tla, applied via INSTANCE so the original spec remains free of tool-specific idiosyncrasies. Nodes are modelled as an uninterpreted Apalache type (NODE); the NoNode @@ -7,8 +7,8 @@ typed. Run bounded model checking for executions of at most 20 Next steps with: - apalache-mc check --config=APGermanCoherence.cfg --length=20 APGermanCoherence.tla - This completes in under 10 minutes on a 2021 M1 MacBook. + apalache-mc check --config=APGermanControl.cfg --length=20 APGermanControl.tla + This completes in about 4 minutes on a 2021 M1 MacBook. *) CONSTANTS @@ -37,9 +37,9 @@ VARIABLES \* @type: NODE; curPtr -INSTANCE GermanCoherence +INSTANCE GermanControl -\* Concrete values for the constants used by APGermanCoherence.cfg. +\* Concrete values for the constants used by APGermanControl.cfg. NodeVal == { "n1_OF_NODE", "n2_OF_NODE" } NoNodeVal == "noNode_OF_NODE" diff --git a/specifications/GermanProtocol/APGermanWithMutex.cfg b/specifications/GermanProtocol/APGermanData.cfg similarity index 100% rename from specifications/GermanProtocol/APGermanWithMutex.cfg rename to specifications/GermanProtocol/APGermanData.cfg diff --git a/specifications/GermanProtocol/APGermanWithMutex.tla b/specifications/GermanProtocol/APGermanData.tla similarity index 75% rename from specifications/GermanProtocol/APGermanWithMutex.tla rename to specifications/GermanProtocol/APGermanData.tla index 4a07dac2..1600dc72 100644 --- a/specifications/GermanProtocol/APGermanWithMutex.tla +++ b/specifications/GermanProtocol/APGermanData.tla @@ -1,5 +1,5 @@ -------------------------- MODULE APGermanWithMutex ------------------------- -(* Apalache type annotations for GermanWithMutex.tla, applied via INSTANCE so +----------------------------- MODULE APGermanData ----------------------------- +(* Apalache type annotations for GermanData.tla, applied via INSTANCE so the original spec remains free of tool-specific idiosyncrasies. Nodes and data values are modelled as uninterpreted Apalache types (NODE, @@ -8,8 +8,9 @@ Apalache does not verify the liveness properties (FairSpec) of the spec. Run bounded model checking for executions of at most 10 Next steps with: - apalache-mc check --config=APGermanWithMutex.cfg --length=10 APGermanWithMutex.tla - This completes quickly on a 2021 M1 MacBook; length 20 takes over 1.5 hours. + apalache-mc check --config=APGermanData.cfg --length=10 APGermanData.tla + This completes in about 20 seconds on a 2021 M1 MacBook; length 20 takes + over 1.5 hours. *) CONSTANTS @@ -46,9 +47,9 @@ VARIABLES \* @type: DATA; auxData -INSTANCE GermanWithMutex +INSTANCE GermanData -\* Concrete values for the constants used by APGermanWithMutex.cfg. +\* Concrete values for the constants used by APGermanData.cfg. NodeVal == { "n1_OF_NODE", "n2_OF_NODE" } DataVal == { "d1_OF_DATA", "d2_OF_DATA" } NoDataVal == "noData_OF_DATA" diff --git a/specifications/GermanProtocol/German.tla b/specifications/GermanProtocol/GermanCMPWithMutex.tla similarity index 97% rename from specifications/GermanProtocol/German.tla rename to specifications/GermanProtocol/GermanCMPWithMutex.tla index d44697a5..e02ff40c 100644 --- a/specifications/GermanProtocol/German.tla +++ b/specifications/GermanProtocol/GermanCMPWithMutex.tla @@ -1,4 +1,4 @@ --------------------------------- MODULE German -------------------------------- +-------------------------- MODULE GermanCMPWithMutex -------------------------- CONSTANTS NODE, Other, @@ -133,7 +133,7 @@ ABS_RecvInvAck == \* germanNoMutex.m omits it on purpose -- the deadlock-study model that needs \* no noninterference lemma -- so it admits the spurious "bogus InvAck from \* Other" counterexample to mutual exclusion. Dropping this one conjunct makes - \* German.tla bisimilar to germanNoMutex.m. + \* GermanCMPWithMutex.tla bisimilar to germanNoMutex.m. /\ \A j \in NODE : /\ cache[j] # "E" /\ chan2[j] # "GntE" diff --git a/specifications/GermanProtocol/GermanCoherence.tla b/specifications/GermanProtocol/GermanControl.tla similarity index 98% rename from specifications/GermanProtocol/GermanCoherence.tla rename to specifications/GermanProtocol/GermanControl.tla index f3d9120e..46c2c77b 100644 --- a/specifications/GermanProtocol/GermanCoherence.tla +++ b/specifications/GermanProtocol/GermanControl.tla @@ -1,4 +1,4 @@ ----------------------------- MODULE GermanCoherence ---------------------------- +----------------------------- MODULE GermanControl ----------------------------- CONSTANTS NODE, NoNode diff --git a/specifications/GermanProtocol/GermanWithMutex.tla b/specifications/GermanProtocol/GermanData.tla similarity index 98% rename from specifications/GermanProtocol/GermanWithMutex.tla rename to specifications/GermanProtocol/GermanData.tla index 05f740fe..bb77d10d 100644 --- a/specifications/GermanProtocol/GermanWithMutex.tla +++ b/specifications/GermanProtocol/GermanData.tla @@ -1,4 +1,4 @@ ------------------------------ MODULE GermanWithMutex ----------------------------- +------------------------------ MODULE GermanData ------------------------------ EXTENDS Naturals, FiniteSets CONSTANTS @@ -158,7 +158,7 @@ Spec == Init /\ [][Next]_vars ------------------------------------------------------------------------------- -Abstract == INSTANCE GermanCoherence WITH +Abstract == INSTANCE GermanControl WITH cache <- [i \in NODE |-> cache[i].state], chan1 <- [i \in NODE |-> chan1[i].cmd], chan2 <- [i \in NODE |-> chan2[i].cmd], diff --git a/specifications/GermanProtocol/MCGerman.cfg b/specifications/GermanProtocol/MCGermanCMPWithMutex.cfg similarity index 100% rename from specifications/GermanProtocol/MCGerman.cfg rename to specifications/GermanProtocol/MCGermanCMPWithMutex.cfg diff --git a/specifications/GermanProtocol/MCGerman.tla b/specifications/GermanProtocol/MCGermanCMPWithMutex.tla similarity index 69% rename from specifications/GermanProtocol/MCGerman.tla rename to specifications/GermanProtocol/MCGermanCMPWithMutex.tla index 29a5bcd3..54e684b4 100644 --- a/specifications/GermanProtocol/MCGerman.tla +++ b/specifications/GermanProtocol/MCGermanCMPWithMutex.tla @@ -1,5 +1,5 @@ ------------------------------ MODULE MCGerman ----------------------------- -EXTENDS German, TLC +------------------------ MODULE MCGermanCMPWithMutex ------------------------ +EXTENDS GermanCMPWithMutex, TLC \* The concrete nodes are interchangeable, so collapse permutations of NODE. \* Other and NoNode are fixed sentinels and are not permuted. diff --git a/specifications/GermanProtocol/MCGermanCoherence.cfg b/specifications/GermanProtocol/MCGermanControl.cfg similarity index 100% rename from specifications/GermanProtocol/MCGermanCoherence.cfg rename to specifications/GermanProtocol/MCGermanControl.cfg diff --git a/specifications/GermanProtocol/MCGermanCoherence.tla b/specifications/GermanProtocol/MCGermanControl.tla similarity index 73% rename from specifications/GermanProtocol/MCGermanCoherence.tla rename to specifications/GermanProtocol/MCGermanControl.tla index 31cf4cea..ddf8cf52 100644 --- a/specifications/GermanProtocol/MCGermanCoherence.tla +++ b/specifications/GermanProtocol/MCGermanControl.tla @@ -1,12 +1,12 @@ -------------------------- MODULE MCGermanCoherence ------------------------- -EXTENDS GermanCoherence, TLC +--------------------------- MODULE MCGermanControl --------------------------- +EXTENDS GermanControl, TLC CONSTANT Other ASSUME Other \notin NODE /\ Other # NoNode \* The concrete finite-node protocol refines the CMP abstraction by the \* identity mapping; it simply never exercises the abstract node Other. -Abstract == INSTANCE German +Abstract == INSTANCE GermanCMPWithMutex Refinement == Abstract!Spec diff --git a/specifications/GermanProtocol/MCGermanWithMutex.cfg b/specifications/GermanProtocol/MCGermanData.cfg similarity index 92% rename from specifications/GermanProtocol/MCGermanWithMutex.cfg rename to specifications/GermanProtocol/MCGermanData.cfg index 2d406259..10d0f945 100644 --- a/specifications/GermanProtocol/MCGermanWithMutex.cfg +++ b/specifications/GermanProtocol/MCGermanData.cfg @@ -3,8 +3,8 @@ \* property DataProp is exercised non-vacuously. \* \* Besides the safety invariants this model also checks the refinement -\* Spec => Abstract!Spec (the data-forgetting projection onto GermanCoherence, -\* defined in GermanWithMutex.tla). +\* Spec => Abstract!Spec (the data-forgetting projection onto GermanControl, +\* defined in GermanData.tla). CONSTANTS NODE = {n1, n2} DATA = {d1, d2} diff --git a/specifications/GermanProtocol/MCGermanWithMutex.tla b/specifications/GermanProtocol/MCGermanData.tla similarity index 72% rename from specifications/GermanProtocol/MCGermanWithMutex.tla rename to specifications/GermanProtocol/MCGermanData.tla index 1aaa7006..d4df03e6 100644 --- a/specifications/GermanProtocol/MCGermanWithMutex.tla +++ b/specifications/GermanProtocol/MCGermanData.tla @@ -1,5 +1,5 @@ -------------------------- MODULE MCGermanWithMutex ------------------------- -EXTENDS GermanWithMutex, TLC +----------------------------- MODULE MCGermanData ----------------------------- +EXTENDS GermanData, TLC \* Nodes and data values are independently interchangeable. The NoNode and \* NoData sentinels are fixed because they are outside these sets. diff --git a/specifications/GermanProtocol/README.md b/specifications/GermanProtocol/README.md index bd1489c9..de401f31 100644 --- a/specifications/GermanProtocol/README.md +++ b/specifications/GermanProtocol/README.md @@ -7,6 +7,25 @@ describe the *same* system as its Murphi counterpart — not just that they sati the same properties, but that they exhibit exactly the same behavior, step for step. +## Specifications + +- `GermanData.tla` models the concrete protocol with cache and message data. +- `GermanControl.tla` is its data-forgetting control-state abstraction. +- `GermanCMPWithMutex.tla` applies the CMP abstraction: `Other` summarizes + omitted nodes, and the mutex-derived noninterference guard keeps that + abstraction sound. + +Their checked refinement order is: + +```text +GermanData => GermanControl => GermanCMPWithMutex +``` + +The `MC*` modules and configurations run TLC, including the two refinement +checks. The `AP*` modules and configurations provide Apalache type annotations +and bounded safety checks. The names describe each TLA+ model's role; the +original Murphi filenames are retained in the provenance below. + ## What "equivalent" means here Murphi and TLA+ share essentially the same underlying semantics: each defines a diff --git a/specifications/GermanProtocol/manifest.json b/specifications/GermanProtocol/manifest.json index 83b45247..8b75121d 100644 --- a/specifications/GermanProtocol/manifest.json +++ b/specifications/GermanProtocol/manifest.json @@ -11,11 +11,11 @@ "tags": [], "modules": [ { - "path": "specifications/GermanProtocol/APGerman.tla", + "path": "specifications/GermanProtocol/APGermanCMPWithMutex.tla", "features": [], "models": [ { - "path": "specifications/GermanProtocol/APGerman.cfg", + "path": "specifications/GermanProtocol/APGermanCMPWithMutex.cfg", "runtime": "00:00:20", "mode": "symbolic", "result": "success" @@ -23,11 +23,11 @@ ] }, { - "path": "specifications/GermanProtocol/APGermanCoherence.tla", + "path": "specifications/GermanProtocol/APGermanControl.tla", "features": [], "models": [ { - "path": "specifications/GermanProtocol/APGermanCoherence.cfg", + "path": "specifications/GermanProtocol/APGermanControl.cfg", "runtime": "00:00:08", "mode": "symbolic", "result": "success" @@ -35,11 +35,11 @@ ] }, { - "path": "specifications/GermanProtocol/APGermanWithMutex.tla", + "path": "specifications/GermanProtocol/APGermanData.tla", "features": [], "models": [ { - "path": "specifications/GermanProtocol/APGermanWithMutex.cfg", + "path": "specifications/GermanProtocol/APGermanData.cfg", "runtime": "00:00:39", "mode": "symbolic", "result": "success" @@ -47,26 +47,26 @@ ] }, { - "path": "specifications/GermanProtocol/German.tla", + "path": "specifications/GermanProtocol/GermanCMPWithMutex.tla", "features": [], "models": [] }, { - "path": "specifications/GermanProtocol/GermanCoherence.tla", + "path": "specifications/GermanProtocol/GermanControl.tla", "features": [], "models": [] }, { - "path": "specifications/GermanProtocol/GermanWithMutex.tla", + "path": "specifications/GermanProtocol/GermanData.tla", "features": [], "models": [] }, { - "path": "specifications/GermanProtocol/MCGerman.tla", + "path": "specifications/GermanProtocol/MCGermanCMPWithMutex.tla", "features": [], "models": [ { - "path": "specifications/GermanProtocol/MCGerman.cfg", + "path": "specifications/GermanProtocol/MCGermanCMPWithMutex.cfg", "runtime": "00:00:01", "mode": "exhaustive search", "result": "success", @@ -77,11 +77,11 @@ ] }, { - "path": "specifications/GermanProtocol/MCGermanCoherence.tla", + "path": "specifications/GermanProtocol/MCGermanControl.tla", "features": [], "models": [ { - "path": "specifications/GermanProtocol/MCGermanCoherence.cfg", + "path": "specifications/GermanProtocol/MCGermanControl.cfg", "runtime": "00:00:01", "mode": "exhaustive search", "result": "success", @@ -92,11 +92,11 @@ ] }, { - "path": "specifications/GermanProtocol/MCGermanWithMutex.tla", + "path": "specifications/GermanProtocol/MCGermanData.tla", "features": [], "models": [ { - "path": "specifications/GermanProtocol/MCGermanWithMutex.cfg", + "path": "specifications/GermanProtocol/MCGermanData.cfg", "runtime": "00:00:01", "mode": "exhaustive search", "result": "success",