lei.chen/myxce
1
0
Fork 1
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(raft-commit-safety): raft_advance_commit Figure-8 current-term rule (tasks 3.1-3.3, 6.1)

Browse source 
AdvanceCommitIndex (raft.tla:259/270, closes G4): leader-only (-EPERM); Max(agreeIndexes)
= highest N with a quorum ((n_peers/2)+1) of match_index>=N, self counted as log_len;
scan log_len downward. CURRENT-TERM RULE: advance commit_index to N only when
on_get_entry_term(N)==s->term, else HOLD (Figure-8 safety — never commit a previous-term
entry on replication count alone; a later current-term commit indirectly commits it).
Monotonic; fires on_commit_advanced once per strict advance; commit_index<=log_len.

3.3: raft_on_append_entries_reply left untouched — verified it never advances commit
(separation, Req 2.6). 6.1: sim commit-driver helper raft_sim_advance_commit added.

Req 6.3 two-phase indirect-commit transition covered end-to-end by task 7.1 (sim).
ASAN green (230 tests).
This commit is contained in:
Rongsong Shen 2026-06-21 23:27:12 +00:00
parent 3ba6f03a9e
commit 195f660f9a
5 changed files with 350 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
.kiro/specs/raft-commit-safety/tasks.md
View file

@ -44,7 +44,7 @@
## 3. AdvanceCommitIndex with the current-term Figure-8 rule (raft.tla:259/270, closes G4)
- [ ] 3.1 RED: commit-advance tests (current-term advance, Figure-8 hold, monotonic, non-leader)
- [x] 3.1 RED: commit-advance tests (current-term advance, Figure-8 hold, monotonic, non-leader)
- Test (advance): leader with `match_index[]` quorum-agreeing through index `k`, entry at `k` from `currentTerm` → `commit_index` advances to `k`, `on_commit_advanced(k)` fired once
- Test (Figure-8 hold): quorum agrees through a previous-term entry at `k` with no current-term entry above → `commit_index` unchanged, `on_commit_advanced` NOT fired
- Test (empty agreeIndexes): no index reaches quorum → unchanged, no callback
@ -55,7 +55,7 @@
- _Boundary: test_raft.c_
- _Depends: 2.1_
- [ ] 3.2 GREEN: implement `raft_advance_commit`
- [x] 3.2 GREEN: implement `raft_advance_commit`
- Leader-only guard (`-EPERM` otherwise); compute `Max(agreeIndexes)` by scanning candidate indexes from `log_len` downward, seeding the agree-count with self, until a quorum `((n_peers/2)+1)` is reached
- Apply the current-term rule: advance to `Max(agreeIndexes)` only when `on_get_entry_term(Max) == s->term`; else hold
- Monotonic: only ever move `commit_index` forward; fire `on_commit_advanced(commit_index)` exactly once on a strict advance; read entry terms only via `on_get_entry_term`
@ -64,7 +64,7 @@
- _Boundary: raft.c_
- _Depends: 3.1_
- [ ] 3.3 RED+GREEN: commit-advance is a separate action from append-entries reply
- [x] 3.3 RED+GREEN: commit-advance is a separate action from append-entries reply
- Test: a `raft_on_append_entries_reply` that updates `match_index[]` to a committable quorum does NOT by itself change `commit_index` or fire `on_commit_advanced`; only a subsequent `raft_advance_commit` does
- Verify (no implementation change expected in `raft_on_append_entries_reply` — it is owned upstream and must stay untouched); if a regression is found, the fix belongs upstream, not here
- Observable completion: test passes; `raft_on_append_entries_reply` remains free of any commit-advance side effect
@ -109,7 +109,7 @@
## 6. Simulator backing: commit-advance driver + freshness plumbing
- [ ] 6.1 Wire `on_commit_advanced` and a commit-advance driver in `raft_sim.c`
- [x] 6.1 Wire `on_commit_advanced` and a commit-advance driver in `raft_sim.c`
- Add a per-`raft_sim_node_t` `commit_index` mirror updated from `on_commit_advanced`; implement the callback (record the value + count fires for assertions)
- Add a sim helper to drive `raft_advance_commit` on a given node (or all leaders) after delivery
- Pass each node's restored `initial_commit_index` (default 0) in `raft_sim_init`; wire `on_commit_advanced` for every node