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/APGermanCMPWithMutex.cfg b/specifications/GermanProtocol/APGermanCMPWithMutex.cfg new file mode 100644 index 00000000..a655b707 --- /dev/null +++ b/specifications/GermanProtocol/APGermanCMPWithMutex.cfg @@ -0,0 +1,11 @@ +CONSTANT + NODE <- NodeVal + Other <- OtherVal + NoNode <- NoNodeVal + +INVARIANT + TypeOK + Coherence + Lemma_1 + +SPECIFICATION Spec diff --git a/specifications/GermanProtocol/APGermanCMPWithMutex.tla b/specifications/GermanProtocol/APGermanCMPWithMutex.tla new file mode 100644 index 00000000..e4c4977b --- /dev/null +++ b/specifications/GermanProtocol/APGermanCMPWithMutex.tla @@ -0,0 +1,49 @@ +------------------------ 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 + environment node Other and the NoNode sentinel share that type so that + `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=APGermanCMPWithMutex.cfg --length=20 APGermanCMPWithMutex.tla + This completes in about 20 minutes on a 2021 M1 MacBook. +*) + +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: Set(NODE); + invSet, + \* @type: Set(NODE); + shrSet, + \* @type: Bool; + exGntd, + \* @type: Str; + curCmd, + \* @type: NODE; + curPtr + +INSTANCE GermanCMPWithMutex + +\* 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/APGermanControl.cfg b/specifications/GermanProtocol/APGermanControl.cfg new file mode 100644 index 00000000..400dfd0e --- /dev/null +++ b/specifications/GermanProtocol/APGermanControl.cfg @@ -0,0 +1,9 @@ +CONSTANT + NODE <- NodeVal + NoNode <- NoNodeVal + +INVARIANT + TypeOK + Coherence + +SPECIFICATION Spec diff --git a/specifications/GermanProtocol/APGermanControl.tla b/specifications/GermanProtocol/APGermanControl.tla new file mode 100644 index 00000000..d4118387 --- /dev/null +++ b/specifications/GermanProtocol/APGermanControl.tla @@ -0,0 +1,46 @@ +--------------------------- 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 + sentinel shares that type so that `curPtr \in NODE \cup {NoNode}` is well + typed. + + Run bounded model checking for executions of at most 20 Next steps with: + apalache-mc check --config=APGermanControl.cfg --length=20 APGermanControl.tla + This completes in about 4 minutes on a 2021 M1 MacBook. +*) + +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: Set(NODE); + invSet, + \* @type: Set(NODE); + shrSet, + \* @type: Bool; + exGntd, + \* @type: Str; + curCmd, + \* @type: NODE; + curPtr + +INSTANCE GermanControl + +\* 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/APGermanData.cfg b/specifications/GermanProtocol/APGermanData.cfg new file mode 100644 index 00000000..138f50d7 --- /dev/null +++ b/specifications/GermanProtocol/APGermanData.cfg @@ -0,0 +1,16 @@ +CONSTANT + NODE <- NodeVal + DATA <- DataVal + NoData <- NoDataVal + NoNode <- NoNodeVal + +INVARIANT + TypeOK + Coherence + DataProp + TransactionConsistency + DirectoryAccurate + ExclusiveIsolation + WritebackCarriesLatest + +SPECIFICATION Spec diff --git a/specifications/GermanProtocol/APGermanData.tla b/specifications/GermanProtocol/APGermanData.tla new file mode 100644 index 00000000..1600dc72 --- /dev/null +++ b/specifications/GermanProtocol/APGermanData.tla @@ -0,0 +1,58 @@ +----------------------------- 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, + 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. + + Run bounded model checking for executions of at most 10 Next steps with: + 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 + \* @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: Set(NODE); + invSet, + \* @type: Set(NODE); + shrSet, + \* @type: Bool; + exGntd, + \* @type: Str; + curCmd, + \* @type: NODE; + curPtr, + \* @type: DATA; + memData, + \* @type: DATA; + auxData + +INSTANCE GermanData + +\* 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" +NoNodeVal == "noNode_OF_NODE" + +============================================================================== diff --git a/specifications/GermanProtocol/GermanCMPWithMutex.tla b/specifications/GermanProtocol/GermanCMPWithMutex.tla new file mode 100644 index 00000000..e02ff40c --- /dev/null +++ b/specifications/GermanProtocol/GermanCMPWithMutex.tla @@ -0,0 +1,175 @@ +-------------------------- MODULE GermanCMPWithMutex -------------------------- +CONSTANTS + NODE, + Other, + NoNode + +ASSUME Other \notin NODE +ASSUME NoNode \notin NODE /\ NoNode # Other + +CacheState == {"I", "S", "E"} + +VARIABLES + cache, chan1, chan2, chan3, invSet, shrSet, exGntd, curCmd, curPtr + +vars == <> + +------------------------------------------------------------------------------- + +TypeOK == + /\ cache \in [NODE -> CacheState] + /\ chan1 \in [NODE -> {"Empty", "ReqS", "ReqE"}] + /\ chan2 \in [NODE -> {"Empty", "Inv", "GntS", "GntE"}] + /\ chan3 \in [NODE -> {"Empty", "InvAck"}] + /\ invSet \subseteq NODE + /\ shrSet \subseteq NODE + /\ exGntd \in BOOLEAN + /\ curCmd \in {"Empty", "ReqS", "ReqE"} + /\ 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 = {} + /\ shrSet = {} + /\ exGntd = FALSE + /\ curCmd = "Empty" + /\ curPtr = NoNode + +------------------------------------------------------------------------------- + +SendReq(i) == + /\ chan1[i] = "Empty" + /\ \E c \in {"ReqS", "ReqE"} : + /\ cache[i] \in (IF c = "ReqS" THEN {"I"} ELSE {"I", "S"}) + /\ chan1' = [chan1 EXCEPT ![i] = c] + /\ UNCHANGED <> + +RecvReq(i) == + /\ curCmd = "Empty" + /\ chan1[i] \in {"ReqS", "ReqE"} + /\ curCmd' = chan1[i] + /\ curPtr' = i + /\ chan1' = [chan1 EXCEPT ![i] = "Empty"] + /\ invSet' = shrSet + /\ UNCHANGED <> + +SendInv(i) == + /\ chan2[i] = "Empty" + /\ i \in invSet + /\ (curCmd = "ReqE" \/ (curCmd = "ReqS" /\ exGntd = TRUE)) + /\ chan2' = [chan2 EXCEPT ![i] = "Inv"] + /\ invSet' = invSet \ {i} + /\ 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 \ {i} + /\ exGntd' = FALSE + /\ UNCHANGED <> + +SendGnt(i) == + /\ curCmd \in {"ReqS", "ReqE"} + /\ curPtr = i + /\ chan2[i] = "Empty" + /\ exGntd = FALSE + /\ curCmd = "ReqE" => shrSet = {} + /\ chan2' = [chan2 EXCEPT ![i] = IF curCmd = "ReqS" THEN "GntS" ELSE "GntE"] + /\ shrSet' = shrSet \cup {i} + /\ exGntd' = (curCmd = "ReqE") + /\ curCmd' = "Empty" + /\ curPtr' = NoNode + /\ UNCHANGED <> + +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 <> + +------------------------------------------------------------------------------- + +\* 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 + /\ curPtr' = Other + /\ invSet' = shrSet + /\ UNCHANGED <> + +ABS_SendGnt == + /\ curCmd \in {"ReqS", "ReqE"} + /\ curPtr = Other + /\ exGntd = FALSE + /\ curCmd = "ReqE" => shrSet = {} + /\ exGntd' = (curCmd = "ReqE") + /\ 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 + \* 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 + \* GermanCMPWithMutex.tla bisimilar to germanNoMutex.m. + /\ \A j \in NODE : + /\ cache[j] # "E" + /\ chan2[j] # "GntE" + /\ chan3[j] # "InvAck" + /\ exGntd' = FALSE + /\ UNCHANGED <> + +------------------------------------------------------------------------------- + +Next == + \/ \E i \in NODE : + \/ SendReq(i) + \/ RecvReq(i) + \/ SendInv(i) \/ SendInvAck(i) \/ RecvInvAck(i) + \/ SendGnt(i) + \/ RecvGnt(i) + \/ ABS_RecvReq + \/ ABS_SendGnt + \/ 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 \ {i} : + /\ cache[j] # "E" + /\ chan2[j] # "GntE" + /\ chan3[j] # "InvAck" + +============================================================================= diff --git a/specifications/GermanProtocol/GermanControl.tla b/specifications/GermanProtocol/GermanControl.tla new file mode 100644 index 00000000..46c2c77b --- /dev/null +++ b/specifications/GermanProtocol/GermanControl.tla @@ -0,0 +1,128 @@ +----------------------------- MODULE GermanControl ----------------------------- +CONSTANTS + NODE, + NoNode + +ASSUME NoNodeNotInNODE == NoNode \notin NODE + +CacheState == {"I", "S", "E"} + +VARIABLES + cache, + chan1, + chan2, + chan3, + invSet, + shrSet, + exGntd, + curCmd, + curPtr + +vars == <> + +------------------------------------------------------------------------------- + +TypeOK == + /\ cache \in [NODE -> CacheState] + /\ chan1 \in [NODE -> {"Empty", "ReqS", "ReqE"}] + /\ chan2 \in [NODE -> {"Empty", "Inv", "GntS", "GntE"}] + /\ chan3 \in [NODE -> {"Empty", "InvAck"}] + /\ invSet \subseteq NODE + /\ shrSet \subseteq NODE + /\ exGntd \in BOOLEAN + /\ curCmd \in {"Empty", "ReqS", "ReqE"} + /\ 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 = {} + /\ shrSet = {} + /\ exGntd = FALSE + /\ curCmd = "Empty" + /\ curPtr = NoNode + +------------------------------------------------------------------------------- + +SendReq(i) == + /\ chan1[i] = "Empty" + /\ \E c \in {"ReqS", "ReqE"} : + /\ cache[i] \in (IF c = "ReqS" THEN {"I"} ELSE {"I", "S"}) + /\ chan1' = [chan1 EXCEPT ![i] = c] + /\ UNCHANGED <> + +RecvReq(i) == + /\ curCmd = "Empty" + /\ chan1[i] \in {"ReqS", "ReqE"} + /\ curCmd' = chan1[i] + /\ curPtr' = i + /\ chan1' = [chan1 EXCEPT ![i] = "Empty"] + /\ invSet' = shrSet + /\ UNCHANGED <> + +SendInv(i) == + /\ chan2[i] = "Empty" + /\ i \in invSet + /\ (curCmd = "ReqE" \/ (curCmd = "ReqS" /\ exGntd = TRUE)) + /\ chan2' = [chan2 EXCEPT ![i] = "Inv"] + /\ invSet' = invSet \ {i} + /\ 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 \ {i} + /\ exGntd' = IF exGntd = TRUE THEN FALSE ELSE exGntd + /\ UNCHANGED <> + +SendGnt(i) == + /\ curCmd \in {"ReqS", "ReqE"} + /\ curPtr = i + /\ chan2[i] = "Empty" + /\ exGntd = FALSE + /\ curCmd = "ReqE" => shrSet = {} + /\ chan2' = [chan2 EXCEPT ![i] = IF curCmd = "ReqS" THEN "GntS" ELSE "GntE"] + /\ shrSet' = shrSet \cup {i} + /\ exGntd' = (curCmd = "ReqE") + /\ curCmd' = "Empty" + /\ curPtr' = NoNode + /\ UNCHANGED <> + +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 <> + +------------------------------------------------------------------------------- + +Next == + \E i \in NODE : + \/ SendReq(i) + \/ RecvReq(i) + \/ SendInv(i) \/ SendInvAck(i) \/ RecvInvAck(i) + \/ SendGnt(i) + \/ RecvGnt(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/GermanData.tla b/specifications/GermanProtocol/GermanData.tla new file mode 100644 index 00000000..bb77d10d --- /dev/null +++ b/specifications/GermanProtocol/GermanData.tla @@ -0,0 +1,230 @@ +------------------------------ MODULE GermanData ------------------------------ +EXTENDS Naturals, FiniteSets + +CONSTANTS + NODE, + DATA, + NoData, + NoNode + +ASSUME NoDataNotInDATA == NoData \notin DATA +ASSUME NoNodeNotInNODE == NoNode \notin NODE + +CacheState == {"I", "S", "E"} + +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 : {"Empty", "ReqS", "ReqE"}, data : Payload]] + /\ chan2 \in [NODE -> [cmd : {"Empty", "Inv", "GntS", "GntE"}, data : Payload]] + /\ chan3 \in [NODE -> [cmd : {"Empty", "InvAck"}, data : Payload]] + /\ invSet \subseteq NODE + /\ shrSet \subseteq NODE + /\ exGntd \in BOOLEAN + /\ curCmd \in {"Empty", "ReqS", "ReqE"} + /\ 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 = {} + /\ shrSet = {} + /\ 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 <> + +SendReq(i) == + /\ chan1[i].cmd = "Empty" + /\ \E c \in {"ReqS", "ReqE"} : + /\ cache[i].state \in (IF c = "ReqS" THEN {"I"} ELSE {"I", "S"}) + /\ chan1' = [chan1 EXCEPT ![i].cmd = c] + /\ UNCHANGED <> + +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 <> + +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 <> + +------------------------------------------------------------------------------- + +RecvReq(i) == + /\ curCmd = "Empty" + /\ chan1[i].cmd \in {"ReqS", "ReqE"} + /\ curCmd' = chan1[i].cmd + /\ curPtr' = i + /\ chan1' = [chan1 EXCEPT ![i].cmd = "Empty"] + /\ invSet' = shrSet + /\ UNCHANGED <> + +SendInv(i) == + /\ chan2[i].cmd = "Empty" + /\ i \in invSet + /\ (curCmd = "ReqE" \/ (curCmd = "ReqS" /\ exGntd = TRUE)) + /\ chan2' = [chan2 EXCEPT ![i].cmd = "Inv"] + /\ invSet' = invSet \ {i} + /\ UNCHANGED <> + +RecvInvAck(i) == + /\ chan3[i].cmd = "InvAck" + /\ curCmd # "Empty" + /\ shrSet' = shrSet \ {i} + /\ 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 <> + +SendGnt(i) == + /\ curCmd \in {"ReqS", "ReqE"} + /\ curPtr = i + /\ chan2[i].cmd = "Empty" + /\ exGntd = FALSE + /\ curCmd = "ReqE" => shrSet = {} + /\ chan2' = [chan2 EXCEPT ![i].cmd = IF curCmd = "ReqS" THEN "GntS" ELSE "GntE", + ![i].data = memData] + /\ shrSet' = shrSet \cup {i} + /\ exGntd' = (curCmd = "ReqE") + /\ curCmd' = "Empty" + /\ curPtr' = NoNode + /\ UNCHANGED <> + +------------------------------------------------------------------------------- + +Next == + \/ \E i \in NODE, d \in DATA : Store(i, d) + \/ \E i \in NODE : + \/ SendReq(i) + \/ RecvReq(i) + \/ SendInv(i) \/ SendInvAck(i) \/ RecvInvAck(i) + \/ SendGnt(i) + \/ RecvGnt(i) + +Spec == Init /\ [][Next]_vars + +------------------------------------------------------------------------------- + +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], + 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 + +TransactionConsistency == + (curCmd = "Empty") <=> (curPtr = NoNode) + +DirectoryAccurate == + \A i \in NODE : cache[i].state \in {"S", "E"} => i \in shrSet + +ExclusiveIsolation == + \A i \in NODE : + 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" + +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" + +------------------------------------------------------------------------------- + +Fairness == + \A i \in NODE : + /\ SF_vars(RecvReq(i)) + /\ WF_vars(SendInv(i)) + /\ WF_vars(SendInvAck(i)) + /\ WF_vars(RecvInvAck(i)) + /\ WF_vars(SendGnt(i)) + /\ WF_vars(RecvGnt(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/MCGermanCMPWithMutex.cfg b/specifications/GermanProtocol/MCGermanCMPWithMutex.cfg new file mode 100644 index 00000000..c7f4e6fb --- /dev/null +++ b/specifications/GermanProtocol/MCGermanCMPWithMutex.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/MCGermanCMPWithMutex.tla b/specifications/GermanProtocol/MCGermanCMPWithMutex.tla new file mode 100644 index 00000000..54e684b4 --- /dev/null +++ b/specifications/GermanProtocol/MCGermanCMPWithMutex.tla @@ -0,0 +1,8 @@ +------------------------ 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. +Symmetry == Permutations(NODE) + +============================================================================== diff --git a/specifications/GermanProtocol/MCGermanControl.cfg b/specifications/GermanProtocol/MCGermanControl.cfg new file mode 100644 index 00000000..28ecdc1d --- /dev/null +++ b/specifications/GermanProtocol/MCGermanControl.cfg @@ -0,0 +1,16 @@ +\* 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 + Other = other + +SYMMETRY Symmetry + +SPECIFICATION Spec + +INVARIANT + TypeOK + Coherence + +PROPERTY Refinement diff --git a/specifications/GermanProtocol/MCGermanControl.tla b/specifications/GermanProtocol/MCGermanControl.tla new file mode 100644 index 00000000..ddf8cf52 --- /dev/null +++ b/specifications/GermanProtocol/MCGermanControl.tla @@ -0,0 +1,16 @@ +--------------------------- 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 GermanCMPWithMutex + +Refinement == Abstract!Spec + +\* Nodes are interchangeable, so collapse permutations of NODE. +Symmetry == Permutations(NODE) + +============================================================================== diff --git a/specifications/GermanProtocol/MCGermanData.cfg b/specifications/GermanProtocol/MCGermanData.cfg new file mode 100644 index 00000000..10d0f945 --- /dev/null +++ b/specifications/GermanProtocol/MCGermanData.cfg @@ -0,0 +1,27 @@ +\* 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 GermanControl, +\* defined in GermanData.tla). +CONSTANTS + NODE = {n1, n2} + DATA = {d1, d2} + NoData = noData + NoNode = noNode + +SYMMETRY Symmetry + +SPECIFICATION Spec + +INVARIANT + TypeOK + Coherence + DataProp + TransactionConsistency + DirectoryAccurate + ExclusiveIsolation + WritebackCarriesLatest + +PROPERTY Refinement diff --git a/specifications/GermanProtocol/MCGermanData.tla b/specifications/GermanProtocol/MCGermanData.tla new file mode 100644 index 00000000..d4df03e6 --- /dev/null +++ b/specifications/GermanProtocol/MCGermanData.tla @@ -0,0 +1,8 @@ +----------------------------- 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. +Symmetry == Permutations(NODE) \union Permutations(DATA) + +============================================================================== diff --git a/specifications/GermanProtocol/README.md b/specifications/GermanProtocol/README.md new file mode 100644 index 00000000..de401f31 --- /dev/null +++ b/specifications/GermanProtocol/README.md @@ -0,0 +1,132 @@ +# 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. + +## 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 +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..8b75121d --- /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/APGermanCMPWithMutex.tla", + "features": [], + "models": [ + { + "path": "specifications/GermanProtocol/APGermanCMPWithMutex.cfg", + "runtime": "00:00:20", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "path": "specifications/GermanProtocol/APGermanControl.tla", + "features": [], + "models": [ + { + "path": "specifications/GermanProtocol/APGermanControl.cfg", + "runtime": "00:00:08", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "path": "specifications/GermanProtocol/APGermanData.tla", + "features": [], + "models": [ + { + "path": "specifications/GermanProtocol/APGermanData.cfg", + "runtime": "00:00:39", + "mode": "symbolic", + "result": "success" + } + ] + }, + { + "path": "specifications/GermanProtocol/GermanCMPWithMutex.tla", + "features": [], + "models": [] + }, + { + "path": "specifications/GermanProtocol/GermanControl.tla", + "features": [], + "models": [] + }, + { + "path": "specifications/GermanProtocol/GermanData.tla", + "features": [], + "models": [] + }, + { + "path": "specifications/GermanProtocol/MCGermanCMPWithMutex.tla", + "features": [], + "models": [ + { + "path": "specifications/GermanProtocol/MCGermanCMPWithMutex.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 1107, + "totalStates": 3281, + "stateDepth": 19 + } + ] + }, + { + "path": "specifications/GermanProtocol/MCGermanControl.tla", + "features": [], + "models": [ + { + "path": "specifications/GermanProtocol/MCGermanControl.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 735, + "totalStates": 1946, + "stateDepth": 19 + } + ] + }, + { + "path": "specifications/GermanProtocol/MCGermanData.tla", + "features": [], + "models": [ + { + "path": "specifications/GermanProtocol/MCGermanData.cfg", + "runtime": "00:00:01", + "mode": "exhaustive search", + "result": "success", + "distinctStates": 852, + "totalStates": 2493, + "stateDepth": 19 + } + ] + } + ] +}