Merge branch 'main' into consensus_tv_todo_cleanup

tla/consistency/ExternalHistory.tla

@@ -24,6 +24,7 @@ TxStatuses == {
 \* Although views start at 1 in the consistency spec, this constant allows increasing the first branch
 \* that can be appended to, to enable trace validation against the implementation, where view starts at 2
 CONSTANT FirstBranch
+ASSUME FirstBranch \in Nat \ {0}
 
 \* Views start at 1, 0 is used a null value
 Views == Nat
@@ -37,9 +38,12 @@ TxIDs == Views \X SeqNums
 \* This models uses a dummy application where read-write transactions 
 \* append an integer to a list and then reads the list
 \* Read-only transactions simply read the list
+\* Transactions themselves simply consist of a natural number
 Txs == Nat
 
-\* History of events visible to clients
+\* History of events visible externally
+\* There is a single shared history for all nodes. The events themselves do not include timestamps.
+\* The order of events in the history is the order in which they were observed by a client (according to some global clock)
 VARIABLES history
 
 HistoryTypeOK ==
@@ -59,6 +63,9 @@ HistoryTypeOK ==
 HistoryMonoProp ==
     [][IsPrefix(history, history')]_history
 
+----
+\* The following are helper definitions for handling histories
+
 \* Indexes into history for events where a committed status is received
 CommittedEventIndexes == 
     {i \in DOMAIN history: 
@@ -69,7 +76,8 @@ CommittedEventIndexes ==
 \* Transaction IDs which received committed status messages
 CommittedTxIDs ==
     {history[i].tx_id: i \in CommittedEventIndexes}
-
+
+\* Indexes into history for events where a invalid status is received
 InvalidEventIndexes == 
     {i \in DOMAIN history: 
         /\ history[i].type = TxStatusReceived
@@ -80,7 +88,7 @@ InvalidEventIndexes ==
 InvalidTxIDs ==
     {history[i].tx_id: i \in InvalidEventIndexes}
 
-\* Highest commit sequence number
+\* Highest committed sequence number
 CommitSeqNum == 
     Max({i[2]: i \in CommittedTxIDs} \cup {0})
 
@@ -90,11 +98,12 @@ RwTxResponseEventIndexes ==
 RoTxResponseEventIndexes ==
     {x \in DOMAIN history : history[x].type = RoTxResponse}
 
+\* Indexes into history for events where a transaction was responded to
 TxResponseEventIndexes ==
     RwTxResponseEventIndexes \union RoTxResponseEventIndexes
 
-
-\* Note these index are the events where the transaction was responded to
+\* Indexes into history for events where a committed rw transaction was responded to
+\* Note these index are the events where the transaction was responded to, not the events where the transaction was committed
 RwTxResponseCommittedEventIndexes ==
     {x \in DOMAIN history : 
         /\ history[x].type = RwTxResponse

tla/consistency/ExternalHistoryInvars.tla

@@ -52,7 +52,6 @@ UniqueTxRequestsInv ==
         /\ i # j
         => history[i].tx # history[j].tx
 
-
 \* Each transaction has a unique transaction ID
 UniqueTxIdsInv ==
     \A i, j \in {x \in DOMAIN history : history[x].type \in {RwTxResponse, RoTxResponse}} :
@@ -88,6 +87,14 @@ OnceCommittedPrevCommittedInv ==
         /\ history[j].tx_id[2] <= history[i].tx_id[2]
         => history[j].status = CommittedStatus
 
+\* If a transaction is committed then all others from greater (or equal) seqnums but strictly smaller terms are invalid
+OnceCommittedNextInvalidInv ==
+    \A i, j \in TxStatusReceivedEventIndexes:
+        /\ history[i].status = CommittedStatus
+        /\ history[i].tx_id[2] <= history[j].tx_id[2]
+        /\ history[j].tx_id[1] < history[i].tx_id[1]
+        => history[j].status = InvalidStatus
+
 \* If a transaction is invalid then so are all others from the same term with greater seqnums
 OnceInvalidNextInvalidInv ==
     \A i, j \in TxStatusReceivedEventIndexes:
@@ -99,6 +106,7 @@ OnceInvalidNextInvalidInv ==
 \* The following is strengthened variant of CommittedOrInvalidInv
 CommittedOrInvalidStrongInv ==
     /\ OnceCommittedPrevCommittedInv
+    /\ OnceCommittedNextInvalidInv
     /\ OnceInvalidNextInvalidInv
 
 

tla/consistency/MCMultiNode.cfg

@@ -5,14 +5,14 @@ CONSTANTS
     HistoryLimit = 6
     ViewLimit = 3
 
-    RwTxRequest = RwTxRequest
-    RwTxResponse = RwTxResponse
-    RoTxRequest = RoTxRequest
-    RoTxResponse = RoTxResponse
-    TxStatusReceived = TxStatusReceived
+    RwTxRequest = T_RwTxRequest
+    RwTxResponse = T_RwTxResponse
+    RoTxRequest = T_RoTxRequest
+    RoTxResponse = T_RoTxResponse
+    TxStatusReceived = T_TxStatusReceived
 
-    CommittedStatus = CommittedStatus
-    InvalidStatus = InvalidStatus
+    CommittedStatus = S_CommittedStatus
+    InvalidStatus = S_InvalidStatus
 
 INVARIANTS
     AllReceivedIsFirstSentInv

tla/consistency/MCMultiNodeCommitReachability.cfg

@@ -1,6 +1,5 @@
 SPECIFICATION MCSpecMultiNodeReads
 
-
 CONSTANTS
     FirstBranch = 1
     HistoryLimit = 6

tla/consistency/MCMultiNodeInvalidReachability.cfg

@@ -1,22 +1,21 @@
 SPECIFICATION MCSpecMultiNodeReads
 
-
 CONSTANTS
     FirstBranch = 1
     HistoryLimit = 7
     ViewLimit = 2
 
-    RwTxRequest = RwTxRequest
-    RwTxResponse = RwTxResponse
-    RoTxRequest = RoTxRequest
-    RoTxResponse = RoTxResponse
-    TxStatusReceived = TxStatusReceived
+    RwTxRequest = T_RwTxRequest
+    RwTxResponse = T_RwTxResponse
+    RoTxRequest = T_RoTxRequest
+    RoTxResponse = T_RoTxResponse
+    TxStatusReceived = T_TxStatusReceived
 
-    CommittedStatus = CommittedStatus
-    InvalidStatus = InvalidStatus
+    CommittedStatus = S_CommittedStatus
+    InvalidStatus = S_InvalidStatus
 
 INVARIANTS
-   SomeInvalidTxDebugInv
+    SomeInvalidTxDebugInv
 
 CHECK_DEADLOCK
     FALSE

tla/consistency/MCMultiNodeReadsNotLinearizable.cfg

@@ -1,20 +1,18 @@
 SPECIFICATION MCSpecMultiNodeReads
 
-
 CONSTANTS
     FirstBranch = 1
     HistoryLimit = 8
     ViewLimit = 2
 
-    RwTxRequest = RwTxRequest
-    RwTxResponse = RwTxResponse
-    RoTxRequest = RoTxRequest
-    RoTxResponse = RoTxResponse
-    TxStatusReceived = TxStatusReceived
-
-    CommittedStatus = CommittedStatus
-    InvalidStatus = InvalidStatus
+    RwTxRequest = T_RwTxRequest
+    RwTxResponse = T_RwTxResponse
+    RoTxRequest = T_RoTxRequest
+    RoTxResponse = T_RoTxResponse
+    TxStatusReceived = T_TxStatusReceived
 
+    CommittedStatus = S_CommittedStatus
+    InvalidStatus = S_InvalidStatus
 INVARIANTS
     AllCommittedObservedRoInv
 

tla/consistency/MCSingleNode.tla

@@ -1,17 +1,15 @@
 ---- MODULE MCSingleNode ----
-\* Bounded version of SingleNode
+\* Bounded version of SingleNode for model checking
 
 EXTENDS SingleNode
 
+\* Capping the number of events in the history
 CONSTANT HistoryLimit
 
 MCRwTxRequestAction ==
     /\ Len(history) < HistoryLimit
     /\ RwTxRequestAction
 
-MCRwTxExecuteAction ==
-    RwTxExecuteAction
-
 MCRwTxResponseAction ==
     /\ Len(history) < HistoryLimit
     /\ RwTxResponseAction
@@ -22,7 +20,7 @@ MCStatusCommittedResponseAction ==
 
 MCNextSingleNodeAction ==
     \/ MCRwTxRequestAction
-    \/ MCRwTxExecuteAction
+    \/ RwTxExecuteAction
     \/ MCRwTxResponseAction
     \/ MCStatusCommittedResponseAction
 

tla/consistency/MCSingleNodeCommitReachability.cfg

@@ -1,18 +1,17 @@
 SPECIFICATION MCSpecSingleNode
 
-
 CONSTANTS
     FirstBranch = 1
     HistoryLimit = 3
 
-    RwTxRequest = RwTxRequest
-    RwTxResponse = RwTxResponse
-    RoTxRequest = RoTxRequest
-    RoTxResponse = RoTxResponse
-    TxStatusReceived = TxStatusReceived
+    RwTxRequest = T_RwTxRequest
+    RwTxResponse = T_RwTxResponse
+    RoTxRequest = T_RoTxRequest
+    RoTxResponse = T_RoTxResponse
+    TxStatusReceived = T_TxStatusReceived
 
-    CommittedStatus = CommittedStatus
-    InvalidStatus = InvalidStatus
+    CommittedStatus = S_CommittedStatus
+    InvalidStatus = S_InvalidStatus
 
 INVARIANTS
     SomeCommittedTxDebugInv

tla/consistency/MultiNode.tla

@@ -45,6 +45,7 @@ StatusInvalidResponseAction ==
             )
     /\ UNCHANGED ledgerBranches
 
+\* Compared to SingleNode, the multi-node model has two additional actions to simulate view change
 NextMultiNodeAction ==
     \/ NextSingleNodeAction
     \/ TruncateLedgerAction

tla/consistency/SingleNode.tla

@@ -7,30 +7,30 @@
 EXTENDS ExternalHistoryInvars, TLC
 
 
-\* Abstract ledgers that contains only client transactions (no signatures)
+\* Abstract ledgers that contain transactions
 \* Indexed by view, each ledger is the ledger associated with leader of that view 
 \* In practice, the ledger of every CCF node is one of these or a prefix for one of these
-\* This could be switched to a tree which can represent forks more elegantly
 VARIABLES ledgerBranches
 
 LedgerTypeOK ==
     \A view \in DOMAIN ledgerBranches:
         \A seqnum \in DOMAIN ledgerBranches[view]:
-            \* Each ledger entry is tuple containing a view and tx
-            \* The ledger entry index is the sequence number
+            \* Each ledger entry is a record containing a view and optionally a tx
+            \* The ledger entry index is its sequence number
             /\ ledgerBranches[view][seqnum].view \in Views
             /\ "tx" \in DOMAIN ledgerBranches[view][seqnum] => ledgerBranches[view][seqnum].tx \in Txs
 
+TypeOK ==
+    /\ HistoryTypeOK
+    /\ LedgerTypeOK
+
 \* In this abstract version of CCF's consensus layer, each ledger is append-only
+\* Each ledger branch is the log of a leader in a view and thus is not overwritten/rolled back
 LedgersMonoProp ==
     [][\A view \in DOMAIN ledgerBranches: IsPrefix(ledgerBranches[view], ledgerBranches'[view])]_ledgerBranches
 
 vars == << history, ledgerBranches >>
 
-TypeOK ==
-    /\ HistoryTypeOK
-    /\ LedgerTypeOK
-
 Init ==
     /\ history = <<>>
     /\ ledgerBranches = [ x \in 1..FirstBranch |-> <<>>]