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

feat(raft-log-replication): raft_send_append_entries AppendEntries emit (tasks 4.1, 4.2)

Browse source 
Leader-only emit (raft.tla AppendEntries:204, Req 3.5 — no-op off leader);
prev_log_index=next_index[j]-1, prev_log_term via on_get_entry_term (0/unqueried
at index 0, Req 3.2-3.3); n_entries=1 when next_index[j]<=log_len else 0 heartbeat
(Req 3.4); leader_commit opaque passthrough. Trace fires only on successful send
(consistency with raft_log_append) and non-leader RAFT_OK asserted — both from
review. 4 spy-based tests. ASAN green.
This commit is contained in:
Rongsong Shen 2026-06-21 16:01:17 +00:00
parent e5b9b83955
commit a1aacc0389
3 changed files with 247 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
.kiro/specs/raft-log-replication/tasks.md
View file

@ -65,14 +65,14 @@
## 4. AppendEntries emission — raft_send_append_entries (raft.tla:204)
- [ ] 4.1 RED: emit tests (prevLogIndex/prevLogTerm, ≤1 entry, leader-only)
- [x] 4.1 RED: emit tests (prevLogIndex/prevLogTerm, ≤1 entry, leader-only)
- Test: for peer `j`, emit computes `prevLogIndex = next_index[j]-1` and `prevLogTerm` via `on_get_entry_term` (0 when `prevLogIndex==0`), sends ≤1 entry, passes `leader_commit` through opaquely; a non-leader emits nothing
- Observable completion: tests compile and FAIL
- _Requirements: 3.2, 3.3, 3.4, 3.5_
- _Boundary: test_raft.c_
- _Depends: 2.2_
- [ ] 4.2 GREEN: implement `raft_send_append_entries`
- [x] 4.2 GREEN: implement `raft_send_append_entries`
- Compute prev index/term; `lastEntry = Min(log_len, next_index[j])`; one entry or heartbeat; call `on_send_append_entries` with the opaque `leader_commit`; leader-only guard
- Observable completion: 4.1 tests pass; heartbeat (0 entries) emitted when `next_index[j] > log_len`
- _Requirements: 3.2, 3.3, 3.4, 3.5_