Skip to content

migration: complete target promotion catalog state#1090

Open
bootjp wants to merge 3 commits into
design/hotspot-split-m2-cross-groupfrom
design/hotspot-split-m2-promotion-complete
Open

migration: complete target promotion catalog state#1090
bootjp wants to merge 3 commits into
design/hotspot-split-m2-cross-groupfrom
design/hotspot-split-m2-promotion-complete

Conversation

@bootjp

@bootjp bootjp commented Jul 13, 2026

Copy link
Copy Markdown
Owner

Author: bootjp

Summary:

  • Add the default-group target promotion completion transition.
  • Clear only staged route fields while retaining min_write_ts_exclusive.
  • Persist the route descriptor update and SplitJob promotion witness in one catalog batch.
  • Cover idempotent cleared-descriptor retries and stale input rejection.

Tests:

  • go test ./distribution -run 'Test(CompleteTargetPromotion|CatalogStoreCompleteSplitJobTargetPromotion)'\n- go test ./distribution\n- go test -run '^$' ./...\n- GOCACHE=$(pwd)/.cache GOLANGCI_LINT_CACHE=$(pwd)/.golangci-cache golangci-lint run ./distribution --timeout=5m

@coderabbitai

coderabbitai Bot commented Jul 13, 2026

Copy link
Copy Markdown

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: 478239af-9add-4c7e-8c62-7185186e297a

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

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 (351477d):

  • distribution/migration_promotion_complete.go
  • distribution/migration_promotion_complete_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 13, 2026

Copy link
Copy Markdown
Owner Author

@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 the target promotion completion logic for split job migrations, including the state transition function CompleteTargetPromotionState and the transactional catalog store method CompleteSplitJobTargetPromotion. Feedback suggests strengthening defensive checks by validating the route's parent ID and start key during route clearing, and removing a redundant history lookup that could impact performance.

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 on lines +83 to +85
if !route.StagedVisibilityActive || route.GroupID != job.TargetGroupID {
return nil, errors.WithStack(ErrMigrationInvalidRoute)
}

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.

medium

To enforce defensive programming and ensure catalog consistency, we should also validate that the target route's ParentRouteID and Start key match the split job's SourceRouteID and SplitKey before clearing the staged visibility fields. This prevents accidentally promoting an inconsistent or incorrect route descriptor.

Suggested change
if !route.StagedVisibilityActive || route.GroupID != job.TargetGroupID {
return nil, errors.WithStack(ErrMigrationInvalidRoute)
}
if !route.StagedVisibilityActive || route.GroupID != job.TargetGroupID || route.ParentRouteID != job.SourceRouteID || !bytes.Equal(route.Start, job.SplitKey) {
return nil, errors.WithStack(ErrMigrationInvalidRoute)
}

Comment on lines +151 to +158
if err := s.expectLiveSplitJobAt(ctx, expected.JobID, expectedRaw, readTS); err != nil {
return 0, 0, nil, err
}
if _, found, err := s.historySplitJobAt(ctx, expected.JobID, readTS); err != nil {
return 0, 0, nil, err
} else if found {
return 0, 0, nil, errors.WithStack(ErrCatalogSplitJobConflict)
}

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.

medium

The check s.historySplitJobAt is redundant and inefficient here. Since s.expectLiveSplitJobAt has already succeeded, the split job is guaranteed to be in the live state. In a consistent MVCC catalog, a split job cannot exist in both the live state and the history state simultaneously. Scanning the entire history of split jobs (which can grow very large in production) is expensive and unnecessary. We can safely remove this check.

Suggested change
if err := s.expectLiveSplitJobAt(ctx, expected.JobID, expectedRaw, readTS); err != nil {
return 0, 0, nil, err
}
if _, found, err := s.historySplitJobAt(ctx, expected.JobID, readTS); err != nil {
return 0, 0, nil, err
} else if found {
return 0, 0, nil, errors.WithStack(ErrCatalogSplitJobConflict)
}
if err := s.expectLiveSplitJobAt(ctx, expected.JobID, expectedRaw, readTS); err != nil {
return 0, 0, nil, err
}
References
  1. Remove dead or unreachable code paths, such as asynchronous handlers for tasks that are always performed synchronously, to improve code clarity and maintainability.

@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: 351477d4e1

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

out.Changed = true
out.ClearedRouteIDs = cleared
out.Job.TargetPromotionDone = true
out.Job.PromotionCompletedTS = completionTS

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 Record the catalog CAS timestamp

In the promotion-complete path, this stores the caller-supplied completionTS in promotion_completed_ts, but the design contract for that field is the HLC commit timestamp of the default-group CAS that clears the descriptor (see docs/design/2026_06_11_proposed_hotspot_split_milestone2_migration.md, promotion_completed_ts). In normal calls the target-local promotion timestamp/max promoted timestamp can differ from the catalog MVCC commit timestamp chosen later in applyPromotionCompleteMutations, so target cleared-descriptor ACKs can prove or wait on the wrong timestamp; compute the catalog commit timestamp before encoding the job and persist that value instead.

Useful? React with 👍 / 👎.

@bootjp
bootjp force-pushed the design/hotspot-split-m2-promotion-complete branch from 351477d to c57e42a Compare July 13, 2026 16:27
@bootjp

bootjp commented Jul 13, 2026

Copy link
Copy Markdown
Owner Author

Addressed review feedback in c57e42a:

  • validate target parent route and split key before clearing staged route fields
  • remove the redundant live+history conflict scan from the promotion-complete read path
  • store the actual catalog CAS commit timestamp in promotion_completed_ts

@codex review

@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 (c57e42a):

  • distribution/migration_promotion_complete.go
  • distribution/migration_promotion_complete_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 force-pushed the design/hotspot-split-m2-promotion-complete branch from c57e42a to 2edefb8 Compare July 13, 2026 16:31
@bootjp

bootjp commented Jul 13, 2026

Copy link
Copy Markdown
Owner Author

Follow-up in 2edefb8:

  • removed caller-supplied completion timestamp from the promotion-complete APIs
  • the catalog CAS commit timestamp is now assigned immediately before encoding the SplitJob witness

@codex review

@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 (2edefb8):

  • distribution/migration_promotion_complete.go
  • distribution/migration_promotion_complete_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 14, 2026

Copy link
Copy Markdown
Owner Author

Current head 2edefb8 has green CI and no current-head inline blockers found in the latest check. Requesting current-head review.\n\n@codex review

@chatgpt-codex-connector

Copy link
Copy Markdown

Codex Review: Didn't find any major issues. More of your lovely PRs please.

Reviewed commit: 2edefb8553

ℹ️ 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 14, 2026

Copy link
Copy Markdown
Owner Author

@codex review

Latest head has green CI and no current-head top-level inline findings from the review-comments API. Requesting a fresh review for the current head.

@chatgpt-codex-connector

Copy link
Copy Markdown

Codex Review: Didn't find any major issues. Keep it up!

Reviewed commit: 2edefb8553

ℹ️ 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 14, 2026

Copy link
Copy Markdown
Owner Author

@codex review

Merged latest design/hotspot-split-m2-promote into this branch and fixed the promotion-complete compatibility with the updated catalog save plan/v2 route descriptor write gate in 9d9e051.

Validation:

  • go test ./distribution -run "Test(CompleteTargetPromotionState|CatalogStoreCompleteSplitJobTargetPromotion)" -count=1 -timeout=240s
  • go test ./adapter ./store ./kv -run "Test(DistributionServerSplitRange|PromoteVersionsIgnoresClientCursorWhenStateMissing|PromoteVersionsMovesStagedVersionsAndDeletesStagedRows|PebblePromoteVersionsAdvancesLastCommitTS|ValidatePromotionCursorForRangeAcceptsOnlyEmittedPositions|ShardStore.*Raft|ApplyMutationsRaft|DeletePrefixAtRaft)" -count=1 -timeout=240s
  • GOLANGCI_LINT_CACHE=/tmp/elastickv-golangci-1090 golangci-lint --config=.golangci.yaml run ./adapter ./distribution ./kv ./store --timeout=5m
  • git diff --check

