EPaxos: footprint-aware certified checkpoints#14
Conversation
📝 WalkthroughSummary by CodeRabbit
WalkthroughChangesEPaxos now uses explicit entry kinds and canonical point/span footprints, caller-supplied TOQ time, Suggested reviewers: 🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✨ Finishing Touches✨ Simplify code
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 6
Note
Quiet mode is enabled, so only the most important comments were posted inline. Other review comments are grouped below.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (4)
tests/faultcampaign/invariants.go (1)
216-225: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
commandsConflictonly understands one of three footprint kinds.
FootprinthasPoints,Spans, andAll(epaxos/footprint.go). This function only walksPoints. A command withFootprint.All = trueconflicts with everything by definition, and rangeSpansconflict on overlap — neither is checked. MeanwhilesameChosenTuple, three functions up in this exact same file, already knows how to compare all three fields correctly. This is an internal inconsistency, not a stylistic nit.Right now it's dormant because
CommandForPut/CommandForTxnin the kv example only ever populatePoints, so the campaign never actually exercisesAll/Spans. That's exactly the problem: the invariant checker silently passes even where it has zero power to catch a real conflict-ordering bug for two of the three footprint representations this whole PR was built to support. Don't wait for someone to add a range-scan command and discover the checker was toothless the whole time.🐛 Proposed fix (at minimum handle `All`; `Spans` overlap needs real interval logic on top of this)
func commandsConflict(left, right epaxos.Command) bool { + if left.Footprint.All || right.Footprint.All { + return true + } for _, leftKey := range left.Footprint.Points { for _, rightKey := range right.Footprint.Points { if bytes.Equal(leftKey, rightKey) { return true } } } + // TODO: Spans-vs-Spans range overlap and Points-vs-Spans containment are + // still unchecked here. return false }🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@tests/faultcampaign/invariants.go` around lines 216 - 225, Update commandsConflict to evaluate all Footprint representations, not only Points: return true when either command has Footprint.All, retain point equality checks, and add span-overlap detection using the same interval semantics as the existing footprint comparison logic. Reuse sameChosenTuple or its established span-comparison behavior where appropriate so conflicts match the three-field Footprint contract.examples/kv/cmd/kvnode/main.go (1)
1664-1715: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick winGET's ordered-read path lies about the failure mode - 500 instead of 503.
Look at this branch versus everything else in the file. PUT (line 1726), DELETE (line 1736), Txn (line 1809), and even Scan's own ordered branch two hundred lines below (1909) all special-case
proposeAndWait's error and return503 Service Unavailable- that's the signal a client needs to know "retry me, don't treat this as broken." GET just lets the propose error fall through the same genericif err != nilbucket as a decode failure and slaps a500on it. That's not a stylistic quirk, that's a correctness regression in your own error contract, and you wrote the correct version four times elsewhere in this same file.🐛 Fix: make GET match its four siblings
} else { command := kv.CommandForGet(uint64(s.id), s.next(), key) - if err = s.proposeAndWait(ctx, command); err == nil { - var result kv.OrderedGetResult - var found bool - value, found, err = s.db.CommandResult(command.ID) - if err == nil && !found { - err = fmt.Errorf("ordered read completed without a durable result") - } - if err == nil { - result, err = kv.DecodeOrderedGetResult(value) - value, ok = result.Value, result.Found - } - } + if proposeErr := s.proposeAndWait(ctx, command); proposeErr != nil { + http.Error(w, proposeErr.Error(), http.StatusServiceUnavailable) + return + } + var result kv.OrderedGetResult + var found bool + value, found, err = s.db.CommandResult(command.ID) + if err == nil && !found { + err = fmt.Errorf("ordered read completed without a durable result") + } + if err == nil { + result, err = kv.DecodeOrderedGetResult(value) + value, ok = result.Value, result.Found + } }🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@examples/kv/cmd/kvnode/main.go` around lines 1664 - 1715, Update the ordered-read branch in handleKV’s GET case so errors returned by proposeAndWait are sent as 503 Service Unavailable, matching the PUT, DELETE, transaction, and scan paths. Keep decode, CommandResult, and other non-proposal failures on the existing 500 response path.examples/kv/cluster.go (1)
387-454: 🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick winCompare
Kind,ConfChange, andProtocolControlhere too.sameEPaxosRecordTupleandsameChosenEPaxosRecordstill ignore the fields that were moved offCommand, so a checkpoint record can differ in entry type or control bytes and still pass these equality checks. This is checkpoint-validation code; it needs the same record-value comparison the core uses.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@examples/kv/cluster.go` around lines 387 - 454, The equality helpers sameEPaxosRecordTuple and sameChosenEPaxosRecord must also compare each record’s Kind, ConfChange, and ProtocolControl fields. Add these comparisons using the same value semantics as the core record comparison, while preserving all existing comparisons and helper behavior.epaxos/sim_test.go (1)
163-176: 🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick winThe test transports are masking broken MEP3 wire output.
Protocol-generated messages must reach
RawNode.Stepunchanged;canonicalTestMessagecan repair invalid checksums or voter-incarnation fields and let broken production output pass.
epaxos/sim_test.go#L163-L176: pass the emittedMessagedirectly toStep.epaxos/sim_test.go#L331-L340: step theReady.Messagesduplicate directly; build a separate fixture for target corruption.epaxos/stress_test.go#L109-L116: pass the emitted stress message directly toStep.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@epaxos/sim_test.go` around lines 163 - 176, The test transports currently normalize protocol messages and hide invalid production wire output. In epaxos/sim_test.go lines 163-176, update simCluster.deliver to pass the emitted Message directly to RawNode.Step; in epaxos/sim_test.go lines 331-340, step the Ready.Messages duplicate directly and create a separate fixture for target corruption; in epaxos/stress_test.go lines 109-116, pass the emitted stress message directly to Step. Remove canonicalTestMessage from these transport paths while preserving explicit corruption fixtures.
🟡 Other comments (2)
examples/kv/cmd/kvnode/main_test.go-120-123 (1)
120-123: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winSet the record kind or this test exercises the wrong failure.
The fixture leaves
InstanceRecord.Kindat zero. With the new schema, startup can reject the unknown entry kind before reaching the intended ambiguous legacy timing-domain validation.Proposed fix
Status: epaxos.StatusAccepted, + Kind: epaxos.EntryCommand, Seq: 1,🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@examples/kv/cmd/kvnode/main_test.go` around lines 120 - 123, Update the InstanceRecord fixture in the relevant test setup to explicitly assign the legacy record kind, ensuring startup reaches the intended ambiguous legacy timing-domain validation instead of failing on an unknown zero-value kind.EPAXOS.MD-128-128 (1)
128-128: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winStop calling opaque payloads canonical.
Only the footprint has a canonical form. This wording contradicts Line 34 and may make embedders transform payload bytes before transferring ownership.
Proposed clarification
-With `ZeroCopyProposals`, the caller transfers already-canonical payload, footprint, and cycle buffers +With `ZeroCopyProposals`, the caller transfers payload, canonical-footprint, and cycle-key buffers🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@EPAXOS.MD` at line 128, Update the ZeroCopyProposals documentation to state that only footprint buffers are already canonical; describe payload buffers as transferred or aliased input bytes without calling them canonical. Ensure the wording remains consistent with the canonical-form guidance near Line 34 and does not imply embedders must transform payload data before ownership transfer.
🧹 Nitpick comments (8)
epaxos/message.go (1)
536-537: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winLocal var
commandEmptyshadows the package functioncommandEmpty()it calls on the same line.
commandEmpty := m.Kind == 0 && commandEmpty(m.Command) && ...compiles and works — Go resolves the RHS call against the outer-scope function since the new variable's scope only starts at the end of the declaration — but it's a landmine for the next person who greps forcommandEmptyor edits nearby code expecting the identifier to mean one specific thing.✏️ Suggested rename
- commandEmpty := m.Kind == 0 && commandEmpty(m.Command) && + valueIsEmpty := m.Kind == 0 && commandEmpty(m.Command) && m.ConfChange == (ConfChange{}) && len(m.ProtocolControl) == 0(and rename the ~6 later uses of the local
commandEmptybool in this function accordingly)🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@epaxos/message.go` around lines 536 - 537, Rename the local boolean declared in the message emptiness check to avoid shadowing the package-level commandEmpty function, and update all later references to that boolean within the same function. Keep the commandEmpty(m.Command) function call unchanged.epaxos/footprint.go (1)
212-243: 🚀 Performance & Scalability | 🔵 Trivial
footprintsConflictignores that both inputs are already sorted.Nested-loop compare over Points×Points, Points×Spans, Spans×Spans — up to 128×128
bytes.Compare/bytes.Equalcalls per side given the wire limits. Bothaandbare canonicalized (sorted, deduped) by the time they reach this function, so a two-pointer merge sweep would get this down to O(n+m) instead of O(n·m). Not flagging as urgent since footprints are typically tiny in practice and this doesn't appear to sit on the conflict_engine.go hot path (that uses the interval index instead) — just worth tightening if this ever gets called per-instance under real load.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@epaxos/footprint.go` around lines 212 - 243, Update footprintsConflict to exploit the sorted, deduplicated Points and Spans by replacing the nested comparisons with linear two-pointer merge sweeps. Preserve the existing All handling and half-open interval semantics, covering point-point, point-span, and span-span conflicts while reducing each comparison phase to O(n+m).epaxos/conflict_engine_test.go (1)
191-193: 🎯 Functional Correctness | 🔵 Trivial | ⚡ Quick winTest oracle doesn't know about
Footprint.All— the fuzzer never exercises it.Four helpers in this file (
assertConflictEngineMatchesModel'swantGlobal/wantKeyLanes,modelKeyMax,assertExactKeyPostings) gate onentryHasGlobalConflictScope(rec.Kind)alone. That's the narrow,Kind-only predicate. The engine itself gates onrecordHasGlobalConflictScope(rec), which isentryHasGlobalConflictScope(rec.Kind) || (rec.Kind == EntryCommand && rec.Command.Footprint.All)— compareengineModelAttrsat line 268, which correctly usesentryHasGlobalConflictScope(query.Kind) || query.Command.Footprint.All.Since
randomFoldRecord/randomConflictRecordnever generateFootprint.All: trueeither, this 2000-iteration property fuzzer (TestConflictEngineRandomFoldDomination) never actually tests the group-wide-scope command path at all — one of the three footprint forms this PR introduces. If someone ever adds anAll:truecase to the generators without fixing these four call sites first, the oracle would silently produce wrong expectations and either mask a real engine bug or fail on a correct engine.Fix: use
recordHasGlobalConflictScope(rec)consistently in these four spots, and add aFootprint.Allcase to the record generators so this path actually gets fuzzed.Also applies to: 217-237, 338-349, 630-646
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@epaxos/conflict_engine_test.go` around lines 191 - 193, Update the four oracle helpers—assertConflictEngineMatchesModel’s wantGlobal/wantKeyLanes logic, modelKeyMax, and assertExactKeyPostings—to use recordHasGlobalConflictScope(rec) instead of the Kind-only entryHasGlobalConflictScope(rec.Kind) predicate. Extend randomFoldRecord and randomConflictRecord with generated EntryCommand records whose Command.Footprint.All is true, ensuring the group-wide scope path is exercised by the property fuzzer.examples/kv/epaxos_storage.go (4)
512-521: 🚀 Performance & Scalability | 🔵 Trivial | ⚡ Quick win
validateApplicationSnapshotruns twice perSnapshotInstallReady.
DB.ApplyReadycallsdb.validateApplicationSnapshot(rd.Snapshot.Checkpoint)here, theninstallApplicationSnapshot(line 217-218) calls the exact same function again a few lines later in the sameApplyReady. Each call re-fetches the bundle from Pebble and re-hashes the entire application snapshot with blake3, then re-parses every entry. For anything but a trivially small snapshot that's a wasted full pass. Either skip the pre-check forSnapshotInstall(since install re-validates anyway) or thread the already-validatedentriesthrough instead of re-deriving them.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@examples/kv/epaxos_storage.go` around lines 512 - 521, Update DB.ApplyReady’s snapshot validation flow to avoid calling validateApplicationSnapshot twice for SnapshotInstall: skip the pre-check for epaxos.SnapshotInstall because installApplicationSnapshot re-validates the checkpoint, while retaining validation for other supported snapshot modes.
1084-1096: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winNew v9 early-return makes the old v9 terminal check dead code.
This new
if version == epaxosRecordCodecbranch (JSON path) always returns before falling through to the legacy binary-decode path below. But further down, the pre-existing block:if version == epaxosRecordCodec { if epaxos.VerifyRecordChecksum(rec) { return rec, nil } return epaxos.InstanceRecord{}, epaxos.ErrChecksumMismatch }(lines 1282-1287) can now never execute -
version == epaxosRecordCodecis fully intercepted above. That block used to be the terminal check back whenepaxosRecordCodecwas the top binary-format version; now that v9 is JSON and v8 gets its own explicitfinalizeMigrationpath (1276-1281), this leftover is just confusing dead code sitting between two real migration branches. Delete it.🧹 Proposed removal
if version == 8 { if epaxos.VerifyRecordChecksumWithoutMembershipResult(rec) { return finalizeMigration(rec) } return epaxos.InstanceRecord{}, epaxos.ErrChecksumMismatch } - if version == epaxosRecordCodec { - if epaxos.VerifyRecordChecksum(rec) { - return rec, nil - } - return epaxos.InstanceRecord{}, epaxos.ErrChecksumMismatch - } if version == 7 {🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@examples/kv/epaxos_storage.go` around lines 1084 - 1096, Remove the obsolete terminal `if version == epaxosRecordCodec` checksum-validation block in the legacy decode flow, including its `epaxos.VerifyRecordChecksum` check and returns. Keep the preceding v8 `finalizeMigration` path and subsequent migration branches unchanged.
413-423: 🗄️ Data Integrity & Integration | 🔵 Trivial | ⚡ Quick winJSON as a content digest is fragile - nil vs. empty slices hash differently.
digestEPaxosCommandhashesjson.Marshal(command)to detect "command ID reused with a different command" inapplyReadyCommand.Command/Footprintare full of[]byte/[][]bytefields; Go'sencoding/jsonencodes anilslice asnulland a non-nil empty slice as""/[]. Two callers that construct a logically identical command but differ in nil-ness ofPayload/Footprint.Points/CycleKeywould get different digests, and a legitimate retry could then be rejected as "command ID reused with a different command." This is probably masked today becausePropose/decode paths consistently go throughappend([]byte(nil), ...)/CanonicalizeFootprint, but that's an invariant this digest function doesn't enforce or even document - a future field addition or an alternate construction path (e.g. buildingCommanddirectly for a test or a different transport) can silently break dedup correctness.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@examples/kv/epaxos_storage.go` around lines 413 - 423, Update digestEPaxosCommand to hash a canonical representation of the command rather than raw json.Marshal output, normalizing nil and empty []byte/[][]byte fields such as Payload, Footprint.Points, and CycleKey to the same form. Reuse the existing command/footprint canonicalization path where applicable, while preserving deterministic hashing for all command fields.
132-162: 🚀 Performance & Scalability | 🔵 Trivial | 🏗️ Heavy liftBound these scans.
CreateApplicationCheckpointandinstallApplicationSnapshotboth usedb.pebble.NewIter(nil)and then throw away most keys in memory.applicationStateKeyonly matches therecordPrefix('d') range plus theepaxosStorePrefixapplication-state entries ('e'/'a'and'e'/'d'), so use bounded iterators for those key ranges instead.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@examples/kv/epaxos_storage.go` around lines 132 - 162, Update CreateApplicationCheckpoint and installApplicationSnapshot to replace unbounded db.pebble.NewIter(nil) scans with bounded iterators covering only the application-state key ranges: recordPrefix ('d') and the epaxosStorePrefix entries ('e'/'a' and 'e'/'d'). Iterate each bounded range while preserving the existing applicationStateKey filtering and snapshot behavior.epaxos/bootstrap.go (1)
2901-2905: 🚀 Performance & Scalability | 🔵 Trivial | ⚡ Quick winSame "validate, then decode again" waste in two places. Both
applyMembershipControlandCheckpointOfferthrow away a validator's already-parsed/canonically-verified wire value and immediately re-run the identical JSON unmarshal + re-marshal + byte-compare on the same bytes.
epaxos/bootstrap.go#L2901-L2905: havemembershipCommandValidForReftake the already-decodedmembershipCommandWire(decoded once byapplyMembershipControl) instead of re-decodingcontrolitself.epaxos/checkpoint.go#L630-L644: havevalidateCheckpointControlMessagereturn the decodedcheckpointControlWiresoCheckpointOfferdoesn't calldecodeCheckpointControla second time.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@epaxos/bootstrap.go` around lines 2901 - 2905, Eliminate duplicate control-message decoding in both validation paths: update epaxos/bootstrap.go lines 2901-2905 so membershipCommandValidForRef accepts the membershipCommandWire already decoded by applyMembershipControl, and update epaxos/checkpoint.go lines 630-644 so validateCheckpointControlMessage returns its decoded checkpointControlWire for CheckpointOffer to reuse instead of calling decodeCheckpointControl again.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@epaxos/clone_into_test.go`:
- Around line 9-17: The clone ownership test fixtures must cover all newly owned
mutable buffers, not only Footprint.Points. Update both largeCommand and
smallCommand to initialize Footprint.Spans and CycleKey, then mutate the cloned
span endpoints and cycle key in the relevant assertions to verify
Command.CloneInto does not alias them while preserving the existing points
checks.
In `@epaxos/message.go`:
- Around line 307-309: Keep the early return in Validate for MsgCheckpointVote,
MsgCheckpointCertificate, and MsgCheckpointOffer, and remove those checkpoint
types from every later switch case list, including the duplicate validation
block near the end. Preserve all non-checkpoint cases and their existing
validation behavior.
In `@epaxos/pool.go`:
- Around line 75-84: Update the span-pool cleanup logic to preserve reusable
Start and End endpoint buffers instead of resetting every pooled Span to Span{}.
Apply the existing per-endpoint and aggregate arena limits when retaining
buffers, while still discarding oversized pools; then add a span-shaped
AllocsPerRun test covering ordered-range commands and verifying the
zero-allocation reuse path.
In `@examples/kv/epaxos_storage.go`:
- Around line 557-630: Update ApplyReady and applyReadyCommand so all
Ready.Apply commands share one indexed batch (or equivalent read-your-writes
view), allowing later ordered reads to observe earlier staged writes. Move the
single pebble.Sync commit to the end of ApplyReady, remove per-command batch
creation/commit from applyReadyCommand, and preserve nextTime updates and error
propagation.
In `@examples/kv/kv.go`:
- Around line 467-468: Enforce the configured maximum scan limit in both
CommandForScan and executeOrderedRead, not only during constructor validation.
Reject any positive limit above that maximum before replicas accumulate or
JSON-encode rows, including commands reconstructed from decoded input. Preserve
the existing malformed-scan validation for other invalid values.
In `@tla/EPaxosCertifiedCompaction.tla`:
- Around line 77-88: Add the ~crashed guard to ChooseCheckpoint,
PersistSnapshot, Compact, and Receive so none of these local actions can execute
for a crashed node. Apply the changes at tla/EPaxosCertifiedCompaction.tla
ranges 77-88, 89-97, 115-124, and 153-164 respectively; all four sites require
direct changes.
---
Outside diff comments:
In `@epaxos/sim_test.go`:
- Around line 163-176: The test transports currently normalize protocol messages
and hide invalid production wire output. In epaxos/sim_test.go lines 163-176,
update simCluster.deliver to pass the emitted Message directly to RawNode.Step;
in epaxos/sim_test.go lines 331-340, step the Ready.Messages duplicate directly
and create a separate fixture for target corruption; in epaxos/stress_test.go
lines 109-116, pass the emitted stress message directly to Step. Remove
canonicalTestMessage from these transport paths while preserving explicit
corruption fixtures.
In `@examples/kv/cluster.go`:
- Around line 387-454: The equality helpers sameEPaxosRecordTuple and
sameChosenEPaxosRecord must also compare each record’s Kind, ConfChange, and
ProtocolControl fields. Add these comparisons using the same value semantics as
the core record comparison, while preserving all existing comparisons and helper
behavior.
In `@examples/kv/cmd/kvnode/main.go`:
- Around line 1664-1715: Update the ordered-read branch in handleKV’s GET case
so errors returned by proposeAndWait are sent as 503 Service Unavailable,
matching the PUT, DELETE, transaction, and scan paths. Keep decode,
CommandResult, and other non-proposal failures on the existing 500 response
path.
In `@tests/faultcampaign/invariants.go`:
- Around line 216-225: Update commandsConflict to evaluate all Footprint
representations, not only Points: return true when either command has
Footprint.All, retain point equality checks, and add span-overlap detection
using the same interval semantics as the existing footprint comparison logic.
Reuse sameChosenTuple or its established span-comparison behavior where
appropriate so conflicts match the three-field Footprint contract.
---
Other comments:
In `@EPAXOS.MD`:
- Line 128: Update the ZeroCopyProposals documentation to state that only
footprint buffers are already canonical; describe payload buffers as transferred
or aliased input bytes without calling them canonical. Ensure the wording
remains consistent with the canonical-form guidance near Line 34 and does not
imply embedders must transform payload data before ownership transfer.
In `@examples/kv/cmd/kvnode/main_test.go`:
- Around line 120-123: Update the InstanceRecord fixture in the relevant test
setup to explicitly assign the legacy record kind, ensuring startup reaches the
intended ambiguous legacy timing-domain validation instead of failing on an
unknown zero-value kind.
---
Nitpick comments:
In `@epaxos/bootstrap.go`:
- Around line 2901-2905: Eliminate duplicate control-message decoding in both
validation paths: update epaxos/bootstrap.go lines 2901-2905 so
membershipCommandValidForRef accepts the membershipCommandWire already decoded
by applyMembershipControl, and update epaxos/checkpoint.go lines 630-644 so
validateCheckpointControlMessage returns its decoded checkpointControlWire for
CheckpointOffer to reuse instead of calling decodeCheckpointControl again.
In `@epaxos/conflict_engine_test.go`:
- Around line 191-193: Update the four oracle
helpers—assertConflictEngineMatchesModel’s wantGlobal/wantKeyLanes logic,
modelKeyMax, and assertExactKeyPostings—to use recordHasGlobalConflictScope(rec)
instead of the Kind-only entryHasGlobalConflictScope(rec.Kind) predicate. Extend
randomFoldRecord and randomConflictRecord with generated EntryCommand records
whose Command.Footprint.All is true, ensuring the group-wide scope path is
exercised by the property fuzzer.
In `@epaxos/footprint.go`:
- Around line 212-243: Update footprintsConflict to exploit the sorted,
deduplicated Points and Spans by replacing the nested comparisons with linear
two-pointer merge sweeps. Preserve the existing All handling and half-open
interval semantics, covering point-point, point-span, and span-span conflicts
while reducing each comparison phase to O(n+m).
In `@epaxos/message.go`:
- Around line 536-537: Rename the local boolean declared in the message
emptiness check to avoid shadowing the package-level commandEmpty function, and
update all later references to that boolean within the same function. Keep the
commandEmpty(m.Command) function call unchanged.
In `@examples/kv/epaxos_storage.go`:
- Around line 512-521: Update DB.ApplyReady’s snapshot validation flow to avoid
calling validateApplicationSnapshot twice for SnapshotInstall: skip the
pre-check for epaxos.SnapshotInstall because installApplicationSnapshot
re-validates the checkpoint, while retaining validation for other supported
snapshot modes.
- Around line 1084-1096: Remove the obsolete terminal `if version ==
epaxosRecordCodec` checksum-validation block in the legacy decode flow,
including its `epaxos.VerifyRecordChecksum` check and returns. Keep the
preceding v8 `finalizeMigration` path and subsequent migration branches
unchanged.
- Around line 413-423: Update digestEPaxosCommand to hash a canonical
representation of the command rather than raw json.Marshal output, normalizing
nil and empty []byte/[][]byte fields such as Payload, Footprint.Points, and
CycleKey to the same form. Reuse the existing command/footprint canonicalization
path where applicable, while preserving deterministic hashing for all command
fields.
- Around line 132-162: Update CreateApplicationCheckpoint and
installApplicationSnapshot to replace unbounded db.pebble.NewIter(nil) scans
with bounded iterators covering only the application-state key ranges:
recordPrefix ('d') and the epaxosStorePrefix entries ('e'/'a' and 'e'/'d').
Iterate each bounded range while preserving the existing applicationStateKey
filtering and snapshot behavior.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: QUIET
Plan: Pro
Run ID: f29255b0-9371-4502-974d-a4a51793c9b6
📒 Files selected for processing (99)
EPAXOS.MDEPAXOS_IMPLEMENTATION_PROOF.mdMODEL_EQ_REPORT.MDREADME.mdRELEASE_SCOPE.mdepaxos/bootstrap.goepaxos/bootstrap_core_test.goepaxos/bootstrap_fence_test.goepaxos/bootstrap_recovery_test.goepaxos/branch_test.goepaxos/checkpoint.goepaxos/checkpoint_node.goepaxos/checkpoint_test.goepaxos/checksum.goepaxos/checksum_migration_test.goepaxos/clone_into_test.goepaxos/codec.goepaxos/codec_evidence_scratch_test.goepaxos/config_change_ordering_test.goepaxos/config_crash_migration_test.goepaxos/conflict_engine.goepaxos/conflict_engine_test.goepaxos/conflict_ordering_test.goepaxos/coverage_boundaries_test.goepaxos/doc.goepaxos/dst_test.goepaxos/exhaustion_test.goepaxos/faultsim_harness_test.goepaxos/faultsim_oracle_test.goepaxos/footprint.goepaxos/hard_state_ready_test.goepaxos/internal_test.goepaxos/interval_index.goepaxos/malformed_fuzz_test.goepaxos/message.goepaxos/message_recovery_evidence_test.goepaxos/node.goepaxos/optimized_test.goepaxos/performance_benchmark_test.goepaxos/pool.goepaxos/pool_capacity_test.goepaxos/pool_ownership_test.goepaxos/protocol_coverage_test.goepaxos/ready_durability_test.goepaxos/ready_ownership_additional_test.goepaxos/record_load_test.goepaxos/recovery_boundary_test.goepaxos/recovery_test.goepaxos/remaining_test.goepaxos/retire_test.goepaxos/revisited_test.goepaxos/runtime_stats_test.goepaxos/sim_test.goepaxos/sparse_progress.goepaxos/storage.goepaxos/stress_test.goepaxos/toq_test.goepaxos/types.goepaxos/visit_conflicts_test.goexamples/kv/backup.goexamples/kv/checkpoint_hard_state_test.goexamples/kv/cluster.goexamples/kv/cmd/kvcheckpoint/main.goexamples/kv/cmd/kvcheckpoint/main_test.goexamples/kv/cmd/kvnode/capped_ready_test.goexamples/kv/cmd/kvnode/main.goexamples/kv/cmd/kvnode/main_test.goexamples/kv/cmd/kvnode/performance_benchmark_test.goexamples/kv/cmd/kvnode/protocol_driver_test.goexamples/kv/cmd/kvnode/retention_test.goexamples/kv/epaxos_hard_state_test.goexamples/kv/epaxos_record_timing_codec_test.goexamples/kv/epaxos_storage.goexamples/kv/epaxos_storage_benchmark_test.goexamples/kv/footprint_checkpoint_test.goexamples/kv/kv.goexamples/kv/kv_test.goexamples/kv/more_test.goexamples/kv/storage_stats_test.gorelease/EPAXOS_READINESS_EVIDENCE.mdtests/faultcampaign/campaign.gotests/faultcampaign/invariants.gotests/faultcampaign/invariants_test.gotests/faultcampaign/main_test.gotests/faultcampaign/native_darwin.gotests/faultcampaign/proxy_test.gotests/faultcampaign/trace.gotests/faultcampaign/trace_test.gotests/lifecyclecollector/collect.gotests/lifecyclecollector/model.gotests/refinementtrace/inventory_test.gotests/refinementtrace/scenarios.gotests/refinementtrace/semantic.gotests/refinementtrace/trace_test.gotests/tla_model_check_runner.pytests/trace_refinement_check.shtla/EPaxosCertifiedCompaction.tlatla/EPaxosCertifiedCompactionFast.cfgtla/EPaxosCertifiedCompactionFull.cfg
💤 Files with no reviewable changes (1)
- epaxos/visit_conflicts_test.go
👮 Files not reviewed due to content moderation or server errors (7)
- epaxos/checkpoint_node.go
- epaxos/checksum.go
- epaxos/codec.go
- epaxos/conflict_ordering_test.go
- epaxos/doc.go
- epaxos/internal_test.go
- epaxos/interval_index.go
📜 Review details
⏰ Context from checks skipped due to timeout. (1)
- GitHub Check: verification
🧰 Additional context used
🪛 GitHub Check: CodeQL
examples/kv/epaxos_storage.go
[failure] 426-426: Size computation for allocation may overflow
This operation, which is used in an allocation, involves a potentially large value and might overflow.
This operation, which is used in an allocation, involves a potentially large value and might overflow.
🪛 LanguageTool
README.md
[grammar] ~39-~39: Ensure spelling is correct
Context: ...and operational clock discipline remain embedder responsibilities. - The example KV uses...
(QB_NEW_EN_ORTHOGRAPHY_ERROR_IDS_1)
MODEL_EQ_REPORT.MD
[grammar] ~38-~38: Ensure spelling is correct
Context: ...shot code, focused lifecycle tests, and TestCheckpointCompactionThreeReplicaRestartSmoke. | | tla/EPaxosRollbackAllocation.tla...
(QB_NEW_EN_ORTHOGRAPHY_ERROR_IDS_1)
[style] ~119-~119: Three successive sentences begin with the same word. Consider rewording the sentence or use a thesaurus to find a synonym.
Context: ... - bash tests/tla_model_check_fast.sh passes all 32 configured jobs, including the c...
(ENGLISH_WORD_REPEAT_BEGINNING_RULE)
EPAXOS.MD
[style] ~101-~101: This phrase is redundant. Consider writing “same”.
Context: ...ponents pause, so all replicas take the same exact application cut. ## Configuration chang...
(SAME_EXACT)
🔍 Remote MCP Github Grep
I found:
- Public GitHub search hits for the old terms
ConflictKeys,CommittedCommand, andReady.Committedare common in unrelated Go projects, so this PR is a real API/terminology cutover rather than a cosmetic rename. Examples includedgogf/gf,dgraph-io/badger,cockroachdb/cockroach, andetcd-io/raft. - Searches for the new EPaxos-specific forms (
ProvideCheckpoint,EPaxosCertifiedCompaction,ProcessTOQ(now uint64),epaxos.ApplyCommand{},LoadInstances(epaxos.ExecutionFrontier{}, ...),epaxos.Footprint{Points:) returned no public GitHub matches, so I couldn’t validate these new APIs against external examples.
| largeCommand := Command{ | ||
| ID: CommandID{Client: 601, Sequence: 1}, | ||
| Payload: []byte("large-command-payload"), | ||
| ConflictKeys: [][]byte{[]byte("large-key-one"), []byte("large-key-two")}, | ||
| ID: CommandID{Client: 601, Sequence: 1}, | ||
| Payload: []byte("large-command-payload"), | ||
| Footprint: Footprint{Points: [][]byte{[]byte("large-key-one"), []byte("large-key-two")}}, | ||
| } | ||
| smallCommand := Command{ | ||
| ID: CommandID{Client: 601, Sequence: 2}, | ||
| Payload: []byte("small"), | ||
| ConflictKeys: [][]byte{[]byte("key")}, | ||
| ID: CommandID{Client: 601, Sequence: 2}, | ||
| Payload: []byte("small"), | ||
| Footprint: Footprint{Points: [][]byte{[]byte("key")}}, |
There was a problem hiding this comment.
🩺 Stability & Availability | 🟠 Major | ⚡ Quick win
Test every newly owned mutable buffer, not just points.
Add Footprint.Spans and CycleKey to both fixtures, then mutate the cloned span endpoints and cycle key. The current test still passes if Command.CloneInto aliases either field, which would violate the zero-copy/Ready ownership contract.
Also applies to: 44-45, 62-62, 84-84, 92-96
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@epaxos/clone_into_test.go` around lines 9 - 17, The clone ownership test
fixtures must cover all newly owned mutable buffers, not only Footprint.Points.
Update both largeCommand and smallCommand to initialize Footprint.Spans and
CycleKey, then mutate the cloned span endpoints and cycle key in the relevant
assertions to verify Command.CloneInto does not alias them while preserving the
existing points checks.
| if m.Type == MsgCheckpointVote || m.Type == MsgCheckpointCertificate || m.Type == MsgCheckpointOffer { | ||
| return validateCheckpointControlMessage(m) | ||
| } |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟠 Major | ⚡ Quick win
Checkpoint-type cases added throughout this switch statement below are dead code.
Line 307-309 unconditionally returns for MsgCheckpointVote/MsgCheckpointCertificate/MsgCheckpointOffer before switch m.Type even starts. Every later addition of those three types to a case list is therefore unreachable:
- Line 323-324 (
case MsgPreAcceptResp, ..., MsgCheckpointVote, ...:) - Line 400-401
- Line 439
- Line 458-459
- Line 491-492
- Line 507-508
- Line 526-527
- Line 597-598
- Line 700-701 (
case MsgCheckpointVote, ...: return validateCheckpointControlMessage(m)— literally the same call already made at 308, now unreachable)
This isn't just cosmetic clutter in a security-critical validator: it actively misrepresents the control flow to the next person editing this function — they'll reasonably assume checkpoint messages flow through the per-type switches (they don't), and if the line 307-309 guard is ever removed under that assumption, Validate()'s behavior for checkpoint messages silently changes.
Pick one design and delete the other: either drop the early return at 307-309 and let checkpoint types fall through the switches naturally (ending at 700-701), or keep 307-309 and strip the checkpoint cases from every switch below it.
🧹 Minimal fix keeping the early return, stripping the 9 dead branches
- case MsgPreAcceptResp, MsgAcceptResp, MsgCommit, MsgPrepareResp, MsgTryPreAcceptResp, MsgEvidenceResp,
- MsgCheckpointVote, MsgCheckpointCertificate, MsgCheckpointOffer:
+ case MsgPreAcceptResp, MsgAcceptResp, MsgCommit, MsgPrepareResp, MsgTryPreAcceptResp, MsgEvidenceResp:(repeat for lines 400-401, 439, 458-459, 491-492, 507-508, 526-527, 597-598, and delete the now-duplicate case MsgCheckpointVote, MsgCheckpointCertificate, MsgCheckpointOffer: block at 700-701 entirely)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@epaxos/message.go` around lines 307 - 309, Keep the early return in Validate
for MsgCheckpointVote, MsgCheckpointCertificate, and MsgCheckpointOffer, and
remove those checkpoint types from every later switch case list, including the
duplicate validation block near the end. Preserve all non-checkpoint cases and
their existing validation behavior.
| for i := range spans[:cap(spans)] { | ||
| clear(spans[:cap(spans)][i].Start) | ||
| clear(spans[:cap(spans)][i].End) | ||
| spans[:cap(spans)][i] = Span{} | ||
| } | ||
| if cap(spans) > maxWireFootprintSpans { | ||
| spans = nil | ||
| } else { | ||
| spans = spans[:0] | ||
| } |
There was a problem hiding this comment.
🚀 Performance & Scalability | 🟠 Major | 🏗️ Heavy lift
Stop throwing away every pooled span endpoint.
Resetting each entry to Span{} guarantees new allocations for every non-empty Start and End, making ordered-range commands miss the pool’s zero-allocation objective. Retain bounded endpoint buffers using per-endpoint and aggregate arena limits, then add a span-shaped AllocsPerRun case.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@epaxos/pool.go` around lines 75 - 84, Update the span-pool cleanup logic to
preserve reusable Start and End endpoint buffers instead of resetting every
pooled Span to Span{}. Apply the existing per-endpoint and aggregate arena
limits when retaining buffers, while still discarding oversized pools; then add
a span-shaped AllocsPerRun test covering ordered-range commands and verifying
the zero-allocation reuse path.
| for _, command := range rd.Apply { | ||
| if err := db.applyReadyCommand(command); err != nil { | ||
| return err | ||
| } | ||
| } | ||
| return nil | ||
| } | ||
|
|
||
| func (db *DB) applyReadyCommand(command epaxos.ApplyCommand) error { | ||
| id := command.Command.ID | ||
| if id == (epaxos.CommandID{}) { | ||
| return fmt.Errorf("kv: applied command requires a nonzero command ID") | ||
| } | ||
| digest, err := digestEPaxosCommand(command.Command) | ||
| if err != nil { | ||
| return err | ||
| } | ||
| batch := db.newWriteBatch() | ||
| defer func() { _ = batch.Close() }() | ||
| newRecords, err := stageAndCountEPaxosRecords(batch, rd.Records, db.durableRefs) | ||
| value, closer, err := db.pebble.Get(epaxosCommandResultKey(id)) | ||
| if err == nil { | ||
| storedDigest, _, decodeErr := decodeEPaxosCommandResult(value) | ||
| closeErr := closer.Close() | ||
| if decodeErr != nil { | ||
| return decodeErr | ||
| } | ||
| if closeErr != nil { | ||
| return closeErr | ||
| } | ||
| if storedDigest != digest { | ||
| return fmt.Errorf("kv: command ID reused with a different command") | ||
| } | ||
| return nil | ||
| } | ||
| if !errors.Is(err, pebble.ErrNotFound) { | ||
| return err | ||
| } | ||
|
|
||
| legacyApplied, err := db.appliedReadyCommand(command.Ref) | ||
| if err != nil { | ||
| return err | ||
| } | ||
| var response []byte | ||
| batch := db.newWriteBatch() | ||
| defer func() { _ = batch.Close() }() | ||
| next := db.nextRecordTime() | ||
| for _, committed := range rd.Committed { | ||
| done, err := db.appliedReadyCommand(committed.Ref) | ||
| advancesTime := false | ||
| if !legacyApplied { | ||
| var handled bool | ||
| response, handled, err = db.executeOrderedRead(command.Command) | ||
| if err != nil { | ||
| return err | ||
| } | ||
| if done { | ||
| continue | ||
| } | ||
| if _, err := db.stageCommitted(batch, committed, &next); err != nil { | ||
| return err | ||
| } | ||
| if err := batch.Set(epaxosAppliedKey(committed.Ref), []byte{1}, nil); err != nil { | ||
| return err | ||
| if !handled { | ||
| if _, err := db.stageCommitted(batch, command, &next); err != nil { | ||
| return err | ||
| } | ||
| advancesTime = true | ||
| } | ||
| } | ||
| if hardState != nil { | ||
| if err := batch.Set(epaxosHardStateKey, hardState, nil); err != nil { | ||
| if err := batch.Set(epaxosCommandResultKey(id), encodeEPaxosCommandResult(digest, response), nil); err != nil { | ||
| return err | ||
| } | ||
| if !command.Ref.IsZero() { | ||
| if err := batch.Set(epaxosAppliedKey(command.Ref), []byte{1}, nil); err != nil { | ||
| return err | ||
| } | ||
| } | ||
| if err := batch.Commit(pebble.Sync); err != nil { | ||
| return err | ||
| } | ||
| addDurableRecords(db.durableRefs, rd.Records) | ||
| db.nextTime = next | ||
| db.durableRecords.Add(newRecords) | ||
| if advancesTime { | ||
| db.nextTime = next | ||
| } | ||
| return nil | ||
| } |
There was a problem hiding this comment.
🚀 Performance & Scalability | 🟠 Major | 🏗️ Heavy lift
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Check whether executeOrderedRead reads through db.pebble (committed-only)
# or through an indexed batch (would allow safely coalescing commits).
rg -n 'func.*executeOrderedRead' -A 25 examples/kv
rg -n 'func.*newWriteBatch' -A 10 examples/kv
rg -n 'NewIndexedBatch' examples/kvRepository: gosuda/moreconsensus
Length of output: 2014
🏁 Script executed:
#!/bin/bash
set -euo pipefail
sed -n '330,520p' examples/kv/kv.go
printf '\n----\n'
sed -n '520,700p' examples/kv/epaxos_storage.go
printf '\n----\n'
rg -n 'ApplyReady|ApplyCommitted|executeOrderedRead|OrderedGet|OrderedScan|newWriteBatch|NewIndexedBatch|batch.Get|db.Get\(' examples/kvRepository: gosuda/moreconsensus
Length of output: 29809
🏁 Script executed:
#!/bin/bash
set -euo pipefail
rg -n 'OrderedGetResult|OrderedScanResult|ordered get|ordered scan|opGet|opScan|ApplyReady\(\s*epaxos\.Ready' examples/kv/*test.go
printf '\n----\n'
sed -n '2760,2895p' examples/kv/more_test.go
printf '\n----\n'
sed -n '1680,1955p' examples/kv/cmd/kvnode/main.goRepository: gosuda/moreconsensus
Length of output: 18552
🏁 Script executed:
#!/bin/bash
set -euo pipefail
rg -n 'type Ready struct|Apply \[\]|Records \[\]|MustSync|CommandResult\(|appliedReadyCommand\(' -S .
printf '\n----\n'
sed -n '1,220p' $(git ls-files | rg '(^|/)ready\.go$|(^|/)types\.go$|(^|/)epaxos.*\.go$' | head -n 20)Repository: gosuda/moreconsensus
Length of output: 23488
🏁 Script executed:
#!/bin/bash
set -euo pipefail
rg -n 'type Ready struct|Apply \[\]ApplyCommand|MustSync bool|CommandResult\(' .Repository: gosuda/moreconsensus
Length of output: 2147
🏁 Script executed:
#!/bin/bash
set -euo pipefail
sed -n '100,140p' EPAXOS.MD
printf '\n----\n'
sed -n '650,710p' epaxos/types.go
printf '\n----\n'
sed -n '980,1045p' examples/kv/epaxos_storage.goRepository: gosuda/moreconsensus
Length of output: 11723
Batch Ready.Apply before syncing. ApplyReady already treats Ready.Apply as ordered work, so this is burning one WAL fsync per command for no good reason. The current loop opens a fresh batch and calls Commit(pebble.Sync) on every entry; if ordered reads need to see earlier in-Ready writes, use an indexed batch or equivalent read-your-writes view and commit once. examples/kv/epaxos_storage.go:581-626
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@examples/kv/epaxos_storage.go` around lines 557 - 630, Update ApplyReady and
applyReadyCommand so all Ready.Apply commands share one indexed batch (or
equivalent read-your-writes view), allowing later ordered reads to observe
earlier staged writes. Move the single pebble.Sync commit to the end of
ApplyReady, remove per-command batch creation/commit from applyReadyCommand, and
preserve nextTime updates and error propagation.
| if p.err || len(p.b) != 0 || limit == 0 || limit > uint64(^uint(0)>>1) || reverse > 1 { | ||
| return nil, true, fmt.Errorf("kv: malformed ordered scan") |
There was a problem hiding this comment.
🩺 Stability & Availability | 🟠 Major | ⚡ Quick win
Do not turn replicated scans into an OOM primitive.
Any positive limit up to MaxInt is accepted, after which every replica accumulates and JSON-encodes that many rows for durable storage. Enforce a configured maximum in both CommandForScan and executeOrderedRead; constructor validation alone is bypassable by decoded commands.
Also applies to: 809-810
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@examples/kv/kv.go` around lines 467 - 468, Enforce the configured maximum
scan limit in both CommandForScan and executeOrderedRead, not only during
constructor validation. Reject any positive limit above that maximum before
replicas accumulate or JSON-encode rows, including commands reconstructed from
decoded input. Preserve the existing malformed-scan validation for other invalid
values.
| ChooseCheckpoint(cut) == | ||
| /\ checkpoint = Zero | ||
| /\ cut \in Frontiers | ||
| /\ \A lane \in Lanes: | ||
| /\ cut[lane] > 0 | ||
| /\ cut[lane] = executed[lane] | ||
| /\ cut[lane] = applied[lane] | ||
| /\ checkpoint' = cut | ||
| /\ UNCHANGED <<executed, applied, applicationBase, snapshotDurable, | ||
| snapshotApp, votes, certified, compacted, records, | ||
| summary, crashed, restored, rejected>> | ||
|
|
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
Fix your zombie crash model.
Your "crash model" lacks basic common sense: a crashed node shouldn't be making checkpoints, persisting snapshots, running compactions, or receiving messages. You remembered to guard Execute, Apply, and ReplayDelta with ~crashed, but completely left it out of the other local actions, allowing the TLC model checker to explore garbage states where a powered-off machine does disk I/O and network processing.
tla/EPaxosCertifiedCompaction.tla#L77-L88: Add/\ ~crashedtoChooseCheckpointso a dead node doesn't initiate a checkpoint.tla/EPaxosCertifiedCompaction.tla#L89-L97: Add/\ ~crashedtoPersistSnapshotso a dead node doesn't write snapshots to disk.tla/EPaxosCertifiedCompaction.tla#L115-L124: Add/\ ~crashedtoCompactso a dead node doesn't delete records.tla/EPaxosCertifiedCompaction.tla#L153-L164: Add/\ ~crashedtoReceiveso a dead node doesn't mutate its local storage from incoming packets.
📍 Affects 1 file
tla/EPaxosCertifiedCompaction.tla#L77-L88(this comment)tla/EPaxosCertifiedCompaction.tla#L89-L97tla/EPaxosCertifiedCompaction.tla#L115-L124tla/EPaxosCertifiedCompaction.tla#L153-L164
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@tla/EPaxosCertifiedCompaction.tla` around lines 77 - 88, Add the ~crashed
guard to ChooseCheckpoint, PersistSnapshot, Compact, and Receive so none of
these local actions can execute for a crashed node. Apply the changes at
tla/EPaxosCertifiedCompaction.tla ranges 77-88, 89-97, 115-124, and 153-164
respectively; all four sites require direct changes.
2 participants
Summary
Ready.Apply, durable command results, certified checkpoints, atomic protocol compaction, and snapshot-plus-delta restartEPaxosCertifiedCompactionTLC profilesRollout
CompactedThroughremain receiver-localVerification
go vet ./...golangci-lint run ./...(cd examples/kv && golangci-lint run ./...)tests/ci.shpython3 -m unittest tests.tla_model_check_runner_testRelease boundary
The authoritative decision remains No-go. The single open release row is broader unbounded Go/TLA refinement and checked action correspondence, including the recorded TLAPS and trace-replay gaps plus external evidence requirements.