Skip to content

distribution: add split HLC route codec#1066

Open
bootjp wants to merge 5 commits into
mainfrom
design/hotspot-split-hlc-catalog
Open

distribution: add split HLC route codec#1066
bootjp wants to merge 5 commits into
mainfrom
design/hotspot-split-hlc-catalog

Conversation

@bootjp

@bootjp bootjp commented Jul 11, 2026

Copy link
Copy Markdown
Owner

Author: bootjp

Summary

  • Add SplitAtHLC to durable route descriptors for hotspot split cooldown reconstruction.
  • Encode/decode route descriptor v2 records with a strict SplitAtHLC tail while preserving v1 decode compatibility and forward-version tail tolerance.
  • Cover v1/v2/v3 codec cases plus clone/equality preservation.

Validation

  • go test ./distribution -run 'Test.*RouteDescriptor|TestCatalog' -count=1\n- go test ./distribution -count=1\n- go test ./... -run '^$' -count=1\n- golangci-lint run ./distribution --timeout=5m\n- git diff --check\n- git verify-commit HEAD

@coderabbitai

coderabbitai Bot commented Jul 11, 2026

Copy link
Copy Markdown

Warning

Review limit reached

@bootjp, you've reached your PR review limit, so we couldn't start this review.

Next review available in: 17 minutes

Enable usage-based reviews in Billing to review now. Otherwise, wait until the next included review is available.
You're only billed for reviews past your plan's rate limits ($0.25/file).

How can I continue?

After more reviews become available, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews.

How do review limits work?

CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability.

For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window.

Please refer docs for additional details.

Review details
⚙️ Run configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro

Run ID: 6fca5b41-c546-4da9-a980-df6497400c5f

📥 Commits

Reviewing files that changed from the base of the PR and between cd58354 and d0a7c4c.

⛔ Files ignored due to path filters (2)
  • proto/distribution.pb.go is excluded by !**/*.pb.go
  • proto/internal.pb.go is excluded by !**/*.pb.go
📒 Files selected for processing (15)
  • adapter/distribution_server.go
  • adapter/distribution_server_test.go
  • adapter/internal.go
  • adapter/internal_test.go
  • distribution/catalog.go
  • distribution/catalog_test.go
  • kv/commit_ts_patch.go
  • kv/commit_ts_patch_test.go
  • kv/coordinator.go
  • kv/coordinator_txn_test.go
  • kv/sharded_coordinator.go
  • kv/sharded_coordinator_txn_test.go
  • kv/transcoder.go
  • proto/distribution.proto
  • proto/internal.proto

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

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

@github-actions

Copy link
Copy Markdown
Contributor

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 (4e3bff7):

  • distribution/catalog.go
  • distribution/catalog_test.go

What to check, by subsystem:

  • kv/hlc*.goNext() 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.goRunHLCLeaseRenewal, 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

bootjp commented Jul 11, 2026

Copy link
Copy Markdown
Owner Author

Ready for review.

This implements the hotspot split catalog codec slice:

  • Add SplitAtHLC to RouteDescriptor.
  • Emit v2 records with a strict SplitAtHLC tail and keep v1 records decodable as SplitAtHLC=0.
  • Preserve SplitAtHLC through clone/equality helpers.

Validation:

  • go test ./distribution -run 'Test.*RouteDescriptor|TestCatalog' -count=1\n- go test ./distribution -count=1\n- go test ./... -run '^$' -count=1\n- golangci-lint run ./distribution --timeout=5m\n- git diff --check\n- git verify-commit HEAD\n\n@codex review

@chatgpt-codex-connector

Copy link
Copy Markdown

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

@gemini-code-assist gemini-code-assist Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Code Review

This pull request introduces a new SplitAtHLC field to the RouteDescriptor struct, upgrading the route codec version to V2. It updates the encoding, decoding, cloning, and equality logic to support this new field while maintaining backward compatibility with V1 route descriptors. Feedback was provided to optimize the decoding of SplitAtHLC by using binary.BigEndian.Uint64 instead of binary.Read to avoid reflection and heap allocations.

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.

Comment thread distribution/catalog.go Outdated
@chatgpt-codex-connector

Copy link
Copy Markdown

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

Reviewed commit: 4e3bff77dc

ℹ️ 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".

@bootjp

bootjp commented Jul 11, 2026

Copy link
Copy Markdown
Owner Author

@codex review

対応しました。

  • SplitAtHLC decode を binary.Read から固定長 buffer と binary.BigEndian.Uint64 に変更

検証:

  • go test ./distribution -run "Test.*RouteDescriptor|TestCatalog" -count=1
  • go test ./distribution -count=1
  • go test ./... -run "^$" -count=1
  • golangci-lint run ./distribution --timeout=5m
  • git diff --check
  • git verify-commit HEAD

@github-actions

Copy link
Copy Markdown
Contributor

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 (9856a5c):

  • distribution/catalog.go
  • distribution/catalog_test.go

What to check, by subsystem:

  • kv/hlc*.goNext() 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.goRunHLCLeaseRenewal, 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

Copy link
Copy Markdown

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

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 9856a5cc28

ℹ️ 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".

Comment thread distribution/catalog.go
@github-actions

Copy link
Copy Markdown
Contributor

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 (14962c3):

  • distribution/catalog.go
  • distribution/catalog_test.go

What to check, by subsystem:

  • kv/hlc*.goNext() 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.goRunHLCLeaseRenewal, 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

Copy link
Copy Markdown

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

@bootjp

bootjp commented Jul 11, 2026

Copy link
Copy Markdown
Owner Author

@codex review

対応しました。

  • SplitRange で catalog snapshot の ReadTS を観測したうえで fenced commit timestamp を事前確保
  • child route descriptor の SplitAtHLC にその commit timestamp を設定してから catalog mutation を encode
  • Dispatch には同じ CommitTS を渡し、durable descriptor と実 commit timestamp がずれないように修正
  • regression として persisted catalog child routes の SplitAtHLC が Dispatch commitTS と一致することを追加

検証:

  • go test ./adapter -run 'TestDistributionServerSplitRange|TestMilestone1SplitRange' -count=1 -timeout=60s\n- go test ./distribution -run 'TestRouteDescriptor|TestCatalog|Test.*SplitAtHLC' -count=1\n- go test ./... -run '^$' -count=1\n- golangci-lint run ./adapter ./distribution --timeout=5m\n- git diff --check\n- git verify-commit HEAD\n\n補足: go test ./adapter ./distribution -count=1 -timeout=180s は adapter 全体の統合テストがローカルで timeout しました。今回変更対象の SplitRange/codec targeted tests と compile/lint は通過しています。

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 14962c3641

ℹ️ 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".

Comment thread adapter/distribution_server.go Outdated
@github-actions

Copy link
Copy Markdown
Contributor

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 (eea7ea0):

  • distribution/catalog.go
  • distribution/catalog_test.go
  • kv/coordinator.go
  • kv/sharded_coordinator.go

What to check, by subsystem:

  • kv/hlc*.goNext() 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.goRunHLCLeaseRenewal, 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

Copy link
Copy Markdown

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

@bootjp

bootjp commented Jul 11, 2026

Copy link
Copy Markdown
Owner Author

@codex review

対応しました。

  • SplitRange から handler 側の事前 CommitTS 確保を削除し、Dispatch には CommitTS を渡さないように変更
  • child route descriptor は commit 前に SplitAtHLC=0 の placeholder として encode し、committing coordinator / forwarded leader が確定した transaction commit timestamp を mutation value に patch
  • single-shard / multi-shard / leader-forwarded txn の各 path で commit timestamp patch を検証・適用し、元の Elem.Value を retry 間で汚染しないように clone
  • SplitRange response は commit 後に reload した catalog snapshot の child descriptors を返すように変更
  • regression として coordinator stub / forwarded txn / coordinator patch helper のテストを追加

検証:

  • go test ./adapter -run 'TestDistributionServerSplitRange|TestMilestone1SplitRange|TestFillForwardedTxnCommitTS|TestStampTxnTimestamps' -count=1 -timeout=120s
  • go test ./kv -run 'Test(CoordinateDispatchTxn|ShardedCoordinatorDispatchTxn|StampMutationCommitTS)' -count=1 -timeout=120s
  • go test ./distribution -run 'TestRouteDescriptor|TestCatalog|Test.*SplitAtHLC' -count=1 -timeout=120s
  • go test ./... -run '^$' -count=1 -timeout=240s
  • golangci-lint run ./adapter ./kv ./distribution --timeout=5m
  • git diff --check
  • git verify-commit HEAD

補足: go test ./adapter ./kv ./distribution -count=1 -timeout=240s は adapter package 全体が timeout しました。今回変更対象の targeted tests / compile / lint は通過しています。

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: eea7ea0353

ℹ️ 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".

CatalogVersion: saved.Version,
Left: toProtoRouteDescriptor(left),
Right: toProtoRouteDescriptor(right),
Left: toProtoRouteDescriptor(savedLeft),

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Include SplitAtHLC in route descriptors

When SplitRange is called through the Distribution API, savedLeft now contains the leader-stamped SplitAtHLC, but toProtoRouteDescriptor/pb.RouteDescriptor still omit that field, so the response serializes the same descriptor shape as before. Any caller that relies on the SplitRange/ListRoutes RPC output to seed or reconstruct split cooldowns will see no durable split timestamp and can treat just-created children as not cooling down; add a split_at_hlc field to distribution.proto and populate it here.

Useful? React with 👍 / 👎.

if err := s.applyEngineSnapshot(saved); err != nil {
return nil, err
}
savedLeft, savedRight, err := splitChildrenFromSnapshot(saved, left.RouteID, right.RouteID)

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Reload the exact split version

Because saveSplitResultViaCoordinator reloads any snapshot with Version >= nextVersion, a concurrent SplitRange on another node can advance the catalog again before this line runs. If that follow-up split targets one of these just-created children, the newer snapshot no longer contains left.RouteID or right.RouteID, so splitChildrenFromSnapshot returns an Internal error even though this split already committed successfully; load the snapshot at this transaction's commit timestamp/exact catalog version before extracting the response descriptors.

Useful? React with 👍 / 👎.

Comment thread kv/sharded_coordinator.go
// preserving SSI.
return c.dispatchSingleShardTxn(ctx, startTS, commitTS, prevCommitTS, primaryKey, gids[0], elems, readKeys, observedRouteVersion)
}
if err := StampGroupedMutationCommitTS(grouped, commitTS); err != nil {

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Clear patch offsets before forwarding PREPARE

For a multi-shard transaction with a CommitTSValueOffset, this stamps the grouped mutations but leaves CommitTsValueOffset set on the PREPARE payloads. When one of those shard commits goes through a LeaderProxy, forward() sends the PREPARE to Internal.Forward, whose txn stamping sees no commit meta for PREPARE and then calls StampMutationCommitTS with commitTS == 0, causing an ErrTxnCommitTSRequired rejection even though the value was already patched; clear the offset after stamping or skip commit-TS patching for PREPARE forwarding.

Useful? React with 👍 / 👎.

@bootjp

bootjp commented Jul 13, 2026

Copy link
Copy Markdown
Owner Author

@codex review

対応しました。

  • RouteDescriptor RPC payload に split_at_hlc を追加し、ListRoutes / SplitRange response が durable SplitAtHLC を返すように修正
  • SplitRange commit 後の catalog reload を「version >= nextVersion」ではなく、Dispatch が返した CommitTS での exact snapshot に変更
  • CommitTSValueOffset を value patch 後に 0 に戻し、2PC PREPARE が leader forward されても forwarded stamping で commitTS=0 の再 patch を試みないように修正

検証:

  • make -C proto gen
  • go test ./adapter -run 'TestDistributionServer(ListRoutes|SplitRange)|TestFillForwardedTxnCommitTS|TestStampTxnTimestamps' -count=1 -timeout=180s
  • go test ./kv -run 'TestStampMutationCommitTS|TestCoordinateDispatchTxn_StampsCommitTSValueOffsetWithoutMutatingElem|TestShardedCoordinatorDispatchTxn_CrossShardPhasesAndCommitIndex' -count=1 -timeout=180s
  • go test ./distribution -run 'TestRouteDescriptor|TestCatalog|Test.*SplitAtHLC' -count=1 -timeout=180s
  • go test ./distribution ./kv ./proto -count=1 -timeout=300s
  • go test ./... -run '^$' -count=1 -timeout=300s
  • golangci-lint run ./adapter ./distribution ./kv ./proto --timeout=5m
  • git diff --check
  • git verify-commit HEAD

補足: go test ./adapter ./distribution ./kv ./proto -count=1 -timeout=600s は adapter package の統合テスト群で 600s timeout しました。今回変更対象の focused tests、distribution/kv/proto package tests、全体 compile、lint は通過しています。

@github-actions

Copy link
Copy Markdown
Contributor

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 (d0a7c4c):

  • distribution/catalog.go
  • distribution/catalog_test.go
  • kv/coordinator.go
  • kv/sharded_coordinator.go

What to check, by subsystem:

  • kv/hlc*.goNext() 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.goRunHLCLeaseRenewal, 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

Copy link
Copy Markdown

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

@chatgpt-codex-connector

Copy link
Copy Markdown

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

Reviewed commit: d0a7c4c950

ℹ️ 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".

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant