Skip to content

store: add migration version import export#1085

Open
bootjp wants to merge 38 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 38 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 Plus

Run ID: 8b865865-3a99-49e4-9962-ac27512b0efa

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.

@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: 061275ab2e

ℹ️ 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
return false, false, errors.WithStack(err)
}
rawKey := iter.Key()
if isPebbleMetaKey(rawKey) {

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 Skip writer registry rows during Pebble exports

When the Pebble DB contains encryption writer-registry rows (!encryption|writers|...), a whole-range export starting at StartKey == nil will iterate those raw non-MVCC keys before normal user keys. Because this guard only skips the existing meta/migration keys, decodeExportedPebbleVersion then parses the 12-byte registry value as an MVCC value, which can either fail the export with a value-header error or emit a bogus version for import. Migration exports of encrypted stores need to exclude this metadata prefix before decoding user versions.

Useful? React with 👍 / 👎.

Comment thread store/lsm_migration.go Outdated
Comment on lines +109 to +110
if userKey == nil || pebbleExportCursorEqual(pos, userKey, commitTS) {
return true, 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 Resume past keys pruned by MinCommitTSExclusive

When skipPebbleExportVersionBelowMinTS hits MaxScannedBytes, the cursor it returns names the first version at or below MinCommitTSExclusive, which means the entire rest of that user key is known to be outside the export window. On resume this equality check skips only that exact version and then continues with older versions of the same key, so a hot key with many old versions can produce one empty scan-budget chunk per obsolete version instead of advancing to the next user key. If the cursor timestamp is already <= MinCommitTSExclusive, resume should skip the rest of that key.

Useful? React with 👍 / 👎.

Comment thread store/snapshot_pebble.go
Comment on lines 79 to 81
for iter.First(); iter.Valid(); iter.Next() {
k := iter.Key()
v := iter.Value()

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 Preserve migration import metadata in Raft snapshots

kvFSM.Snapshot delegates to store.Snapshot, so this filter also applies to Raft snapshots, not just ad-hoc backups. During an in-flight import, dropping _migack / _mighlc from the snapshot makes a restored voter forget the per-bracket high-water mark and HLC floor; after a leader change it can reject the next batch as ErrImportBatchGap or lose the target-local floor needed after cutover. Migration metadata that is part of the target group's applied state needs to survive FSM snapshot/restore, or the backup/export path needs a separate filter.

Useful? React with 👍 / 👎.

Comment thread store/lsm_migration.go Outdated
Comment on lines +166 to +168
for prefixLen := range userKey {
prefix := userKey[:prefixLen]
if (startKey == nil || bytes.Compare(prefix, startKey) >= 0) && bytes.Compare(prefix, endKey) < 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 Stop end-only Pebble exports at the range boundary

For a first-route export with StartKey == nil and a non-empty EndKey, the prefixLen == 0 iteration makes the empty prefix look like a possible in-range key, so this returns false for every key at or beyond EndKey. skipPebbleExportKeyOutsideRange then skips those out-of-range keys one user key at a time without charging ScannedBytes, meaning the final page for [nil, EndKey) can walk the entire rest of the Pebble DB to EOF despite the requested range and any scan budget.

Useful? React with 👍 / 👎.

@bootjp

bootjp commented Jul 13, 2026

Copy link
Copy Markdown
Owner Author

@codex review

Addressed the current migration export/snapshot findings in 31ed507:

  • skip encryption writer-registry raw Pebble rows during migration exports
  • resume MinCommitTSExclusive-pruned hot keys past the whole pruned user key instead of re-walking stale versions chunk by chunk
  • preserve migration import ack/HLC-floor metadata in native Pebble snapshots and restores so Raft snapshots keep in-flight import state
  • stop end-only Pebble exports once the decoded user key reaches the route end boundary

Caller audit:

  • Snapshot callers are kvFSM/raft snapshot persistence and LeaderRoutedStore pass-through; preserving migration metadata matches the Raft snapshot safety requirement.
  • ExportVersions/ImportVersions/MigrationHLCFloor are implemented in store and passed through by LeaderRoutedStore; ShardStore remains unsupported in this PR.

Validation:

  • go test ./store -run TestExportVersions(MinTSPruneCursorSkipsWholeKey|MinTSSkipHonorsScanBudget|MinTSPruneDoesNotSkipPrefixedKeys|UsesUserKeyRangeBounds)|TestPebbleExport(SkipsWriterRegistryRows|StopsAtEndKey)|TestPebbleSnapshotPreservesMigrationMetadata|TestPebbleImportMetadataPersistsAcrossReopen -count=1
  • go test ./store -run TestPebbleStore_SnapshotRestore|TestPebbleStore_Restore|TestPebbleSnapshotPreservesMigrationMetadata|TestPebbleExportSkipsWriterRegistryRows -count=1
  • go test ./store -count=1
  • go test ./kv -run Test.*Snapshot|TestFSM.*Snapshot -count=1
  • golangci-lint --config=.golangci.yaml run ./store --timeout=5m
  • git diff --check HEAD~1..HEAD
  • commit hook: golangci-lint --config=.golangci.yaml run --fix (0 issues)

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

  • 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: 31ed5074c4

ℹ️ 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_store.go Outdated
bytes.Equal(rawKey, metaAppliedIndexBytes)
bytes.Equal(rawKey, metaAppliedIndexBytes) ||
isMigrationMetadataKey(rawKey) ||
bytes.HasPrefix(rawKey, encryption.WriterRegistryPrefix)

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 Do not drop user keys under writer prefix

When a user key starts with !encryption|writers|, its MVCC Pebble row is encoded as userKey || timestamp, so this new prefix check treats the committed version as writer-registry metadata and skips it during Pebble ExportVersions. PutAt still accepts such keys and the in-memory exporter returns them, so a migration from a Pebble store can silently omit data for those keys; restrict the skip to actual registry-row shapes or reject this namespace before writes.

Useful? React with 👍 / 👎.

Comment thread store/lsm_migration.go
Comment thread store/lsm_migration.go

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

ℹ️ 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 thread internal/s3keys/keys.go
Comment thread distribution/migrator.go
Comment thread store/list_helpers.go
@bootjp
bootjp force-pushed the design/hotspot-split-m2-wire branch 3 times, most recently from 6b40846 to 644fd08 Compare July 23, 2026 09:18

@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: 93dfbb3c44

ℹ️ 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/mvcc_store.go Outdated
Comment on lines +1021 to +1022
s.migrationAcks = make(map[migrationAckID]migrationImportAck)
s.migrationHLCFloors = make(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 Preserve migration metadata in memory snapshots

On the in-memory MVCC store path, if a snapshot is taken after ImportVersions has acknowledged a migration batch, restoring that snapshot rebuilds the data tree but then drops the snapshotted ack/floor state because writeSnapshotBody never writes these maps. The restored target will accept the same BatchSeq: 1 again as non-duplicate and MigrationHLCFloor returns 0, diverging from the Pebble implementation and breaking import idempotency for tests or any in-memory shard; the snapshot format needs to serialize and restore these maps rather than always recreating them empty.

Useful? React with 👍 / 👎.

Comment thread proto/distribution.proto
rpc GetTimestamp (GetTimestampRequest) returns (GetTimestampResponse) {}
rpc ListRoutes (ListRoutesRequest) returns (ListRoutesResponse) {}
rpc SplitRange (SplitRangeRequest) returns (SplitRangeResponse) {}
rpc StartSplitMigration (StartSplitMigrationRequest) returns (StartSplitMigrationResponse) {}

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 Implement advertised split-migration RPCs

With this method now in the public Distribution service, generated clients can call StartSplitMigration, but the registered adapter.DistributionServer still only gets this method from its embedded pb.UnimplementedDistributionServer and repo-wide search shows no server implementation for it or the sibling split-job RPCs. In deployments registering NewDistributionServer, starting a migration through the advertised API will return gRPC Unimplemented; either wire the server methods in this change or keep the RPCs out of the service until they are usable.

Useful? React with 👍 / 👎.

Comment thread adapter/dynamodb_transact.go Outdated
}

func isRetryableTransactWriteError(err error) bool {
return errors.Is(err, store.ErrWriteConflict) || errors.Is(err, kv.ErrTxnLocked) || errors.Is(err, kv.ErrRouteWriteFenced)

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 Retry forwarded route fences

This retry predicate only recognizes a typed kv.ErrRouteWriteFenced, but follower-routed writes that go through Coordinate.redirect receive the leader's Internal.Forward failure as a gRPC status with the original error chain stripped; the Redis retry code already needs explicit wire parsing for write conflicts/locks for the same path. When a DynamoDB/SQS mutation is served locally on a follower and hits a route fence, it now falls out of the retry loop as a non-retryable server error instead of waiting for migration; add a wire/status matcher for the route-fence error wherever these new retry branches are used.

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 (1df401d):

  • distribution/catalog.go
  • distribution/catalog_test.go
  • 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.

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

  • distribution/catalog.go
  • distribution/catalog_test.go
  • 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 23, 2026

Copy link
Copy Markdown
Owner Author

対応しました。

変更内容:

  • memory MVCC streaming snapshot v2でmigration import ack/HLC floorを保存・復元
  • memory snapshotをPebbleへ復元する経路でもmigration metadataをPebble metadataとして保存
  • route write fenceをtyped errorだけでなくgRPC status経由でもretry対象化し、attempt保存/race無視からは除外

検証:

  • go test ./store -run 'TestMVCCStore_(SnapshotRestoreRoundTrip|RestoreRejectsInvalidChecksum|RestoreClearsMigrationMetadata|SnapshotRestorePreservesMigrationMetadata)|TestPebbleStore_RestoreFromStreamingMVCC$' -count=1\n- go test ./adapter -run 'Test(WriteFenceErrorsAreAdapterRetryable|WireWriteFenceErrorsAreAdapterRetryable|WireWriteFenceMatcherRequiresSentinelSuffix)' -count=1\n- go test ./store -run 'Test(ImportVersionsIdempotencyAndMetadata|PebbleMigrationMetadataSurvivesReopen|PebbleSnapshotPreservesMigrationMetadata|PebbleStore_RestoreFromStreamingMVCCPreservesMinRetainedTS|MVCCStore_RestoreClearsMigrationMetadata|MVCCStore_SnapshotRestorePreservesMigrationMetadata)' -count=1\n- go test ./adapter -run 'Test(WriteFenceErrorsAreAdapterRetryable|WireWriteFenceErrorsAreAdapterRetryable|WireWriteFenceMatcherRequiresSentinelSuffix|S3Server_AdminDeleteBucket_RetriesSafetyNetRouteFence|S3Server_AdminDeleteBucket_SwallowsPersistentSafetyNetRouteFence|DynamoDB|SQS).*RouteFence|Test.*RouteFence' -count=1\n- go test ./... -run '^$'\n- golangci-lint run ./... --timeout=5m\n- git diff --check\n\n@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 (c7dd014):

  • distribution/catalog.go
  • distribution/catalog_test.go
  • 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 23, 2026

Copy link
Copy Markdown
Owner Author

追加でCIのJepsen Test起動失敗を修正しました。

変更内容:

  • kv.ShardStoreにLocalStores()を追加し、S3 chunkblob backfill startup scannerがsharded storeでも動くようにしました。

追加検証:

  • go test ./kv -run 'TestShardStoreLocalStoresReturnsLocalShardStoresInStableOrder' -count=1\n- go test ./adapter -run 'TestS3BlobBackfiller(StartupScanRecoversUnobservedRef|FetchesAppliedRefFromAlternatePeerAfterMismatch|RepairsCorruptLocalBlob)|TestS3BlobBackfillConfigFromEnvRejectsUnboundedValues' -count=1\n- go test ./... -run '^$'\n- golangci-lint run ./... --timeout=5m\n- git diff --check\n- go build -o /tmp/elastickv-bin .\n- CIと同じ3ノード起動手順でredis/dynamo/s3/sqs listenerが全てopenすることをローカル確認\n\n@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 (dcb7e2c):

  • distribution/catalog.go
  • distribution/catalog_test.go
  • 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 23, 2026

Copy link
Copy Markdown
Owner Author

対応内容:

  • SplitRange の coordinator dispatch に採番済み commit timestamp を渡し、catalog split の SplitAtHLC patch と実コミット timestamp を一致させました。
  • CI の go test -race ./... で失敗していた TestDistributionServerSplitRange_UsesCoordinatorForCatalogWrites をローカル再現し、修正後に通常/ -race の両方で確認しました。

検証:

  • go test ./adapter -run 'TestDistributionServerSplitRange_UsesCoordinatorForCatalogWrites' -count=1 (修正前に同失敗を再現)
  • go test ./adapter -run 'TestDistributionServerSplitRange_(UsesCoordinatorForCatalogWrites|ReturnsExactCommittedSplitVersion|RetriesCatalogReloadUntilVisible)' -count=1
  • go test -race ./adapter -run 'TestDistributionServerSplitRange_UsesCoordinatorForCatalogWrites' -count=1
  • go test ./... -run '^$'
  • golangci-lint run ./... --timeout=5m
  • git diff --check

GitHub確認:

  • latest head: dcb7e2c
  • latest-head unresolved current review threads: 0
  • mergeable: MERGEABLE
  • CI はこの head の新しい run を監視中です。

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

ℹ️ 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_store.go Outdated
Comment thread proxy/blocking.go
Comment thread kv/shard_store.go Outdated
@bootjp

bootjp commented Jul 23, 2026

Copy link
Copy Markdown
Owner Author

Evidence for current HEAD db7493c:

Addressed the latest findings:

  • LatestCommitTS now uses the same point-read route set as GetAt, preserving the legacy Redis wide-column raw-route fallback and returning the max visible latest timestamp across normalized and legacy routes.
  • Redis hash/set/zset wide-column scans now include both normalized logical routes and legacy raw internal-key routes, deduplicated by group.
  • Blocking XREADGROUP in dual-write mode is replayed to the secondary through the blocking replay queue so consumer-group pending/delivery state advances there too.

Caller audit:

  • Audited LatestCommitTSWithReadFence, pointReadRoutesWithVersion, latestCommitTSForRoute, routesForInternalScanWithVersion, redisWideColumnScanRoutesWithVersion, blockingReplayCommand, and DualWriter.Blocking dispatch paths.

Validation:

  • go test ./kv -run 'TestShardStore(RoutesForScanUsesWideColumnUserKeyAndLegacyRoute|ScanAt_RoutesExactRedisWideColumnScan|LatestCommitTS_IncludesLegacyRedisWideColumnRoute)' -count=1
  • go test ./proxy -run 'TestDualWriter_Blocking_(ReplaysXReadGroupToSecondary|XReadDoesNotUseWriteSemaphore|Replays)' -count=1
  • go test ./kv ./proxy -count=1
  • go test ./... -run '^$' -count=1 -timeout=10m
  • golangci-lint --config=.golangci.yaml run ./kv ./proxy --timeout=5m --allow-parallel-runners
  • git diff --check
  • commit signature verified locally for bootjp contact@bootjp.me

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

  • distribution/catalog.go
  • distribution/catalog_test.go
  • 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.

@chatgpt-codex-connector

Copy link
Copy Markdown

Codex Review: Didn't find any major issues. What shall we delve into next?

Reviewed commit: db7493c8e2

ℹ️ About Codex in GitHub

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

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

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

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

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant