Skip to content

store: add migration version import export#1085

Open
bootjp wants to merge 53 commits into
design/hotspot-split-m2-wirefrom
design/hotspot-split-m2-store-export
Open

store: add migration version import export#1085
bootjp wants to merge 53 commits into
design/hotspot-split-m2-wirefrom
design/hotspot-split-m2-store-export

Conversation

@bootjp

@bootjp bootjp commented Jul 13, 2026

Copy link
Copy Markdown
Owner

Summary

  • Add raw MVCC version export/import APIs for migration chunks across memory and Pebble stores.
  • Persist per-bracket import acknowledgements and target-local migration HLC floors.
  • Preserve tombstones and expire_at metadata, including sparse zero-version progress chunks.

Tests

  • go test ./store -count=1 -timeout=180s
  • GOCACHE=$(pwd)/.cache GOLANGCI_LINT_CACHE=$(pwd)/.golangci-cache golangci-lint run ./store ./kv --timeout=5m
  • go test ./store ./kv ./distribution ./adapter -run TestNonExistentForCompileOnly -count=1 -timeout=180s
  • git diff --check

Author: bootjp

@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: 90e177d8-ab7f-4498-967c-b5356cc36436

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.

@bootjp

bootjp commented Jul 13, 2026

Copy link
Copy Markdown
Owner Author

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

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

@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 adds support for range migrations by implementing ExportVersions, ImportVersions, and MigrationHLCFloor across the storage implementations, allowing raw MVCC versions (including tombstones and TTL metadata) to be exported and imported idempotently. The review feedback highlights a potential synchronization/performance improvement by using atomic operations for updating s.lastCommitTS, and points out an O(N^2) complexity issue in finishExportIfLimited when calculating exported version sizes, suggesting tracking the size incrementally instead.

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 store/lsm_migration.go Outdated
Comment thread store/migration_versions.go
@bootjp

bootjp commented Jul 13, 2026

Copy link
Copy Markdown
Owner Author

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

  • 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: edf74ffa0e

ℹ️ 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 store/migration_versions.go
Comment thread store/lsm_migration.go Outdated
Comment on lines +80 to +84
iterOpts := &pebble.IterOptions{
LowerBound: encodeKey(opts.StartKey, math.MaxUint64),
}
if opts.EndKey != nil {
iterOpts.UpperBound = encodeKey(opts.EndKey, math.MaxUint64)

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 user-key bounds for Pebble export ranges

For Pebble, bounding the iterator with encodeKey(start/end, MaxUint64) compares against the raw encoded key (userKey || invertedTS), not just the user key, so prefix-related keys cross the range boundary. For example, exporting ["aa", "b") can still emit key "a" because "a" || ^ts sorts after "aa" || 0, while exporting [nil, "aa") can omit the same "a" row; range migration would then copy keys from outside the bracket or miss keys inside it. The export loop needs to either avoid these raw bounds or re-check userKey >= StartKey in addition to the existing end check.

Useful? React with 👍 / 👎.

Comment thread store/mvcc_store.go Outdated
Comment on lines +68 to +69
migrationAcks map[string]migrationImportAck
migrationHLCFloors map[uint64]uint64

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 Reset migration metadata on in-memory restore

These new maps live outside the snapshot tree, but restoreStreamingSnapshot only replaces tree, lastCommitTS, and minRetainedTS. If an in-memory store imports a migration batch and then restores a snapshot from before that import, the imported versions are gone while the stale ack/floor remain, so retrying the same batch_seq is reported as a duplicate (or later batches see a false high-water mark) and MigrationHLCFloor can return a floor for data that was rolled back. Restore should clear or rebuild this metadata together with the tree.

Useful? React with 👍 / 👎.

Comment thread store/migration_versions.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 (e3079c0):

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

@bootjp

bootjp commented Jul 13, 2026

Copy link
Copy Markdown
Owner Author

@codex review

Addressed current-head migration export blockers in store:

  • Pebble export now filters decoded user-key ranges instead of relying on raw encoded iterator bounds.
  • Export cursors now distinguish an empty user key from no cursor.
  • In-memory snapshot restore clears migration ack/floor metadata with the restored tree.
  • Sparse exports with AcceptKey now default to a bounded scanned-byte budget when unset.

Validation:

  • go test ./store -run 'TestExportVersions|TestImportVersions|TestPebbleImportMetadataPersistsAcrossReopen|TestMVCCStore_RestoreClearsMigrationMetadata'
  • go test ./store
  • git diff --check

@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: e3079c09fd

ℹ️ 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 store/lsm_migration.go Outdated
Comment on lines +119 to +121
if opts.EndKey != nil && bytes.Compare(userKey, opts.EndKey) >= 0 {
_ = s.skipToNextUserKey(iter, userKey)
return false, true, 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 Account for skipped Pebble range rows

When a bounded export reaches a decoded key at or beyond EndKey, this branch skips to the next user key and keeps scanning without updating ScannedBytes or NextCursor. Because the iterator is created without an upper bound, an empty or small bracket such as [a,b) on a Pebble DB with many later keys can walk the rest of the LSM in a single call, and MaxScannedBytes cannot break it into chunks because these skipped rows are not counted. This can make migration export RPCs time out; either terminate when it is safe or charge/cursor the skipped positions.

Useful? React with 👍 / 👎.

Comment thread store/migration_versions.go
Comment thread store/lsm_migration.go Outdated
return true, true, nil
}
if opts.StartKey != nil && bytes.Compare(userKey, opts.StartKey) < 0 {
_ = s.skipToNextUserKey(iter, userKey)

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 Clone iterator keys before skipping

When this path skips a decoded key that sorts before StartKey (for example exporting from aa with existing keys a and b), userKey is a slice into Pebble's iterator buffer. skipToNextUserKey repositions the same iterator, so that slice can mutate to the next key and the helper then advances once more, dropping that key's newest version from the export; the same aliasing affects the other skip calls in this function. Clone the decoded user key before passing it to a helper that seeks the iterator.

Useful? React with 👍 / 👎.

Comment thread store/migration_versions.go Outdated
Comment on lines +97 to +98
return (len(rawKey) == len(migrationAckPrefix)+migrationAckKeyIDBytes && bytes.HasPrefix(rawKey, []byte(migrationAckPrefix))) ||
(len(rawKey) == len(migrationHLCFloorPrefix)+migrationUint64Bytes && bytes.HasPrefix(rawKey, []byte(migrationHLCFloorPrefix)))

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 Avoid treating user versions as migration metadata

This predicate classifies any raw Pebble key with the migration prefix and length as metadata, but a normal MVCC entry is encoded as userKey || invertedTS. A real user key such as !migstage|ack| plus eight bytes therefore has an encoded raw key with exactly this prefix/length and is skipped by export/scan/compaction through isPebbleMetaKey, even though GetAt can still read it. Use an encoding or exact metadata marker that cannot collide with encoded user keys.

Useful? React with 👍 / 👎.

Comment thread store/lsm_migration.go Outdated
Comment on lines +249 to +252
if err := batch.Set(migrationAckKey(opts.JobID, opts.BracketID), encodeMigrationImportAck(migrationImportAck{
batchSeq: opts.BatchSeq,
cursor: opts.Cursor,
}), nil); 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 Keep migration acks out of Pebble snapshots

Persisting the import ack as an ordinary Pebble key means native Pebble snapshots stream it along with data. If a snapshot is taken after importing job/bracket (J,B) and restored into another store, ImportVersions for batch 1 of (J,B) is reported as a duplicate with the old cursor and the new batch's versions are skipped, even though the restored data image should not carry target-local migration progress. Store these acks outside the snapshot stream or filter them when writing/restoring snapshots.

Useful? React with 👍 / 👎.

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

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

@bootjp

bootjp commented Jul 13, 2026

Copy link
Copy Markdown
Owner Author

対応内容:

  • Pebble export の range skip で iterator key を安全に扱い、StartKey 前の skip で次 key を落とさないようにしました。
  • EndKey 到達時に安全に終了できる範囲は即終了し、不要な LSM 後続走査を避けました。
  • memory exporter の cursor を StartKey/EndKey に対して検証し、範囲外 cursor を ErrInvalidExportCursor にしました。
  • migration ack/HLC floor metadata を通常 MVCC encoded key と衝突しない Pebble metadata key に移し、snapshot write/restore から migration metadata を除外しました。

検証:

  • go test ./store -run 'TestExportVersions|TestImportVersions|TestPebbleImportMetadataPersistsAcrossReopen|TestPebbleSnapshotExcludesMigrationMetadata|TestPebbleExportStopsAtEndKey|TestMVCCStore_RestoreClearsMigrationMetadata'
  • go test ./store
  • golangci-lint run ./... --timeout=5m
  • git diff --check
  • go test ./... は adapter/TestRedis_StreamXReadLatencyIsConstant が write conflict で失敗しました。store は同 run 内でも pass しており、go test ./adapter -count=1 -timeout=20m でも同じ adapter test が write conflict で失敗しました。

@codex review

@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: 643a5a6a5f

ℹ️ 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 store/migration_versions.go Outdated
}

func normalizeExportVersionsOptions(opts ExportVersionsOptions) ExportVersionsOptions {
if opts.AcceptKey != nil && opts.MaxScannedBytes == 0 {

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 Apply a scan budget without AcceptKey too

When a caller exports a bounded snapshot/delta with MaxCommitTSInclusive set but no AcceptKey, versions newer than the ceiling are rejected by the export filters and therefore do not count toward MaxVersions or MaxBytes. Because this normalization leaves MaxScannedBytes at zero in that case, a hot key or prefix with many post-ceiling versions can be scanned to exhaustion in a single ExportVersions call instead of yielding a progress cursor; the defensive scan-budget default should not depend only on AcceptKey.

Useful? React with 👍 / 👎.

Comment thread store/lsm_migration.go Outdated
return false, true, err
}
if commitTS <= opts.MinCommitTSExclusive {
_ = s.skipToNextUserKey(iter, userKey)

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 Don't seek past prefixed keys when pruning old versions

When the latest version for a Pebble user key is at or below MinCommitTSExclusive, this branch uses skipToNextUserKey, which seeks to the synthetic key userKey + 0xff.... For binary keys where a distinct in-range key has the current key as a prefix and sorts before that marker (for example a key like a\xff... after pruning key a), the export jumps over that key entirely, so a delta export can miss versions that should be migrated; advance only over exact matches for the current user key instead of seeking to the prefix upper marker here.

Useful? React with 👍 / 👎.

Comment thread store/lsm_migration.go Outdated
Comment on lines +115 to +116
if commitTS <= opts.MinCommitTSExclusive {
_ = s.skipToNextUserKey(iter, userKey)

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 Count min-TS skips against the scan budget

When exporting a delta over a mostly unchanged range, every key whose newest version is already <= MinCommitTSExclusive takes this branch before updating ScannedBytes or NextCursor. Even if the caller set MaxScannedBytes, a chunk can therefore walk the entire range of old keys and return done=true with no progress cursor, defeating the sparse-scan pacing that migration relies on for large unchanged brackets; record the skipped position and honor the scan budget before moving past the key.

Useful? React with 👍 / 👎.

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

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

@bootjp

bootjp commented Jul 13, 2026

Copy link
Copy Markdown
Owner Author

Addressed the current migration export scan blockers in 061275a.

Changes:

  • apply the default scanned-byte budget to timestamp-filtered exports even without AcceptKey
  • record cursor/scanned bytes when MinCommitTSExclusive prunes a key
  • advance Pebble export skips only past exact current user-key versions so prefixed keys are not skipped
  • add regression coverage for timestamp-filter budgets, min-TS scan budgets, and prefixed-key pruning

Caller audit:

  • ExportVersions is implemented in store, passed through by LeaderRoutedStore, and unsupported by ShardStore in this PR; no external pagination caller changes were required.

Validation:

  • go test ./store -run 'TestExportVersions(AppliesDefaultScanBudgetForTimestampFilter|MinTSPruneDoesNotSkipPrefixedKeys|MinTSSkipHonorsScanBudget|AppliesDefaultSparseScanBudget|SparseScanBudgetAdvancesRejectedRows|UsesUserKeyRangeBounds|RejectsCursorOutsideRequestedRange)|TestPebbleExportStopsAtEndKey' -count=1\n- go test ./store -run 'TestExportVersions|TestImportVersions|TestPebbleImportMetadataPersistsAcrossReopen|TestPebbleSnapshotExcludesMigrationMetadata|TestMVCCStore_RestoreClearsMigrationMetadata' -count=1\n- go test ./store -count=1\n- golangci-lint --config=.golangci.yaml run ./store --timeout=5m\n- git diff --check\n\n@codex review

@chatgpt-codex-connector

Copy link
Copy Markdown

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

@bootjp

bootjp commented Jul 14, 2026

Copy link
Copy Markdown
Owner Author

@codex review

Validated latest head 84704f947f5691a5875aea41f4e295d19e08419c against current-head inline findings. No additional code changes were needed; the branch already covers the P1/P2 findings around export cursors/end bounds/scan budgets, Pebble trailing empty-key export, txn-lock exclusion, legacy list-delta migration brackets, broad legacy-delta route scans, compactor route-group deletes, combined list-delta caps, leader-routed export fencing, and Pebble registry-key collision handling.

Checks run:

  • GOCACHE=$(pwd)/.cache GOTMPDIR=$(pwd)/.cache/tmp go test ./store ./distribution ./adapter ./kv (store, distribution, and kv passed; adapter hit the package-level 10m timeout)
  • GOCACHE=$(pwd)/.cache GOTMPDIR=$(pwd)/.cache/tmp go test ./adapter -run 'TestDeltaCompactor_(LegacyListDeltaFoldedIntoBaseMeta|LegacyListCursorAdvancesPastFilteredRawRows|LegacyListCursorAdvancesPastFilteredTailAfterBacktrack|LegacyListCursorAdvancesPastRejectedPrefixBeforeAcceptedTail|ListDeltaDeletesPreserveScanRouteGroup)|TestResolveListMetaEnforcesDeltaLimitAcrossCurrentAndLegacyPrefixes|TestRedisTxnLoadListState(FiltersLegacyDeltaPrefixCollisions|EnforcesDeltaLimitAcrossCurrentAndLegacyPrefixes)' -count=1 -timeout=300s
  • GOCACHE=$(pwd)/.cache GOLANGCI_LINT_CACHE=$(pwd)/.golangci-cache golangci-lint run ./store ./distribution ./adapter ./kv --timeout=5m

Unresolved blocker: full adapter package test suite timed out when run as part of the four-package sweep; focused review-regression tests passed.

@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: 84704f947f

ℹ️ 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/migrator.go
Comment on lines +255 to +256
return routeKeyInRange(store.ExtractLegacyListUserKeyFromDelta(rawKey), routeStart, routeEnd) ||
routeKeyInRange(store.ExtractListUserKey(rawKey), routeStart, routeEnd)

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 Avoid routing legacy list deltas by synthetic base keys

For real legacy list delta rows (!lst|meta|d|<len><user><ts><seq>), the fallback ExtractListUserKey treats the same bytes as a base list-meta key whose user key starts with d|.... In a migration whose route range includes that synthetic d| key (for example [d|, d})), this OR includes legacy deltas for unrelated list users, so those raw delta versions can be exported/imported into the wrong shard in addition to the shard owning the decoded legacy user key. The base-meta fallback needs to be disambiguated from actual legacy delta rows, rather than accepting both route interpretations unconditionally.

Useful? React with 👍 / 👎.

Comment thread store/lsm_migration.go
Comment on lines +215 to +216
if startKey == nil {
return false

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 Preserve empty keys for explicit empty starts

When callers pass StartKey: []byte{} with a non-empty EndKey, the logical range still includes the empty user key, but Pebble's encoded empty key sorts after ordinary non-empty keys. Because this stop check treats explicit empty start as safe to stop at the first userKey >= EndKey, ExportVersions returns Done before reaching a trailing empty-key version (e.g. ["", "b") with keys "" and "b" exports nothing). Treat an empty start like the unbounded case here so migrations do not drop empty user keys.

Useful? React with 👍 / 👎.

bootjp added 22 commits July 14, 2026 23:19
## Summary

Author: bootjp

Implements the M2-PR5 migration guards:

- reject writes that target `WriteFenced` routes in the coordinator and
FSM
- reject `DEL_PREFIX` by route-footprint intersection, including
full-range deletes
- add a route-faithful transaction-lock drain helper that scans lock
storage and filters by decoded route key
- reject same-group `SplitRange` requests that overlap a live split job
while allowing disjoint same-group splits

## Validation

- `GOCACHE=$(pwd)/.cache GOTMPDIR=$(pwd)/.cache/tmp go test ./kv
./distribution ./adapter -run
'TestFSMRejects|TestShardedCoordinatorRejects|TestPendingTxnLocksInRoute|TestDistributionServerSplitRange_(RejectsLiveSplitJobOverlap|AllowsDisjointRouteWhileSplitJobLive|Success|UsesCoordinatorForCatalogWrites)|TestPlanMigrationBrackets|TestMigrationKnownInternalPrefixes|TestValidateMigrationRouteRange|TestSplitJobPlanner|TestVerifyComposed1|TestKvFSM'
-count=1 -timeout=240s`
- `GOCACHE=$(pwd)/.cache GOTMPDIR=$(pwd)/.cache/tmp go test ./kv
./distribution -count=1 -timeout=240s`
- `GOCACHE=$(pwd)/.cache GOLANGCI_LINT_CACHE=$(pwd)/.golangci-cache
golangci-lint run ./kv ./distribution ./adapter --timeout=5m`
@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 (549a786):

  • distribution/engine.go
  • distribution/engine_test.go
  • distribution/migrator.go
  • distribution/migrator_export_plan_test.go
  • distribution/split_job_catalog.go
  • kv/coordinator.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 16, 2026

Copy link
Copy Markdown
Owner Author

@codex review

1 similar comment
@bootjp

bootjp commented Jul 16, 2026

Copy link
Copy Markdown
Owner Author

@codex review

@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: 549a78689d

ℹ️ 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/shard_key.go
Comment on lines +151 to +158
func listRouteKey(key []byte) []byte {
if userKey := store.ExtractListUserKeyFromDelta(key); userKey != nil {
return userKey
}
if user := redisSetRouteKey(key); user != nil {
return user
if userKey := store.ExtractListUserKeyFromClaim(key); userKey != nil {
return userKey
}
return redisZSetRouteKey(key)
return 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 Decode legacy list deltas before generic list keys

When a pre-upgrade list still has uncompacted !lst|meta|d|... delta rows, this normalizer does not handle the legacy delta prefix. Those keys then fall through to the generic ExtractListUserKey extractor as if they were base !lst|meta| keys for a user key beginning with d|..., so RouteKeyFilter can assign the legacy delta to the wrong route and omit it from split migration/export cleanup for the actual list key. Add ExtractLegacyListUserKeyFromDelta here before generic list-key extraction.

Useful? React with 👍 / 👎.

Comment thread cmd/redis-proxy/main.go
Comment on lines 125 to 128
secondarySeeds := parseAddrList(cfg.SecondaryAddr)
if len(secondarySeeds) == 0 {
return fmt.Errorf("at least one secondary address is required")
return nil, nil, fmt.Errorf("at least one secondary address is required")
}

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 Allow redis-only mode without secondary seeds

In redis-only mode the switch below returns a NoopBackend for the secondary, and raw passthrough never uses ElasticKV, but this unconditional check still rejects -secondary "". Operators trying to run the new Redis-only/raw proxy without configuring an ElasticKV address will fail startup with at least one secondary address is required; move this validation into the modes that actually dial ElasticKV.

Useful? React with 👍 / 👎.

Comment thread adapter/redis_txn.go
Comment on lines +1657 to +1661
func (r *stringReplacement) needsFullLogicalDelete() bool {
if !r.rawTypKnown {
return true
}
return isNonStringCollectionType(r.rawTyp)

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 Delete legacy string encodings on transactional SET

When MULTI/EXEC SET replaces a key whose existing raw encoding is still reported as redisTypeString but is not the new !redis|string| row, such as a HyperLogLog under !redis|hll|... or a pre-migration bare string, this predicate now skips deleteLogicalKeyElems. buildReplacementElems then writes the new string without deleting those old rows; for example PFCOUNT explicitly checks redisHLLKey and can keep returning the stale HLL cardinality after the transaction instead of seeing the replaced string. Preserve the full logical delete for HLL/legacy string encodings, not only for non-string collection types.

Useful? React with 👍 / 👎.


setter, hasSetter := fsm.(raftengine.SnapshotHeaderApplier)
ceiling, cutover, err := readSnapshotHeaderOrDrain(setter, hasSetter, tee)
ceiling, cutover, err := setter.ParseSnapshotHeader(io.LimitReader(file, payloadSize))

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 Verify the snapshot header before applying skip state

On the cold-start skip path where the local FSM has already applied at least the snapshot index, this now applies header state after only checking that the stored footer still equals the token CRC. If the .fsm header bytes are corrupted in place while the old footer remains, ParseSnapshotHeader can still return a plausible but wrong HLC ceiling or cutover and ApplySnapshotHeader installs it; the full restore path would have caught the same corruption by recomputing the CRC over the payload before applying state. Reintroduce integrity verification for the bytes used to derive header side effects, or store a separate header checksum.

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