From 4115b7d02a81b8c2b5beaaa9874591674f9f16ca Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 18 Jun 2026 11:18:24 -0700 Subject: [PATCH 1/3] 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 2/3] 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 3/3] 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