diff --git a/tests/e2e_batched.py b/tests/e2e_batched.py index 3e48af7734ae..0fd8870be5a9 100644 --- a/tests/e2e_batched.py +++ b/tests/e2e_batched.py @@ -17,7 +17,6 @@ @reqs.description("Running batch submission of new entries") -@reqs.supports_methods("/app/batch/submit", "/app/batch/fetch") def test(network, args, batch_size=100, write_key_divisor=1, write_size_multiplier=1): LOG.info(f"Number of batched entries: {batch_size}") primary, _ = network.find_primary() diff --git a/tests/raft_scenarios/5879_deprecated b/tests/raft_scenarios/5879_deprecated new file mode 100644 index 000000000000..360965332335 --- /dev/null +++ b/tests/raft_scenarios/5879_deprecated @@ -0,0 +1,65 @@ +nodes,0,1 +connect,0,1 + +# Node 0 starts first, and begins sending messages first +periodic_one,0,110 +dispatch_all + +periodic_all,30 +dispatch_all + +state_all +assert_is_primary,0 +assert_is_backup,1 + +## ... with the same logs upto index 7. +replicate,1,txAtIdx1 +replicate,1,txAtIdx2 +replicate,1,txAtIdx3 +replicate,1,txAtIdx4 +replicate,1,txAtIdx5 +replicate,1,txAtIdx6 +emit_signature,1 +periodic_all,30 +dispatch_all + +assert_commit_idx,0,7 +assert_commit_idx,1,0 + +periodic_all,30 +dispatch_all +assert_state_sync + +assert_commit_idx,0,7 +assert_commit_idx,1,7 + +## At index 8, the leader n2 reconfigures to remove n1. +replicate_new_configuration,1,0 + +periodic_all,30 +dispatch_all + +state_all +assert_is_primary,0 +assert_is_backup,1 +## Index 9 is a signature, index 10 some random transaction and index 11 is a signature. +emit_signature,1 +assert_commit_idx,0,7 + +replicate,1,txAt10 +assert_commit_idx,0,7 + +emit_signature,1 +assert_commit_idx,0,7 + + +## When the ACI action taken by n2, it should be able to commit index 11 but instead it will commit index 9. +periodic_all,30 +dispatch_all + +assert_is_primary,0 +assert_is_backup,1 +assert_is_retired,1 + +assert_commit_idx,0,11 +assert_commit_idx,1,7 diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla index d9692f15feaf..566cca9efe25 100644 --- a/tla/consensus/ccfraft.tla +++ b/tla/consensus/ccfraft.tla @@ -669,38 +669,47 @@ ChangeConfiguration(i) == AdvanceCommitIndex(i) == /\ state[i] = Leader /\ LET - \* We want to get the smallest such index forward that is a signature - \* This index must be from the current term, - \* as explained by Figure 8 and Section 5.4.2 of https://raft.github.io/raft.pdf - \* See find_highest_possible_committable_index in raft.h - new_index == SelectInSubSeq(log[i], commitIndex[i]+1, Len(log[i]), - LAMBDA e : e.contentType = TypeSignature /\ e.term = currentTerm[i]) - new_log == - IF new_index > 1 THEN - [ j \in 1..new_index |-> log[i][j] ] - ELSE - << >> - new_config_index == LastConfigurationToIndex(i, new_index) - new_configurations == RestrictDomain(configurations[i], LAMBDA c : c >= new_config_index) + \* Select those configs that need to have a quorum to agree on this leader. + \* Compare https://github.com/microsoft/CCF/blob/75670480c53519fcec1a09d36aefc11b23a597f9/src/consensus/aft/raft.h#L2081 + HasConsensusWatermark(idx) == + \A config \in {c \in DOMAIN(configurations[i]) : idx >= c } : + \* In all of these configs, we now need a quorum in the servers that have the correct matchIndex + LET config_servers == configurations[i][config] + required_quorum == Quorums[config_servers] + agree_servers == {k \in config_servers : matchIndex[i][k] >= idx} + IN (IF i \in config_servers THEN {i} ELSE {}) \cup agree_servers \in required_quorum + \* The function find_highest_possible_committable_index in raft.h returns the largest committable index + \* in the current term (Figure 8 and Section 5.4.2 of https://raft.github.io/raft.pdf explains why it has + \* to be the *current* term). Finding the largest index is an (implementation-level) optimization that + \* reduces the number of AdvanceCommitIndex calls, but this optimization also shrinks this spec's state-space. + \* + \* Theoretically, any committable index in the current term works, i.e., highestCommittableIndex could be + \* defined non-deterministically as: + \* \E idx \in { j \in (commitIndex[i]+1)..Len(log[i]) : /\ log[i][j].term = currentTerm[i] + \* /\ log[i][j].contentType = TypeSignature } + \* /\ HasConsensusWatermark(idx) + \* /\ ... + \* + \* Max({0} \cup {...}) to default to 0 if no committable index is found. + highestCommittableIndex == Max({0} \cup { j \in (commitIndex[i]+1)..Len(log[i]) : + /\ log[i][j].term = currentTerm[i] + /\ log[i][j].contentType = TypeSignature + /\ HasConsensusWatermark(j) }) IN - /\ \* Select those configs that need to have a quorum to agree on this leader - \A config \in {c \in DOMAIN(configurations[i]) : new_index >= c } : - \* In all of these configs, we now need a quorum in the servers that have the correct matchIndex - LET config_servers == configurations[i][config] - required_quorum == Quorums[config_servers] - agree_servers == {k \in config_servers : matchIndex[i][k] >= new_index} - IN (IF i \in config_servers THEN {i} ELSE {}) \cup agree_servers \in required_quorum - \* only advance if necessary (this is basically a sanity check after the Min above) - /\ commitIndex[i] < new_index - /\ commitIndex' = [commitIndex EXCEPT ![i] = new_index] + \* only advance if necessary (this is basically a sanity) + /\ commitIndex[i] < highestCommittableIndex + /\ commitIndex' = [commitIndex EXCEPT ![i] = highestCommittableIndex] /\ committableIndices' = [ committableIndices EXCEPT ![i] = @ \ 0..commitIndex'[i] ] \* If commit index surpasses the next configuration, pop configs, and retire as leader if removed /\ IF /\ Cardinality(DOMAIN configurations[i]) > 1 - /\ new_index >= NextConfigurationIndex(i) + /\ highestCommittableIndex >= NextConfigurationIndex(i) THEN + LET new_configurations == RestrictDomain(configurations[i], + LAMBDA c : c >= LastConfigurationToIndex(i, highestCommittableIndex)) + IN /\ configurations' = [configurations EXCEPT ![i] = new_configurations] \* Retire if i is not in active configuration anymore - /\ IF i \notin configurations[i][Min(DOMAIN new_configurations)] + /\ IF i \notin configurations[i][Min(DOMAIN configurations'[i])] THEN \E j \in PlausibleSucessorNodes(i) : /\ state' = [state EXCEPT ![i] = RetiredLeader] /\ LET msg == [type |-> ProposeVoteRequest,