forked from lei.chen/myxce
feat(raft-commit-safety): (lastLogTerm,lastLogIndex) vote+prevote freshness (tasks 1.3, 4.1-4.2, 5.1-5.2, 6.2)
logOk (raft.tla:285, closes G6): local_last_log_term = log_len>0 ? on_get_entry_term(log_len):0; logOk = cand_last_log_term > local || (== && cand_last_log_index >= log_len). Lexicographic: term dominates, tie decided by index. Shared raft_log_ok helper. Vote (4.2): logOk deny inserted after stale-term/UpdateTerm/role-gate/one-vote-per-term and BEFORE on_vote_eligible (denies even when the app gate would grant); persist-before-grant intact. PreVote (5.2): identical logOk, fully side-effect-free (no term/vote/role/commit mutation, no on_persist). Signatures extended (1.3) on raft_on_vote_request/pre_vote_request; all 39 lib call sites + sim routing updated; sim captures the candidate's send-time last-log tuple (raft_sim_rpc_t). Empty-log call sites pass (0,0) → logOk true → existing outcomes preserved. 9 freshness tests. NOTE: controller cluster.c vote callers still use the old signatures and will NOT compile — an accepted, design-documented revalidation trigger; the controller adapter plumbing is owned by the downstream ha-term-safety spec (to be implemented next). Library suite ASAN green (239 tests).
This commit is contained in:
parent
195f660f9a
commit
56485e2fa3
5 changed files with 449 additions and 62 deletions
|
|
@ -23,7 +23,7 @@
|
|||
- _Boundary: raft.h_
|
||||
- _Depends: 1.1_
|
||||
|
||||
- [ ] 1.3 Declare `raft_advance_commit` and extend the vote/PreVote signatures with last_log_term/last_log_index
|
||||
- [x] 1.3 Declare `raft_advance_commit` and extend the vote/PreVote signatures with last_log_term/last_log_index
|
||||
- Declare `int raft_advance_commit(raft_state_t *s)`
|
||||
- Extend `raft_on_vote_request` and `raft_on_pre_vote_request` to accept `cand_last_log_term` and `cand_last_log_index` (the chosen "library owns logOk" plumbing — Option B in design.md)
|
||||
- Update the header doc comments to describe the new logOk gate and the commit-advance action
|
||||
|
|
@ -74,7 +74,7 @@
|
|||
|
||||
## 4. (lastLogTerm, lastLogIndex) vote freshness (raft.tla:285, closes G6)
|
||||
|
||||
- [ ] 4.1 RED: binding-vote freshness tests
|
||||
- [x] 4.1 RED: binding-vote freshness tests
|
||||
- Test: candidate with stale `last_log_term` denied even when `last_log_index` is greater; candidate with fresher `last_log_term` granted with a smaller `last_log_index`; tie on term grants only when `cand_last_log_index >= log_len`; the voter's own last-log term/index come from `on_get_entry_term(log_len)`/`log_len` (term 0 when empty)
|
||||
- Test: `!logOk` denies even when `on_vote_eligible` would grant (logOk applied BEFORE the application gate); persist-before-grant unchanged on the grant path
|
||||
- Observable completion: tests compile and FAIL
|
||||
|
|
@ -82,7 +82,7 @@
|
|||
- _Boundary: test_raft.c_
|
||||
- _Depends: 1.3_
|
||||
|
||||
- [ ] 4.2 GREEN: implement the logOk gate in `raft_on_vote_request`
|
||||
- [x] 4.2 GREEN: implement the logOk gate in `raft_on_vote_request`
|
||||
- Compute `local_last_log_term = (log_len > 0) ? on_get_entry_term(log_len) : 0`; `logOk = (cand_last_log_term > local_last_log_term) || (cand_last_log_term == local_last_log_term && cand_last_log_index >= log_len)`
|
||||
- Insert the logOk deny BEFORE `on_vote_eligible`, after the existing stale-term/UpdateTerm/one-vote-per-term steps; leave persist-before-grant and all existing invariants in place
|
||||
- Observable completion: 4.1 tests pass; no regression in existing vote tests; the logOk block is clearly before `on_vote_eligible` in `raft.c`
|
||||
|
|
@ -92,7 +92,7 @@
|
|||
|
||||
## 5. (lastLogTerm, lastLogIndex) PreVote freshness (raft.tla:285, side-effect-free)
|
||||
|
||||
- [ ] 5.1 RED: PreVote freshness tests (identical rule, no side effects)
|
||||
- [x] 5.1 RED: PreVote freshness tests (identical rule, no side effects)
|
||||
- Test: `raft_on_pre_vote_request` applies the SAME `(lastLogTerm, lastLogIndex)` logOk as the binding vote; a stale tuple is denied; the existing stale-term deny and `on_vote_eligible` gate remain in force
|
||||
- Test: across grant and deny, no mutation of `term`/`voted_for`/`voted_for_term`/`role`/`commit_index` and no `on_persist` call (PreVote invariant)
|
||||
- Observable completion: tests compile and FAIL
|
||||
|
|
@ -100,7 +100,7 @@
|
|||
- _Boundary: test_raft.c_
|
||||
- _Depends: 1.3_
|
||||
|
||||
- [ ] 5.2 GREEN: implement the logOk gate in `raft_on_pre_vote_request`
|
||||
- [x] 5.2 GREEN: implement the logOk gate in `raft_on_pre_vote_request`
|
||||
- Apply the identical logOk predicate (factored to match 4.2) before/with the existing eligibility gate; mutate nothing; no `on_persist`
|
||||
- Observable completion: 5.1 tests pass; no regression in existing PreVote tests; the predicate matches the binding-vote path exactly
|
||||
- _Requirements: 4.1, 4.2, 4.3, 4.4, 4.5_
|
||||
|
|
@ -118,7 +118,7 @@
|
|||
- _Boundary: raft_sim.c_
|
||||
- _Depends: 3.2_
|
||||
|
||||
- [ ] 6.2 Plumb `(last_log_term, last_log_index)` through the sim vote/PreVote routing
|
||||
- [x] 6.2 Plumb `(last_log_term, last_log_index)` through the sim vote/PreVote routing
|
||||
- Update the sim's vote and PreVote delivery to read the candidate's last-log `(term, index)` from its in-memory log (`term at log_len` / `log_len`) and pass them to the extended `raft_on_vote_request` / `raft_on_pre_vote_request`
|
||||
- Observable completion: existing election sim tests still pass with the extended signatures; a node with a stale last-log term is denied a vote it would previously have won on LSN alone
|
||||
- _Requirements: 6.5, 3.2, 4.2_
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue