mirror of
https://github.com/seaweedfs/seaweedfs.git
synced 2026-09-20 13:30:46 +02:00
docs(sw-block): normative Drive/Apply pseudocode and cross-links
Add §6.3 Drive(input) and §6.10 ApplyWAL/ApplyBASE blocks with state, atomic envelope, and INV wiring; align cursor/head with exclusive-slot semantics plus §6.1/CHK-REWIND note; revise §13 StrictRealtimeOrdering for cursor convention. Wal-shipper spec §7.3 references consensus §6.3; §7.4 points at §6.10 pseudocode. Mini-plan §12 defers Drive to consensus §6.3 only (v0.11). Consensus v3.14.
This commit is contained in:
pingqiu
@@ -24,7 +24,7 @@ These are **not** preferences — they are the **minimal joint axioms**. Everyth
|
||||
### 1. Boundary & truth (**P1**)
|
||||
|
||||
- **Recover is a bounded session**, not ambient state (`StartSession … EndSession` / fail).
|
||||
- **Authoritative convergence** toward **healthy replicated state** is proven only via **explicit barrier handshake** **`AchievedLSN ≥ engineered target`** together with **`baseDone` / layer-1 conjunct as defined by product**. **Inferring “done” from traffic silence, Kind ratios, or sender idle windows is forbidden.**
|
||||
- **Authoritative convergence** toward **healthy replicated state** is proven only via **explicit barrier handshake** whose **`AchievedLSN`** and receiver conjuncts match the **engine-authored cut semantics** for **that session** (**§6.9**, **§IV `T2`**) together with **`baseDone` / layer-1 conjunct as defined by product**. **Inferring “done” from traffic silence, Kind ratios, or sender idle windows is forbidden.**
|
||||
|
||||
### 2. Exactly one causal WAL frontier per peer-session (**P2**)
|
||||
|
||||
@@ -54,7 +54,8 @@ These are **not** preferences — they are the **minimal joint axioms**. Everyth
|
||||
|
||||
### 7. Engine owns trigger numbers (**P7**)
|
||||
|
||||
- **`fromLSN` / `pinLSN` / `targetLSN`** are **frozen or engine-authored** facts at session admission; transport **silently overwriting** (`fromLSN := 0` when engine chose `R+1`) violates **parity** with decision logic.
|
||||
- **`fromLSN` / pin lower bound** (**`pinLSN` when product distinguishes them**): **frozen or engine-authored** at session admission; transport **silently overwriting** (`fromLSN := 0` when engine chose `R+1`) violates **parity** with decision logic.
|
||||
- **`targetLSN` (when carried on wire / coordinator)**: names **only** the **historical WAL job upper bound `Y`** per **§6.9** — **not** the Primary tape’s physical end (**`head` keeps moving**). Implementations MUST NOT treat “`shipCursor` reached `targetLSN`” as equivalent to **`cursor == head`** or **steady healthy** unless **§6.9 Phase C** is already satisfied under the closed **§IV `T2`** semantics.
|
||||
|
||||
---
|
||||
|
||||
@@ -122,6 +123,55 @@ Implementations **must** obey the **scheduler choices** below. Prose **`send(...
|
||||
|
||||
**Dual-mode carve-out (**`WalShipper`**)**: **`ModeBacklog`** vs **`ModeRealtime`** (**steady / no substrate replay**) is **architect‑approved** under **`§13 — E‑WALSHIPPER‑DUAL‑MODE`**. **`§6.3**(A)(B)** and **§6.8**(3)(4)(9) remain **literally normative in Backlog**; Realtime semantics **do not** replace **P2 / §6.8(1)/(5) / §6.4**.
|
||||
|
||||
##### Reference pseudocode — **`Drive(input)`** (**single serializer**, **`HOPE‑SHIPPER‑MONOTONIC`**)
|
||||
|
||||
**Purpose**: every reviewer instantiates the **same** (**a**) state, (**b**) atomic boundaries, (**c**) **`INV`** links — not a second informal compilation.
|
||||
|
||||
**Dense‑LSN product**: sparse / non‑contiguous LSNs **`MUST`** replace literal **`+1`** step and dense **`ReadAtLSN`** with **`NextPresentLSN` / product scan — **architect leaf**. **Substrate** **`ReadAtLSN(k)`** is **semantic** only — **batch prefetch** **MAY** hide behind it (**mini-plan §12.4 #1**).
|
||||
|
||||
**§6.1 / §V (`CHK‑RECOVER‑REWIND‑ONCE`) alignment**: **`cursor`** here is **`next LSN to emit`** (**same convention as **`v3-recovery-wal-shipper-spec.md` §7.1** `while cursor < head`**). **`§6.1 **`cursor[P] := fromLSN`** **and** engine **`fromLSN`** **MUST** be paired so **first lawful ship `lsn`**, **`ReadAtLSN(cursor)`** (debt path), and receiver **`expect_next_LSN`** after rewind (**spec §7.4**) **agree** — **exclusive‑floor **`fromLSN`** ⇒ commonly **`cursor := fromLSN+1`** for first frame **`lsn = fromLSN+1`**; **inclusive / product variants** **`MUST`** document the mapping **without** drifting **`Drive`** cases.
|
||||
|
||||
```text
|
||||
# —— (a) STATE (per peer P, under one serializer lock) ——
|
||||
state:
|
||||
cursor : LSN # next LSN to emit (unsent prefix starts at cursor; §6.2 debt = cursor < head)
|
||||
fifo : queue<Append> # single mailbox — NO separate backlog/live queues
|
||||
head() : LSN # consistent read: exclusive next-assign slot (dense: new append takes lsn==head, then head++)
|
||||
|
||||
# —— (b) ATOMIC BOUNDARY — entire body runs under shipMu / single-writer serializer (P2, §6.4) ——
|
||||
# Event sources:
|
||||
# NotifyAppend(...) → fifo.push(Append); Drive(peek)
|
||||
# timer / ShipOpportunity → Drive(∅)
|
||||
|
||||
def Drive(input): # input ∈ { ∅, Append{lba,lsn,data} }
|
||||
|
||||
# CASE A — debt: next emit exists before tail (cursor < head).
|
||||
# FIFO: pending Append WAITS (§6.3(A) “incoming does not overtake debt”).
|
||||
if cursor < head():
|
||||
e := substrate.ReadAtLSN(cursor) # MUST be the record at exactly this LSN (dense)
|
||||
emit(e.lba, e.lsn, e.data)
|
||||
cursor := cursor + 1 # exactly one LSN advanced
|
||||
return # input (if any) stays in fifo
|
||||
|
||||
# CASE B — no debt: cursor == head. Tail path (steady / post-catch-up).
|
||||
if input is Append{lba, lsn, data}:
|
||||
if lsn == cursor: # dense: next assigned tail
|
||||
emit(lba, lsn, data)
|
||||
cursor := cursor + 1
|
||||
fifo.pop()
|
||||
return
|
||||
if lsn < cursor:
|
||||
fifo.pop() # idempotent retry / duplicate notify
|
||||
return
|
||||
# lsn > cursor — gap / contract violation. NO silent substrate scan to fill (§13 T4a spirit).
|
||||
raise CursorGap{cursor, lsn} # engine MUST rebuild-on-gap / re-anchor (NEGATIVE‑EQUITY ban on “heal by scan”)
|
||||
|
||||
# CASE C — ∅, cursor == head: nothing to ship
|
||||
return
|
||||
```
|
||||
|
||||
**Derived invariant (sender → wire)** — **`INV‑WIRE‑WAL‑LSN‑MONOTONIC`**: **successful** **`emit(...)`** sequence in a session yields **strictly increasing `lsn`** with **no gaps** (dense) — **precondition** for **`INV‑RECV‑WAL‑NAIVE`** (**§6.10**).
|
||||
|
||||
#### 6.4 Flip / “mode transition” atomicity = **Primary Wal + ship serialization** (**R1**)
|
||||
|
||||
The historical **gap-at-flip** bug is **not** a magical “mode bit” — it is **check-then-act** between **“`cursor` caught `head`”** and **a concurrent append** extending **`head`**.
|
||||
@@ -176,7 +226,111 @@ If **sustained append rate > sustainable ship rate** for the session, **`head−
|
||||
|
||||
**Dual-mode scope (`§13`)**: Checklist items **(3)(4)(9)** (debt-before-tail priority, periodic idle drain tied to **`send(∅, debt)`**) are **`MUST`** in **`ModeBacklog`**; **`ModeRealtime`** obeys **`§13 — E‑WALSHIPPER‑DUAL‑MODE`**.
|
||||
|
||||
**Still open**: flip hysteresis (**§IV `T1`**), **`targetLSN`** vs **`head` at barrier** (**`T2`**), bearer policy while backlog exists (**`T3`**). Closing those rows **updates** checklist edge semantics but **does not** relax **(1)**–**(4)** **in **`ModeBacklog`**, **`§13`**, or **(9)** as read **`ModeBacklog`**.
|
||||
**Still open**: flip hysteresis (**§IV `T1`**), **`targetLSN`** vs **`head` at barrier** (**`T2`** — **process refinement in §6.9** must close into an explicit phased rule before code claims “healthy”), bearer policy while backlog exists (**`T3`**). Closing those rows **updates** checklist edge semantics but **does not** relax **(1)**–**(4)** **in **`ModeBacklog`**, **`§13`**, or **(9)** as read **`ModeBacklog`**.
|
||||
|
||||
### 6.9 `targetLSN` — **when to use what words** (**job-bound slice** vs **single-tape ship**)
|
||||
|
||||
Normative **`WalShipper`** truth is always **§6.2–6.4**: **one ordered tape**, **`cursor` vs `head`**, **`send(incoming, debt)` / `send(∅, debt)`**, **single serializer** (**P2**). **Recover does not contradict steady Wal**: it temporarily adds **lanes** (**base**, dual‑lane framing), not a **second causal ship owner**.
|
||||
|
||||
#### **Receiver-hard invariant — `Y` does not cut the WAL into two tapes**
|
||||
|
||||
**Normative**: A numeric **`targetLSN = Y` MUST NOT mean** “Primary WAL becomes **two independent ordered logs** (**≤Y** vs **>Y**).” The replica consumes **one** recover-WAL apply story: **§7 `checkMonotonic` / session state** advances on **every** **`(LSN, LBA, data)`** in **strict LSN order** relevant to **`StartSession..EndSession`**, regardless of wire **frame kind** (`WALKindBacklog` vs `WALKindSessionLive` …) or **whether** Primary used **`ScanLBAs`** vs **`NotifyAppend`** to **choose** emission order.
|
||||
|
||||
Permitted meaning of **`Y`** (**only**): a **sender-side scheduling / enumerator bound** (**how** Primary drains its **single** tape into frames) plus a **frozen lineage field for barrier/certification**. **Forbidden**: any design where the receiver treats **≤Y** and **>Y** as **separate ingest frontiers**, **restart rewind semantics**, or **reorder-permitted halves** — that **engineering shape is incompatible** (**applies-before / applies-after fights**, **duplicate or stale LSN**, **barrier nonsense**).
|
||||
|
||||
**Informative**: Framing prefixes “historical blob then tail blob” **on the wire** is allowed **only if** arrival + apply preserves **single global LSN monotonicity** as seen by **`RebuildSession`** — i.e. it is **one tape carried in two envelopes**, **not two truths**.
|
||||
|
||||
#### **Product veto — interpreting `target` as WAL “segmentation” is negative equity**
|
||||
|
||||
If **`targetLSN=Y`** appears in **architecture narrative** as **segmenting WAL** — i.e. “first segment done, mission accomplished” — without **WalShipper `cursor→head`** closure, architects classify that pattern as **`NEGATIVE‑EQUITY`**: recurring sessions, stalled adoption, confusion at **receiver** (**§6.9 invariant**) and **`MinPin`/retention** pressure. **`Y` MAY exist as lineage text** (**§IV `T2`**) but MUST NOT substitute for **tape monotonicity**.
|
||||
|
||||
#### **Positive model (`HOPE‑SHIPPER‑MONOTONIC`) — the only durable fix**
|
||||
|
||||
Implementations converge by keeping **WalShipper** as the **sole** causal advance of **unsent LSN prefix** (**P2**): **`cursor` moves forward monotonically** on **Primary’s one order** (**§6**), never “two halves decide independently.” Recover **inherits** steady Wal **strategy abstraction** (**§6.3**) — **explicitly**:
|
||||
|
||||
| Ship opportunity kind | **`send` form** | Role when **`cursor < head` (backlog / debt)** |
|
||||
|-----------------------|----------------|-----------------------------------------------|
|
||||
| **No freshly paired append on this tick** | **`send(∅, debt)`** | **Periodic / timer‑driven** **`emit-from-cursor`** — backlog **cannot** rely only on arrivals (**Primary‑idle starvation forbidden** — **§6.8 item 4** **`ModeBacklog`**). |
|
||||
| **Append visible / tail visible** | **`send(incoming, debt)`** | **Oldest‑unsent first** whenever debt non‑empty (**§6.3**(A)); **`incoming` extends** tape; **never** mailbox split. |
|
||||
|
||||
**Normative shorthand**: backlog’s “extra oxygen” is **empty‑input advancement** (**`send(∅, debt)`**); **choose‑among‑eligible** advancement when **`incoming` exists** is **`send(incoming, debt)`** — **same serializer**, **monotone `cursor`**. **Realtime carve‑outs** (**§13**) do **not** fork this story into **Wal segmentation**.
|
||||
|
||||
Some implementations (**today `seaweed_block`**) also carry **`targetLSN = Y`** on **lineage / coordinator**. **Mandatory reading**: **`Y` is not “the WAL tape ends here.”** **`head` may exceed `Y` at any instant** during the same session — new appends **extend** backlog as **`cursor < head`** on the **same** tape (**§6.2 operational debt**). Therefore:
|
||||
|
||||
| Phrase | Meaning |
|
||||
|--------|---------|
|
||||
| **Stream Wal ship** (**primary**) | **`WalShipper` decisions** advancing **`cursor` toward live `head`** under **§6.3 / §13** — **continuous**, append‑fed and timer‑fed in **ModeBacklog** as applicable. |
|
||||
| **Historical WAL job bound at `Y` (sender-only helper)** | **Primary-only**: a **bounded substrate read** that emits **backlog-class** frames for **`(fromLSN, Y]`** (e.g. **`ScanLBAs`** stops at **`LSN > Y`**). This is **one emission tactic** on the **same** tape — **not** “first tape then second tape” at the receiver (**see invariant above**). |
|
||||
| **`targetLSN = Y`** | **Lineage + coordinator**: freezes **`Y`** for **barrier text** and **sender bookkeeping**; **does not** fork replica apply order. |
|
||||
|
||||
#### Recover **process** (how a `Y`-bearing session reaches caught up and stays healthy)
|
||||
|
||||
Architects + implementers **MUST** document which phases their code performs; mismatches (**stopping after step 3 alone**) are **§IV `T2` bugs**. **Informative canonical skeleton**:
|
||||
|
||||
1. **Admit**: Engine publishes **`fromLSN`** (often **≈ rebuild semantic lower bound**) and **`Y`** (**`targetLSN`**) unchanged to **receiver lineage** (**§I P7**). **Coordinator** **`StartSession`** records both; **`pin`/recycle** obey **§I P6** / pin wire doc.
|
||||
2. **Base / extent lane** (**if used**): **GLOBAL block sweep** (**§5**) — dense or sparse **per product** — subject to **`bitmap`** arbitration (**P5**). **Independent of LSN**, except synthetic frontiers pinned by session contract.
|
||||
3. **Sender: bounded read for backlog-class frames ending at `Y`**: Emit **`(LSN,LBA,*)`** with **`fromLSN < LSN ≤ Y`** through recover bearer (**does not authorize a second replica WAL frontier** — **§6.9 invariant**).
|
||||
4. **Same serializer: tape tail (**`LSN > Y`**) into frames** (**Phase C**) via **WalShipper** only — **`NotifyAppend`**, **SessionLive**/seal, **`DrainBacklog`**, **ModeRealtime** per **§13**; obeys **`cursor→head`**. **`ScanLBAs` stopping at `Y` does not** permit **`cursor < head`** on Primary to stall without **WalShipper** drain (**§6.2**).
|
||||
5. **Barrier**: Receiver answers **`AchievedLSN`** consistent with **`Y` + Phase C semantics** (**§IV `T2`** must pin the exact predicate: e.g. **conjunct **`walApplied ≥ Y`** ∧ tail policy ∧ `baseDone`**). **§I P1** completion uses this handshake, **not** “silence after step 3 alone”.
|
||||
6. **End session → steady**: **`EndSession`**, steady **`Ship`/`NotifyAppend`** resumes; **`cursor == head`** in steady means **implementation‑lag‑only**, not **semantic policy debt reopened** (**§6.2** last paragraph). **Healthy** ⇒ engine **probe/decision** predicates satisfied (**control plane**, not **`Sender.Run` idle** alone).
|
||||
|
||||
#### Anti‑patterns (**normative DON’Ts**)
|
||||
|
||||
- **Treat “historical WAL job finished ( enumerator past `Y` / coordinator saw through `Y` )” as “WAL recover done”** while **`head > cursor`** on Primary — **violates §6.2**.
|
||||
- **`targetLSN=Y` marketed as WAL segmentation semantics** (**“Tape A then Tape B”**) — **`NEGATIVE‑EQUITY`** (**§6.9 Product veto**) — violates **receiver invariant**.
|
||||
- **`targetLSN` as UX throttle** forcing **cheap barrier** followed by **new session churn** whenever **`head` moves**, without **explicit product policy** — **risk per execution institution § Risk envelope**.
|
||||
- **`targetLSN` as silent substitute** for **`fromLSN` / rewind** (**P7 parity** violation).
|
||||
|
||||
Implementations aiming to **omit `Y`** on wire (**pure stream recover**) MUST still obey **§I P1** barrier conjunct with an **alternative engine‑authored cut** — **rename only**, not weaker proof.
|
||||
|
||||
### 6.10 **Receiver recover invariants** — **`bitmap` core** (**P5**) · **WAL naive** · **race‑free arbitration**
|
||||
|
||||
**§I P5** already requires **`bitmap`** visibility for **Wal‑claims** vs **base**. **Normative clarification**: the **`bitmap` is not an optional “parallelism tax”** detachable from recover — it is the **receiver’s single arbitration surface** for **“has a Wal touched this LBA in this session scope?”** regardless of whether base is **dense**, **sparse**, **striped workers**, or **wall‑clock overlapped** with Wal (**§6.8 item 6 / G3**). **Dropping `bitmap` in favor of naive base-only apply** is a **different product mode** (typically **serial BASE → Wal**) and **MUST** be labeled as such (**mini-plan §12 candidate “A‑serial”**).
|
||||
|
||||
| ID | Invariant (**receiver recover path**) |
|
||||
|----|----------------------------------------|
|
||||
| **`INV‑RECV‑BITMAP‑CORE`** | **`bitmap`** is the **sole** gate that lets **recover base** mutate an LBA after **Wal** may have asserted **Wal‑truth** on that LBA. **Base apply** **`MUST`** follow a **single critical pattern**: **observe / claim “not Wal‑protected” and write base bytes in one race‑free atomic step** — e.g. **`CAS`/compare‑and‑set** style **`0→1`** on **`bitmap[lba]`** (or **`TryClaimBase(lba)`** with equivalent semantics); **winner** performs **`ApplyBaseBlock`** and sets **`claimed`**; **loser** **skips** base write. **Wal apply** **`MUST NOT`** rely on a **read‑then‑later‑write** of **`bitmap`** that can interleave with base (**§6.10 anti‑pattern** below). |
|
||||
| **`INV‑RECV‑WAL‑NAIVE`** | **Recover Wal tuples** (**`frameWALEntry`**) **`MUST`** apply with **substrate LWW** (**write payload**) **without** consulting **`bitmap`** before write **for stale‑Wal micro‑comparison** — **Wal vs Wal ordering** is **`LSN`** monotonic on the **single ingest frontier** (**§6.9 receiver-hard**, **`checkMonotonic`**, precondition **`INV‑WIRE‑WAL‑LSN‑MONOTONIC`** **§6.3** pseudocode). After successful Wal substrate write, **`MUST`** **set **`bitmap`/Wal‑claim** for **`lba`** so **later base** loses **`CAS`**. Ordering inside the implementation **`MUST`** be **Wal data durable before observable claim** (or use one **`per‑LBA` / `shipMu`‑compatible** serialization that merges data+claim — product picks; **wrong interleavings** ⇒ **NEGATIVE‑EQUITY‑class bugs**). |
|
||||
|
||||
##### Reference pseudocode — **`ApplyWAL` / `ApplyBASE`** (**per‑LBA atomic envelope`)
|
||||
|
||||
**Naming**: **`store.lock(lba)`** = **one race‑free critical section** **`MUST`** cover **`data write` ∪ `bitmap` transition** together — equivalent **`bitmap.CAS`** patterns — **informative** notes below.
|
||||
|
||||
```text
|
||||
# —— (a) STATE ——
|
||||
state:
|
||||
bitmap : array[NumLBAs] of bit, init 0 # CORE — INV-RECV-BITMAP-CORE
|
||||
store : substrate # exposes per-LBA lock OR global writer (see equivalence note)
|
||||
|
||||
# —— WAL — precondition: ingest order ≡ strict LSN increase (INV-WIRE-WAL-LSN-MONOTONIC §6.3) ——
|
||||
def ApplyWAL(lba, lsn, data):
|
||||
with store.lock(lba): # atomic envelope (INV-RECV-BITMAP-CORE + WAL-NAIVE)
|
||||
store.write(lba, data) # naive LWW vs prior Wal bytes — no bitmap pre-check
|
||||
bitmap[lba] := 1 # claim set BEFORE releasing lock
|
||||
|
||||
# —— BASE — may race WAL on same lba under BASE ∥ WAL (§6.8 #6) ——
|
||||
def ApplyBASE(lba, data):
|
||||
with store.lock(lba): # SAME lock family as ApplyWAL
|
||||
if bitmap[lba] == 0:
|
||||
store.write(lba, data)
|
||||
bitmap[lba] := 1
|
||||
# else: Wal already authoritative for this session scope — stale base snapshot SKIP
|
||||
|
||||
# ANTI-PATTERN (banned — same prose as §6.10 DON’T below):
|
||||
# if bitmap[lba] == 0:
|
||||
# with store.lock(lba): store.write(lba, data)
|
||||
# bitmap[lba] := 1
|
||||
```
|
||||
|
||||
**Informative equivalence**: if substrate serializes **all** **`Apply*`** via **one** goroutine, lock may degrade to **global queue** + **`bitmap` atomic** — **`CAS`**‑only formulations **remain valid** (**§9** tests **may** simulate either).
|
||||
|
||||
**Informative (**substrate **`Write` arity**)**: **`ApplyBASE`** payloads **typically lack author Wal **`LSN`****; **synthetic frontier** for extent layer **MAY** use **session **`targetLSN` / lineage anchor** per **`RebuildSession` / §5** — **architect** pins if **`Write(lba, data, effectiveLSN)`** becomes required.
|
||||
|
||||
**Anti-pattern (normative DON’T)** — **`read bit; compute elsewhere; later base write`** without **`CAS`/lock** vs concurrent **`Wal`** — permits **Wal data then base overwrite** (**lost update**).
|
||||
|
||||
**Session scope**: recover **`bitmap`** state **`SHOULD`** be **scoped to `StartSession…EndSession`** (or **`RebuildSession`** lifetime) **unless** substrate definition extends Wal‑claims — **explicit** in leaf spec (**architect**) so **`streamBase`/parallel base** races cannot cross **stale boundaries**.
|
||||
|
||||
---
|
||||
|
||||
### 7. Replica routing table (**P5 operationalized**)
|
||||
|
||||
@@ -186,7 +340,7 @@ If **sustained append rate > sustainable ship rate** for the session, **`head−
|
||||
| Recover `frameWALEntry` | WAL tuple | Substrate apply **+** **`bitmap` WAL-claim** |
|
||||
| Recover `frameBaseBlock` | Bytes | **`bitmap` gate** → **`ApplyBaseBlock` / synthetic frontier** |
|
||||
|
||||
**`checkMonotonic`**: protocol defense on **recover WAL** stream (**gap / backward / dup / +1**).
|
||||
**`checkMonotonic`**: protocol defense on **recover WAL** stream (**gap / backward / dup / +1**). **Bitmap / base race atomicity** (**`INV‑RECV-*`**) — **`§6.10`**.
|
||||
|
||||
---
|
||||
|
||||
@@ -215,7 +369,7 @@ Bearer differs; **§7 semantic is P3**.
|
||||
| ID | Open question | Why it can bite at code time |
|
||||
|----|----------------|------------------------------|
|
||||
| **T1** | **“Caught up” / flip policy** (**refines §6.4**): strict `cursor == head` vs hysteresis **`head − cursor < ε`** vs **time-based idle**; **product** semantics when **flip races append** — serializer already required | Premature declaring **normal** ⇒ **gap** if **outside §6.4**; late flip ⇒ long session / pin |
|
||||
| **T2** | **`targetLSN` vs moving `head`**: if **`head > target`** at session start, does backlog drain stop at **target** for **barrier** only, or always emit to **head**? **Related (§6.2)**: **catch-up closes `cursor→head` gap** (operational debt), not “match **`head`’s value at an instant**”; **barrier / pin** still need an **engine-chosen cut** agreed with receiver. | **Barrier false negatives** or **double application** if sender/receiver disagree |
|
||||
| **T2** | **Close into §6.9 + explicit barrier predicate** — **`Y` never forks receiver WAL ingest** (**one LSN-monotonic stream**); **`targetLSN = Y`** is **sender enumerator / lineage freeze** only; **tail** **`LSN > Y`** ships via **WalShipper** same session (**Phase C**); **Barrier `AchievedLSN`** predicate agreed with replica (**exact tail clause** vs **moving `head`**) (**§IV T2 residual**). | Premature success, duplicate/stale apply, or **ordering chaos** if **≤Y vs >Y** modeled as **split tapes** |
|
||||
| **T3** | **Bearer choice while `cursor < head`**: **steady bearer silent vs dual-lane only** (**§II–§III** closes); **either way** obey **§6 P2 single serializer** | **P2** if two pumps both emit unconsumed prefix |
|
||||
| **T4** | **Duplicate** `lsn == applied` on recover path: **hard error** vs **idempotent no-op** | Retransmit policy vs **checkMonotonic** |
|
||||
| **T5** | **Sparse base** vs dense full-LBA — contract with **bitmap** density | Performance / correctness on huge volumes |
|
||||
@@ -268,7 +422,7 @@ Controlled relaxations of **§6** prose **without** weakening **§I**. Each row
|
||||
| **Motivation (**T4a / fresh receiver**)**: Substrate‑scan WAL ship during **steady Realtime** **`NotifyAppend`** can replay **dead‑window** bytes and violate **no‑replay** session invariants asserted by tests/product. |
|
||||
| **`ModeBacklog`** (recover / catch‑up Wal path on WalShipper) | **`§6.3**(A)** `send(incoming, debt)`, **`§6.3**(B)** `send(∅, debt)` / periodic **`ShipOpportunity`**, and **§6.8**(3)(4)(9) **`MUST`** hold **in full**. Timer **`MUST`** attempt **`emit-from-cursor`** when **`cursor < head`** even if Primary append‑idle (**§6.8 item 4**). **Priority (= oldest unsent)** **`MUST`** use substrate **`ScanLBAs`** (or equivalent single‑tape authoritative read). |
|
||||
| **`ModeRealtime`** (steady per‑append **`NotifyAppend`**) | **Literal §6.3(B)** “idle timer **`MUST`”** **`MUST NOT`** apply — ship is **`NotifyAppend`**‑driven. **Hot path **`MUST NOT`** substrate‑replay** for ship byte selection (**caller `data`** is canonical on optimized tail emit). **`send(incoming, debt)` debt‑priority **`MUST NOT`** be re‑interpreted as “Realtime must drain before tail”**: gap **`cursor < head`** **`MUST`** be corrected only via **`ModeBacklog`** + **`DrainBacklog`** / coordinator **re‑anchor**, not Realtime substrate scan. **`CHK‑WALSHIPPER‑TIMER‑DRAIN`** applies to **Backlog** only (see **§12** predicate). |
|
||||
| **Safety switch** | Implementations **SHOULD** expose **`StrictRealtimeOrdering`**: **log‑warn** on **`lsn ≠ cursor + 1`** (dense WAL) **by default**; **strict / error path** optional **production** opt‑in. **Hard opt‑in** (`strict=true`): engine **SHOULD** require prior proof of **ordering discipline** (**rebuild‑on‑gap**, fresh peer policy). Operational detail **`v3-recovery-wal-shipper-mini-plan.md` §11.6**. |
|
||||
| **Safety switch** | Implementations **SHOULD** expose **`StrictRealtimeOrdering`**: **log‑warn** on dense WAL when **`NotifyAppend`** **`lsn`** **≠** **`expected_next_tail`** **by default** — **canonical** (**§6.3 **`Drive`**, **`cursor` = next emit**): **`lsn == cursor`** on the debt‑free path; **`lastEmitted`‑style** internal fields **`MUST`** compare **`lsn == lastEmitted + 1`** **equivalently** (**single contract** across shipper code, **`Drive`** prose, and tests). **Strict / error path** optional **production** opt‑in. **Hard opt‑in** (`strict=true`): engine **SHOULD** require prior proof of **ordering discipline** (**rebuild‑on‑gap**, fresh peer policy). Operational detail **`v3-recovery-wal-shipper-mini-plan.md` §11.6**. |
|
||||
| **Not relaxed** | **P2** single serializer (**§6.8(1)**); **§6.4** (**R1**); **§6.8(5)** framing≠second tape; **§6.6** (**R2**) observability hooks; **§I P1–P7**. |
|
||||
|
||||
**Doc bridge**: **`v3-recovery-wal-shipper-mini-plan.md`** **§11.2 dual‑mode contract** ⇄ this exception.
|
||||
@@ -289,18 +443,23 @@ Controlled relaxations of **§6** prose **without** weakening **§I**. Each row
|
||||
| **2026-04-30** | **v3.7**: **`§6.8` implementer checklist** (single serializer, priority, timer drain, framing≠tape, **`G3` pointer**); **§V** **`CHK-WALSHIPPER-TIMER-DRAIN`** |
|
||||
| **2026-04-30** | **v3.8**: **§6.2–6.3** — **policy vs operational debt**, **moving-target / gap→0**, **`send(incoming, debt)` / `send(∅, debt)`** strategy abstraction + **steady debt-free sends**; **§6.8** item **(9)**; **`T2`** cross-ref |
|
||||
| **2026-04-30** | **v3.9**: **§13** (**E‑WALSHIPPER‑DUAL‑MODE**); **`§14`/`§15` renumber**; **§6.3** carve‑out pointer; **`CHK‑WALSHIPPER‑TIMER‑DRAIN`** scoped per **§13** |
|
||||
| **2026-04-30** | **v3.10**: **§6.9** — **`targetLSN=Y`** as **historical WAL job bound** (`(fromLSN,Y]`) vs **WalShipper `cursor→head` stream**; phased **recover process**; **§I P7** / **P1** / **§IV T2** aligned (**`Y` is not tape end**) |
|
||||
| **2026-04-30** | **v3.11**: **§6.9** — **receiver-hard invariant**: **`Y` MUST NOT denote two WAL tapes** / **dual apply frontiers**; **one LSN order** (**frame kind ≠ second truth**) |
|
||||
| **2026-04-30** | **v3.12**: **§6.9** — **`NEGATIVE‑EQUITY`** if **`target`** read as WAL **segmentation**; **`HOPE‑SHIPPER‑MONOTONIC`**: backlog = **`send(∅, debt)`** + **`send(incoming, debt)`** (**§6.3**) |
|
||||
| **2026-04-30** | **v3.13**: **§6.10** — **`INV‑RECV‑BITMAP‑CORE`** (**`CAS`‑style base**); **`INV‑RECV‑WAL‑NAIVE`**; **`bitmap`** = **core P5 arbitration** (not optional “parallel bit” alone); session scope |
|
||||
| **2026-04-27** | **v3.14**: **§6.3** — normative **`Drive(input)`** pseudocode (**state / atomic boundary / `INV‑WIRE‑WAL‑LSN‑MONOTONIC`**); **§6.10** — **`ApplyWAL`/`ApplyBASE`** pseudocode (**`INV‑RECV‑*`**); **§6.1/§V** cursor↔rewind alignment note; **§13** **`StrictRealtimeOrdering`** keyed to **`Drive`** **`cursor`** convention |
|
||||
|
||||
### 15. Document map
|
||||
|
||||
| Doc | Role |
|
||||
|-----|------|
|
||||
| **This** | **Foundation + index**; **`§6.8`** implementer checklist; **`§13`** architect-approved exceptions (**E‑WALSHIPPER‑DUAL‑MODE**) |
|
||||
| **This** | **Foundation + index**; **`§6.8`** checklist; **`§13`**; **`§6.3`/`§6.9–§6.10`** — **`Drive`/`Apply*`** pseudocode, **`INV‑WIRE‑WAL‑LSN‑MONOTONIC`**, **`NEGATIVE‑EQUITY`**, **`HOPE‑SHIPPER‑MONOTONIC`**, **`INV‑RECV‑BITMAP‑CORE`** / **`INV‑RECV‑WAL‑NAIVE`** |
|
||||
| `v3-recovery-pin-floor-wire.md` | Pin bytes |
|
||||
| `v3-recovery-wal-shipper-mini-plan.md` | **Implementation bridge** (**seaweed_block** phased PR ↔ spec §INV) |
|
||||
| `v3-recovery-wal-shipper-spec.md` | **WalShipper algorithm** (priority, **R1**, **INV-***) |
|
||||
| `v3-recovery-unified-wal-stream-*.md` | **Align to WalShipper spec** or mark superseded |
|
||||
| `v3-recovery-wiring-plan.md` | Ports / flags |
|
||||
| `v3-recovery-inv-test-map.md` | INV ↔ tests |
|
||||
| `v3-recovery-execution-institution.md` | Lifecycle + **risk envelope** / spec→delete-code ordering |
|
||||
| `v3-recovery-execution-institution.md` | Lifecycle + **risk envelope** / spec→delete-code ordering + **entity layering & assembly contract** (SW: where **attempt** / muscles may attach) + **§ Management plane vs data-plane recover** (**single index** for probe / quorum / RF>2 admission — **no parallel recovery hub**) |
|
||||
| `v3-recovery-live-line-backlog-spec.md` | Retired stub → **here** |
|
||||
| `v3-storage-logical-pin-gate.md` | **LogicalStorage substrates + `RecycleFloorGate` / pin** |
|
||||
|
||||
@@ -3,7 +3,7 @@
|
||||
**Status**: Draft — executable sequence from **`v3-recovery-wal-shipper-spec.md`** to **`seaweed_block`** concrete diffs.
|
||||
**Supersedes narrative scope of**: **`v3-recovery-unified-wal-stream-mini-plan.md` §3.2 (#3 unified stream implementation)** — that track treated recovery `sender` as the Wal scheduler; **non-compliant** with consensus **§6** + wal-shipper-spec **INV-NO-DOUBLE-LIVE**. Architect may add formal **SUPERSEDED** banners on kickoff/unified docs; **this file does not block on that.**
|
||||
|
||||
**Normative**: **`v3-recovery-wal-shipper-spec.md`** (**§2–§§7**) + **`v3-recovery-algorithm-consensus.md`** **§I / §II §6**.
|
||||
**Normative**: **`v3-recovery-wal-shipper-spec.md`** (**§2–§§7**) + **`v3-recovery-algorithm-consensus.md`** **§I / §II §6** (**§6.3 `Drive`**, **§6.10 `Apply*`** pseudocode).
|
||||
|
||||
**Anti‑archive branch**: **`g7-redo/unified-wal-impl`** — **do not PR** as WalShipper truth; cherry-pick only **tests/fixtures** if still valid after refactor audit.
|
||||
|
||||
@@ -138,6 +138,9 @@ Wal-shipper-spec **§9** names coarse tests — here map **package + style**:
|
||||
| 2026-04-30 | v0.6 — **Dual-mode **`ModeBacklog`/ModeRealtime`** + consensus **`§13` E‑WALSHIPPER‑DUAL‑MODE** (**T4a carve-out**) — rewrote **§11.2**, **§11.3** `#3/#4/#9`, §11.4 anchors, §11.5 (**StrictRealtimeOrdering**, TOCTOU); **§11.6 migrations** (**replicaID**, rebuild-on-gap); CHK/timer scope = **Backlog** |
|
||||
| 2026-04-30 | v0.7 — **§11.6** + **`v3-recovery-execution-institution.md`** **Entity layering & assembly contract** (**architect → SW**); Phase 0 **replicaID** vs Phase 1 **attempt binder** guardrails |
|
||||
| 2026-04-30 | v0.8 — **§11.7** heavy integration proof (**manager-assembled session**): pillars **WalShipper / dual-line / receiver convergence**; ordering **Phase 0 → (2) fault-inject → matrix → soak** |
|
||||
| 2026-04-30 | v0.9 — **§11.7 pillar 3**: **slice-2** **`190ee56`** (`TestPillar3Slice2_EngineDriven_SameLBAArbitration`); **T2 / hardware soak** called out **open** pending §IV |
|
||||
| 2026-04-30 | v0.10 — **§12** **design candidate** — §6.9‑driven **Drive** simplification + **three receiver models** + **`bitmap`/`CAS`** (**consensus §6.10** cross-ref); **not** normative until architect promotes |
|
||||
| 2026-04-27 | v0.11 — **§12.3**: **normative `Drive` = consensus §6.3 only** (remove duplicate sketch); **§12.1–12.2** cross-ref **§6.3** |
|
||||
|
||||
---
|
||||
|
||||
@@ -297,9 +300,48 @@ Choice — **per-connection format dispatch**, not single-format unification. Du
|
||||
|--------|------------|---------------------|
|
||||
| **1 — WalShipper: backlog vs incoming** | **`ModeBacklog`**: timer + **`DrainBacklog`** / **`ScanLBAs`**, **`NotifyAppend`** lag-only; **`ModeRealtime`**: **`NotifyAppend`** tail + **`StrictRealtimeOrdering`**; **§13** carve-out | `core/transport`: **`TestC2_*`**, **`TestWalShipper_*`**, **`replicaid_unified_test`**; add **assembled-path** sessions (real **`RecoverySink`**, not shipper-only) |
|
||||
| **2 — Dual-line execution** | **BASE ∥ WAL** overlap, **`writeMu`**-bounded interleave; correct **profile / port**; **no corrupted frames** | **`TestC3_BaseWalParallel_FramesInterleave`**, dual-lane E2E; **item (2)**: **C3 ctx fault-injection** (**`7d051e2`** — `TestC3FaultInjection_BaseError_WalExitsViaCtx` / `_OuterCancel_BothLanesWindDown` / `_WalError_RunTerminates_NarrowVariantA`); assembled-stack lift (**`9f62ebe`** — `TestPillar2A_BaseError_AssembledStack_FailReason` / `TestPillar2B_LiveWrites_HighPressure_BarrierIntegrity` / `TestPillar2C_WireAbortMidSession_AssembledStack_RestoresEmitContext`) |
|
||||
| **3 — Receiver recover convergence** | Replica accepts **interleaved base + WAL** on recover path, **bitmap / `checkMonotonic`**, **barrier `achievedLSN`**, moves toward **idle / healthy** | **`core/recovery` E2E**, **`dual_lane_engine_test`**, **`replication/component` cluster**; stress: **live writes during session**; **T2** when §IV closed. **Slice-1 landed 2026-04-30** (**`291e652`** + polish **`3495a12`**) — `TestPillar3Slice1_ReceiverConvergence_LiveOverwritesBacklog_SameLBAs` (transport-stack only; **slice-2** lifts to engine-driven path via `dual_lane_engine_test.go`) |
|
||||
| **3 — Receiver recover convergence** | Replica accepts **interleaved base + WAL** on recover path, **bitmap / `checkMonotonic`**, **barrier `achievedLSN`**, moves toward **idle / healthy** | **`core/recovery` E2E**, **`dual_lane_engine_test`**, **`replication/component` cluster**; stress: **live writes during session**; **T2** when §IV closed (hardware soak — **still open** pending §IV). **Slice-1** (**`291e652`** + polish **`3495a12`**) — `TestPillar3Slice1_ReceiverConvergence_LiveOverwritesBacklog_SameLBAs` (transport stack). **Slice-2** (**`190ee56`**) — `TestPillar3Slice2_EngineDriven_SameLBAArbitration` (full adapter→engine→executor dispatch; **`RouteSessionLane`** on each live push). Slice-3+ / wire-tap / C3‑#2B **optional backlog** |
|
||||
|
||||
**Order**: **(1)** Phase 0 **committed + §11.6 receipt (SHA)** → **(2)** fault-injection → **(3)** widen matrix → **hardware soak** (**T2 / T7**).
|
||||
|
||||
**Stop rule**: Failure at **assembled-session** layer → fix **algorithm / wiring** before **Phase 1** (binder fixes **identity**, not WAL/base correctness).
|
||||
|
||||
---
|
||||
|
||||
## 12. Design candidate — **`§6.9`‑driven shipper/receiver simplification** (**not normative until promoted**)
|
||||
|
||||
**Status**: **Design candidate** — for **architect decision**; **does not** replace **§11.2–§11.7** receipts or **§13** until consensus + this section are **explicitly revised** and code lands on a **named branch**.
|
||||
|
||||
### 12.1 **Document stack** — what SW should read in what order
|
||||
|
||||
| Layer | Doc | Role |
|
||||
|-------|-----|------|
|
||||
| **Consensus** | **`v3-recovery-algorithm-consensus.md`** **§I P5**, **§6.2–6.4**, **§6.3 `Drive`**, **§6.9**, **§6.10** (`Apply*` pseudocode), **§13**, **§IV T2** | **Normative** truth: single tape intent, **`targetLSN`** non‑segmentation, **`send(∅,·)`/`send(incoming,·)`**, **`bitmap`** CORE + **`INV‑RECV-*`** race rules. |
|
||||
| **Algorithm leaf** | **`v3-recovery-wal-shipper-spec.md`** **§7** | **Implementable sketches** (**§7.1 loop**, **receiver rewind + monotone §7.4**); **primary recover emit** = **§6.3 `Drive`** (**normative consensus**); **`Apply`/`bitmap` detail** ⇒ **§6.10**. |
|
||||
| **Bridge / receipts** | **This mini-plan §11** | What **already merged** on **`g7-redo/wal-shipper-impl`** + **pilots**. |
|
||||
| **This §12** | **Candidate refactor** | **Single normative `Drive(input)`** (**consensus §6.3** — **avoid duplicating here**); barrier‑only **`target`**, receiver **Wal naive**, **bitmap `CAS`** base — **diff** from today's **dual‑mode + bridging sink**. |
|
||||
|
||||
### 12.2 **Receiver — three models** (clears SW confusion)
|
||||
|
||||
| Model | WAL apply | BASE vs WAL | Typical cost |
|
||||
|-------|-----------|-------------|--------------|
|
||||
| **① Today bridging sink + ordered seal** | **Naive substrate write** | **Mostly ordered by sender buffer/seal luck** — **§6.8 #6 parallelism still risky under races** | No **per‑LBA Wal** table; **ordering not a hard invariant** without proof. |
|
||||
| **②** (**`NEGATIVE‑EQUITY`**) | Needs **per‑LBA Wal frontier** (**e.g. 64‑bit last‑LSN**) for stale compare | **Dual WAL truth** at receiver — violates **§6.9** mono‑ingest story | **Expensive** |
|
||||
| **§6.9 / §12 candidate (`HOPE‑SHIPPER‑MONOTONIC`)** | **`INV‑RECV‑WAL‑NAIVE`**: naive write; **Wal–Wal order = wire LSN order** (**sender `cursor` monotone + single apply frontier**) | **`INV‑RECV‑BITMAP‑CORE`**: **`bitmap` not optional ornament** — **sparse / dense / parallel base** all **CAS (or equiv.)‑gate** base; **Wal sets claim after write** (**§6.10**) | **Small `bitmap` + `CAS`**; **drops** brittle **dual‑mailbox Wal** story. |
|
||||
|
||||
**Key correction for SW**: **`bitmap`** is **`P5` core arbitration for BASE vs WAL**, not “only pay 1‑bit because we chose parallel BASE.” **`§6.10`** pins **`CAS`/atomicity** so **Wal data vs lazy base check** cannot **race‑overwrite**.
|
||||
|
||||
### 12.3 **Candidate sender** — normative reference only
|
||||
|
||||
**Normative pseudocode** **`Drive(input)`**: **`v3-recovery-algorithm-consensus.md` §6.3** — **do not** fork a second **`Drive`** sketch in this mini‑plan (prevents **§6 ↔ §12** drift). **§12.4 #1** (**`ReadAtLSN`** vs prefetch **N**) and **`targetLSN=Y`** barrier semantics remain **architect / implementation** leaves.
|
||||
|
||||
### 12.4 **Architect checklist** (open before implementation)
|
||||
|
||||
| # | Topic | Decision |
|
||||
|---|-------|----------|
|
||||
| **1** | **Substrate** | **`ReadEntryByLSN`** vs **prefetch‑N inner queue** (same observable **next‑emit **`cursor`** advancement** vs **§6.3 **`Drive`**) — **WalStore/smartwal index** cost |
|
||||
| **2** | **`target`/lineage** | **Barrier admission only** + **§IV T2** sweep for **legacy hidden dependencies** |
|
||||
| **3** | **`bitmap` lifetime** | **Session‑scoped**, cleared / reset on **`EndSession`** (**exact hook** ties **receiver FSM**) |
|
||||
| **4** | **`streamBase`** | **`groupCtx`** / **fail‑fast with `Drive`** (**C3 #2B** follow‑up) |
|
||||
| **5** | **BASE vs WAL wall‑clock** | **Candidate B** (overlap + **`§6.10`**) vs **A** (serial BASE→Wal **may relax `bitmap` policy** explicitly) |
|
||||
|
||||
|
||||
@@ -15,6 +15,7 @@
|
||||
| In scope | Out of scope (link elsewhere) |
|
||||
|----------|--------------------------------|
|
||||
| **One ordered Wal tape** on Primary: `head`, per-peer **`cursor[P]`**, **emit** order to **P** | **Extent/base bulk** — `v3-recovery-algorithm-consensus.md` §5; bytes `v3-recovery-pin-floor-wire.md` |
|
||||
| **§7.3 — sender recover emit** (**normative = consensus **`Drive`**) · **§7.4** — illustrative **recover receive** rewind + monotone + **`bitmap`** pseudocode (**consensus §II §7 routing**) | **§7.4** **`ApplyWalWithWalClaimBitmap` / **`ApplyBaseUnderBitmapGate` **→** **`v3-recovery-algorithm-consensus.md` §6.10** pseudocode (**`INV‑RECV‑*`**). Receiver detail — **`seaweed_block`** `core/recovery` + tests; **`checkMonotonic`** |
|
||||
| **Single serializer** for “next LSN sent to P” (**P2**) | Receiver **`checkMonotonic`**, **`bitmap`** — consensus §7; replica apply |
|
||||
| **R1** transition (caught-up vs append race) | **Engine** retry / escalate after fail-close — executor / engine |
|
||||
| **R2** saturation observability hooks | **`MinPin`/recycle** full story — coordinator + substrate |
|
||||
@@ -119,7 +120,9 @@ Timer **priority drain** (**§4**) remains required for **liveness** but **does
|
||||
|
||||
---
|
||||
|
||||
## 7. Pseudocode (**reference shape**)
|
||||
## 7. Pseudocode (**reference shapes**)
|
||||
|
||||
### 7.1 Primary **`WalShipper`** core loop (**steady + recover**)
|
||||
|
||||
```text
|
||||
// One goroutine OR all entrypoints take shipMu.
|
||||
@@ -148,7 +151,89 @@ function EmitAccordingTo§4UntilBudgetOrBlocked():
|
||||
emit(head); clear pending_tail_flag // depends on refactor; simplest: append path calls Emit once after advancing head while cursor tracked
|
||||
```
|
||||
|
||||
Implementations **flatten** this; the **semantic** contract is **§3–§5**, not the sketch’s loop details.
|
||||
Implementations **flatten** this sketch; **§3–§5** remain the semantic contract.
|
||||
|
||||
### 7.2 **Recover-visible high layer** (**session** + **`backlog` pointer**)
|
||||
|
||||
Pairs with **`v3-recovery-algorithm-consensus.md` §6.9** (**`NEGATIVE‑EQUITY`**, **`HOPE‑SHIPPER‑MONOTONIC`**). Recover adds **no** parallel “Wal ownership” beside:
|
||||
|
||||
| Artifact | Meaning |
|
||||
|----------|---------|
|
||||
| **Recover session envelope** | **`sessionID`, epoch/ev, lineage`** (may carry optional **`targetLSN=Y`** as **frozen lineage text** — **not** a backlog pointer — **never** WAL segmentation rhetoric). |
|
||||
| **Backlog pointer** | **`cursor`** on the **same** Primary tape — **`cursor < head` ⇔ debt** (**§6.3** **`send(incoming, debt)`** / **`send(∅, debt)`**). |
|
||||
|
||||
```text
|
||||
type RecoverSessionView = record
|
||||
session_id : uint64
|
||||
lineage : opaque // echoed on bearer + barrier; includes engine-authored fromLSN/target text
|
||||
end
|
||||
|
||||
// cursor + head owned ONLY by WalShipper (§2). Executor/coordinator publishes RecoverSessionView + brackets.
|
||||
WalShipper.OnRecoverSessionBracket(StartSession(fromLSN), …, EndSession)
|
||||
```
|
||||
|
||||
### 7.3 **Primary recover — monotone emit**
|
||||
|
||||
**Normative**: **`v3-recovery-algorithm-consensus.md` §6.3 — reference pseudocode `Drive(input)`** — single **`fifo`**, **`cursor < head ⇒ ReadAtLSN(cursor)` before tail**, **`lsn > cursor` ⇒ `CursorGap`** (**no realtime scan‑fill**). **`(a)`** state, **`(b)`** **`shipMu`** atomic boundary, **`(c)`** **`INV‑WIRE‑WAL‑LSN‑MONOTONIC`**.
|
||||
|
||||
Optional **`ScanLBAs(...,≤Y]`** emits **Backlog‑class** frames yet **still** advances **`cursor`** only **under **`shipMu`** — **INV-SINGLE** / **INV-MONOTONIC-CURSOR** unchanged.
|
||||
|
||||
**Informative**: one lock hold often **loops** **`Drive(∅ | fifo.peek())`** until transport budget clears or **blocked** — **observable semantics remain** **`Drive`** **per step** per **§6.3**.
|
||||
|
||||
### 7.4 Replica recover session (**monotone receive**, **one rewind**, **`bitmap` overlap**)
|
||||
|
||||
**“One rewind”**: not an arbitrary backward LSN cascade — the session **resets** ingest expectation to **`fromLSN + 1`** (dense default; **`CHK-RECOVER-REWIND-ONCE`** in **consensus §V §12**), validates the **first lawful** recover-WAL frame, then **`monotonic_armed`** — only **strict monotone** (`checkMonotonic`) thereafter.
|
||||
|
||||
**Normative ingest**: exactly **one** recover-WAL monotonic frontier after contractual **rewind**; **Wal-vs-base overlap** gated by **`bitmap`** (**§I P5** — operationalized **`v3-recovery-algorithm-consensus.md` §7 routing table**, **`checkMonotonic`**); substrate **Wal-vs-Wal LWW** after ingest order holds.
|
||||
|
||||
```text
|
||||
type RecoverRcvrSession = record
|
||||
open : bool
|
||||
fromLSN_exclusive : uint64
|
||||
expect_next_LSN : uint64 // rewound expectation baseline
|
||||
monotonic_armed : bool // after first lawful recover-WAL ingest
|
||||
end
|
||||
|
||||
procedure OpenRecoverRcvr(s: RecoverRcvrSession*, fromLSN, lineage_blob):
|
||||
require not s.open
|
||||
s.open := true
|
||||
s.fromLSN_exclusive := fromLSN
|
||||
|
||||
// INFORMATIVE (CHK-RECOVER-REWIND-ONCE): first post-open WAL expects fromLSN+1 on dense products
|
||||
s.expect_next_LSN := fromLSN + 1
|
||||
s.monotonic_armed := false
|
||||
BITMAP_scope_for_session(lineage_blob)
|
||||
|
||||
procedure OnRecoverWalTuple(s: RecoverRcvrSession*, frame_kind /* Backlog | SessionLive | … */, lsn, lba, data):
|
||||
require s.open
|
||||
|
||||
if not s.monotonic_armed:
|
||||
REWIND_VALIDATE(lsn, s.expect_next_LSN, s.fromLSN_exclusive)
|
||||
// after success, ingest at lsn establishes monotonic stream
|
||||
s.monotonic_armed := true
|
||||
else:
|
||||
FAIL_IF_NOT checkMonotonic(lsn, s.expect_next_LSN) // gaps / backwards / unlawful dup vs policy
|
||||
|
||||
ApplyWalWithWalClaimBitmap(s, lsn, lba, data)
|
||||
|
||||
s.expect_next_LSN := AdvanceDenseOrProductRule(lsn)
|
||||
|
||||
|
||||
procedure OnRecoverBaseBlock(s: RecoverRcvrSession*, lba, bytes):
|
||||
require s.open
|
||||
ApplyBaseUnderBitmapGate(s, lba, bytes) // overlaps with Wal claims (**P5**); does NOT bypass Wal LSN frontier
|
||||
|
||||
|
||||
procedure CloseRecoverRcvr(s: RecoverRcvrSession*):
|
||||
s.open := false
|
||||
```
|
||||
|
||||
```text
|
||||
// Receiver-hard invariant (consensus §6.9): all recover WAL frames obey ONE global LSN order to this session —
|
||||
// bearer “kind” reshapes encoding only — never splits into independent tapes.
|
||||
```
|
||||
|
||||
**`bitmap` arbitration + races** — **`INV‑RECV‑BITMAP‑CORE`** / **`INV‑RECV‑WAL‑NAIVE`**: normative **`ApplyWAL` / `ApplyBASE`** pseudocode (**(a)–(c)**) — **`v3-recovery-algorithm-consensus.md` §6.10**. This §7.4 sketch (**`OpenRecoverRcvr` / `OnRecoverWalTuple`**) is **routing glue**; **`ApplyWalWithWalClaimBitmap`** / **`ApplyBaseUnderBitmapGate`** **MUST** implement **§6.10** lock/`CAS` discipline (**not** anti‑pattern check‑outside‑lock).
|
||||
|
||||
---
|
||||
|
||||
@@ -183,6 +268,9 @@ Implementations **flatten** this; the **semantic** contract is **§3–§5**, no
|
||||
| **2026-04-30** | Pointer to consensus **§6.8** implementer checklist; **§V** **`CHK-WALSHIPPER-TIMER-DRAIN`** cross-ref in **§9**. |
|
||||
| **2026-04-30** | **§2** vocabulary **`incoming` / `debt` / `send(·,·)`**; **§4.1–4.2** strategy split; tests cross-ref **§6.3**; checklist **nine** items (**§6.8(9)**). |
|
||||
| **2026-04-30** | **§1** intro + **consensus §6.3(B)** cross-ref — **`ModeBacklog` vs `ModeRealtime`** (**§13** E‑WALSHIPPER‑DUAL‑MODE); mini-plan **§11.2a** bridge |
|
||||
| **2026-04-30** | **§7** split: **7.1–7.4** — recover **session/backlog pointer**, **monotone send (`send(∅,·)` / `send(incoming,·)`)**, receiver **rewind + monotone + `bitmap`** pseudocode |
|
||||
| **2026-04-30** | **§7.4** foot — **`bitmap`/`CAS`** cross-ref **consensus §6.10** (`INV‑RECV-*`) |
|
||||
| **2026-04-27** | **§7.3** — primary sender recover emit: normative **`Drive(input)` → `v3-recovery-algorithm-consensus.md` §6.3** (removed duplicate **`ShipOpportunity_RecoverMerged`** skeleton); **§7.4** note → consensus **§6.10** **`ApplyWAL`/`ApplyBASE`** pseudocode |
|
||||
|
||||
---
|
||||
|
||||
@@ -190,8 +278,8 @@ Implementations **flatten** this; the **semantic** contract is **§3–§5**, no
|
||||
|
||||
| Doc | Role |
|
||||
|-----|------|
|
||||
| **`v3-recovery-algorithm-consensus.md` §6 + §6.8** | **Axioms + stability + implementer MUST checklist** |
|
||||
| **This** | **Algorithm steps + invariants for one implementation** |
|
||||
| **`v3-recovery-algorithm-consensus.md` §6, §6.3 **`Drive`**, §6.8–§6.9, §II §7** | **Axioms** + **`Drive`/`Apply*`** pseudocode (**`INV‑WIRE‑*`**, **`INV‑RECV‑*`**) + **implementer checklist** + **`targetLSN`** process + **replica routing / `checkMonotonic`** |
|
||||
| **This** | **Algorithm + §7 pseudocode** (**Primary shipper** + **recover receive sketch**) |
|
||||
| **`v3-recovery-wal-shipper-mini-plan.md`** | **Phased PR / file anchoring (**`seaweed_block`**) **↔** §INV tests** |
|
||||
| `v3-recovery-wiring-plan.md` | Bearer / port |
|
||||
| `v3-recovery-unified-wal-stream-*.md` | Historical kickoff — **align or supersede** with this spec |
|
||||
|
||||
Reference in New Issue
Block a user