diff --git a/tla/consistency/ExternalHistory.tla b/tla/consistency/ExternalHistory.tla index 8fd42651a262..b543f73820ce 100644 --- a/tla/consistency/ExternalHistory.tla +++ b/tla/consistency/ExternalHistory.tla @@ -48,7 +48,8 @@ HistoryTypeOK == /\ history[i].tx \in Txs \/ /\ history[i].type \in {RwTxResponse, RoTxResponse} /\ history[i].tx \in Txs - /\ history[i].observed \in Seq(Txs) + /\ DOMAIN history[i].observed \subseteq Views + /\ Range(history[i].observed) \subseteq Txs /\ history[i].tx_id \in TxIDs \/ /\ history[i].type = TxStatusReceived /\ history[i].tx_id \in TxIDs diff --git a/tla/consistency/ExternalHistoryInvars.tla b/tla/consistency/ExternalHistoryInvars.tla index 146fd2818043..b46e8ffef506 100644 --- a/tla/consistency/ExternalHistoryInvars.tla +++ b/tla/consistency/ExternalHistoryInvars.tla @@ -1,6 +1,6 @@ ---- MODULE ExternalHistoryInvars ---- -EXTENDS ExternalHistory +EXTENDS ExternalHistory, Functions \* Read-write transaction responses always follow an associated request AllRwReceivedIsFirstSentInv == @@ -127,7 +127,7 @@ AllCommittedObservedInv == \A k \in RwTxResponseCommittedEventIndexes : /\ history[k].tx = history[j].tx /\ i < j - => Contains(history[k].observed, history[i].tx) + => \E idx \in DOMAIN history[k].observed : history[k].observed[idx] = history[i].tx \* All committed read-only txs observe all previously committed txs (wrt to real-time) \* Note that this requires committed txs to be observed from their response, @@ -178,8 +178,8 @@ RwSerializableInv == \A i,j \in DOMAIN history: /\ history[i].type = RwTxResponse /\ history[j].type = RwTxResponse - => \/ IsPrefix(history[i].observed, history[j].observed) - \/ IsPrefix(history[j].observed, history[i].observed) + => \/ IsRestriction(history[i].observed, history[j].observed) + \/ IsRestriction(history[j].observed, history[i].observed) \* A weaker version of RwSerializableInv which only considers committed requests \* If any committed request observes A before B then every committed request must observe A before B @@ -195,8 +195,8 @@ CommittedRwSerializableInv == /\ history[l].type = TxStatusReceived /\ history[l].status = CommittedStatus /\ history[j].tx_id = history[l].tx_id - => \/ IsPrefix(history[i].observed, history[j].observed) - \/ IsPrefix(history[j].observed, history[i].observed) + => \/ IsRestriction(history[i].observed, history[j].observed) + \/ IsRestriction(history[j].observed, history[i].observed) \* Linearizability for read-write transactions \* Or equivalently, strict serializability as we are modeling a single object system diff --git a/tla/consistency/MCMultiNode.cfg b/tla/consistency/MCMultiNode.cfg index 420e7295282a..946142c2ae85 100644 --- a/tla/consistency/MCMultiNode.cfg +++ b/tla/consistency/MCMultiNode.cfg @@ -15,6 +15,7 @@ CONSTANTS InvalidStatus = InvalidStatus INVARIANTS + TypeOK AllReceivedIsFirstSentInv AllCommittedObservedInv OnlyObserveSentRequestsInv diff --git a/tla/consistency/MCMultiNodeCommitReachability.cfg b/tla/consistency/MCMultiNodeCommitReachability.cfg index e5fefbceca7b..c5752c3d0e0f 100644 --- a/tla/consistency/MCMultiNodeCommitReachability.cfg +++ b/tla/consistency/MCMultiNodeCommitReachability.cfg @@ -16,6 +16,7 @@ CONSTANTS InvalidStatus = InvalidStatus INVARIANTS + TypeOK MultiCommittedTxDebugInv CHECK_DEADLOCK diff --git a/tla/consistency/MCMultiNodeInvalidReachability.cfg b/tla/consistency/MCMultiNodeInvalidReachability.cfg index adc532549beb..a2e8ea5a15a8 100644 --- a/tla/consistency/MCMultiNodeInvalidReachability.cfg +++ b/tla/consistency/MCMultiNodeInvalidReachability.cfg @@ -16,6 +16,7 @@ CONSTANTS InvalidStatus = InvalidStatus INVARIANTS + TypeOK SomeInvalidTxDebugInv CHECK_DEADLOCK diff --git a/tla/consistency/MCMultiNodeReads.cfg b/tla/consistency/MCMultiNodeReads.cfg index 4e4c5acc8d86..c77d932765cc 100644 --- a/tla/consistency/MCMultiNodeReads.cfg +++ b/tla/consistency/MCMultiNodeReads.cfg @@ -15,6 +15,7 @@ CONSTANTS InvalidStatus = InvalidStatus INVARIANTS + TypeOK AllReceivedIsFirstSentInv AllCommittedObservedInv OnlyObserveSentRequestsInv diff --git a/tla/consistency/MCMultiNodeReadsAlt.cfg b/tla/consistency/MCMultiNodeReadsAlt.cfg index be994db35b1b..3678682c6194 100644 --- a/tla/consistency/MCMultiNodeReadsAlt.cfg +++ b/tla/consistency/MCMultiNodeReadsAlt.cfg @@ -15,6 +15,7 @@ CONSTANTS InvalidStatus = InvalidStatus INVARIANTS + TypeOK AllReceivedIsFirstSentInv AllCommittedObservedInv OnlyObserveSentRequestsInv diff --git a/tla/consistency/MCMultiNodeReadsNotLinearizable.cfg b/tla/consistency/MCMultiNodeReadsNotLinearizable.cfg index 2d3e9472ef9f..d23f74fa95e5 100644 --- a/tla/consistency/MCMultiNodeReadsNotLinearizable.cfg +++ b/tla/consistency/MCMultiNodeReadsNotLinearizable.cfg @@ -16,6 +16,7 @@ CONSTANTS InvalidStatus = InvalidStatus INVARIANTS + TypeOK AllCommittedObservedRoInv CHECK_DEADLOCK diff --git a/tla/consistency/MCSingleNode.cfg b/tla/consistency/MCSingleNode.cfg index f9c69fc0b471..ab554ec9a3c7 100644 --- a/tla/consistency/MCSingleNode.cfg +++ b/tla/consistency/MCSingleNode.cfg @@ -14,6 +14,7 @@ CONSTANTS InvalidStatus = InvalidStatus INVARIANTS + TypeOK AllReceivedIsFirstSentInv AllCommittedObservedInv OnlyObserveSentRequestsInv diff --git a/tla/consistency/MCSingleNodeCommitReachability.cfg b/tla/consistency/MCSingleNodeCommitReachability.cfg index e6bb8725eca7..98453dae1661 100644 --- a/tla/consistency/MCSingleNodeCommitReachability.cfg +++ b/tla/consistency/MCSingleNodeCommitReachability.cfg @@ -15,6 +15,7 @@ CONSTANTS InvalidStatus = InvalidStatus INVARIANTS + TypeOK SomeCommittedTxDebugInv CHECK_DEADLOCK diff --git a/tla/consistency/MCSingleNodeReads.cfg b/tla/consistency/MCSingleNodeReads.cfg index 3fa5b8efc900..f35acb9169e1 100644 --- a/tla/consistency/MCSingleNodeReads.cfg +++ b/tla/consistency/MCSingleNodeReads.cfg @@ -14,6 +14,7 @@ CONSTANTS InvalidStatus = InvalidStatus INVARIANTS + TypeOK AllReceivedIsFirstSentInv AllCommittedObservedInv OnlyObserveSentRequestsInv diff --git a/tla/consistency/SingleNode.tla b/tla/consistency/SingleNode.tla index ab211f111a05..0266107d2953 100644 --- a/tla/consistency/SingleNode.tla +++ b/tla/consistency/SingleNode.tla @@ -6,7 +6,6 @@ EXTENDS ExternalHistoryInvars, TLC - \* Abstract ledgers that contains only client transactions (no signatures) \* 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 @@ -63,11 +62,11 @@ RwTxExecuteAction == \* that it can be picked up by the current leader or any former leader /\ \E view \in FirstBranch..Len(ledgerBranches): ledgerBranches' = [ledgerBranches EXCEPT ![view] = - Append(@,[view |-> view, tx |-> history[i].tx])] + @ @@ (Max(DOMAIN ledgerBranches[view] \cup {0})+1) :> [view |-> view, tx |-> history[i].tx]] /\ UNCHANGED history LedgerBranchTxOnly(branch) == - LET SubBranch == SelectSeq(branch, LAMBDA e : "tx" \in DOMAIN e) + LET SubBranch == [ i \in {j \in DOMAIN branch : "tx" \in DOMAIN branch[j] } |-> branch[i] ] IN [i \in DOMAIN SubBranch |-> SubBranch[i].tx] \* Response to a read-write transaction @@ -87,7 +86,7 @@ RwTxResponseAction == history,[ type |-> RwTxResponse, tx |-> history[i].tx, - observed |-> LedgerBranchTxOnly(SubSeq(ledgerBranches[view],1,seqnum)), + observed |-> LedgerBranchTxOnly([j \in DOMAIN ledgerBranches[view] \cap 1..seqnum |-> ledgerBranches[view][j]]), tx_id |-> <>] ) /\ UNCHANGED ledgerBranches @@ -98,8 +97,8 @@ StatusCommittedResponseAction == LET view == history[i].tx_id[1] seqno == history[i].tx_id[2] IN /\ history[i].type = RwTxResponse - /\ Len(Last(ledgerBranches)) >= seqno - /\ Last(ledgerBranches)[seqno].view = view + /\ Max(DOMAIN ledgerBranches[Len(ledgerBranches)] \cup {0}) >= seqno + /\ ledgerBranches[Len(ledgerBranches)][history[i].tx_id[2]].view = view \* There is no future InvalidStatus that's incompatible with this commit \* This is to accomodate StatusInvalidResponseAction making future commits invalid, \* and is an unnecessary complication for model checking. It does facilitate trace @@ -121,9 +120,8 @@ StatusCommittedResponseAction == \* Append a transaction to the ledger which does not impact the state we are considering AppendOtherTxnAction == - /\ \E view \in FirstBranch..Len(ledgerBranches): - ledgerBranches' = [ledgerBranches EXCEPT ![view] = - Append(@,[view |-> view])] + /\ \E view \in (DOMAIN ledgerBranches) \ 0..(FirstBranch-1): + ledgerBranches' = [ledgerBranches EXCEPT ![view] = @ @@ (Max(DOMAIN ledgerBranches[view] \cup {0})+1) :> [view |-> view] ] /\ UNCHANGED history \* A CCF service with a single node will never have a view change diff --git a/tla/consistency/SingleNodeReads.tla b/tla/consistency/SingleNodeReads.tla index aaba5e1a6a19..9ad92f964e75 100644 --- a/tla/consistency/SingleNodeReads.tla +++ b/tla/consistency/SingleNodeReads.tla @@ -22,14 +22,14 @@ RoTxResponseAction == /\ j > i /\ history[j].type = RoTxResponse /\ history[j].tx = history[i].tx} = {} - /\ \E view \in FirstBranch..Len(ledgerBranches): - /\ Len(ledgerBranches[view]) > 0 + /\ \E view \in (DOMAIN ledgerBranches) \ 1..(FirstBranch-1): + /\ ledgerBranches[view] # <<>> /\ history' = Append( history,[ type |-> RoTxResponse, tx |-> history[i].tx, observed |-> LedgerBranchTxOnly(ledgerBranches[view]), - tx_id |-> <>] ) + tx_id |-> <>] ) /\ UNCHANGED ledgerBranches NextSingleNodeReadsAction ==