[bootjp]

Summary

• Preserve an unknown attempt decision after a lost primary commit reply, including Raft leader loss with a pending proposal. Prepared secondaries remain for decision-based lock resolution; typed definitive apply verdicts and pre-append leadership rejection still abort them.
• Treat nil commit responses as unknown on single- and multi-group paths. This coordinator behavior also affects the default non-strict transaction path.
• Add persisted process-kill tests for generation fencing and two-group primary decisions, a direct-store secondary recovery assertion, and mounted Raft-node SIGKILL/restart checks for acknowledged FUSE mutations and fsync.
• Measure legacy and strict FUSE write/fsync throughput, p50/p95/p99 latency, and hot-inode worker fairness over three trials. Add a two-group benchmark that waits for both Raft listeners and a responsive mount. Expose strict journal session, pending and retained-byte gauges.

Validation

• Targeted go test -race for coordinator and filesystem passed; changed-code golangci-lint and actionlint reported zero issues.
• All 23 jobs passed in Jepsen stress run 40322309957 at daebcb7, including mounted node crash, SQLite, filesystem workloads and paired single-group benchmarks.
• The first two-group benchmark in run 40325784929 failed with a transaction lock. Run 40327671052 returned EIO while the catalog watcher still reported a local listener connection refusal. The revised readiness check and expanded crash test are running in stress run 40328639750 at 48755a5. A passing two-group measurement is not yet established.
• Current evidence and open gates are recorded in docs/design/2026_10_26_fuse_strict_rollout_evidence.md.

Risk and rollout

• Strict mode remains opt-in. Unknown primary decisions may delay conflicting operations until lock resolution. Pending proposals failed after leader loss may already be appended; any caller that retries a non-transactional write in that window needs idempotency or an explicit outcome check.
• Median strict throughput was about 61% of legacy in the measured single-group cases. Multi-group crash failpoints, broader no-retry mounted durability evidence, numerical canary limits, and maintainer approval remain required before default-on rollout.

Author: bootjp

[coderabbitai]

Caution

Review failed

The pull request is closed.

Finishing Touches

📝 Generate docstrings

• Commit to this branch
• Create a new PR

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

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.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (1b21dce):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (a33dad1):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (daebcb7):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[bootjp]

@codex review

Please review current HEAD daebcb7 and the full PR diff, with particular attention to ambiguous primary commit decisions and the new crash and benchmark jobs. Report actionable findings for this SHA.

[bootjp]

@claude review

Please review current HEAD daebcb7 and the full PR diff. The prior review on PR #1341 could not fetch the base; please report the actual scope reviewed and any actionable findings. Emit a completion marker only after reviewing the complete diff.

[claude]

Claude finished @bootjp's task in 38s —— View job

---

Review of HEAD daebcb7 (full diff vs origin/main)

Scope reviewed: all 7 changed files (+548/−17), diffed against origin/main...HEAD. The base fetched fine here, so the earlier #1341 base-fetch problem did not recur. benchmark-fuse.py and the design doc I only skimmed, since they are evidence and tooling and not on the commit path. I did not run tests or the new workflows.

Findings

1. Medium: every non-conflict primary-commit error is now "outcome unknown" (kv/sharded_coordinator.go:~1993-2005)

The new condition only aborts when the error is ErrWriteConflict. All other errors from commitPrimaryTxn are wrapped as ErrTransactionOutcomeUnknown and the prepared intents are left in place. That is correct for a lost response or an ambiguous Raft result. It is too broad for errors that are provably pre-commit:

• txnGroupForID failing, or primaryGroupIDForKey returning ErrInvalidRequest, in commitPrimaryTxn.
• Definitive FSM rejections, such as route-version or write-fence mismatches, ErrNotLeader before the proposal, and context cancelled before send.

Consequences:

• Prepared secondaries now wait for LockResolver expiry instead of being aborted immediately, which is a latency and contention regression for these cases.
• Callers that check errors.Is(err, ErrTransactionOutcomeUnknown) skip their retry loops (kv/sharded_coordinator.go:1210, kv/coordinator.go:652/703/832). Retryable, definitive rejections therefore stop being retried.

