Complete centralized TSO runtime operations

[bootjp]

Summary

• add atomic runtime reload for the one-way legacy -> shadow -> cutover -> phase-d sequence
• preserve durable cutover and Phase-D overrides while rejecting operator-requested rollback and phase skipping
• export bounded TSO latency, shadow divergence, mode, reload, and durable-state metrics with checked Prometheus alerts
• add a 16-writer, 1/3/8-way fanout benchmark and record three-run batch-size evidence
• promote the centralized TSO design from partial to implemented and update all references

Safety

Legacy mode keeps the coordinator allocator logically absent, preserving existing HLC fallback callers. Cutover activation is published before batch invalidation, durable group-0 markers can only advance the local mode, and invalid reloads leave the active allocator unchanged.

Validation

• go test ./kv ./monitoring . -count=1
• go test -race ./kv ./monitoring . -count=1
• golangci-lint run ./... --timeout=5m --allow-parallel-runners
• go test ./kv -run ^'$' -bench ^'BenchmarkTSOWriteFanout$' -benchmem -benchtime=1s -count=3\n- promtool check config monitoring/prometheus/prometheus.yml (8 rules)\n- go test ./store -count=1 -timeout=15m\n- git diff --check\n- caller audit across allocator providers, coordinator fields, runtime flags, activation, and Phase-D state\n- zero references to the former partial design path

[bootjp]

Validation evidence at d94ba5b63c9f4b3f296a158494533eb1de1d2370:

• affected unit and latest-code race suites pass
• repository lint passes with zero findings
• Prometheus config and all 8 TSO alert rules pass promtool
• three-run 16-writer fanout benchmark is recorded in docs/centralized_tso_operations.md
• caller audit found no unresolved legacy-fallback or Phase-D paths
• former partial design path has zero references

@codex review

[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 (d94ba5b):

• kv/coordinator.go
• 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.

[coderabbitai]

Important

Review skipped

Auto reviews are disabled on base/target branches other than the default branch.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro

Run ID: ed61757b-ed87-4e72-aa0f-f3e6d35d17be

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

---

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.}

[chatgpt-codex-connector]

To use Codex here, create a Codex account and connect to github.

[gemini-code-assist]

Code Review

This pull request implements runtime mode changes, configuration reload, and production monitoring for the centralized Timestamp Oracle (TSO). It introduces a TSORuntimeController to manage safe, one-way transitions between TSO modes, along with a DynamicTimestampAllocator for atomic allocator swapping. Additionally, it adds Prometheus metrics, alert rules, and a concurrent write-fanout benchmark. Feedback on the changes suggests improving error handling in ValidateDurableTimestamp by explicitly checking for a nil allocator and returning ErrTSOAllocatorRequired instead of failing the type assertion.

Important

The consumer version of Gemini Code Assist on GitHub is being sunset. Starting June 18, 2026, new organization installations will be blocked, and all code review activity will officially cease on July 17, 2026.
For more details on the timeline and next steps, please review the Help Documentation.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: d94ba5b63c

ℹ️ 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 (1b3fa86):

• kv/coordinator.go
• 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]

To use Codex here, create a Codex account and connect to github.

[bootjp]

Evidence at current head 1b3fa86327e343409824340071053942d089412a:

• integrated checksum/cache hardening: tla-tools revalidates cached artifacts and pins stable tla2tools.jar v1.7.4 at SHA-256 936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88; the full local make tla-check safe/gap suite passed
• corrected the centralized TSO design back to Status: Partial and 2026_04_16_partial_centralized_tso.md until Implement centralized TSO phase D #1114 current-head P1 safety findings and final audits clear; rg found zero references to the premature implemented path
• GitHub CI is fully green: build, unit, Jepsen, golangci-lint, TLA model check, and spec-divergence trigger
• affected unit and race suites, repository lint, Prometheus config plus all 8 TSO alert rules, and the three-run 16-writer fanout benchmark passed locally
• caller audit covered coordinator and sharded-coordinator persistence timestamp paths plus adapter read-modify-write helpers; final Phase-D caller audit will be repeated after the corrected Implement centralized TSO phase D #1114 dependency head is merged

@codex review

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 1b3fa86327

ℹ️ 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 (ef59050):

• kv/coordinator.go
• 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]

To use Codex here, create a Codex account and connect to github.

[bootjp]

Evidence for current HEAD ef59050f139fd931ebfb9413f7b176e4f5fc4952 (parent c8018656811d1a9511f0495b4c14a85678452bce):

• PR history is one GitHub-verified commit; author and committer are bootjp <contact@bootjp.me>.
• Persistent reload failures now increment elastickv_tso_mode_reload_total on every failed poll; duplicate suppression only affects logs.
• No-op reloads pass through ApplyMode and refresh both durable-state gauges.
• A consensus cutover/Phase-D marker immediately overrides a stale legacy slot during allocator resolution; the route is promoted monotonically, so concurrent observation cannot lower Phase D.
• Caller audit covered Coordinate and ShardedCoordinator, startup/keyviz provider wrappers, Internal forwarded writes, DynamoDB item-write retries, S3 transaction timestamps, Redis transaction/compaction timestamps, and all direct DynamicTimestampAllocator operations. All resolve through TimestampAllocatorThrough / NextTimestamp*Through; the coordinator-level regression test proves cutover-active legacy mode cannot fall back to HLC.
• The central M1-M8 scope is complete, so the design was promoted with a rename to docs/design/2026_04_16_implemented_centralized_tso.md; header/status and all references were updated, intentional future extensions remain explicit, and rg reports zero old partial/proposed path references.
• The stable TLA+ v1.7.4 checksum/cache revalidation remains included. make tla-check passed all safe/gap outcomes; current-head GitHub tla-check is already green.
• Local verification passed: go test ./kv -count=1 -timeout=15m; focused go test -race ./kv; go test . ./monitoring; go test ./... -run ^$; make gen; full golangci-lint with 0 issues; docker compose -f monitoring/docker-compose.yml config --quiet; and git diff --check.
• The 8-rule alert blob is identical to the prior promtool-validated blob and is now mounted from monitoring/prometheus/rules; current Docker compose parsing passes.
• The 16-writer fanout benchmark was rerun three times on Go 1.26.5 / Apple M1 Max. Batch 256 medians for fanout 1/3/8 are 8.92/17.30/39.43 us per operation with p99 0.000292/1.272/1.302 ms; full evidence is recorded in the operations runbook.
• Review roots 3610385986, 3610397253, 3610439459, 3610439462, and 3610439463 were replied to and resolved.

@codex review

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: ef59050f13

ℹ️ 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]

Preserve runtime allocator for forwarded writes

When a node starts with --tsoModeFile containing legacy, this resolves the DynamicTimestampAllocator to nil; main.go's internalTimestampOptions is evaluated once at startup and therefore does not pass any allocator to adapter.Internal. After the intended runtime rollout reloads shadow, cutover, or phase-d, forwarded writes still run adapter.Internal.nextTimestamp with a nil allocator and use the HLC fallback, so data-group leaders can keep issuing non-TSO timestamps after cutover. Keep a stable runtime-aware allocator in the Internal path rather than snapshotting the currently active slot.

Useful? React with 👍 / 👎.

[chatgpt-codex-connector]

Allow Phase D after a durable cutover override

If a running node misses the local cutover reload but observes the durable cutover marker, then the shared mode file may already contain phase-d; with current still legacy or shadow, this check rejects that reload as a skipped phase even though durableFloor is already cutover. The node can be stuck rejecting every poll of the cluster-wide phase-d file until operators temporarily roll that file back to cutover, so use the durable floor as the effective current step before enforcing adjacency.

Useful? React with 👍 / 👎.