wdgzyjx/myxce
1
0
Fork 0
forked from lei.chen/myxce
Code Pull requests Activity
myxce/.kiro/specs/raft-sim-conformance/tasks.md

16 KiB
Raw Blame History

Implementation Plan

TDD-mandatory (testing.md): every checker, scheduler action, and scenario lands as a RED test in src/lib/testsuite/test_raft.c (with the raft_sim.c backing) that fails before the harness logic exists and passes after. Build/run library tests via /xce-build lib. All harness code is XCE_TESTING-gated.

Spec boundary (applies to ALL tasks): this spec owns src/lib/raft/raft_sim.c, the XCE_TESTING sim section of src/lib/raft/raft.h, and the conformance tests in src/lib/testsuite/test_raft.c ONLY. It does NOT modify the protocol implementation: no task changes raft.c protocol logic or any protocol declaration in raft.h, and no task edits a controller file. The harness drives the published library entry points and consumes the raft-log-replication + raft-commit-safety callback contract verbatim.

Depends (whole spec): raft-log-replication (log model + AppendEntries entry points

  • the four callbacks), raft-commit-safety (raft_advance_commit, on_commit_advanced, (lastLogTerm, lastLogIndex) freshness). If those signatures change, re-validate per the design's Revalidation Triggers.

1. Harness types and in-memory adapter backing

  • 1.1 Extend the XCE_TESTING sim section of raft.h with the harness data types

    • Add raft_sim_msg_kind_t, raft_sim_msg_t (vote/AE req+rsp union fields), raft_sim_log_entry_t {term, value}, raft_sim_action_t {kind, actor, msg_index, term, index}, and the RAFT_SIM_MAX_LOG/MSGS/STEPS bounds
    • Extend raft_sim_node_t with log[], log_len, commit_index, applied[], and a persisted-(term, votedFor) shadow for Restart; extend raft_sim_cluster_t with bag[]+bag_count, PRNG state, seed, and trace[]+trace_len
    • Observable completion: raft.h compiles under XCE_TESTING; no protocol declaration changed; sizeof(raft_sim_cluster_t) grows by the new fixed arrays
    • Requirements: 1.1, 1.3, 2.5
    • Boundary: raft.h (XCE_TESTING section only)

  • 1.2 Implement the seeded PRNG and the in-memory adapter callbacks

    • Add a small inlined deterministic generator (e.g. SplitMix64) seeded by cluster.seed; add on_persist_entry → node.log[], on_get_entry_term → term|0, on_truncate_from → shrink log_len, on_commit_advanced → set commit_index + apply into applied[]; route on_send_vote_request/on_send_append_entries to a bag push
    • Add raft_sim_conformance_init(c, n, timeout, seed) wiring all six callbacks + the bag
    • Observable completion: a test initializes a cluster, drives one raft_log_append on a forced leader, and reads the entry back via the in-memory log and on_get_entry_term
    • Requirements: 1.1, 1.2, 2.1
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 1.1

2. Message bag (mirrors raft.tla messages)

  • 2.1 RED+GREEN: bag push/deliver routes vote and AppendEntries RPCs through the library handlers

    • Test: pushing a vote-req and an AE-req then delivering them invokes raft_on_vote_request / raft_on_append_entries_request, and the handler reply is pushed back as a *_RSP message
    • Implement raft_sim_bag_push and raft_sim_bag_deliver(i) (route by kind, honor node.partition, push replies)
    • Observable completion: delivered requests produce matching responses in the bag; partitioned endpoints are not delivered
    • Requirements: 2.2, 2.4
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 1.2

  • 2.2 RED+GREEN: Drop / Duplicate / Reorder mutate only the bag

    • Test: raft_sim_bag_drop/_duplicate change bag multiplicity without mutating any node's term/role/log; reorder delivers in a PRNG-chosen order
    • Implement the three bag operations (mirroring raft.tla:443/448 UNCHANGED of non-message vars)
    • Observable completion: node snapshots are identical before/after a drop or duplicate of an undelivered message
    • Requirements: 2.5
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 2.1

