Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion SAFETY.md
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ The invariant registry (invariant IDs referenced below) lives in
| `pkg/preflight` — precondition verifier, refusals | ✅ core | exists; copy-and-swap target proof declaration exists | ST-6, RF-1..RF-5 |
| `pkg/executor` — bounded optimistic attempt; native concurrent index build with invalid-index recovery; native sequence executor for the safer idioms | ✅ core | exists (Phase 1: attempt-under-budget; Phase 3.1: concurrent index build; Phase 3.2: sequence executor) | LK-2 (attempt bound + the CONCURRENTLY wait-policy exception), CO-9 (qualified proof reads), ST-9 (create owner verified, never repaired) |
| `pkg/checksum` — chunk verifier, continuous checker, repair | ✅ core | types and proof-type declarations exist; verifier planned | CO-1, CO-2, CO-3 |
| `pkg/copier` — shadow-table chunked copy | ✅ core | contract types and the keyset `Chunker` exist (row-count chunks over the proven key, first chunk open below and last open above, a cut frontier for the applier's discard rule, time-targeted sizing); copy step planned | CO-4 (chunk coverage), LK-3 |
| `pkg/copier` — shadow-table chunked copy | ✅ core | contract types and the keyset `Chunker` exist (row-count chunks over the proven key, first chunk open below and last open above, a cut frontier for the applier's discard rule, time-targeted sizing) and the parallel `Copier` (one bounded never-overwriting insert per chunk under the table lock session, in-flight registry, `Position.Classify` for the applier) exist; progress fillers planned | CO-4 (chunk coverage, copy SQL shape, in-flight registry), LK-1, LK-3 |
| `pkg/applier` — change apply, buffer, flush scheduling | ✅ core | package contract exists; applier planned | CO-4, CO-5, CO-6, CO-8, LK-3 |
| `pkg/decode` — logical decoding, LSN/position accounting, per-column presence | ✅ core | contract types exist; decoder planned | ST-4, CO-4, CO-8 |
| `pkg/checkpoint` — durable resume state | ✅ core | checkpoint contract exists; persistence planned | ST-1, ST-2 |
Expand Down
2 changes: 1 addition & 1 deletion docs/architecture.md
Original file line number Diff line number Diff line change
Expand Up @@ -200,7 +200,7 @@ different levels of commitment:
| `pkg/router` | Route classified statements to native / copy-and-swap / refuse dispositions; copy-and-swap reports unavailable until that backend lands | exists (Phase 2.4) |
| `pkg/executor` | Native backend with stable outcome codes: the bounded optimistic attempt, the concurrent index build and its invalid-index recovery, the autocommit safer-sequence runner, the greenfield `CREATE TABLE` path, and the accepted-blocking passthrough primitive; the full `Executor` contract (`Plan`/`Execute`/`Status`/`Abort`) arrives with the copy-and-swap backend | native execution exists |
| `pkg/progress` | Strategy-wide, pollable progress snapshots: native phase/elapsed time, sequence position, retry attempt, and server-reported concurrent-index work; optional copy counters are reserved for copy-and-swap | native progress exists |
| `pkg/copier` | PK-range chunker over one integer-family primary key with dynamic time-based sizing (produces `Chunk` and `Watermark`; composite keys refused in v1), and the parallel chunked copy into the shadow table (never overwrites) — there is no separate chunker package | contracts exist; copy loop Phase 4 |
| `pkg/copier` | PK-range chunker over one integer-family primary key with dynamic time-based sizing (produces `Chunk` and `Watermark`; composite keys refused in v1), and the parallel chunked copy into the shadow table (never overwrites; reports the cut frontier, in-flight chunks, and landed watermark for the applier) — there is no separate chunker package | chunker and copy loop exist; progress fillers planned |
| `pkg/checksum` | The mandatory correctness gate; continuous checker; repair primitive | Phase 5 |
| `pkg/decode` | Logical-decoding change capture, LSN accounting, slot lifecycle | Phase 6, 8 |
| `pkg/applier` | Change apply onto the shadow (always wins), buffer/dedup, flush scheduling | Phase 6 |
Expand Down
6 changes: 3 additions & 3 deletions docs/copy-and-swap-design.md
Original file line number Diff line number Diff line change
Expand Up @@ -277,7 +277,7 @@ observation and policy.
**Where enforced.** `pkg/copier` (`Chunker`: chunks are sized in rows and cut by keyset from the
live table, so sparse and dense key spaces yield equal work per chunk; each timing feedback scales
the measured chunk's own row count toward the target by at most a factor of two, within a configured
floor and ceiling, so concurrent workers' reports do not compound) and `pkg/decode`; LK-3, ST-3.
floor and ceiling, so concurrent workers' reports do not compound; `Copier` times each chunk from claim to commit on an injected clock and feeds it back) and `pkg/decode`; LK-3, ST-3.

### D13 — Recover unique-secondary-key moves batch-wide

Expand Down Expand Up @@ -364,9 +364,9 @@ decoding but adds write-path availability and amplification costs.

| Package | Responsibility and proof types | Invariants |
| --- | --- | --- |
| `pkg/dbconn` | Produces `TableLock`. | LK-1 |
| `pkg/dbconn` | Produces `TableLock`, carried by `TableLockSession`; `Confirm` is the in-transaction check every writer runs from its own connection before its first write. | LK-1 |
| `pkg/preflight` | Produces `CopySwapTarget`, the copy-and-swap route's proof (the table facts `PreflightedTable` carries plus the v1 shape, replica identity, dependent-object, decoding, and headroom checks above); owns Tier-3 refusals. | ST-6, RF-1..RF-3 |
| `pkg/copier` | Produces `Chunk` and `Watermark`; `Chunker` (built only from a `CopySwapTarget`) cuts consecutive chunks that tile the whole int64 key space — first open below, last open above — so every key a row can carry belongs to exactly one chunk and a watermark at the largest value means the copy is complete. | CO-4, LK-3 |
| `pkg/copier` | Produces `Chunk` and `Watermark`; `Chunker` (built only from a `CopySwapTarget`) cuts consecutive chunks that tile the whole int64 key space — first open below, last open above — so every key a row can carry belongs to exactly one chunk and a watermark at the largest value means the copy is complete. `Copier` (built from a `CopySwapTarget`, a `Shadow` — the shape `schemachange.BuiltShadow` satisfies — and the table's `TableLockSession`) copies chunks with several workers, each in its own bounded transaction under the owner's role that confirms the lock and both relation OIDs before one frozen never-overwriting insert; `Position` snapshots the cut frontier, in-flight chunks, and landed watermark, and `Position.Classify` is the applier's uncut / in-flight / landed rule. | CO-4, LK-1, LK-3 |
| `pkg/checksum` | Produces `VerifiedShadow` and `CleanWatermark`; their constructors are private to this package. | CO-1, CO-2, CO-3 |
| `pkg/decode` | Produces `ChangeEvent`, including per-column presence and `OldKey` for an UPDATE that moved the primary key. | ST-3, ST-4, CO-4, CO-8 |
| `pkg/applier` | Applies presence-aware events from the per-key buffer. | CO-4, CO-5, CO-6, CO-8, LK-3 |
Expand Down
25 changes: 18 additions & 7 deletions docs/invariants.md
Original file line number Diff line number Diff line change
Expand Up @@ -101,8 +101,14 @@ defers for keys in in-flight chunks. With one worker the two positions coincide.
whole int64 key space (first open below, last open above), so every key a row can carry belongs
to exactly one chunk, and `Cut` reports the frontier so that "not yet cut" always names a chunk
the copier will still read (coverage, resume-from-watermark, empty-table, frontier-after-each-cut,
and cross-type key tests). *Planned enforcement:* copier/applier SQL shapes, the in-flight chunk
registry, and flush scheduling that defers any flush overlapping an in-flight chunk's key range
and cross-type key tests); `pkg/copier` `Copier` — every chunk runs one frozen
`INSERT … SELECT … WHERE pk BETWEEN $1 AND $2 ON CONFLICT (pk) DO NOTHING` in its own bounded
transaction, a chunk is registered in flight before its transaction begins and removed only after
it commits or rolls back, and `Position` snapshots the cut frontier, the in-flight chunks, and the
landed watermark under one lock so `Position.Classify` gives the applier the three-way answer
(uncut / in-flight / landed) for any key (whole-table, never-overwrites, resume-from-watermark,
out-of-order landing, and pinned-chunk cancellation tests). *Planned enforcement:* the applier's
SQL shape and flush scheduling that defers any flush overlapping an in-flight chunk's key range
(mutual exclusion, not tombstone retention). *Test obligation:* a
marker-bearing UPDATE for a key inside an in-flight chunk asserts the flush waits for the chunk
and the row is then completed from the copied shadow row, never an absent-row abort; a
Expand Down Expand Up @@ -255,9 +261,11 @@ cancellation tests); `pkg/schemachange` shadow build, drop, and inspect each req
session for the proven table, run under its `Bind` context, and confirm from their own
transaction that the session's backend holds the lock before the first write (nil-session,
wrong-table, reported-loss, gone-session, rival-backend, mid-build-loss, and mid-drop-loss
tests). *Planned enforcement:* the copier and
cutover acquire the same session before their first write and run under it, so loss of the
lock aborts the change at every stage.
tests); `pkg/copier` `Copier` requires the same session, runs every chunk transaction under
its `Bind` context, and calls `TableLockSession.Confirm` from each chunk's own connection before
the insert (wrong-table, gone-session, rival-backend, and mid-copy-loss tests). *Planned
enforcement:* cutover acquires the same session before its first write and runs under it, so
loss of the lock aborts the change at every stage.
*Source:* Spirit `pkg/dbconn/metadatalock.go` (stated pool invariants). This resolves the
mutual-exclusion gap called out in the validation review.

Expand Down Expand Up @@ -291,8 +299,11 @@ pending set **and** incrementing an in-flight counter **in the same critical sec
one path (success, error, or cancellation cleanup) can claim an entry, so its completion callback
runs exactly once. The claimer invokes the callback **without** holding the lock (callbacks may
be slow or re-enter the applier). `Wait()` returns only when the pending set is empty **and** the
in-flight counter is zero — it can never return while a callback is still running. *Enforced:*
applier/copier concurrency structure. *Source:* Spirit `pkg/applier/single_target.go` +
in-flight counter is zero — it can never return while a callback is still running. *Enforced
today:* `pkg/copier` `Copier.Run` returns only after every worker has exited, so no chunk
transaction is in flight and the in-flight set is empty when a caller checkpoints the watermark
(cancellation and lock-loss tests pin one chunk mid-insert and assert nothing remains in flight).
*Planned enforcement:* applier concurrency structure. *Source:* Spirit `pkg/applier/single_target.go` +
`sharded.go` ("Completion invariant", block/spirit#765).

### LK-4 — An ambiguous cutover outcome is resolved by inspection, never assumed
Expand Down
Loading
Loading