From 166386e4dfc1948532b18045e0de9b3be5a44ea8 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 20 Oct 2023 10:38:31 +0200 Subject: [PATCH] Raft Paper section 5.4.2: "[A leader] never commits log entries from previous terms...". (#5748) Related: https://github.com/microsoft/CCF/issues/3950 --- tla/MCccfraft.cfg | 1 + tla/MCccfraftWithReconfig.cfg | 1 + tla/SIMccfraft.cfg | 1 + tla/ccfraft.tla | 7 +++++++ 4 files changed, 10 insertions(+) diff --git a/tla/MCccfraft.cfg b/tla/MCccfraft.cfg index 0306cd59a66d..8f423a9a5cb3 100644 --- a/tla/MCccfraft.cfg +++ b/tla/MCccfraft.cfg @@ -57,6 +57,7 @@ PROPERTIES PermittedLogChangesProp StateTransitionsProp PendingBecomesFollowerProp + NeverCommitEntryPrevTermsProp INVARIANTS LogInv diff --git a/tla/MCccfraftWithReconfig.cfg b/tla/MCccfraftWithReconfig.cfg index 1598f702bda2..623def14095c 100644 --- a/tla/MCccfraftWithReconfig.cfg +++ b/tla/MCccfraftWithReconfig.cfg @@ -57,6 +57,7 @@ PROPERTIES PermittedLogChangesProp StateTransitionsProp PendingBecomesFollowerProp + NeverCommitEntryPrevTermsProp INVARIANTS LogInv diff --git a/tla/SIMccfraft.cfg b/tla/SIMccfraft.cfg index 79a9c72466de..e91d7f01dbbf 100644 --- a/tla/SIMccfraft.cfg +++ b/tla/SIMccfraft.cfg @@ -47,6 +47,7 @@ PROPERTIES PermittedLogChangesProp StateTransitionsProp PendingBecomesFollowerProp + NeverCommitEntryPrevTermsProp INVARIANTS LogInv diff --git a/tla/ccfraft.tla b/tla/ccfraft.tla index 9b139f8e7089..7f48fd93de18 100644 --- a/tla/ccfraft.tla +++ b/tla/ccfraft.tla @@ -1364,6 +1364,13 @@ PendingBecomesFollowerProp == s \in GetServerSet(s)' => state[s]' = Follower]_vars +\* Raft Paper section 5.4.2: "[A leader] never commits log entries from previous terms...". +NeverCommitEntryPrevTermsProp == + [][\A i \in { s \in Servers : state[s] = Leader }: + \* If the commitIndex of a leader changes, the log entry's term that the new commitIndex + \* points to equals the leader's term. + commitIndex'[i] > commitIndex[i] => log[i][commitIndex'[i]].term = currentTerm'[i] ]_vars + LogMatchingProp == \A i, j \in Servers : []<>(log[i] = log[j])