From 35f44e5fcb7e18965d96c913bfdfbd5c7f4d0905 Mon Sep 17 00:00:00 2001 From: Amaury Chamayou Date: Mon, 8 Jan 2024 15:59:49 +0000 Subject: [PATCH] Fix LogConfigurationConsistentInv to account for joining nodes --- tla/consensus/ccfraft.tla | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla index 0f857388e6d4..d05e0ca720a5 100644 --- a/tla/consensus/ccfraft.tla +++ b/tla/consensus/ccfraft.tla @@ -550,6 +550,7 @@ AppendEntries(i, j) == \* No messages to itself and sender is primary /\ state[i] = Leader /\ i /= j + /\ j \in GetServerSet(i) \* AppendEntries must be sent for historical entries, unless \* snapshots are used. Whether the node is in configuration at \* that index makes no difference. @@ -1222,13 +1223,18 @@ MonoLogInv == LogConfigurationConsistentInv == \A i \in Servers : \/ state[i] = None + \* Follower, but no known configurations yet + \/ /\ state[i] = Follower + /\ Cardinality(DOMAIN configurations[i]) = 0 \/ \* Configurations should have associated reconfiguration txs in the log /\ \A idx \in DOMAIN (configurations[i]) : /\ log[i][idx].contentType = TypeReconfiguration /\ log[i][idx].configuration = configurations[i][idx] - \* Current configuration should be committed - /\ commitIndex[i] >= CurrentConfigurationIndex(i) + \* Current configuration should be committed if there is one + \* but a configuration may not be committable yet. + \* /\ Cardinality(DOMAIN configurations[i]) > 0 + \* => commitIndex[i] >= CurrentConfigurationIndex(i) \* Pending configurations should not be committed yet /\ Cardinality(DOMAIN configurations[i]) > 1 => commitIndex[i] < NextConfigurationIndex(i)