feat(raft-log-replication): Log Matching assertion helper (task 8.3)
raft_sim_check_log_matching: for every node pair and every shared index i, if both entries at i have equal term, assert the whole prefix 1..i is term-and-byte identical (Req 8.4, raft.tla Log Matching). Read-only, framework-agnostic (returns 1/0), bounded. Self-tests: pass on a converged cluster, fail on a hand-divergent pair sharing (i=2,term=7) but differing at the index-1 prefix. ASAN green.
This commit is contained in:
parent
0e8c6ed05a
commit
6ff07e5843
4 changed files with 152 additions and 1 deletions
|
|
@ -498,6 +498,21 @@ void raft_sim_fire_timeout(raft_sim_cluster_t *c, int node_idx);
|
|||
*/
|
||||
void raft_sim_partition(raft_sim_cluster_t *c, int node_idx, int isolated);
|
||||
|
||||
/*
|
||||
* raft_sim_check_log_matching: assert the Raft Log Matching property over the
|
||||
* cluster's in-memory logs (Req 8.4).
|
||||
*
|
||||
* For every pair of nodes (a, b) and every index i present in BOTH logs
|
||||
* (1 <= i <= min(log_count_a, log_count_b)), if the entries at i carry the
|
||||
* SAME term, then the logs must be identical for all indices 1..i — same term
|
||||
* AND same payload (length + bytes) at every k in 1..i.
|
||||
*
|
||||
* Returns 1 if Log Matching holds across the whole cluster, 0 if any pair/index
|
||||
* violates it. 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.
|
||||
*/
|
||||
int raft_sim_check_log_matching(const raft_sim_cluster_t *c);
|
||||
|
||||
#endif /* XCE_TESTING */
|
||||
|
||||
#endif /* RAFT_H */
|
||||
|
|
|
|||
|
|
@ -373,4 +373,44 @@ void raft_sim_partition(raft_sim_cluster_t *c, int node_idx, int isolated)
|
|||
c->nodes[node_idx].partition = isolated;
|
||||
}
|
||||
|
||||
/* Two log entries are identical iff their term, length, and payload bytes
|
||||
* (over the recorded length) all match. */
|
||||
static int sim_entry_identical(const raft_sim_entry_t *a,
|
||||
const raft_sim_entry_t *b)
|
||||
{
|
||||
if (a->term != b->term || a->len != b->len)
|
||||
return 0;
|
||||
return memcmp(a->bytes, b->bytes, a->len) == 0;
|
||||
}
|
||||
|
||||
int raft_sim_check_log_matching(const raft_sim_cluster_t *c)
|
||||
{
|
||||
/* For every ordered-pair-free pair (a < b) and every index i present in
|
||||
* both logs: if the entries at i carry the same term, the prefixes 1..i
|
||||
* must be entry-identical. Pairs are symmetric, so a < b suffices. */
|
||||
for (int a = 0; a < c->n; a++) {
|
||||
const raft_sim_node_t *na = &c->nodes[a];
|
||||
for (int b = a + 1; b < c->n; b++) {
|
||||
const raft_sim_node_t *nb = &c->nodes[b];
|
||||
|
||||
int shared = na->log_count < nb->log_count
|
||||
? na->log_count : nb->log_count;
|
||||
|
||||
for (int i = 1; i <= shared; i++) {
|
||||
const raft_sim_entry_t *ea = &na->log[i - 1];
|
||||
const raft_sim_entry_t *eb = &nb->log[i - 1];
|
||||
|
||||
/* Same (index, term) ⇒ prefixes through i must be identical. */
|
||||
if (ea->term != eb->term)
|
||||
continue;
|
||||
for (int k = 1; k <= i; k++) {
|
||||
if (!sim_entry_identical(&na->log[k - 1], &nb->log[k - 1]))
|
||||
return 0; /* Log Matching violated */
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
return 1; /* holds */
|
||||
}
|
||||
|
||||
#endif /* XCE_TESTING */
|
||||
|
|
|
|||
|
|
@ -3100,6 +3100,100 @@ static void test_sim_deliver_append_entries_replicates(void)
|
|||
TEST_ASSERT_EQUAL_INT(0, c.nodes[2].log_count);
|
||||
}
|
||||
|
||||
/*
|
||||
* test_sim_check_log_matching_pass_on_converged (task 8.3)
|
||||
*
|
||||
* Log Matching helper must return PASS (1) when two nodes hold identical logs.
|
||||
* Build a 3-node cluster, elect node 0, append two entries, replicate both to
|
||||
* node 1; assert raft_sim_check_log_matching == 1 and node 1's prefix matches
|
||||
* node 0's byte-for-byte.
|
||||
*/
|
||||
static void test_sim_check_log_matching_pass_on_converged(void)
|
||||
{
|
||||
raft_sim_cluster_t c;
|
||||
memset(&c, 0, sizeof(c));
|
||||
|
||||
TEST_ASSERT_EQUAL_INT(0, raft_sim_init(&c, 3, 2000));
|
||||
|
||||
raft_start_election(&c.nodes[0].state);
|
||||
raft_sim_deliver_pending(&c);
|
||||
TEST_ASSERT_EQUAL_INT(RAFT_LEADER, c.nodes[0].state.role);
|
||||
|
||||
/* Append two client entries on the leader and replicate each to node 1.
|
||||
* One AppendEntries carries at most one entry, so replicate index by index. */
|
||||
unsigned char p1[3] = { 0x01, 0x02, 0x03 };
|
||||
unsigned char p2[3] = { 0x04, 0x05, 0x06 };
|
||||
uint64_t out_index = 0;
|
||||
|
||||
TEST_ASSERT_EQUAL_INT(RAFT_OK,
|
||||
raft_log_append(&c.nodes[0].state, p1, sizeof(p1), &out_index));
|
||||
TEST_ASSERT_EQUAL_UINT64(1, out_index);
|
||||
TEST_ASSERT_EQUAL_INT(RAFT_OK,
|
||||
raft_send_append_entries(&c.nodes[0].state, 1, /*leader_commit=*/0));
|
||||
raft_sim_deliver_append_entries(&c);
|
||||
|
||||
TEST_ASSERT_EQUAL_INT(RAFT_OK,
|
||||
raft_log_append(&c.nodes[0].state, p2, sizeof(p2), &out_index));
|
||||
TEST_ASSERT_EQUAL_UINT64(2, out_index);
|
||||
TEST_ASSERT_EQUAL_INT(RAFT_OK,
|
||||
raft_send_append_entries(&c.nodes[0].state, 1, /*leader_commit=*/0));
|
||||
raft_sim_deliver_append_entries(&c);
|
||||
|
||||
/* Node 1 holds the leader's prefix byte-for-byte. */
|
||||
TEST_ASSERT_EQUAL_INT(2, c.nodes[0].log_count);
|
||||
TEST_ASSERT_EQUAL_INT(2, c.nodes[1].log_count);
|
||||
|
||||
/* Log Matching holds across the cluster. */
|
||||
TEST_ASSERT_EQUAL_INT(1, raft_sim_check_log_matching(&c));
|
||||
}
|
||||
|
||||
/*
|
||||
* test_sim_check_log_matching_fail_on_divergence (task 8.3)
|
||||
*
|
||||
* Log Matching helper must return FAIL (0) when two nodes share the same
|
||||
* (index, term) at some i but their prefixes differ. Hand-craft node 0 and
|
||||
* node 1 so that index 2 carries the SAME term but index 1 differs in bytes —
|
||||
* a Log Matching violation (equal (i,term) but non-identical prefix through i).
|
||||
*/
|
||||
static void test_sim_check_log_matching_fail_on_divergence(void)
|
||||
{
|
||||
raft_sim_cluster_t c;
|
||||
memset(&c, 0, sizeof(c));
|
||||
|
||||
TEST_ASSERT_EQUAL_INT(0, raft_sim_init(&c, 3, 2000));
|
||||
|
||||
/* Hand-craft node 0: index1=(term 5, "AAA"), index2=(term 7, "XXX"). */
|
||||
c.nodes[0].log[0].term = 5;
|
||||
c.nodes[0].log[0].bytes[0] = 'A';
|
||||
c.nodes[0].log[0].bytes[1] = 'A';
|
||||
c.nodes[0].log[0].bytes[2] = 'A';
|
||||
c.nodes[0].log[0].len = 3;
|
||||
c.nodes[0].log[1].term = 7;
|
||||
c.nodes[0].log[1].bytes[0] = 'X';
|
||||
c.nodes[0].log[1].bytes[1] = 'X';
|
||||
c.nodes[0].log[1].bytes[2] = 'X';
|
||||
c.nodes[0].log[1].len = 3;
|
||||
c.nodes[0].log_count = 2;
|
||||
|
||||
/* Hand-craft node 1: SAME (index2, term 7) but a DIFFERENT index1 prefix
|
||||
* (term 5 but bytes "BBB"). This must be flagged: equal (i=2, term=7) yet
|
||||
* the prefix through 2 is not byte-identical. */
|
||||
c.nodes[1].log[0].term = 5;
|
||||
c.nodes[1].log[0].bytes[0] = 'B';
|
||||
c.nodes[1].log[0].bytes[1] = 'B';
|
||||
c.nodes[1].log[0].bytes[2] = 'B';
|
||||
c.nodes[1].log[0].len = 3;
|
||||
c.nodes[1].log[1].term = 7;
|
||||
c.nodes[1].log[1].bytes[0] = 'X';
|
||||
c.nodes[1].log[1].bytes[1] = 'X';
|
||||
c.nodes[1].log[1].bytes[2] = 'X';
|
||||
c.nodes[1].log[1].len = 3;
|
||||
c.nodes[1].log_count = 2;
|
||||
|
||||
/* Same (index2, term7) with divergent index1 ⇒ Log Matching violated. */
|
||||
TEST_ASSERT_EQUAL_INT(0, raft_sim_check_log_matching(&c));
|
||||
}
|
||||
|
||||
/* ---------- Group A: Basic Election Correctness (task 5.1) ---------- */
|
||||
|
||||
/*
|
||||
|
|
@ -5348,6 +5442,8 @@ void test_raft(void)
|
|||
RUN_TEST(test_sim_partition_no_quorum);
|
||||
RUN_TEST(test_sim_fire_timeout_steps_down);
|
||||
RUN_TEST(test_sim_deliver_append_entries_replicates);
|
||||
RUN_TEST(test_sim_check_log_matching_pass_on_converged);
|
||||
RUN_TEST(test_sim_check_log_matching_fail_on_divergence);
|
||||
|
||||
/* Group A: basic election correctness (task 5.1) */
|
||||
RUN_TEST(test_proto_A1_single_node_self_elects);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue