kv(composed1): M3 — verifyComposed1 apply-time gate + retry sentinels#895
kv(composed1): M3 — verifyComposed1 apply-time gate + retry sentinels#895bootjp wants to merge 1 commit into
Conversation
Third milestone of the Composed-1 cross-group commit-time guard per docs/design/2026_05_29_proposed_composed1_cross_group_commit_guard.md §M3. Wires the safety property at apply time using the M2 versioned-snapshot ring and the M1 ObservedRouteVersion field. Stacked on PR #894 (M2 plumbing). What's enforced: (a) Observed-version owner — the spec-level Composed-1 check from tla/composed/Composed.tla. Every write key of a Composed-1- pinned txn must be owned by THIS Raft group at the txn's observed catalog version (the version it read its read-set at, set in M1 via OperationGroup.ObservedRouteVersion). Refusal returns ErrComposed1Violation. (b) Current-version cross-version-read fence — the §4.4 / §3 codex P1 trace. Even when (a) passes, a route shift between BeginTxn and Commit can leave the write landing on the OLD owner while readers at the new version route to the NEW owner and miss the write. The current-version fence refuses that case so M4 retry can re-route. Refusal returns ErrComposed1Violation with a different diagnostic prefix ("current-version" vs "observed-version") so the retry path can distinguish. (c) Retention-miss fail-closed — when the txn's observed version has been evicted from the M2 ring (long-running txn or high catalog churn), return ErrComposed1VersionGCd. Per design doc §4.3, the not-found semantics is a hard retryable error, NOT a soft pass, because soft-pass would let the gate be bypassed exactly in the cases where the cross-version-read hazard is most likely. Short-circuits cleanly in three legacy / not-applicable cases: * FSM constructed without WithRouteHistory (legacy / test seam): routes == nil, gate returns nil. * Request carries ObservedRouteVersion == 0 (unpinned — pre-M1 caller, or 2PC ABORT request that doesn't carry the version): gate returns nil. This is what keeps M3 from regressing every caller that has not migrated to set OperationGroup. ObservedRouteVersion. * Engine.Current returns (zero, false) — engine has no history (bare-struct test seam): the (b) fence falls through. Changes: * distribution/engine.go — adds Engine.Current() returning the snapshot at the current catalogVersion (used by the M3 fence). Adds SetHistoryDepthForTest as the cross-package test seam that lets kv-side tests trigger eviction without bypassing the package boundary (claude review on PR #894 — fragile-but- test-local lock contract documented inline). * kv/fsm.go — defines ErrComposed1Violation and ErrComposed1VersionGCd sentinels with the wrapped-error diagnostic shape M4 retry will use. Adds verifyComposed1 and verifyOwnerFromSnapshot. Wires verifyComposed1 into handleTxnRequest at the top so PREPARE / COMMIT / ABORT / NONE all pass through the gate (ABORT carries ObservedRouteVersion=0 and falls through naturally). * kv/route_history.go — RouteHistory interface gains Current(). Adapter forwards to distribution.Engine.Current(). Tests (kv/fsm_composed1_test.go): * TestVerifyComposed1_StaleObservedVersionWithMovedKeyFails — design doc M3 "done when" criterion (i): observed-version snapshot resolves the key to a different group than this FSM. * TestVerifyComposed1_ObservedVersionOlderThanRingFails — criterion (ii): observed version is outside the ring → ErrComposed1VersionGCd. Uses depth=2 via the cross-package SetHistoryDepthForTest seam. * TestVerifyComposed1_ObservedPassesButCurrentDiffersFails — criterion (iii) / the §3 codex P1 trace: observed-version check passes (routes[1][k1]=g1) but the current snapshot at v=2 has moved k1 to g2 → ErrComposed1Violation with the "current-version" diagnostic prefix. * TestVerifyComposed1_ObservedVersionZeroSkipsGate — legacy caller (ObservedRouteVersion=0) bypasses the gate. * TestVerifyComposed1_NilRouteHistorySkipsGate — unwired FSM (no WithRouteHistory option) bypasses the gate; matches the pre-feature posture. Verification: * go build ./... — clean * go vet ./... — clean * go test -race -count=1 ./kv ./distribution — 10.2 s + 1.0 s, pass Self-review (5 lenses): 1. Data loss — the gate refuses commits but cannot lose them. Every rejection emits a sentinel the M4 coordinator path will convert into a successful commit on the correct owner. 2. Concurrency — the gate runs under the FSM's apply loop (Raft applies are serial), so no new lock ordering. RouteHistory reads take the engine's read lock; SnapshotAt and Current each acquire and release in a single call. 3. Performance — two map lookups + a per-mutation linear scan of the snapshot's sorted routes per Composed-1-pinned commit. OwnerOf short-circuits via the M2 round-1 break optimisation, so the per-mutation cost is bounded by the first non-covering gap rather than the full routes slice. Legacy callers (ObservedRouteVersion=0) pay one branch per commit and exit. 4. Data consistency — closes the Composed-1 (observed) and Composed-1a (current) gaps end-to-end. Spec correspondence: tla/composed/Composed.tla's Commit precondition is now enforced at apply time; the §4.4 fence matches Composed1a_CommitToCurrentOwner from PR #878. 5. Test coverage — 5 new unit tests cover the three design doc criteria + the two legacy short-circuit paths. Existing handleTxnRequest tests pass unchanged (their requests carry ObservedRouteVersion=0 from M1's behaviour-neutral default). Next milestone (separate PR per design doc §6): M4 — coordinator retry path. When either Composed-1 sentinel returns, the coordinator re-reads the route cache, re-routes the txn against the new owning group, and re-issues it once.
|
@claude review |
📝 WalkthroughWalkthroughThis PR introduces a Composed-1 gate that enforces transaction correctness by validating ownership at both historical and current catalog versions. It extends the route-history mechanism with ChangesComposed-1 Gate for Transaction Consistency
Sequence DiagramsequenceDiagram
participant Client
participant FSM as kvFSM<br/>(handleTxnRequest)
participant Gate as verifyComposed1()
participant Observed as RouteHistory<br/>(SnapshotAt)
participant Current as RouteHistory<br/>(Current)
Client->>FSM: Txn with ObservedRouteVersion
FSM->>Gate: verifyComposed1(request)
Gate->>Observed: SnapshotAt(ObservedVersion)
alt Observed version evicted
Observed-->>Gate: nil, false
Gate-->>FSM: ErrComposed1VersionGCd
else Observed version found
Observed-->>Gate: RouteSnapshot
Gate->>Gate: Check key owners vs shard group
alt Owner mismatch at observed
Gate-->>FSM: ErrComposed1Violation(observed-version)
else Owner match at observed
Gate->>Current: Current()
Current-->>Gate: RouteSnapshot
Gate->>Gate: Check key owners vs shard group
alt Owner mismatch at current
Gate-->>FSM: ErrComposed1Violation(current-version)
else All checks pass
Gate-->>FSM: nil
FSM->>FSM: Proceed to phase dispatch
end
end
end
Estimated code review effort🎯 3 (Moderate) | ⏱️ ~20 minutes Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
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 |
TLA+ spec divergence review (auto-triggered)This PR touches files that the TLA+ safety spec has an anchor on (per Anchored files changed in this PR head (c94e0d1):
What to check, by subsystem:
If the change is correct but requires a spec update, edit @claude review please verify TLA+ spec divergence per the checklist above. @codex review please verify TLA+ spec divergence per the checklist above. |
|
To use Codex here, create a Codex account and connect to github. |
|
Claude finished @bootjp's task in 3m 24s —— View job Code Review — kv(composed1): M3 — verifyComposed1 apply-time gate + retry sentinels
Overall the implementation is solid. The gate logic matches the TLA+ spec (§4.2(a)) and the cross-version fence (§4.4) is correctly wired. No data-loss paths, no lock-ordering issues, no safety bugs found. A few issues worth addressing are called out below in order of severity. Issues1. Misleading comment in
|
| Lens | Result |
|---|---|
| Data loss | Clean — gate can only reject, never silently drop committed writes |
| Concurrency | Clean — gate runs under the serial Raft apply loop; SnapshotAt/Current acquire and release e.mu.RLock atomically |
| Performance | Two map lookups + O( |
| Data consistency | Spec correspondence correct; write-set only check matches Composed1_CommitToOwningGroup; fail-closed on ring miss is correct per §4.3 |
| Test coverage | 5 failure/short-circuit tests present; missing happy-path test (see issue 2 above); no multi-key test |
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
There was a problem hiding this comment.
Code Review
This pull request implements the apply-time Composed-1 gate to prevent cross-version-read anomalies during route shifts. It introduces the Current() method to retrieve the latest route catalog snapshot, defines ErrComposed1Violation and ErrComposed1VersionGCd errors, and adds verification logic in kvFSM.handleTxnRequest to validate key ownership against both the observed and current catalog versions. Comprehensive unit tests are also added. The reviewer identified two critical issues: first, ABORT requests must bypass the Composed-1 gate to avoid leaking MVCC locks, and a short-circuit is needed when shardGroupID is unset (0); second, reducing history depth via SetHistoryDepthForTest on an already populated engine can cause a runtime panic unless excess history entries are immediately truncated.
| func (f *kvFSM) verifyComposed1(r *pb.Request) error { | ||
| if f.routes == nil { | ||
| return nil | ||
| } |
There was a problem hiding this comment.
There are two critical issues here:
- ABORT requests must not be blocked by the Composed-1 gate: If an
ABORTrequest is rejected due to a route shift (ErrComposed1Violation) or history eviction (ErrComposed1VersionGCd), the transaction's locks and intents will be permanently leaked in the MVCC store, blocking future writes. Aborts should always bypass the gate to ensure successful cleanup. - Missing short-circuit for unset shardGroupID: The comments state that a
shardGroupIDof0represents an unset/legacy state and should short-circuit the gate. However, the code does not check forf.shardGroupID == 0, which will cause spuriousErrComposed1Violationerrors on unset groups.
func (f *kvFSM) verifyComposed1(r *pb.Request) error {
if r.Phase == pb.Phase_ABORT {
return nil
}
if f.routes == nil || f.shardGroupID == 0 {
return nil
}| func (e *Engine) SetHistoryDepthForTest(depth int) { | ||
| e.mu.Lock() | ||
| defer e.mu.Unlock() | ||
| e.historyDepth = depth | ||
| } |
There was a problem hiding this comment.
If SetHistoryDepthForTest is called to reduce the history depth after the history ring has already been populated with more entries than the new depth, a subsequent call to recordHistorySnapshotLocked will trigger a runtime panic. This is because make([]uint64, len(e.historyOrder)-1, e.historyDepth) will be invoked with a length greater than its capacity. To prevent this, truncate the excess history entries immediately when updating the depth.
| func (e *Engine) SetHistoryDepthForTest(depth int) { | |
| e.mu.Lock() | |
| defer e.mu.Unlock() | |
| e.historyDepth = depth | |
| } | |
| func (e *Engine) SetHistoryDepthForTest(depth int) { | |
| e.mu.Lock() | |
| defer e.mu.Unlock() | |
| e.historyDepth = depth | |
| if len(e.historyOrder) > depth { | |
| excess := len(e.historyOrder) - depth | |
| for i := 0; i < excess; i++ { | |
| delete(e.history, e.historyOrder[i]) | |
| } | |
| retained := make([]uint64, depth) | |
| copy(retained, e.historyOrder[excess:]) | |
| e.historyOrder = retained | |
| } | |
| } |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
| // docs/design/2026_05_29_proposed_composed1_cross_group_commit_guard.md | ||
| // §4.2(a) + §4.4. Runs two checks before the txn's writes land: | ||
| // | ||
| // (a) Observed-version owner — the txn's read-set was captured |
There was a problem hiding this comment.
🚫 [golangci] reported by reviewdog 🐶
File is not properly formatted (gci)
| // in main.go's buildShardGroups; this helper short-circuits to the | ||
| // test-only fixture without spinning up a real Raft group. | ||
| // | ||
| //nolint:unparam // shardGroupID is currently always 1 in tests but |
There was a problem hiding this comment.
🚫 [golangci] reported by reviewdog 🐶
File is not properly formatted (gci)
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
🧹 Nitpick comments (1)
kv/fsm_composed1_test.go (1)
32-35: ⚡ Quick winDrop the new
//nolint:unparamand refactor the helper instead.This suppression is avoidable in new test code: either bake in the single currently used group ID, or make the group ID vary through actual table cases when you need that coverage.
As per coding guidelines, "Avoid
//nolintannotations — refactor 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 `@kv/fsm_composed1_test.go` around lines 32 - 35, Remove the //nolint:unparam annotation and refactor newComposed1FSM to stop accepting the unused shardGroupID parameter: either bake the single used group ID (1) directly into newComposed1FSM (replace the shardGroupID parameter with the constant 1 inside the function) and update all call sites to call newComposed1FSM(t, e) accordingly, or convert the tests that need varying group IDs into table-driven cases that construct the FSM with different explicit group IDs (so the parameter becomes used). Ensure all references to function newComposed1FSM are updated and delete the //nolint comment.
🤖 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 `@distribution/engine.go`:
- Around line 225-229: SetHistoryDepthForTest should validate the incoming depth
and reject non-positive values to fail fast; inside
Engine.SetHistoryDepthForTest (protected by e.mu), add a check like if depth <=
0 { panic("SetHistoryDepthForTest: depth must be > 0") } (or return an
error/report) before assigning e.historyDepth so recordHistorySnapshotLocked and
the eviction path never encounter an empty historyOrder; update any tests that
call SetHistoryDepthForTest to provide positive depths.
In `@kv/fsm.go`:
- Around line 582-589: verifyComposed1 currently only short-circuits when
f.routes == nil but the documented behavior says shardGroupID == 0 should also
bypass; update kvFSM.verifyComposed1 to return nil immediately when
f.shardGroupID == 0 (before any route/version checks) so callers that install
routes before setting shardGroupID preserve the legacy skip-for-group-0
behavior; keep the existing observedVer handling unchanged.
---
Nitpick comments:
In `@kv/fsm_composed1_test.go`:
- Around line 32-35: Remove the //nolint:unparam annotation and refactor
newComposed1FSM to stop accepting the unused shardGroupID parameter: either bake
the single used group ID (1) directly into newComposed1FSM (replace the
shardGroupID parameter with the constant 1 inside the function) and update all
call sites to call newComposed1FSM(t, e) accordingly, or convert the tests that
need varying group IDs into table-driven cases that construct the FSM with
different explicit group IDs (so the parameter becomes used). Ensure all
references to function newComposed1FSM are updated and delete the //nolint
comment.
🪄 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: defaults
Review profile: CHILL
Plan: Pro
Run ID: af79a132-4d95-4f0c-b28e-0e8008f5f03d
📒 Files selected for processing (4)
distribution/engine.gokv/fsm.gokv/fsm_composed1_test.gokv/route_history.go
| func (e *Engine) SetHistoryDepthForTest(depth int) { | ||
| e.mu.Lock() | ||
| defer e.mu.Unlock() | ||
| e.historyDepth = depth | ||
| } |
There was a problem hiding this comment.
Reject non-positive history depths here.
Passing depth <= 0 makes the next recordHistorySnapshotLocked() hit the eviction path with an empty historyOrder, so the helper panics later with an index-out-of-range instead of failing fast at the call site.
Suggested fix
func (e *Engine) SetHistoryDepthForTest(depth int) {
e.mu.Lock()
defer e.mu.Unlock()
+ if depth <= 0 {
+ panic("SetHistoryDepthForTest: depth must be > 0")
+ }
e.historyDepth = depth
}📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| func (e *Engine) SetHistoryDepthForTest(depth int) { | |
| e.mu.Lock() | |
| defer e.mu.Unlock() | |
| e.historyDepth = depth | |
| } | |
| func (e *Engine) SetHistoryDepthForTest(depth int) { | |
| e.mu.Lock() | |
| defer e.mu.Unlock() | |
| if depth <= 0 { | |
| panic("SetHistoryDepthForTest: depth must be > 0") | |
| } | |
| e.historyDepth = depth | |
| } |
🤖 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 `@distribution/engine.go` around lines 225 - 229, SetHistoryDepthForTest should
validate the incoming depth and reject non-positive values to fail fast; inside
Engine.SetHistoryDepthForTest (protected by e.mu), add a check like if depth <=
0 { panic("SetHistoryDepthForTest: depth must be > 0") } (or return an
error/report) before assigning e.historyDepth so recordHistorySnapshotLocked and
the eviction path never encounter an empty historyOrder; update any tests that
call SetHistoryDepthForTest to provide positive depths.
| func (f *kvFSM) verifyComposed1(r *pb.Request) error { | ||
| if f.routes == nil { | ||
| return nil | ||
| } | ||
| observedVer := r.GetObservedRouteVersion() | ||
| if observedVer == 0 { | ||
| return nil | ||
| } |
There was a problem hiding this comment.
Honor the documented shardGroupID == 0 bypass.
kvFSM.shardGroupID is documented as “unset => short-circuit”, but verifyComposed1() only checks routes == nil. A partially wired caller that installs route history before the group ID will start rejecting every pinned txn against group 0 instead of preserving the legacy skip behavior.
Suggested fix
func (f *kvFSM) verifyComposed1(r *pb.Request) error {
- if f.routes == nil {
+ if f.routes == nil || f.shardGroupID == 0 {
return nil
}
observedVer := r.GetObservedRouteVersion()
if observedVer == 0 {
return nil🤖 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 `@kv/fsm.go` around lines 582 - 589, verifyComposed1 currently only
short-circuits when f.routes == nil but the documented behavior says
shardGroupID == 0 should also bypass; update kvFSM.verifyComposed1 to return nil
immediately when f.shardGroupID == 0 (before any route/version checks) so
callers that install routes before setting shardGroupID preserve the legacy
skip-for-group-0 behavior; keep the existing observedVer handling unchanged.
1 participant
Summary
Third milestone (M3) of the Composed-1 cross-group commit-time guard per
docs/design/2026_05_29_proposed_composed1_cross_group_commit_guard.md§M3.Wires the safety property at apply time using the M2 versioned-snapshot ring and the M1 ObservedRouteVersion field.
Stacked on PR #894 (M2 plumbing).
What's enforced
tla/composed/Composed.tla. Every write key of a Composed-1-pinned txn must be owned by THIS Raft group at the txn's observed catalog version. Refusal returnsErrComposed1Violation.ErrComposed1Violationwith a different diagnostic prefix (current-versionvsobserved-version) so the M4 retry path can distinguish.ErrComposed1VersionGCd. Per design doc §4.3, the not-found semantics is a hard retryable error, NOT a soft pass, because soft-pass would let the gate be bypassed exactly in the cases where the cross-version-read hazard is most likely.Short-circuits
Three legacy / not-applicable cases that the gate explicitly bypasses:
WithRouteHistory(legacy / test seam):routes == nil, gate returns nil.ObservedRouteVersion == 0(unpinned — pre-M1 caller, or 2PC ABORT request that doesn't carry the version): gate returns nil. This is what keeps M3 from regressing every caller that has not migrated to setOperationGroup.ObservedRouteVersion.Engine.Currentreturns(zero, false)— engine has no history (bare-struct test seam): the (b) fence falls through.Changes
distribution/engine.go— addsEngine.Current()returning the snapshot at the currentcatalogVersion. AddsSetHistoryDepthForTestas the cross-package test seam that lets kv-side tests trigger eviction without bypassing the package boundary (claude review on PR kv(composed1): M2 — versioned-snapshot ring + kvFSM RouteHistory wiring #894 — fragile-but-test-local lock contract documented inline).kv/fsm.go— definesErrComposed1ViolationandErrComposed1VersionGCdsentinels with the wrapped-error diagnostic shape M4 retry will use. AddsverifyComposed1andverifyOwnerFromSnapshot. WiresverifyComposed1intohandleTxnRequestat the top so PREPARE / COMMIT / ABORT / NONE all pass through the gate (ABORT carriesObservedRouteVersion=0and falls through naturally).kv/route_history.go—RouteHistoryinterface gainsCurrent(). Adapter forwards todistribution.Engine.Current().Tests (
kv/fsm_composed1_test.go)TestVerifyComposed1_StaleObservedVersionWithMovedKeyFailsTestVerifyComposed1_ObservedVersionOlderThanRingFailsErrComposed1VersionGCdTestVerifyComposed1_ObservedPassesButCurrentDiffersFailsErrComposed1Violation(current-versiondiagnostic)TestVerifyComposed1_ObservedVersionZeroSkipsGateTestVerifyComposed1_NilRouteHistorySkipsGateVerification
go build ./...— cleango vet ./...— cleango test -race -count=1 ./kv ./distribution— 10.2 s + 1.0 s, passmake lint— 0 issuesSelf-review (5 lenses)
SnapshotAtandCurrenteach acquire and release in a single call.OwnerOfshort-circuits via the M2 round-1 break optimisation, so the per-mutation cost is bounded by the first non-covering gap rather than the full routes slice. Legacy callers (ObservedRouteVersion=0) pay one branch per commit and exit.tla/composed/Composed.tla'sCommitprecondition is now enforced at apply time; the §4.4 fence matchesComposed1a_CommitToCurrentOwnerfrom PR tla: Composed-1a current-version fence + currentfence_gap (#870 follow-up) #878.handleTxnRequesttests pass unchanged (their requests carryObservedRouteVersion=0from M1's behaviour-neutral default).Test plan
go test -race ./kv ./distributionmake lintResolves
The M3 row in the Composed-1 design doc.
Summary by CodeRabbit
Bug Fixes
Tests