Add German cache-coherence protocol example (Murphi > TLA+)

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

specifications/GermanProtocol/APGermanCMPWithMutex.cfg

@@ -0,0 +1,11 @@
+CONSTANT
+  NODE   <- NodeVal
+  Other  <- OtherVal
+  NoNode <- NoNodeVal
+
+INVARIANT
+  TypeOK
+  Coherence
+  Lemma_1
+
+SPECIFICATION Spec

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"
+
+==============================================================================

specifications/GermanProtocol/APGermanControl.cfg

@@ -0,0 +1,9 @@
+CONSTANT
+  NODE   <- NodeVal
+  NoNode <- NoNodeVal
+
+INVARIANT
+  TypeOK
+  Coherence
+
+SPECIFICATION Spec

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"
+
+==============================================================================

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

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"
+
+==============================================================================

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 == <<cache, chan1, chan2, chan3, invSet, shrSet, exGntd, curCmd, curPtr>>
+
+-------------------------------------------------------------------------------
+
+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 <<cache, chan2, chan3, invSet, shrSet, exGntd, curCmd, curPtr>>
+
+RecvReq(i) ==
+    /\ curCmd = "Empty"
+    /\ chan1[i] \in {"ReqS", "ReqE"}
+    /\ curCmd' = chan1[i]
+    /\ curPtr' = i
+    /\ chan1' = [chan1 EXCEPT ![i] = "Empty"]
+    /\ invSet' = shrSet
+    /\ UNCHANGED <<cache, chan2, chan3, shrSet, exGntd>>
+
+SendInv(i) ==
+    /\ chan2[i] = "Empty"
+    /\ i \in invSet
+    /\ (curCmd = "ReqE" \/ (curCmd = "ReqS" /\ exGntd = TRUE))
+    /\ chan2' = [chan2 EXCEPT ![i] = "Inv"]
+    /\ invSet' = invSet \ {i}
+    /\ UNCHANGED <<cache, chan1, chan3, shrSet, exGntd, curCmd, curPtr>>
+
+SendInvAck(i) ==
+    /\ chan2[i] = "Inv"
+    /\ chan3[i] = "Empty"
+    /\ chan2' = [chan2 EXCEPT ![i] = "Empty"]
+    /\ chan3' = [chan3 EXCEPT ![i] = "InvAck"]
+    /\ cache' = [cache EXCEPT ![i] = "I"]
+    /\ UNCHANGED <<chan1, invSet, shrSet, exGntd, curCmd, curPtr>>
+
+RecvInvAck(i) ==
+    /\ chan3[i] = "InvAck"
+    /\ curCmd # "Empty"
+    /\ chan3' = [chan3 EXCEPT ![i] = "Empty"]
+    /\ shrSet' = shrSet \ {i}
+    /\ exGntd' = FALSE
+    /\ UNCHANGED <<cache, chan1, chan2, invSet, curCmd, curPtr>>
+
+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 <<cache, chan1, chan3, invSet>>
+
+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 <<chan1, chan3, invSet, shrSet, exGntd, curCmd, curPtr>>
+
+-------------------------------------------------------------------------------
+
+\* 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 <<cache, chan1, chan2, chan3, shrSet, exGntd>>
+
+ABS_SendGnt ==
+    /\ curCmd \in {"ReqS", "ReqE"}
+    /\ curPtr = Other
+    /\ exGntd = FALSE
+    /\ curCmd = "ReqE" => shrSet = {}
+    /\ exGntd' = (curCmd = "ReqE")
+    /\ curCmd' = "Empty"
+    /\ curPtr' = NoNode
+    /\ UNCHANGED <<cache, chan1, chan2, chan3, invSet, shrSet>>
+
+\* 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 <<cache, chan1, chan2, chan3, invSet, shrSet, curCmd, curPtr>>
+
+-------------------------------------------------------------------------------
+
+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"
+
+=============================================================================