3. The four invariant checkers (TDD against hand-built clusters)

  • 3.1 RED+GREEN: Election Safety checker (P)

    • Test: a cluster with two LEADER nodes at the same term fails; a single-leader-per-term cluster passes
    • Implement raft_sim_check_election_safety over roles+terms read from raft_snapshot
    • Observable completion: both directions assert correctly
    • Requirements: 3.1, 3.6
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 1.1

  • 3.2 RED+GREEN: Log Matching checker (P)

    • Test: two logs sharing (idx, term) but differing earlier fail; identical-prefix logs pass
    • Implement raft_sim_check_log_matching (pairwise; shared (idx, term) ⇒ identical 1..idx)
    • Observable completion: both directions assert correctly
    • Requirements: 3.2, 3.6
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 1.1

  • 3.3 RED+GREEN: Leader Completeness checker (P)

    • Test: a committed (index, term) absent from a higher-term leader's log fails; present passes
    • Implement raft_sim_check_leader_completeness using commit_index + per-node logs, tracking the highest-term leader to date
    • Observable completion: both directions assert correctly
    • Requirements: 3.3, 3.6
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 1.1

  • 3.4 RED+GREEN: State Machine Safety checker (P)

    • Test: divergent applied[k] across two nodes fails; identical applied prefixes pass
    • Implement raft_sim_check_state_machine_safety over applied[]
    • Observable completion: both directions assert correctly
    • Requirements: 3.4, 3.6
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 1.1

  • 3.5 RED+GREEN: raft_sim_check_all returns the first failing invariant and halts

    • Test: a cluster violating two invariants reports the first; a clean cluster returns OK
    • Implement raft_sim_check_all composing 3.1–3.4 in a fixed order
    • Observable completion: first-failure semantics verified
    • Requirements: 3.5
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 3.1, 3.2, 3.3, 3.4

4. Action scheduler and trace recorder

  • 4.1 RED+GREEN: trace recorder records every action before it is applied

    • Test: after a fixed step sequence, cluster.trace[] holds the actions in order; raft_sim_dump_trace prints seed, n, and the ordered actions
    • Implement raft_sim_action_t recording (R1.4) + raft_sim_dump_trace (R5.1, R5.2); quiet on success unless RAFT_SIM_VERBOSE (R5.4)
    • Observable completion: a recorded trace round-trips to a readable dump
    • Requirements: 1.4, 5.1, 5.2, 5.4
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 1.1

  • 4.2 RED+GREEN: raft_sim_step drives one Next-equivalent action through the library and checks invariants

    • Test: stepping reaches each enabled action kind over a run; every step calls raft_sim_check_all; a forced violation halts with a trace dump and a <0 return
    • Implement the seeded scheduler dispatch (Restart, Timeout, RequestVote/BecomeLeader via vote delivery, ClientRequest, AppendEntries via raft_send_append_entries, AdvanceCommitIndex via raft_advance_commit, Receive via bag deliver, Duplicate/Drop) selecting only enabled actions, driving only library entry points
    • Observable completion: a multi-step run touches log append, AE replication, commit advance, and message faults; invariants checked each step
    • Requirements: 2.1, 2.2, 2.3, 2.4, 2.6, 3.5
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 2.2, 3.5, 4.1

  • 4.3 RED+GREEN: Restart preserves persisted term/votedFor/log

    • Test: a Restart action re-inits a node while keeping node.log[], recovered log_len, and last-persisted (term, votedFor); volatile state resets per raft.tla Restart
    • Implement the Restart branch (feed initial_log_len + restored (term, votedFor) into raft_init)
    • Observable completion: a restarted node retains its log and term; no invariant violation results from the restart alone
    • Requirements: 2.1
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 4.2

  • 4.4 RED+GREEN: deterministic replay from (n, seed, max_steps)

    • Test: two runs with the same (n, seed, max_steps) reach identical final per-node + bag state and an identical recorded trace
    • Implement raft_sim_run(c, max_steps) and confirm no wall-clock/address/uninitialized input leaks into choices
    • Observable completion: byte-identical replay verified across two runs
    • Requirements: 1.5, 1.6, 5.3
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 4.2

