feat(history): 実行中の耐久性障害をユーザーに届ける (#288, #295 部分) - #317
Open
send wants to merge 13 commits into
Open
Conversation
A deletion whose WAL durability fails and whose fallback checkpoint also fails exists only in memory. Unlike its neighbours it has no startup heal: the old checkpoint still holds the entry and simply wins on the next start. `apply_records` returns `()`, so the only trace was a `warn!` that the shipped lib compiles out. Add the runtime counterpart of `LexHistoryOpenReport`: - a raise/cover generation ledger for unpersisted deletions. Generations rather than a flag because raise and cover race — a compaction reads the generation before snapshotting, so a deletion raised after that snapshot is not cleared by a checkpoint that may not contain it. Covered at the two points where the durable set stops holding the entry: a successful checkpoint save, and clear's empty checkpoint. - `HistoryWal`'s freeze flag becomes a shared atomic the owner lends in, so "learning is memory-only" is readable without the wal mutex the key thread holds across every append. Seeded on adopt, since a freeze inherited from recovery has no transition left to publish. Both surface through `durability_issues()` as a list: on a failing volume both hold at once, and collapsing them would hide one behind the other. No commit-side ledger: `append_record` only returns `Io` from its frozen guard or from an append that freezes, so "a commit is memory-only" is exactly "the WAL is frozen". Tests cover the F1-F15 edge matrix; the three WalIo mocks collapse into one with independently switchable faults, since correlated failures are the case under test.
The engine now reports unpersisted deletions and memory-only learning as they happen; give them a sink. Extract the menu's status rows into `DegradedStatus`, a pure derivation over the two sources. Keeping them separate is the point: init failures latch, runtime issues are polled and clear when the disk recovers, so folding the latter into `initFailures` would make a healed history warn forever. The runtime rows sit outside the old `isDegraded` gate. The main #295 scenario is a clean launch followed by a disk that fails hours later — nested under that check it would have displayed nothing in exactly the case it exists for. Polled, not pushed: the learning path has no seam to notify Swift from (background threads, no session; `LexSessionEvents` is the async candidate channel and mixing durability into it conflates concerns), and `menu()` re-derives its rows on every open regardless.
… one /simplify: three angles independently flagged the adopt-and-seed shape. The WAL already owns the Arc, so a getter makes the handle unconditionally current — no seeding step to forget, and no way for a second adopter to leave the first reading a detached flag. Drops the seeding invariant, its test, and the &mut at both construction sites. The design memo preferred lend-in over handle-out on the grounds that a handle binds to one WAL instance. That reason does not differentiate: if the WAL behind the mutex were ever replaced, a lent flag goes just as stale as a handed-out one. Recorded, with the ledger-relocation proposal the same review raised and why it is blocked. Also drops the now-callerless isDegraded and a test pass-through, and replaces a fixed 500ms sleep with a handshake.
Correctness: - has_unpersisted_deletion read `gen` before `covered`, the one order that can report clean while a deletion is unpersisted: read gen=5, let a cover and a fresh raise land, read covered=5, and 5 > 5 is false. For a menu the user opens once, that miss is the whole notification. - The SyncFailed arm raised the deletion ledger unconditionally, guarded only by a debug_assert that is gone in the shipped build. Gate it on the record kind like the Io arm: were a Committed barrier failure ever routed there, the user would be told a *deletion* did not persist. - Both encode guards in append_record returned Io without freezing, so the "Err(Io) implies frozen" invariant the no-commit-ledger decision rests on was not enforced. Freeze there too. - frozen_flag handed out the Arc, so any holder could store() from outside the wal mutex and let append_record's guard pass on a file whose tail is unreadable. Return a read-only FreezeFlag. - The deletion row named restart as the risk, which is backwards for the SyncFailed half — there the frame is on disk and replay is what applies the deletion. Reword; same for the variant doc and SPEC. Structure over tests: the cover's read-before-clone ordering lived in two statements with a comment holding them in order, and F6 could not have caught a reordering. snapshot_to_cover now takes both under one `inner` read guard, which apply_batch needs for writing — so the pair is atomic with respect to the apply rather than to statement order. Tests: the concurrency smoke's ledger assertion was 0 > 0 (no faults, no raises); add a test that actually raises concurrently and converges once the disk heals, including the transient-fault path a level-triggered switch could not reach. The lock-free test asserted wall-clock elapsed, which flakes under parallel test execution; assert completion while the mutex is held instead. Also: English strings for the four missing degraded rows, and EngineInitFailure split out so the Swift test build stops compiling the whole engine-loading path (~0.4s per run). Out of scope, filed: #311 (failed scrub after a healthy tombstone is silent), #312 (the ledger is process-local, so it is gone on the restart where the deletion resurrects — the residual #295 gap), #313 (clear() can be raced into re-creating the commit log, pre-existing).
The previous commit fixed the read order in has_unpersisted_deletion, then mutation testing showed the test written to guard it does not: it exercises the arithmetic, not the function's internal load order, and restoring the bug leaves it green. That is the same defect the review found in F6, one commit later. The window is two adjacent atomic loads, so no test can interpose on it deterministically. Make the skew unrepresentable instead: raised in the high 32 bits, covered in the low 32, one load for the outstanding test. 32 bits per counter needs 4 billion failed deletions in a session to wrap, and the values never leave the process. What remains testable moves to the write side, and is: a cover must preserve a raise that lands while it is in flight (CAS retry rather than a store), and must not walk backwards. Both mutations are caught.
The parenthetical still described the pre-refactor mechanism (apply releases inner, compactor acquires after the load). The guard now spans both, which is a different and simpler argument.
Axis 5 caught the worst of it: the AGENTS entry justified all three out-of-scope items with "the deletion is durable and startup heals", which is false for the one that matters — on the Io half nothing is durable and nothing heals, and the same paragraph then conceded it is "the real gap in closing #295". A settled entry with a false reason gets cited to suppress the finding it is wrong about. Split per item and state plainly that #295 is only half-closed, with #312 as the remainder. Axis 2 caught a false claim of mine in mise.toml: CI does not run `mise run build` — the swift job runs test-swift and nothing else, so a file absent from that list is never type-checked in CI at all (14 of 22 under Sources/; filed as #316). EngineControlService and EngineContainer go back in; the measured cost is ~0.15s, not the 0.4s I claimed, and the "UniFFI closure" mechanism I gave was wrong since the bindings compile either way. Axis 3 asked why the raise's "under the wal mutex" precondition is a doc comment when the cover's ordering was made structural. Fair: it now takes the guard as a witness parameter. That immediately caught three test call sites that were not holding the lock. Also: SPEC enumerated the two issues with no scope boundary, reading as exhaustive; §個別削除 stopped at the synchronous fallback without saying what happens when that fails too; four documents anchored a design point on `isDegraded`, a symbol this branch deletes; the AGENTS retraction sentence contradicted its own next clause; the "no lock" reason named the wal mutex's cost for the inner RwLock; the frozen_flag plan reversal was argued only in a commit message. The LearningMemoryOnly row said all learning is unsaved when only post-checkpoint learning is at risk — it can sit next to .historyDataLoss's 「学習は継続中」.
Owner
Author
|
@codex review |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 0b164a40f2
ℹ️ 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".
…ntly durability_issues read the ledger and the freeze flag as two independent loads. Their writers are ordered — an Io append freezes inside append_record, and only then does apply_records raise the ledger — so a poll could take the ledger before the raise and the flag after the freeze and report a pair that never simultaneously held, dropping DeletionNotPersisted (no startup heal) while keeping LearningMemoryOnly. Packing the ledger's own counters fixed exactly this defect one level down; the composition was still torn. Read the flag between two ledger loads and accept only when the ledger did not move, so the pair is both values as of the instant the flag was read. The regression test's detector needed the same care: comparing the poll's result against a predicate read after it returned would flag a raise that legitimately landed in between. It instead drives one failing deletion to completion first, after which both conditions hold permanently — blocked checkpoint, so nothing covers; appends still failing, so nothing thaws — making any other result a tear.
Measured: reverting durability_issues to two independent loads leaves it green across repeated runs. What it pins is that the retry loop terminates and stays correct under load; the tear is closed by construction. Same standing as the packed ledger's own counters.
Owner
Author
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e28e7733c5
ℹ️ 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".
…ing it Codex found a reachable path where the report reads clean while a commit is in neither the checkpoint nor the WAL. A commit refused by the frozen guard returns before seq assignment, so last_appended_seq does not move; an in-flight compaction whose snapshot predates that commit then passes truncate_covered's `last_appended_seq <= applied_seq` test and clears the freeze. Demonstrated by test_a_stale_compaction_must_not_unfreeze_over_memory_only_commits. This is the second finding on how the report obtains its facts, so the loop's root-check applies rather than another patch. The mechanism is the defect: LearningMemoryOnly was derived from is_frozen(), justified by "a commit is memory-only <=> the WAL is frozen". That equivalence is false, and I had already patched one breach of it (the encode guards) without questioning it. Deriving a fact from a proxy that needs re-defending every round is what CLAUDE.md calls 場当たり的. So the ledger tracks the fact directly: raised_memory_only beside raised_deletion, three 21-bit generations in one atomic. They are separate facts — a SyncFailed tombstone is on disk yet still breached the flush its contract promises, and an Io commit is memory-only without being a deletion at all. The freeze goes back to meaning what its name says, a property of the file that only OpenReport reads. FreezeFlag, the shared atomic, and R1's retry loop all collapse out: one load again, and the torn-pair fix comes free from the packing. Two tests change semantics, both toward accuracy. A WAL frozen at open with nothing learned puts no learning at risk, and a clear whose truncation failed emptied both memory and checkpoint — neither is memory-only until the next commit is refused, which is when the row now appears. Both still assert that it does.
Owner
Author
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 34d3c77c79
ℹ️ 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".
The mid-loop design re-gate (fired because the same mechanism drew findings two rounds running) found the mechanism had converged but the layer that defines it for readers had not — it was patched only where the diff happened to touch. The substantive one: a deletion-only failing batch raised LearningMemoryOnly, telling the user their learning was unsaved when all they did was delete. That is the same reasoning this branch had just rejected for the frozen-at-open and failed-clear paths — applied in two tests and violated one file over. memory_only is now gated on Committed, which also makes the SPEC sentence and the variant doc true as written. The ledger's 21-bit fields wrapped rather than saturated, and the wrap read back below `covered` — silently dropping the row, the one direction this design forbids — while the carry corrupted the neighbouring generation. Raises now saturate at GEN_MASK, covers cap one lower so a saturated generation stays outstanding, and pack_ledger masks every field. Two settled AGENTS entries contradicted the shipped code: the runtime- channel entry still closed by forbidding the commit ledger its own (b) had just adopted — and AGENTS is Codex's review lens, so it would have suppressed findings about the mechanism this PR ships — and a whole entry defended frozen_flag/FreezeFlag, deleted here. The wal.rs comment at the encode guards still asserted the retracted equivalence as live doctrine, and the set_frozen it justified outlived its reason: freezing a perfectly appendable file to serve a reader that no longer exists. Removed. Also merged two tests with identical bodies, renamed deletion_ledger and cover_unpersisted_deletions now that both settle both facts, and recorded the steady-state flicker (appends failing while checkpoints succeed) that the retraction paragraph did not cover.
Owner
Author
|
@codex review |
|
Codex Review: Didn't find any major issues. Can't wait for the next one! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
Owner
Author
|
Both R3 findings landed on the previous head (`34d3c77`) while
Resolved as already-addressed rather than re-fixed. |
Owner
Author
|
@codex review |
|
Codex Review: Didn't find any major issues. Delightful! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
学習永続化 slice の後半。PR1 (#300) が「durable set の真実」を正したのに続き、こちらはそれをユーザーに届ける経路を作る。
嘘の上に報告経路を作ると「嘘を正確に報告する装置」になるため、この順序で分割している。
問題
apply_recordsは()を返す。削除の WAL 耐久化が失敗し、§5.4 の同期 checkpoint fallback も失敗した場合、削除はメモリにしか存在しないが、痕跡は出荷ビルドでコンパイル除去されるwarn!だけだった（#297）。#288 の memory-only 学習も同じく不可視。入れたもの
LexHistoryOpenReport（起動時）の実行中版としてdurability_issues() -> Vec<LexHistoryDurabilityIssue>。どちらも**「メモリが持っているのに、どの durable checkpoint も覆っていない」**という 1 つの台帳から出る。raise は wal ロック下・メモリ適用の後、被覆は「durable set がそれを含まなくなる」2 点（compaction の
save成功 /clearの空 checkpoint 成功）。DeletionNotPersisted— 削除の耐久化が破れた（Io= frame がディスクに無い /SyncFailed= frame はあるが flush が失敗）LearningMemoryOnly— WAL frame が付かないまま適用された確定がある壊れたディスクでは両方立つのが定常なので、単一 enum には畳まずリストで返す。
Swift 側は
EngineControlService経由でポールし、DegradedStatus（純関数）がステータスメニューの行に落とす。正しさは構造で守った箇所
レビューで 2 回、「コメントで順序を守っている」箇所が実際に壊れていたため、どちらも構造に移した。
snapshot_to_cover— 世代読みと snapshot clone を同じinnerread guard の下で取る。raise 側のapply_batchがinnerの write を要求するので、逆順の interleave が成立しない。以前は 2 つの文の順序をコメントが守っていただけで、それを固定していたテストは順序を入れ替えても通ったdurability_ledger—raised_memory_only/raised_deletion/coveredを各 21bit で 1 つの atomic に詰め、判定を単一 load に。複数 atomic だと安全な load 順が 1 つだけになり、間に raise が入ると同時には成立していないペアを返して重い方の行を落とす。窓が隣接する load 数個分なので決定的なテストが書けず、表現不能にした。世代は wrap ではなく飽和させる（wrap はcoveredを下回って報告が止まる = 唯一許されない方向）そして最大のものが
LearningMemoryOnlyの導出をやめたこと。当初はHistoryWal::is_frozen()から導いており、根拠は「確定が memory-only ⟺ WAL frozen」だった。Codex R1 がこの等価性の破れを 1 件見つけ、私はそれを patch した。R2 で等価性そのものが偽だと示された — frozen guard で弾かれた確定は seq 採番に到達しないのでlast_appended_seqが動かず、その確定より前の snapshot を持つ compaction が freeze を解除してしまう。proxy から事実を導出して毎ラウンド等価性を弁護し直すのは CLAUDE.md の言う「場当たり的」なので、台帳に直接載せた。結果FreezeFlag・共有 atomic・R1 の retry ループがすべて畳まれ、freeze は「ファイルが追記可能か」という本来の意味に戻った。計測
変更した critical section（§14-2 のハーネス、20k エントリ + 競合リーダー 2、release）:
HistoryWal::frozenは plainboolのまま（共有 atomic 化は R2 で撤回）。ホットパスに増えたのは、失敗時のみ実行される CAS 1 回と、成功パスのbool判定 1 個だけ。accuracy への影響なし（コスト・重み・reranker・辞書ソース・変換パスいずれも不変）:
mise run accuracy108/108、mise run accuracy-history7/7。Issue の扱い
Io側の削除が実際に復活する再起動時には報告が消えている。残件は history: the unpersisted-deletion report is process-local, so it is gone on the restart where the deletion resurrects #312（on-disk marker が要る = 永続状態の追加なので別 PR）スコープ外（起票済み）
saveが失敗すると無報告（削除自体は durable・起動時 scrub あり）clear()のレースで commit-log が復活しうる（既存バグ）Sources/22 件中 14 件が CI で一度も型チェックされない（既存、この PR の調査で判明）テストプラン
cargo clippy --workspace --all-targets --all-features -D warnings/ Rust 646 tests / msrv 1.88.0 /mise run auditmise run test-swift150 /mise run buildmemory_onlyを削除限定に戻す など）。1 件は意味的に等価な変異と判定。残り 2 件は決定的なテストでは検出不能と実測で確認し、その旨をテストのコメントに明記した（台帳の read 順と ledger↔freeze の合成 — どちらも窓が atomic load 数個分で、だから構造で表現不能にした）⚠️ 新しい学習内容を保存できていません（再起動すると失われます）が出ることを確認。実履歴（1.1MB）復元後に行が消えることも確認menu()がポール結果をDegradedStatus.rowsに渡す配線は IMKit が要るため上記の実機確認のみゲート
/pre-push全 6 段完了。/simplify4 fix、/code-review max15 findings（12 fix / 3 issue 化）、/review1 fix、/lexime-review15 findings（全 fix / 1 reject）。post-push は
/external-convergeを 4 ラウンド。R1 (P2) / R2 (P1) で実 finding、R3・R4 は dry で TERMINAL。R2 で同一機構 2 ラウンド目の root-check が発火したため、TERMINAL を待たず累積 fix-delta の設計再ゲートを実施し、9 件を追加修正した（そのうち 2 件は R3 で Codex が独立に指摘してきたものと同一だった）。🤖 Generated with Claude Code