feat(raft-sim-conformance): Leader Completeness invariant checker (task 3.3)
This commit is contained in:
parent
d9b5fd51e0
commit
63a9740c85
4 changed files with 143 additions and 1 deletions
|
|
@ -790,6 +790,29 @@ int raft_sim_check_log_matching(const raft_sim_cluster_t *c);
|
|||
*/
|
||||
int raft_sim_check_election_safety(const raft_sim_cluster_t *c);
|
||||
|
||||
/*
|
||||
* raft_sim_check_leader_completeness: assert the Raft Leader Completeness property
|
||||
* over the cluster's observable per-node state (Req 3.3, 3.6).
|
||||
*
|
||||
* Leader Completeness: if an entry is committed in term t, then that entry is
|
||||
* present (same index, same term) in the logs of all leaders of terms > t.
|
||||
*
|
||||
* Computed purely from observable state (Req 3.6): the committed set is every
|
||||
* index k in 1..node->commit_index for each node (carrying that node's
|
||||
* log[k-1].term — the per-node mirror filled by on_commit_advanced); the current
|
||||
* leaders are the nodes with role == RAFT_LEADER (read via raft_snapshot). For
|
||||
* each leader L at term T_L and each committed entry (k, t) with t < T_L, L's log
|
||||
* MUST contain index k at term t; otherwise the property is violated. Presence is
|
||||
* keyed on (index, term) — Log Matching covers payload identity.
|
||||
*
|
||||
* Returns 1 if Leader Completeness holds across the whole cluster, 0 if any
|
||||
* higher-term leader is missing (or carries a different term for) a lower-term
|
||||
* committed entry. Pure read-only over c (no I/O, no Unity assertions) so the lib
|
||||
* stays test-framework-agnostic; the caller asserts on the returned value (same
|
||||
* convention as raft_sim_check_log_matching).
|
||||
*/
|
||||
int raft_sim_check_leader_completeness(const raft_sim_cluster_t *c);
|
||||
|
||||
/*
|
||||
* raft_sim_advance_commit: drive raft_advance_commit on node_idx (task 6.1).
|
||||
*
|
||||
|
|
|
|||
|
|
@ -839,6 +839,49 @@ int raft_sim_check_election_safety(const raft_sim_cluster_t *c)
|
|||
return 1; /* holds */
|
||||
}
|
||||
|
||||
int raft_sim_check_leader_completeness(const raft_sim_cluster_t *c)
|
||||
{
|
||||
/* Leader Completeness: an entry committed in term t must be present (same
|
||||
* index, same term) in the log of every leader of a strictly-higher term.
|
||||
*
|
||||
* Pure per-snapshot observer (Req 3.6): the committed set is every index k in
|
||||
* 1..commit_index over ALL nodes (carrying that node's log[k-1].term); the
|
||||
* current leaders are the role==RAFT_LEADER nodes. For each leader L at term
|
||||
* T_L and each committed (k, t) with t < T_L, L's log must hold index k at
|
||||
* term t — else the property is violated. (index, term) presence suffices;
|
||||
* Log Matching covers payload identity. */
|
||||
for (int L = 0; L < c->n; L++) {
|
||||
raft_snapshot_t sl;
|
||||
raft_snapshot(&c->nodes[L].state, &sl);
|
||||
if (sl.role != RAFT_LEADER)
|
||||
continue;
|
||||
|
||||
const raft_sim_node_t *leader = &c->nodes[L];
|
||||
|
||||
/* Scan every node's committed prefix for entries committed under a term
|
||||
* strictly lower than this leader's term. */
|
||||
for (int d = 0; d < c->n; d++) {
|
||||
const raft_sim_node_t *src = &c->nodes[d];
|
||||
int committed = (int)src->commit_index;
|
||||
if (committed > src->log_count)
|
||||
committed = src->log_count;
|
||||
|
||||
for (int k = 1; k <= committed; k++) {
|
||||
uint64_t t = src->log[k - 1].term;
|
||||
if (t >= sl.term)
|
||||
continue; /* only lower-term committed entries bind */
|
||||
|
||||
/* Leader L must contain index k at term t. */
|
||||
if (k > leader->log_count)
|
||||
return 0; /* leader missing the committed index */
|
||||
if (leader->log[k - 1].term != t)
|
||||
return 0; /* leader has a different term at index k */
|
||||
}
|
||||
}
|
||||
}
|
||||
return 1; /* holds */
|
||||
}
|
||||
|
||||
int raft_sim_restart_node(raft_sim_cluster_t *c, int node_idx)
|
||||
{
|
||||
if (node_idx < 0 || node_idx >= c->n)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue