From 6d07d3b3029955c7530a9a06ceb25d8ebe31bbb1 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 5 Sep 2023 04:33:50 +0000 Subject: [PATCH] matchIndex lower bound for nextIndex https://github.com/microsoft/CCF/issues/5341 --- tla/MCccfraft.cfg | 1 + tla/MCccfraftWithReconfig.cfg | 1 + tla/SIMccfraft.cfg | 4 +++- tla/ccfraft.tla | 9 +++++++-- 4 files changed, 12 insertions(+), 3 deletions(-) diff --git a/tla/MCccfraft.cfg b/tla/MCccfraft.cfg index 3259fdfff078..99727cc2ef30 100644 --- a/tla/MCccfraft.cfg +++ b/tla/MCccfraft.cfg @@ -67,6 +67,7 @@ INVARIANTS MonoLogInv LogConfigurationConsistentInv NoLeaderInTermZeroInv + MatchIndexLowerBoundNextIndexInv \* DebugInvLeaderCannotStepDown \* DebugInvAnyCommitted \* DebugInvAllCommitted diff --git a/tla/MCccfraftWithReconfig.cfg b/tla/MCccfraftWithReconfig.cfg index 51e923d61628..a261dc34c1b1 100644 --- a/tla/MCccfraftWithReconfig.cfg +++ b/tla/MCccfraftWithReconfig.cfg @@ -67,6 +67,7 @@ INVARIANTS MonoLogInv LogConfigurationConsistentInv NoLeaderInTermZeroInv + MatchIndexLowerBoundNextIndexInv \* DebugInvLeaderCannotStepDown \* DebugInvAnyCommitted \* DebugInvAllCommitted diff --git a/tla/SIMccfraft.cfg b/tla/SIMccfraft.cfg index 53cb81a2e8b3..9c41f5e85199 100644 --- a/tla/SIMccfraft.cfg +++ b/tla/SIMccfraft.cfg @@ -63,7 +63,9 @@ INVARIANTS MonoLogInv LogConfigurationConsistentInv NoLeaderInTermZeroInv - + + MatchIndexLowerBoundNextIndexInv + \* DebugInvLeaderCannotStepDown \* DebugInvAnyCommitted \* DebugInvAllCommitted diff --git a/tla/ccfraft.tla b/tla/ccfraft.tla index f932d4670ab3..1fbbd75aad82 100644 --- a/tla/ccfraft.tla +++ b/tla/ccfraft.tla @@ -310,6 +310,8 @@ CandidateVarsTypeInv == \* The next entry to send to each follower. VARIABLE nextIndex +\* nextIndex cannot be zero as its the index of the first log +\* entry in the AE message (recalling that TLA+ is 1-indexed). NextIndexTypeInv == \A i, j \in Servers : i /= j => /\ nextIndex[i][j] \in Nat \ {0} @@ -950,8 +952,7 @@ HandleAppendEntriesResponse(i, j, m) == /\ nextIndex' = [nextIndex EXCEPT ![i][j] = max(@, m.lastLogIndex + 1)] \/ /\ \lnot m.success \* not successful /\ LET tm == FindHighestPossibleMatch(log[i], m.lastLogIndex, m.term) - IN nextIndex' = [nextIndex EXCEPT ![i][j] = - (IF matchIndex[i][j] = 0 THEN tm ELSE min(tm, matchIndex[i][j])) + 1 ] + IN nextIndex' = [nextIndex EXCEPT ![i][j] = max(tm, matchIndex[i][j]) + 1 ] \* UNCHANGED matchIndex is implied by the following statement in figure 2, page 4 in the raft paper: \* "If AppendEntries fails because of log inconsistency: decrement nextIndex and retry" /\ UNCHANGED matchIndex @@ -1231,6 +1232,10 @@ NoLeaderInTermZeroInv == \A i \in Servers : currentTerm[i] = 0 => state[i] # Leader +MatchIndexLowerBoundNextIndexInv == + \A i,j \in Servers : + state[i] = Leader => + nextIndex[i][j] > matchIndex[i][j] ------------------------------------------------------------------------------ \* Properties