5. Targeted adversarial scenarios

  • 5.1 Partition/heal scenario (P)

    • Implement raft_sim_scenario_partition_heal: isolate a minority during appends, heal, drain the bag; assert all four invariants throughout and after convergence
    • Observable completion: scenario passes with zero violations on the correct build
    • Requirements: 4.1
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 4.2

  • 5.2 Restart-churn scenario (P)

    • Implement raft_sim_scenario_restart_churn: restart nodes mid-replication preserving persisted state; assert re-convergence with no violation
    • Observable completion: scenario passes; restarted nodes converge to the leader's prefix
    • Requirements: 4.2
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 4.3

  • 5.3 Drop/duplicate/reorder scenario (P)

    • Implement raft_sim_scenario_drop_dup_reorder: perturb bag delivery order + multiplicity; assert idempotent convergence with all four invariants held
    • Observable completion: scenario passes; duplicated AE is a no-op (already-have branch)
    • Requirements: 4.3
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 4.2

  • 5.4 Figure-8 scenario

    • Implement raft_sim_scenario_figure8: a previous-term entry on a quorum, a leader change; assert the entry is NOT reported committed until a current-term entry commits (Leader Completeness / State Machine Safety preserved)
    • Observable completion: the previous-term entry's commit_index does not cover it until a current-term commit
    • Requirements: 4.4
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 4.2

  • 5.5 Stale-rejoin scenario (bug-851 G5)

    • Implement raft_sim_scenario_stale_rejoin: a term-lagging node rejoins under a higher-term leader; assert it adopts the higher term from the AE/heartbeat path and does not re-elect at a reused term (Election Safety preserved)
    • Observable completion: the rejoining node's term advances via AE; no duplicate-term leader appears
    • Requirements: 4.5
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 4.2

6. CI batch and randomized seed sweep

  • 6.1 RED+GREEN: randomized M-seed sweep with zero violations

    • Test: run raft_sim_run for a fixed max_steps across M seeds (M ≥ configured minimum) plus all targeted scenarios; fail if any seed/scenario violates any invariant
    • Implement the sweep harness in test_raft.c; bound max_steps, M, and array sizes so the target fits the library test-suite budget
    • Observable completion: the full batch runs clean and within budget
    • Requirements: 6.1, 6.2, 6.4
    • Boundary: test_raft.c
    • Depends: 5.1, 5.2, 5.3, 5.4, 5.5

  • 6.2 Verify the conformance batch is ASAN/UBSAN-clean

    • Run the conformance batch under the library test sanitizer build; fix any leak/overflow/UB in the harness (fixed-size arrays, no allocation)
    • Observable completion: /xce-build lib sanitizer run reports no memory errors, leaks, or UB for the conformance target
    • Requirements: 6.3
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 6.1

