From bd25e403c006aadc0cef88f20fa1b24d2cf4b90a Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 6 Sep 2023 18:33:24 +0000 Subject: [PATCH] matchIndex lower bound for nextIndex https://github.com/microsoft/CCF/issues/5341 --- src/consensus/aft/raft.h | 3 ++- tla/ccfraft.tla | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/consensus/aft/raft.h b/src/consensus/aft/raft.h index 89d1cf131a29..49ef6d25e57b 100644 --- a/src/consensus/aft/raft.h +++ b/src/consensus/aft/raft.h @@ -1436,7 +1436,8 @@ namespace aft from); const auto this_match = find_highest_possible_match({r.term, r.last_log_idx}); - node->second.sent_idx = std::min(this_match, node->second.sent_idx); + node->second.sent_idx = std::max( + std::min(this_match, node->second.sent_idx), node->second.match_idx); return; } else diff --git a/tla/ccfraft.tla b/tla/ccfraft.tla index fc74623056a5..e85ed19b1767 100644 --- a/tla/ccfraft.tla +++ b/tla/ccfraft.tla @@ -954,7 +954,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] = max(tm, matchIndex[i][j]) + 1 ] + IN nextIndex' = [nextIndex EXCEPT ![i][j] = max(min(tm, nextIndex[i][j]-1), 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