@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 (9d9e051):

  • distribution/migration_promotion_complete.go
  • distribution/migration_promotion_complete_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: 9d9e051a7f

ℹ️ 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 on lines +146 to +149
if currentVersion != expectedVersion {
return 0, 0, nil, errors.WithStack(ErrCatalogVersionMismatch)
}
if err := s.expectLiveSplitJobAt(ctx, expected.JobID, expectedRaw, readTS); 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 Allow retries after the completion commit lands

If a completion attempt commits but the caller loses the response, retrying the same request still carries the original catalog version and pre-completion SplitJob. The first attempt has already bumped the catalog version and updated the live job, so these checks return ErrCatalogVersionMismatch/ErrCatalogSplitJobConflict before the cleared-descriptor idempotent path can run; the retry reports failure for an already-applied promotion unless the caller reloads and resubmits the new version/job.

Useful? React with 👍 / 👎.

Comment on lines +205 to +207
if err := s.store.ApplyMutations(ctx, mutations, readKeys, plan.readTS, commitTS); err != nil {
if errors.Is(err, store.ErrWriteConflict) {
return errors.WithStack(ErrCatalogSplitJobConflict)

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P3 Badge Preserve catalog-version conflicts on concurrent saves

When another catalog save commits after loadPromotionCompleteInputs but before this batch applies, ApplyMutations will report a write conflict on CatalogVersionKey, but this branch wraps every such conflict as ErrCatalogSplitJobConflict. That makes a plain catalog-version race look like the split job changed, unlike CatalogStore.Save which maps version-key conflicts to ErrCatalogVersionMismatch, so callers cannot distinguish a route catalog retry from a real job-state conflict.

Useful? React with 👍 / 👎.

nextVersion: expectedVersion + 1,
routes: completion.Routes,
}
mutations, err := s.buildSaveMutations(ctx, &plan)

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 Enable V2 writes for promotion-complete stores

In the normal promotion case the cleared route still retains MinWriteTSExclusive, so buildSaveMutations must encode that descriptor as route v2 and will return ErrCatalogRouteV2WriteDisabled unless the CatalogStore was constructed with WithCatalogRouteDescriptorV2Writes(true). The production helper in main.go currently uses the default constructor, so completing a migrated route through that store fails at this point instead of clearing the staged fields.

Useful? React with 👍 / 👎.

Copy link
Copy Markdown
Owner Author

Choose a reason for hiding this comment

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

Resolved in 5dec8cb: distributionCatalogStoreForGroup now constructs the production catalog store with WithCatalogRouteDescriptorV2Writes(true), and TestDistributionCatalogStoreForGroupEnablesRouteDescriptorV2Writes covers the production helper.

Copy link
Copy Markdown
Owner Author

Choose a reason for hiding this comment

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

Addressed in current head 2b7c3af: production promotion-complete catalog stores are now created via distributionCatalogStoreForEngine -> distributionCatalogStoreForGroup, and distributionCatalogStoreForGroup enables distribution.WithCatalogRouteDescriptorV2Writes(true). I also re-ran the route-v2 write/promotion-complete targeted tests and posted the current-head audit summary in the PR discussion.

@codex review

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: Didn't find any major issues. Delightful!

Reviewed commit: 2b7c3af03d

ℹ️ 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 16, 2026

Copy link
Copy Markdown
Owner Author

@codex review

@chatgpt-codex-connector

Copy link
Copy Markdown

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

Reviewed commit: 9d9e051a7f

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

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

  • distribution/migration_promotion_complete.go
  • distribution/migration_promotion_complete_test.go
  • distribution/split_job_catalog.go
  • distribution/split_job_catalog_test.go
  • distribution/split_job_lifecycle.go
  • kv/fsm.go
  • kv/sharded_coordinator.go
  • store/mvcc_store.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: a02b6c1c68

ℹ️ 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 main.go
adapter.WithDistributionActiveTimestampTracker(readTracker),
adapter.WithDistributionKnownRaftGroups(shardGroupIDs(shardGroups)...),
adapter.WithSplitMigrationCapabilityGate(splitMigrationGate),
adapter.WithSplitJobRunnerReady(),

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P1 Badge Keep cap_migration_v2 closed until a runner is wired

In the production wiring this sets splitJobRunnerReady on every node, so GetSplitMigrationCapability advertises cap_migration_v2. I checked the changed code paths for a split-job runner/advance loop and only Start/List/Retry/Abandon plus catalog helpers are wired; no process actually advances the PLANNED job created by StartSplitMigration. In a normal deployment the capability gate can therefore pass and create a live SplitJob that stays PLANNED (blocking the single in-flight migration/split overlap guard), so leave this option off until the runner/full migration path is started.

Useful? React with 👍 / 👎.

Base automatically changed from design/hotspot-split-m2-promote to design/hotspot-split-m2-cross-group July 16, 2026 20:32
@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 (f51ca32):

  • distribution/migration_promotion_complete.go
  • distribution/migration_promotion_complete_test.go
  • distribution/split_job_catalog.go
  • distribution/split_job_catalog_test.go
  • distribution/split_job_lifecycle.go
  • kv/fsm.go
  • kv/sharded_coordinator.go
  • store/mvcc_store.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.

@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 (5dec8cb):

  • distribution/migration_promotion_complete.go
  • distribution/migration_promotion_complete_test.go
  • distribution/split_job_catalog.go
  • distribution/split_job_catalog_test.go
  • distribution/split_job_lifecycle.go
  • kv/fsm.go
  • kv/sharded_coordinator.go
  • store/mvcc_store.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 17, 2026

Copy link
Copy Markdown
Owner Author

@codex review

Updated commit: 5d78d7ade2529f1d940a4f67c23334c82f1e1328

Addressed a target-readiness boundary gap before promotion-complete merges onward:

  • ApplyTargetStagedReadiness now rejects armed readiness requests with min_write_ts_exclusive=0 at the gRPC boundary as InvalidArgument, before proposing to Raft.
  • This matches the store-layer TargetStagedReadiness validation and prevents publishing an armed cutover-readiness proof without a write floor.

Validation:

  • go test ./adapter -run 'TestInternalApplyTargetStagedReadiness(RejectsArmedZeroMinWriteTS|RejectsWhenOpcodeGateClosed|ProposesThroughRaft)' -count=1 -timeout=180s
  • go test ./store -run 'TestTargetStagedReadinessRejectsArmedStateWithoutWriteFloor|TestPebbleTargetStagedReadinessPersistsAcrossReopen' -count=1 -timeout=180s
  • go test ./kv -run 'TestFSMRejectsS3BucketAuxiliaryPointWrite(BelowRouteFloor|WithoutTargetReadinessProof|OnWriteFencedRoute)|TestShardStoreRejectsS3BucketAuxiliaryWriteAtMigrationTimestampFloor|TestShardStoreGetAt_MergesStagedVisibilityForS3BucketAuxiliary|TestShardStoreScanAt_RoutesS3BucketAuxiliaryStagedVisibility' -count=1 -timeout=180s
  • go test ./adapter ./kv ./store -count=1 -timeout=600s
  • golangci-lint --config=.golangci.yaml run ./adapter ./kv ./store --timeout=5m
  • git diff --check
  • git verify-commit HEAD

@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. Keep it up!

Reviewed commit: 5d78d7ad1c

ℹ️ 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 17, 2026

Copy link
Copy Markdown
Owner Author

@codex review

Updated M2 design status to partial in 178fda6.

Changes:

  • Renamed the M2 migration design doc from proposed to partial.
  • Updated the header, parent hotspot doc, and scaling roadmap references.
  • Kept the implemented promotion gated on the §13 acceptance criteria: cross-group jobs reaching DONE, ListRoutes showing the target-group child, leader-kill recovery, and Jepsen split coverage.

Validation:

  • rg found no remaining references to the old proposed M2 filename.
  • git diff --check
  • git diff --cached --check
  • commit hook: golangci-lint --config=.golangci.yaml run --fix
  • 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 (178fda6):

  • distribution/migration_promotion_complete.go
  • distribution/migration_promotion_complete_test.go
  • distribution/split_job_catalog.go
  • distribution/split_job_catalog_test.go
  • distribution/split_job_lifecycle.go
  • kv/fsm.go
  • kv/sharded_coordinator.go
  • store/mvcc_store.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. Hooray!

Reviewed commit: 178fda6e23

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

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 (34706b0):

  • distribution/migration_promotion_complete.go
  • distribution/migration_promotion_complete_test.go
  • distribution/split_job_catalog.go
  • distribution/split_job_catalog_test.go
  • distribution/split_job_lifecycle.go
  • kv/fsm.go
  • kv/sharded_coordinator.go
  • store/mvcc_store.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: 34706b0113

ℹ️ 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 kv/fsm.go Outdated
return nil, err
}
if err := f.verifyRouteWriteTimestampFloorsForMutations(uniq, commitTS); err != nil {
if err := f.verifyRouteNotFencedForMutations(uniq); 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 Honor write-fence bypasses for txn mutation checks

When a PREPARE or one-phase txn is pinned to an explicit/non-owning group, the coordinator populates WriteFenceBypassKeys so that writes can still be applied while the key's normal route is write-fenced; verifyWriteFence and verifyComposed1 honor those keys, but this new unconditional check does not. In that scenario the request is rejected with ErrRouteWriteFenced before the txn can stage/commit, blocking the migration cleanup/drain path for pinned writes; pass the bypass set through here like the raw mutation path does.

Useful? React with 👍 / 👎.

Comment thread adapter/internal.go
Comment on lines +306 to +307
if err := i.verifyMigrationPromoteEnabled(ctx); err != nil {
return nil, err

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 Keep the new readiness opcode behind its own gate

In clusters that already set ELASTICKV_ENABLE_MIGRATION_PROMOTE_OPCODE=true for the existing PromoteStagedVersions rollout, this new RPC is automatically open even if some voters are still on the previous build that only handles the 0x0b promote opcode. Calling this endpoint during that rolling-upgrade window proposes raftEncodeTargetReadiness (0x0c) to those voters, which their applyReservedOpcode does not recognize, so readiness needs a separate fail-closed gate/capability check before proposing the new opcode.

Useful? React with 👍 / 👎.


func splitJobAbandonFromPhase(job SplitJob) (SplitJobPhase, bool) {
switch job.Phase {
case SplitJobPhasePlanned, SplitJobPhaseBackfill, SplitJobPhaseFence, SplitJobPhaseDeltaCopy:

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 Don’t mark PLANNED jobs abandonable unless they encode

When AbandonSplitJob is called on a freshly created PLANNED job, this branch moves it to ABANDONING with AbandonFromPhase=PLANNED, but the catalog encoder still rejects that state because SplitJobPhasePlanned.abandonable() is false. That makes the abandon RPC fail before it can persist the cleanup state for exactly the job phase created by StartSplitMigration; either keep PLANNED out of this transition or allow that abandon origin in catalog validation.

Useful? React with 👍 / 👎.

Comment thread kv/shard_store.go
if routeStart, routeEnd, ok := s3keys.ManifestScanRouteBounds(start, end); ok {
return routeStart, routeEnd
}
return readinessRouteRange(start, end)

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 Normalize S3 bucket scans for readiness checks

For S3 bucket metadata/generation scans, routesForScan maps the raw !s3|bucket|... interval to the bucket route namespace via s3BucketAuxiliaryScanRouteRange, but this readiness helper only normalizes manifest scans and otherwise checks the raw range. While target readiness is armed but the target route snapshot is still stale, a forwarded ListBuckets-style scan can therefore miss the !s3route|... readiness fence and serve live-only data instead of failing closed; use the same scan-route normalization as routing does before checking readiness.

Useful? React with 👍 / 👎.

Comment thread kv/sharded_coordinator.go

func (c *ShardedCoordinator) prewriteTxn(ctx context.Context, startTS, commitTS uint64, primaryKey []byte, grouped map[uint64][]*pb.Mutation, gids []uint64, groupedReadKeys map[uint64][][]byte, observedRouteVersion uint64, bypassKeysByGroup map[uint64][][]byte) ([]preparedGroup, error) {
prepareMeta := txnMetaMutation(primaryKey, defaultTxnLockTTLms, 0)
prepareMeta := txnMetaMutation(primaryKey, defaultTxnLockTTLms, commitTS)

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 Persist PREPARE commit timestamps in txn locks

For two-phase transactions after the migration capability is opened, the moving-range drain needs the already allocated commit timestamp from each prepared lock so it can compute the migration-window floor for locks that survive into BACKFILL/FENCE. This change only puts commitTS in the PREPARE request metadata; buildPrepareStoreMutations drops that metadata and txnLock still encodes only start/TTL/primary fields, so PendingTxnLocksInRoute later has no timestamp for these new locks and must treat them like legacy unknowns. Thread the commit timestamp into the durable lock value when preparing.

Useful? React with 👍 / 👎.

@bootjp

bootjp commented Jul 18, 2026

Copy link
Copy Markdown
Owner Author

Fixed the failing FSM write-fence bypass path in 737b930. PREPARE and one-phase transaction apply now preserve exact-key WriteFenceBypassKeys through the duplicate/fence validation layer. Added one-phase coverage and audited every caller of uniqueMutationsNotFenced.

Validation: targeted normal and race tests pass, ./kv passes, compile-only ./... passes, lint reports 0 issues. The local full suite reached the adapter integration timeout under concurrent load; the affected package and CI reproduction are covered separately.

@codex review

@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 (737b930):

  • distribution/migration_promotion_complete.go
  • distribution/migration_promotion_complete_test.go
  • distribution/split_job_catalog.go
  • distribution/split_job_catalog_test.go
  • distribution/split_job_lifecycle.go
  • kv/fsm.go
  • kv/sharded_coordinator.go
  • store/mvcc_store.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: 737b9301fe

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

defer s.dbMu.RUnlock()
s.mtx.Lock()
defer s.mtx.Unlock()
if err := s.db.Set(migrationReadyKey(state.JobID), encodeTargetStagedReadinessState(state), s.directApplyWriteOpts()); 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 Bundle target-readiness applies with the Raft index

When a target-readiness Raft entry is applied on a Pebble-backed group, this path persists the guard with a bare db.Set but never records the entry's pendingApplyIdx in metaAppliedIndex. Unlike the other durable migration opcodes (ImportVersionsRaft / PromoteVersions), a readiness-only entry leaves LastAppliedIndex() behind the actual on-disk FSM state, so after restart the cold-start skip path under-reports progress and has to replay/restore from an older index even though the guard was already acknowledged and synced. This should use a Raft-aware store path (or batch the readiness key with metaAppliedIndex) for the apply index delivered by the FSM.

Useful? React with 👍 / 👎.

Comment thread kv/shard_store.go
if routeStart, routeEnd, ok := s3keys.ManifestScanRouteBounds(start, end); ok {
return routeStart, routeEnd
}
return readinessRouteRange(start, end)

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 Normalize S3 bucket scans before readiness checks

For broad S3 bucket meta/generation scans, such as ScanGroupAt(..., BucketMetaPrefix, prefixEnd(BucketMetaPrefix), ...), this falls back to readinessRouteRange on the raw !s3|bucket|... bounds rather than the bucket's !s3route|... interval used by routesForS3BucketAuxiliaryScan. A retained target-readiness guard for that bucket therefore looks non-overlapping, so a target voter whose catalog watcher has not loaded the staged/cleared descriptor can serve the target store (or an empty result) instead of returning ErrRouteCutoverPending; this should normalize bucket auxiliary scans with the same route-space bounds as the scan router.

Useful? React with 👍 / 👎.

Comment thread adapter/internal.go
if err := i.verifyInternalLeader(ctx); err != nil {
return nil, err
}
if err := i.verifyMigrationPromoteEnabled(ctx); 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 Add an opcode gate for target readiness

When ApplyTargetStagedReadiness is called during a rolling upgrade where ELASTICKV_ENABLE_MIGRATION_PROMOTE_OPCODE is already enabled for the pre-existing promote opcode but some target voters still run a build without raftEncodeTargetReadiness, this shared promote gate passes and then proposes the new 0x0c entry. Those older FSMs do not handle 0x0c and fall through to legacy protobuf decoding, so Raft apply can fail even though the rollout guard allowed the RPC; add a separate target-readiness/capability gate, or make this gate explicitly require 0x0c support everywhere before proposing.

Useful? React with 👍 / 👎.

@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: 28449f9285

ℹ️ 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/internal.go Outdated
Comment thread store/mvcc_store.go
Comment thread jepsen/src/elastickv/split_workload.clj
Comment thread kv/fsm.go
@bootjp
bootjp force-pushed the design/hotspot-split-m2-cross-group branch 3 times, most recently from 1d0a97d to 0a1b9c8 Compare July 19, 2026 13:41
@bootjp
bootjp force-pushed the design/hotspot-split-m2-promotion-complete branch from 28449f9 to 54cc7b9 Compare July 19, 2026 15:03
@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 (54cc7b9):

  • distribution/migration_promotion_complete.go
  • distribution/migration_promotion_complete_test.go
  • distribution/split_job_catalog.go
  • distribution/split_job_catalog_test.go
  • distribution/split_job_lifecycle.go
  • kv/fsm.go
  • kv/sharded_coordinator.go
  • store/mvcc_store.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 19, 2026

Copy link
Copy Markdown
Owner Author

Current HEAD: 54cc7b9f96f4b2a5cc43b465554f2858479d429c

Resolved the four current findings and the Proto failure:

  • cleanup opcode has an independent rolling-upgrade gate and capability prerequisite
  • ordinary snapshots remain v1; v2 is emitted only when durable readiness state is present
  • Jepsen register keys cover both sides of m2-split
  • FSM and cross-shard transaction read validation fail closed on source read fences
  • current-main S3BlobFetch service definitions are synchronized and generated, satisfying the main-based Proto compatibility gate

Semantic caller audit:

  • all six split-job cleanup RPC call sites still pass through the internal cleanup gate
  • snapshot header/body have one caller and one read-locked version decision
  • transaction read validation covers PREPARE, one-phase, and read-only shard paths
  • write-fence bypass remains independent of migration floor enforcement

Verification:

  • go test ./kv -count=1
  • targeted adapter/store/main tests
  • go test ./... -run "^$" -count=1
  • make -C proto gen and make -C proto breaking
  • Jepsen split workload: 3 tests, 7 assertions, 0 failures
  • make tla-check
  • git diff --check

All PR-visible commits are signed with exact author and committer bootjp <contact@bootjp.me>. The sanitized pre-fix tree was rebuilt without changing its code tree before these review fixes.

@codex review

@bootjp

bootjp commented Jul 19, 2026

Copy link
Copy Markdown
Owner Author

Current HEAD: 48a4da82d36ecc4a337c0aeb84305a0083170479

CI lint follow-up:

  • Reused one voter suffrage constant across the three production call sites flagged by goconst.
  • Removed the invariant write-fence parameter from the migration fence test helper; all callers still install SourceWriteFence: true, while the read-fence cases remain explicit.
  • Caller audit: rg -n 'applySourceMigrationControlToFSM|raftMemberSuffrageVoter' main.go main_leader_balance.go kv/fsm_migration_fence_test.go.
  • go test . ./kv -run 'TestChooseLeaderBalance|TestLeaderBalance|TestFSM(DurableSourceFence|OnePhaseTxnChecksSourceReadFence)' -count=1
  • golangci-lint run --config=.golangci.yaml --timeout=5m --allow-parallel-runners -> 0 issues
  • git diff --check

@codex review

@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 (48a4da8):

  • distribution/migration_promotion_complete.go
  • distribution/migration_promotion_complete_test.go
  • distribution/split_job_catalog.go
  • distribution/split_job_catalog_test.go
  • distribution/split_job_lifecycle.go
  • kv/fsm.go
  • kv/sharded_coordinator.go
  • store/mvcc_store.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: 48a4da82d3

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

state.MigrationJobID = binary.BigEndian.Uint64(rest[:migrationUint64Bytes])
rest = rest[migrationUint64Bytes:]
state.MinWriteTSExclusive = binary.BigEndian.Uint64(rest[:migrationUint64Bytes])
return state, rest[migrationUint64Bytes:], true

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 Decode V1 readiness records from the current offset

When a node loads or restores a version-1 target readiness record, rest has already been advanced past the four fixed uint64 fields, so slicing rest[migrationUint64Bytes:] skips the first 8 bytes of the encoded route range. That makes valid V1 records fail decodeTargetReadinessRange, so a rolling upgrade or snapshot restore with retained V1 readiness metadata can reject the record as corrupt instead of preserving the migration fence state.

Useful? React with 👍 / 👎.

if parent.State != distribution.RouteStateActive {
return distribution.RouteDescriptor{}, grpcStatusError(codes.FailedPrecondition, errDistributionSourceRouteNotActive.Error())
}
splitKey := distribution.CloneBytes(req.GetSplitKey())

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 Normalize migration split keys before planning

When StartSplitMigration is used for filesystem chunk-domain splits, this keeps the raw RPC split key instead of normalizing it the way SplitRange does. A raw chunk key is rejected as outside the virtual route interval, and an in-domain key such as a chunk route plus a suffix can be persisted as the job split key, allowing the async migration path to bisect one file's chunk route and bypass the existing file-pinned hotspot guard; normalize once and use that value for validation and job creation.

Useful? React with 👍 / 👎.


func migrationMutationsIntersect(muts []*pb.Mutation, routeStart []byte, routeEnd []byte) bool {
for _, mut := range muts {
if mut == nil || len(mut.Key) == 0 || isTxnInternalKey(mut.Key) {

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P1 Badge Handle empty-prefix deletes in migration write tracking

When the source write tracker is armed and a supported DEL_PREFIX/flush-all mutation uses an empty key, this guard skips it before routePrefixRange can map it to the whole route keyspace. An in-flight flush with a commit timestamp below the migration snapshot can therefore be omitted from MinAdmittedTS, letting delta copy keep the snapshot floor and miss tombstones for keys that were already backfilled.

Useful? React with 👍 / 👎.

Comment thread kv/shard_store.go
if routeStart, routeEnd, ok := s3keys.ManifestScanRouteBounds(start, end); ok {
return routeStart, routeEnd
}
return readinessRouteRange(start, end)

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P1 Badge Use filesystem scan bounds for readiness ranges

When filesystem chunk scans start at fskeys.ChunkPrefix(home, inode), normal scan routing maps them through fskeys.ChunkScanRouteBounds, but this readiness path falls back to routeKey(start)/routeKey(end). That raw two-u64 prefix does not intersect the virtual !fs|route|chk|... migration readiness/source-read-fence range, so a source-read-fenced file route can still serve chunk scans during cutover instead of returning ErrRouteCutoverPending.

Useful? React with 👍 / 👎.

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