Suggested fix: make the abort-vs-retain decision allow-list based. Abort on known definitive errors, and treat as unknown only errors that may have reached Raft. kv/transaction.go:177 already draws that distinction. Please add a table-driven test with a definitive non-conflict error, for example a route-version mismatch, asserting it aborts and is not classified as unknown.

2. Low: this behavior change is not limited to strict mode

• dispatchSingleShardTxn previously returned an empty CoordinateResponse{} for a nil response and now returns ErrTransactionOutcomeUnknown. The same goes for commitPrimaryTxn.
• The dispatchMultiShardTxn change applies to all ShardedCoordinator users, including legacy/non-strict adapters.
• The PR description says only the strict path is opt-in. Please state that this applies to the default path too, or confirm that no adapter or Transactional implementation legitimately returns (nil, nil).

3. Low: the node-crash script is fragile on restart (scripts/test-fuse-node-crash.py)

• It reads node 1's argv from /proc/<pid>/cmdline and appends --filesystemStrictRecover. If the original process already carried that flag, or if the flag is not idempotent, the restart will fail. It also assumes the first line of the pid file is the node being killed.
• It checks restarted.poll() only once, right after await_contents(paths[0], …). A restarted node that crashes later is not detected.
• After the SIGKILL, the FUSE mount on node 1 is a dead mount until the process restarts. await_contents swallows OSError, which is fine, but a hang is bounded only by the 90s deadline, and the first read_bytes may block on the stale mount. The workflow's timeout-minutes: 5 covers the worst case.

4. Nit: workflow

• "${STRICT_FLAGS[@]}" with an empty array is safe on bash ≥ 4.4 (ubuntu runners), but would break under set -u on older bash.
• Upload of the Jepsen history is now always(), with if-no-files-found: ignore. That is fine, but it raises artifact volume on every green run (7-day retention). Confirm that is intended.

Positives

• The new tests pin both sides of the abort decision. TestStrictLostPrimaryCommitReplyDoesNotAbortPreparedParticipants and TestLostPrimaryReplyResolvesPreparedSecondaryFromDurableDecision check that a lost reply preserves the intents and that LockResolver finishes the commit from the durable primary decision. TestStrictDefinitivePrimaryConflictAbortsPreparedParticipants covers the opposite case.
• The process-kill generation-fence test covers fencing after SIGKILL, including the stale attempt's Publish returning ErrOperationGeneration.

TLA+ divergence (kv/sharded_coordinator.go)

No change to HLC issuance, ceiling renewal, or Observe. The change is confined to the transaction abort/commit decision path, so I see no HLC-4 divergence. The OCC-3 lock-resolution contract is respected, because the intents are retained for LockResolver. Finding 1 narrows that behavior further.

Verdict

Not clean: finding 1 is worth fixing, with a regression test, before merge. The rest are optional.

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-26T19:42:20.585789Z	295b466	Draft marked ready
🔒 Security Review	✅ Completed 2026-10-26T19:43:04.997340Z	295b466	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Drain benchmark results before joining worker processes

When --writes is large enough for a worker's latency samples to exceed the multiprocessing queue's pipe buffer, this join-before-read ordering deadlocks: the worker cannot exit until its queue feeder finishes flushing, while the parent does not call results.get() until after joining every worker. Consequently, a completed benchmark is terminated after 300 seconds and reported as timed out instead of producing results. This is reproducible with 30,000 samples even when write/fsync work is stubbed to finish immediately. Consume the worker results before joining, or drain them concurrently.

Useful? React with 👍 / 👎.

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (9d3468d):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[bootjp]

@codex review

Please review commit 9d3468d, including the typed primary decision classification, journal metrics, and crash-script changes.

[bootjp]

@claude review

Please review commit 9d3468d and confirm whether the earlier concern about deterministic primary commit failures is resolved.

[claude]

Claude finished @bootjp's task in 22s —— View job

---

Review of 9d3468d

Scope: I read the full code diff against origin/main at HEAD 9d3468de3af83672d6e5252acede2caab9d50dfb: the coordinator, the journal stats, the metrics, the main.go collector and the key helper. I read the new coordinator tests. I only skimmed the Python scripts and the design doc, and I did not run tests, lint or workflows. This is not a full-scope review, so I am not emitting a completion marker.

Earlier concern: resolved, for the cases I traced.
primaryCommitDefinitelyRejected (kv/sharded_coordinator.go, new in this commit) is an allow-list. It returns true only for these errors:

• isRawApplyVerdict errors. These include ErrWriteConflict through store.IsApplyVerdict, ErrInvalidRequest, the route-fence and write-timestamp verdicts, ErrComposed1VersionGCd and ErrTxnLocked.
• ErrComposed1Violation.
• ErrNotLeader and ErrLeadershipTransferInProgress.

Anything else is wrapped as ErrTransactionOutcomeUnknown and the intents are kept.

• The two pre-send failures I had flagged before, txnGroupForID and primaryGroupIDForKey, both wrap ErrInvalidRequest. That is a verdict, so they still abort.
• An error that already carries ErrTransactionOutcomeUnknown is never treated as rejected, even when it also wraps a conflict. A test covers this.
• TestPrimaryCommitDecisionClassification and TestPrimaryRouteVerdictAbortsPreparedParticipants lock in both sides.

Remaining notes (none blocking):

1. Cancelled context or deadline before the send. This now counts as unknown, so the intents wait for LockResolver. It is safe, but it is a latency cost when a caller cancels. It is not provably pre-append, so I would leave it.
2. Retry cost on ErrNotLeader. Aborting on ErrNotLeader assumes the error is returned only before the proposal was appended. If any path can return it after an append (a leader change while waiting for apply), a commit could be aborted. Please confirm the engine never does that, or add a comment saying so.
3. Default path. Nil responses now return ErrTransactionOutcomeUnknown on both the single-group and multi-group paths. That affects the default non-strict path. The PR body says so, and the two non-nil tests cover it. Confirm that no Transactional implementation legitimately returns (nil, nil).
4. Journal stats. ListOperationJournalStats scans every session row once per placement interval, so it costs O(sessions). Closed sessions are included in the totals, so a leaked closed session shows up in the gauges, which is what you want for canary observation. MaxBytes is summed but not exported. That is fine.
5. Benchmark deadlock. Codex's P2 on scripts/benchmark-fuse.py (join before draining the queue) is valid. The workers can hang once their sample lists exceed the pipe buffer. Drain results before joining, or read one result per worker first. Per the repo convention, a failing test should come with the fix.

Verdict: The primary-commit classification concern is resolved. Please fix note 5 and confirm note 2 before merging.

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (2e57c65):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Chef's kiss.

Reviewed commit: 9d3468de3a

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

🛡️ Codex Security Review · Automatically triggered

Security review completed. No security issues were found in this pull request.

Reviewed commit: 9d3468de3a

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

• You comment "@codex security review"
• A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (473fc5b):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[bootjp]

@codex review

Please review the current head 473fc5b. The benchmark queue finding is fixed with a large-sample regression, and pending Raft proposals now return ErrLeadershipLost.

[bootjp]

@claude review

Please review current head 473fc5b, including the engine leader-loss path, process-kill decision test, and benchmark queue fix. Please perform a full-scope review.

[claude]

Claude finished @bootjp's task in 23s —— View job

---

Review of HEAD 473fc5b

Scope: I read the full diff against origin/main, including the engine change, the coordinator, the Python scripts and the file list. I did not run tests, lint or workflows. I only skimmed the Go filesystem tests, the metrics and the design doc.

Resolved since earlier reviews

• Leader-loss path: refreshStatus now fails pending proposals with ErrLeadershipLost instead of errNotLeader (internal/raftengine/etcd/engine.go:4036). primaryCommitDefinitelyRejected does not allow-list ErrLeadershipLost, so a pending proposal that loses leadership is now classified as outcome-unknown and the prepared intents are kept. That closes my earlier concern about ErrNotLeader being returned after an append.
• Benchmark queue: collect_worker_results reads one result per worker before joining, which fixes the deadlock. The regression test sends 30,000 samples per worker through the real queue.

Findings

1. Medium: no engine-level test for the leader-loss change. The diff has no test change under internal/raftengine/etcd. A grep of that package's tests finds no assertion that failPending after a leader→follower transition yields ErrLeadershipLost and not ErrNotLeader. The repo convention is a test with the fix. The coordinator tests may inject the error directly and so would not catch a revert in the engine. Please add an engine test, for example a pending proposal that is failed when status leaves StateLeader.
2. Low: wider behavior change from the engine edit. ErrLeadershipLost is handled as a transient/retryable leader error (kv/coordinator.go phrase list, kv/lease_state.go, adapter/redis.go:430), so the common retry paths keep working. Callers that check ErrNotLeader specifically to mean "definitely not applied" lose that guarantee for this transition, which is correct. Please grep for such callers, for example forwarding code that treats ErrNotLeader as safe to retry on another node. Retrying a proposal that may already be in the log is only safe if the operation is idempotent. This is the same trade-off as the nil-response change, and the PR description should mention it.
3. Low: scripts/test-fuse-node-crash.py
   • The pid-file's first line is assumed to be the node being killed.
   • The restarted-process liveness check covers only about 5 seconds.
   • Reading the original argv from /proc is sound, and the empty-argument handling is a good catch.
4. Nit: percentile sorts the full list on each call. It is called three times per summary, which is negligible at these sizes.
5. Carried from earlier reviews: the (nil, nil) → ErrTransactionOutcomeUnknown change also applies to the default non-strict path. The PR body states this. Please confirm no Transactional implementation returns (nil, nil) on success.

TLA+ divergence: none. The change does not touch HLC issuance, ceiling renewal or Observe. It only changes the abort/commit decision when the primary's outcome is ambiguous, and the intents stay for LockResolver, which matches the OCC-3 contract.

Verdict: The correctness fixes look right. Please add the engine regression test from finding 1 before merging. The other items are optional.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Already looking forward to the next diff.

Reviewed commit: 473fc5b7d7

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (ed5efef):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (711a7ba):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (fd1bca4):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[bootjp]

@codex review

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. 👍

Reviewed commit: fd1bca464d

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

🛡️ Codex Security Review · Automatically triggered

Security review completed. No security issues were found in this pull request.

Reviewed commit: fd1bca464d

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

• You comment "@codex security review"
• A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (3e3f4ab):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (7323b1f):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (a8a413e):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[bootjp]

@codex review

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Hooray!

Reviewed commit: a8a413e3fc

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (2f542c4):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (67111e7):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (295b466):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.

[bootjp]

@claude review
@codex review

Please review the current head of #1342 (295b466a) for merge safety. In particular:

1. Check the changes to primary transaction decisions, Raft leadership-loss errors, and lock resolution on the default non-strict path. A missing primary reply must not cause prepared secondaries to abort after a possible commit, and a definitive rejection must not leave them pending indefinitely.
2. Check strict operation-journal accounting across admission, generation fencing, terminal transitions, and ACK retirement, especially when the record and session are on different groups. Identify any path that can make a non-retired record's reservation exceed the session's retained usage, or cause a successful operation to lose its effect.
3. Check cancellation, lost replies, process/node crashes, and recovery for durable pending decisions and eventual journal drain.

The 30-minute strict SQLite Jepsen run 40362040528 ended :unknown after ACK accounting errors and FUSE I/O errors; the matched legacy run 40378658363 passed. Please distinguish actionable merge blockers from the separate default-on strict rollout gates, and cite file/line evidence for any finding.

[claude]

Claude finished @bootjp's task in 1m 10s —— View job

---

Review of HEAD 295b466 (merge-safety pass)

Scope and limits. Base fetch is shallow here (git diff origin/main...HEAD has no merge base), so I used the two-dot diff against origin/main, which matches the PR's 41 files and +1993/−113. I read the production Go changes in full: coordinator, ShardStore.primaryTxnStatus, the Raft engine, and the journal (operation_journal*.go, operation_session.go, service.go). I did not run tests or CI. I did not read the Python scripts, the workflow, the metrics, main.go, or all the new tests. I'm not emitting a completion marker.

Verdict