7. Deliberately-broken-build negative test (the oracle's teeth)

  • 7.1 RED+GREEN: compile-time fault switch emulates the bug-851 defects in the adapter

    • Implement RAFT_SIM_BREAK_TERM_STAMP (adapter on_persist_entry writes term 0) and RAFT_SIM_BREAK_TRUNCATE (adapter on_truncate_from no-op), confined to the test/harness build configuration; default off
    • Observable completion: with a macro off, scenarios are clean; the macro is not set in the default CI run and does not touch raft.c
    • Requirements: 7.1, 7.3
    • Boundary: raft_sim.c
    • Depends: 5.4, 5.5

  • 7.2 RED+GREEN: negative test asserts both directions

    • Test: under the broken configuration the Figure-8 / divergent-suffix scenario triggers a Log Matching / Leader Completeness / State Machine Safety violation (with trace dump); under the correct configuration the same scenario passes — both asserted in one test
    • Observable completion: the broken build is caught and the correct build passes, proving checker sensitivity
    • Requirements: 7.1, 7.2, 7.4
    • Boundary: test_raft.c
    • Depends: 7.1

8. Optional TLC-consumable trace export

  • * 8.1 TLC-consumable trace export (deferred; off by default)
    • Implement raft_sim_export_trace gated by RAFT_SIM_EXPORT: per step, emit the action + tracked raft.tla variables (messages summary, per-node currentTerm/state/log/commitIndex) named per raft/raft.tla, in a stable line-oriented format; off by default
    • Observable completion: with RAFT_SIM_EXPORT set, a run emits a stable, spec-named record stream; default runs emit nothing extra
    • Requirements: 8.1, 8.2, 8.3
    • Boundary: raft_sim.c, test_raft.c
    • Depends: 4.2

## Implementation Notes

- **Task 4.2 — UPSTREAM raft.c BUG SURFACED (bug-1095/1096, bug-851 family).** While building
  the scheduler, the conformance oracle detected a real split-brain defect in `raft.c`
  `raft_on_vote_reply`: (1) vote grants are tallied with a plain counter that ignores
  `from_idx`, so a legitimate `DuplicateMessage` of a vote-response double-counts toward
  quorum; (2) there is no stale-term (`mterm < currentTerm`) reply drop. In `raft.tla`
  `votesGranted` is a SET (idempotent under the legal Duplicate action) and
  `DropStaleResponse` discards stale replies — so a correct implementation must tolerate
  both. Result: two leaders at the same term (Election Safety violation) on some seeds.
  This is OUT OF THIS SPEC'S BOUNDARY (raft.c protocol logic, owned by raft-core /
  ha-term-safety). The harness must NOT mask it (R2.6). **Consequence for downstream
  tasks:** any task asserting "zero invariant violations on the correct build" (5.x targeted
  scenarios, 6.1 M-seed sweep, 7.2 correct-direction) may surface this defect. Implementers
  of those tasks MUST NOT weaken the oracle or hand-pick seeds to hide the bug; if a
  legitimate scenario surfaces it, report BLOCKED with the upstream cause rather than
  working around it. Seed 3 is clean over 600 steps and is used only to prove the 4.2
  scheduler mechanism reaches all action kinds.
- **UPDATE (post-4.2): bug-1095/1096 FIXED in raft.c** (commit `fix(raft): vote-reply
  per-peer dedup + stale-term drop`). `raft_on_vote_reply` now tracks grants in a per-peer
  `vote_replies[]` set (idempotent under DuplicateMessage) and drops stale-term replies
  (DropStaleResponse), mirroring the existing pre-vote idiom; 47 raft / 264 lib tests pass.
  The library is now correct, so downstream tasks (5.x scenarios, 6.1 M-seed sweep, 7.2
  correct-direction) CAN and MUST assert zero invariant violations on the correct build.
  The user authorized this cross-boundary fix. The deliberately-broken-build fault switch
  (task 7) remains the way to deliberately re-introduce a divergence for the negative test.
- **Task 5.1 — scenario commit-propagation pattern (applies to 5.2–5.5).** A follower's
  `commit_index`/`applied[]` only advance when it RECEIVES an AppendEntries carrying a
  `leader_commit` greater than its own (the library applies it). A scenario that replicates
  entries and calls `raft_advance_commit` on the LEADER, but never sends a follow-up
  AE/heartbeat round afterward, leaves followers at `commit_index=0` — making any per-follower
  commit-prefix / State-Machine-Safety / Leader-Completeness assertion VACUOUS on the follower
  side (5.1 has this weakness; Log Matching still validates log convergence there). For
  commit-critical scenarios — ESPECIALLY 5.4 (Figure-8) where follower commit advancement is
  the whole point — after `raft_advance_commit` on the leader, drive ANOTHER AppendEntries
  round so followers observe the new `leader_commit` and advance, then assert follower
  `commit_index`/`applied[]` actually moved. Do NOT assert convergence via a loop bounded by
  `min(commit_index)` when followers are at 0 (it silently passes). 5.1 was accepted as-is
  (meets R4.1 via throughout-checking + log matching); 5.2–5.5 should propagate commit so
  their commit assertions are non-vacuous.