feat(raft-log-replication): raft_on_append_entries_reply (tasks 7.1, 7.2)

HandleAppendEntriesResponse (raft.tla:393): stale-term drop first (applied only
when reply_term==s->term, raft.tla:415, Req 5.4 — both lower and higher dropped);
success -> next_index[peer]=match_index+1, match_index[peer]=match_index (Req
5.1-5.2); failure -> next_index[peer]=Max(next-1,1) floored, match_index unchanged
(Req 5.3); no commit advance. uint64 underflow blocked by the >1 floor guard.
3 tests incl. floor-at-1 and lower/higher stale. ASAN green.
This commit is contained in:
Rongsong Shen 2026-06-21 16:26:42 +00:00
parent 3c5185a5c3
commit eeb95591ae
3 changed files with 144 additions and 2 deletions

View file

@ -677,3 +677,35 @@ int raft_on_append_entries_request(raft_state_t *s, int leader_idx,
return RAFT_OK;
}
}
int raft_on_append_entries_reply(raft_state_t *s, int peer_idx, int success,
uint64_t match_index, uint64_t reply_term)
{
/* ---- Stale-term drop FIRST (raft.tla HandleAppendEntriesResponse 415, Req 5.4) ----
* The response is meaningful only if it pertains to the leader's current
* term (m.mterm == currentTerm[i]). A reply carrying any other term — from
* an old in-flight RPC or a future leader — is discarded with no state
* change. No commit index is ever advanced here (Req 5.4; owned by
* raft-commit-safety). */
if (reply_term != s->term)
return RAFT_OK;
if (success) {
/* success (raft.tla 397, Req 5.2): nextIndex'[peer] = m.mmatchIndex + 1,
* matchIndex'[peer] = m.mmatchIndex. */
s->match_index[peer_idx] = match_index;
s->next_index[peer_idx] = match_index + 1;
} else {
/* failure (raft.tla 401, Req 5.3): nextIndex'[peer] =
* Max(nextIndex[peer] - 1, 1) — back off one index, floored at 1.
* matchIndex is left unchanged. */
uint64_t next = s->next_index[peer_idx];
s->next_index[peer_idx] = (next > 1) ? (next - 1) : 1;
}
if (s->cbs->on_trace)
s->cbs->on_trace(s->ctx, success ? "ae_reply_success" : "ae_reply_fail",
NULL);
return RAFT_OK;
}