No confirmed merge blocker in the Go changes I read. I could not reproduce or explain the strict SQLite :unknown result from code reading. Item 2 below is the one thing I'd settle before merge or label as an explicit open gate.

1. Primary decisions and leadership-loss errors (default path)

• Lost primary reply no longer aborts secondaries. primaryCommitDefinitelyRejected (kv/sharded_coordinator.go:~2029) is an allow-list: apply verdicts, ErrComposed1Violation, ErrNotLeader, and ErrLeadershipTransferInProgress. Everything else, including a nil reply, ErrLeadershipLost and errClosed, is wrapped as ErrTransactionOutcomeUnknown, and the intents are kept. I traced failPending in engine.go. Leader loss now returns ErrLeadershipLost (line 4036), and shutdown and fail paths return errClosed (4075, 4137). All of those are classified unknown. errNotLeader now only comes from pre-append checks (lines 1168, 2038). That is consistent with the allow-list.
• A definitive rejection does not leave secondaries pending. Those errors take the abort path with a detached, bounded context (:~1993-2001). If that abort itself fails or times out, the secondary relies on lease expiry. primaryTxnStatus (kv/shard_store.go:~5421-5440) now returns Pending while the secondary lock is live and aborts the primary once it is expired. That is bounded and strictly more conservative than the old immediate RolledBack when the primary had no lock. The cost is that reads of such a key can see ErrTxnLocked until the secondary TTL passes.
• Callers of the old ErrNotLeader for pending proposals. Retry paths that treat "leadership lost" as transient (kv/coordinator.go, kv/lease_state.go, adapter/redis.go, adapter/distribution_server.go) may now retry a non-transactional proposal that was already appended. The PR body already says idempotency is needed. I recommend recording this under Risk as a default-path behavior change, not only a strict one.

Non-blocking points on this item

• txnLockExpired uses hlcWallNow() (shard_store.go:~5477). It is pre-existing, but CLAUDE.md says lease/expiry decisions must not use the local wall clock. The new Pending-vs-abort decision now leans on it for the absent-primary-lock case too.
• I did not trace whether a late primary COMMIT is fenced by the rollback record that tryAbortExpiredPrimary writes. Previously the same abort was reached, so this is not a regression, but I did not confirm the fence.

2. Journal accounting across groups (the ACK failure)

I could not identify the first invalid transition. What I checked:

• Record is the 2PC primary and the session is a secondary. commit() (operation_journal.go:~76-90) picks the only IsOperationKey element as primary, and IsOperationKey matches only exact record keys (internal/fskeys/keys.go:78). So the record commits first and the session can lag, which fits the PR's "mixed visibility" description.
• Admission, generation fence and ACK each commit record and session together with both keys in the read set. Reservation accounting is symmetric: reserveOperation (:~419), prepareGenerationFence (operation_journal_exec.go:~98-109, record and session both gain operationFenceReservation), and reserveAckRetirement (:~661-676). I found no single-sided update.

Concerns

• (Medium, unverified) The session.retired() early return in reserveAckRetirement (operation_journal_exec.go:~662) can hide the symptom without proving the cause. acknowledgeOnce → terminalAt finds the record present and the session retired, returns ErrOperationRetired, and Acknowledge returns nil. If that state ever occurs with the record still durable, the record stays and is never deleted, while the session no longer counts it. That is exactly the "non-retired record reservation exceeds session usage" shape, now silent. The evidence doc says the earlier hypothesis that duplicate ACK caused it is unproven, so this change should not be taken as the fix. Please add a split-group test that drives ACK with the session committed and the record deletion not yet visible, and asserts the record is eventually deleted. At minimum, log when this branch is taken so the canary can see it.
• (Low) Journal-drain for that case. I did not find a path that deletes a leaked terminal record whose sequence is already retired. A reaper or an assertion would cover it. I did not search for one exhaustively.
• Effect loss. I found no path where a successful operation loses its effect. operationDecisionContext (operation_contention.go) detaches cancellation for the publish and reject loop, with a bounded budget, so cancelled FUSE requests still reach a durable decision.

3. Cancellation, lost replies, crashes, drain

• Pending proposal on leader loss: unknown, intents kept, covered by TestLeaderLossLeavesPendingProposalOutcomeUnknown per earlier reviews.
• retryJournalLocked (operation_journal.go:~102) retries only ErrTxnLocked, never an unknown outcome, with a bounded budget (operationCASRetries). journalCommitPermit is context-aware, which resolves my earlier cancellation note. It is per Service, so cross-mount collisions on a shared session row still depend on the retry loop.
• isDefinitiveWriteConflict (service.go:~758) now treats ErrTxnLocked as retryable, excluding unknown outcomes. That is consistent.
• Crash recovery: the new SIGKILL tests cover generation fence, a two-group primary decision, and mounted node restart. SIGKILL does not prove fsync behavior, as the doc says.

Merge blockers vs rollout gates

• Possible blocker to settle before merge: item 2, a regression test or logging for the "session retired while record still present" branch, because it can mask corruption. If you treat strict mode as opt-in and unreleased, this can instead be recorded as an explicit gate.
• Not merge blockers (default-on gates): the 30-minute strict SQLite :unknown (40362040528) versus the matched legacy pass (40378658363), the ACK reservation mismatch root cause, the HLC ceiling exhaustion, the multi-group crash failpoints at PREPARE and secondary apply, and numerical canary limits. These match the doc's own list. The default non-strict path changes are reasonable and conservative, per item 1.

TLA+ divergence: none. HLC issuance, ceiling renewal and Observe are untouched; retaining intents for the lock resolver matches OCC-3.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Keep them coming!

Reviewed commit: 295b466a59

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

🛡️ Codex Security Review · Automatically triggered

Security review completed. No security issues were found in this pull request.

Reviewed commit: 295b466a59

View security finding report

Only the user who started this review can view the report in Codex.

ℹ️ About Codex security reviews in GitHub

This is an experimental Codex feature. Security reviews are triggered when:

• You comment "@codex security review"
• A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review

Once complete, Codex will leave suggestions, or a comment if no findings are found.

[github-actions]

TLA+ spec divergence review (auto-triggered)

This PR touches files that the TLA+ safety spec has an anchor on (per
docs/design/2026_05_28_implemented_tla_safety_spec.md §3),
so an AI review is requested below to verify the implementation has not drifted
from the model.

Anchored files changed in this PR head (295b466):

• kv/sharded_coordinator.go

What to check, by subsystem:

• kv/hlc*.go — Next() must respect the HLC-4 preconditions (i)/(ii)/(iii) from the design doc: bounded skew, logical-counter handoff on leader change (strategy (c) Observe(MaxAppliedHLC)), and the commit-time ceiling fence (fail-closed when wall_now >= physicalCeiling). Any change to the bit layout (48/16), the CAS loop, or the ceiling getter/setter is in scope.
• kv/coordinator.go, kv/sharded_coordinator.go — RunHLCLeaseRenewal, hlcRenewalInterval, hlcPhysicalWindowMs constants, and the new-term detection that calls Observe(fsm.MaxAppliedHLC()) (strategy (c)). Any change to renewal cadence, group selection, or fail-closed behaviour is in scope.
• kv/transaction.go, kv/lock_resolver.go — OCC commit-ts assignment, lock-map encoding (key, lock_ts) -> start_ts, and the LockResolver action OCC-3 depends on. (M2 spec will land OCC-1..OCC-5; until then the spec doc §5.2 is the contract.)
• kv/fsm.go — FSM apply of HLC lease entries (SetPhysicalCeiling), and any future MaxAppliedHLC() accessor that strategy (c) needs.
• store/mvcc_store.go — version visibility, snapshot install, and the MVCC-1..MVCC-4 invariants (M3 scope).
• distribution/** — route catalog versioning, SplitRange atomicity, and CatalogWatcher async fan-out (M4 scope).

If the change is correct but requires a spec update, edit tla/hlc/HLC.tla (or the corresponding M2..M5 module once landed) and the design doc in the same PR. The tla-check workflow runs the TLC model check on the same paths.

---

@claude review please verify TLA+ spec divergence per the checklist above.

@codex review please verify TLA+ spec divergence per the checklist above.