tla: block campaigns with unapplied config changes

[bug-catcher]

Problem

The TLA+ spec currently allows a server to start a campaign even when its log contains committed but unapplied config change entries. The Go implementation does not allow this. In hup(), raft checks hasUnappliedConfChanges() and abandons the campaign if such entries exist.

This matters because a server counts votes using its active config, and that config only advances when config entries are applied. Without the guard, the spec can let a candidate use a config that is more than one version behind the committed config. That breaks the quorum overlap argument between concurrent candidates.

TLC confirms the issue. With reconfigs {1,2,3} -> +4 -> +5 committed, s2, which has applied both changes, can win term 2 with {2,4,5}. At the same time, s3, which has applied neither change, can also win term 2 with {1,3}. This violates MoreThanOneLeaderInv.

The full schedule is in #456. Credit to the reporter for the counterexample driver.

Fix

This change adds appliedConfChangeIndex[i] to track the latest config change entry each server has applied. It is part of configVars, advances in ApplySimpleConfChange, and is persisted and restored together with config.

Timeout(i) now checks ~HasUnappliedConfChange(i) before allowing a campaign, matching the behavior of hup() in the Go implementation.

The bootstrap initializers in MCetcdraft and Traceetcdraft also mark bootstrap config entries as already applied.

Regression test

tla/SplitBrain456.tla replays the schedule from #456. It runs in about 3 seconds with TLC.

The test checks MoreThanOneLeaderInv and also includes a temporal sanity property that confirms the schedule reaches the point where the final campaign is now blocked. That keeps the test from passing vacuously.

The scenario fails on the parent commit and passes with this change.

Verification

SplitBrain456 is red before this change and green after it, with 82 states before and 71 states after.

A bounded MCetcdraft run reports no violations. Full exhaustive checking does not reach the roughly depth 80 counterexample, which is why this bug was not found by model checking.

Trace validation of tla/example.ndjson against the updated spec passes. This means the new guard does not reject behavior produced by the real implementation.

Why this was missed

Trace validation checks that implementation traces are allowed by the spec. That catches cases where the spec is too restrictive.

This bug was the opposite: the implementation was more restrictive than the spec. As a result, implementation traces still validated successfully.

[kubernetes-prow]

[APPROVALNOTIFIER] This PR is NOT APPROVED

This pull-request has been approved by: bug-catcher
Once this PR has been reviewed and has the lgtm label, please assign spzala for approval. For more information see the Code Review Process.

The full list of commands accepted by this bot can be found here.

Details

Needs approval from an approver in each of these files:

• OWNERS

Approvers can indicate their approval by writing /approve in a comment
Approvers can cancel approval by writing /approve cancel in a comment

[kubernetes-prow]

Hi @bug-catcher. Thanks for your PR.

I'm waiting for a etcd-io member to verify that this patch is reasonable to test. If it is, they should reply with /ok-to-test on its own line. Until that is done, I will not automatically test new commits in this PR, but the usual testing commands by org members will still work.

Regular contributors should join the org to skip this step.

Once the patch is verified, the new status will be reflected by the ok-to-test label.

I understand the commands that are listed here.

Details

Instructions for interacting with me using PR comments are available here. If you have questions or suggestions related to my behavior, please file an issue against the kubernetes-sigs/prow repository.