第16章：それでも壊れる条件

送信されたコマンドは、もう存在しない場所に向かっていた

次の手順を、コードの上でたどってみます。たとえば、ALT+TABで別のウィンドウへ切り替える 場面を考えます。切替の直前、あるウィンドウにフォーカスがある状態で、IMEをオフにするという 決定が下ります。決定はOSへの非同期コマンドとして、キューに置かれます。コマンドが実際に 送信される前に、ユーザーが別のウィンドウへフォーカスを移します。そして、最初の決定に基づく コマンドが、いま存在しないはずの古いフォーカス先へ向けて送信されます。

利用者から見れば、これは次のキー入力が狙った通りに変換されない、という一瞬の不具合として 現れるはずです。ただし、この手順を実際に踏んだという記録は開発ログのどこにも残っておらず、 コードを読む限りこれを止める仕組みが存在しない、という事実だけが分かっています。送信されて しまえば、そのコマンドは取り消せません。OSへ渡った命令は、戻ってきません。

信念(belief)であれば、後から間違いに気づいて書き直せます。しかし、一度OSへ送信された 命令は、awaseの内部にあるどんな値を書き直しても、なかったことにはできません。書き直せる 対象と書き直せない対象を、同じ強さで守る必要はないはずですが、書き直せない対象を守る 仕組みは、まだありません。

第9章で見たFocusEpochは、まさにこの種の事故を防ぐために作られました。それなら、なぜこの 経路だけが素通りするのでしょうか。答えは単純です。FocusEpochが守っている場所と、この コマンドが通る場所が、別の場所だからです。

第9章を書き終えた時点では、観測にまつわる問題は解決したかのように見えました。しかし観測は 目的そのものではなく、最終的にOSへ渡す命令を正しく組み立てるための手段にすぎません。 手段が正しくなったからといって、その先の手続きまで正しくなったとは限りません。

実は第9章の時点にも、答えの出ないまま残された問いが一つありました。admit()でエポックを 照合した後AcceptedObservationを保存してから使うまでの間に新しいエポックへ遷移する ケースをどう防ぐのかという点は、コードを読んで確かめる作業として本章へ持ち越していました。

観測は使うたびに洗い直される。命令はそうではない

確認は、二つの経路に分けて行いました。

一つ目は、観測が受理されてからストアへ書き込まれるまでの経路です。ImmLikeTicket::admit() の呼び出しと、ストアへの書き込みは、with_app(|app| { ... })という一つのクロージャの中で 連続して実行されています(focus_tracking.rs:349、key_pipeline.rs:214,910)。awaseは シングルスレッド・協調的なスケジューリング(win32_async::spawn_local)で動いており、 この区間に割り込みは入りません。受理してから保存するまでの間に、隙間はありませんでした。

そして第9章で見た通り、derive_open()は呼び出しの都度、現在のエポックと記録済みの エポックを再比較します。一度受理されて終わりではなく使われるたびに洗い直され、 第9章の設計が意図した通りに動いています。

二つの経路を並べると、再検証がどこで途切れているかが一目で分かります。

二つ目は、決定がOSへの実際の作用として送信されるまでの経路です。IMEの切替をプロセスを またいで反映させる呼び出しは即座には終わらず完了までに時間を要するため、非同期のキューを 経由する構造になっていますが、非同期であるということは送信を待っている間に世界が 変わりうる、ということでもあります。runtime/executor.rsのdispatch_ime_set_openが担う、 ImmCross向けの非同期処理は次のようになっています。

// 決定(open, origin)はここより前、effective_open() を使った同期処理で確定済み
win32_async::spawn_local(async move {
    let ok = crate::ime::set_ime_open_cross_process_async(open).await;
    // この await の間にフォーカスが変わっても、送信はキャンセルされない
    ...
});

openという値は、awaitに入る前にすでに確定しています。win32_async::spawn_localが使う 協調的なスケジューラ(複数の処理が自分から一時停止しては進行を譲り合う方式)は、 await(結果が返るまでいったん待つ、という意味の構文)に入った瞬間に制御をイベントループへ 戻すため、フォーカス変更を処理するイベントはその間に先に実行されます。送信を待っている openという値は、別のエポックへ遷移したことを何も知らないまま待ち続け、送信は 無条件に実行されます。

完了後の処理はgenerationという値(apply命令を発行するたびに1つ増える番号。第5章で 導入した仕組みです)を照合しますが、これが守るのは「この完了通知を信じてよいか」という 一点だけで、「コマンドがすでに取り消せない形で送信済みである」という事実は照合の対象に なっていません。ここで守ろうとしていたのは状態の一貫性であって、物理的な作用の発火可否 ではなかったのです。

この状態は、二つの独立したフェンシング機構(古い指示や古い通知を、無効なものとして 退ける仕組み)が並んでいる、と整理できます。観測の経路と、効果の経路とでは、保証の 中身が違います。

観測を信じる前にエポックを見る。完了通知を信じる前にgenerationを見る。この二つは対称的な 防御に見えますが、まだ実行していない効果を実行する直前にもう一度照合するという三つ目の 防御は、どちらの機構にも含まれていません。表の上三行と下二行の間には境界線があります。 観測が信念を汚す経路は二重に守られ、drift correctionだけは鮮度フェンスを持つように なりましたが、この節の冒頭で見たdispatch_ime_set_openという最終送出の一点は、まだ 一度も検査されていません。

なお、観測の経路にも隙間は残っています。GJI(Google Japanese Input、Google 日本語入力)・ TSF(Text Services Framework、Windowsの入力方式を仲介する仕組み)のようなイベント駆動の 観測はエポック照合の対象外で、3000ミリ秒の鮮度ウィンドウだけに守られています(同期 ポーリングのObserverPollには、この不一致は起こり得ません)。この隙間は、本章の主題である 効果経路の欠落とは区別しておくべきです。

「型で防げる」と言うとき、実際に防げている範囲を、こうして書き出しておく必要があります。 おおよそ塞がっているという手触りと、実際に塞がっている範囲は、別のものです。

「採用した」と「実機で確かめた」は、章ごとに進み方が違う

この境目は、この章だけの話ではありません。本書の後半で「採用した」と書いた工夫の多くが、 同じ境目を抱えたまま執筆を終えています。

「未実装」と「実装済みだが実機で走っていない」は、別の状態として区別しておく必要があります。 前者はコードがまだ存在しません。後者はコードが存在していても、Windows実機という最後の 関門をまだ通っていません。本書が「採用した」と書いた工夫のうち、実機で確かめられたと 言えるものは、まだ一つもありません。

この自己監査そのものを裏づける出来事も、後から見つかっています。2026年8月、TsfNative アプリへのフォーカス復帰時、実際には何もOSへ送信していないのに、appliedという記録を Confirmed{open: belief}へ書き換えてしまう欠陥が見つかりました(ADR-098、BUG-69)。 beliefを、actuationが完了した証拠として書いてしまう、という同じ形の欠陥です。 docs/known-bugs.mdは、これをBUG-19・33・48・68に続く5例目の同一パターンと記録しています。 本章冒頭で見たFocusEpochが閉じたのは観測の入口であり、beliefと実際の作用の証拠を 取り違えないという規律までは、型の導入だけでは自動的に守られませんでした。

同じ形の欠陥が場所を変えて何度現れたか、時系列で並べると再発の重みが分かります。

5回という再発回数は、それ自体が一つの判断材料です。同じ形の欠陥が3回目・4回目と 別の場所で独立に見つかるなら、それはもう個別修正で足りる段階ではなく、「その形を 型で書けなくする」規律へ格上げすべきだ、というシグナルとして扱うべきでした。実機での 検証は2026年8月22日に1回だけ行われており、長時間のソークはまだありません。

まだ存在しない設計

先の表の下二行のうち、drift correction経路を除いたdispatch_ime_set_openを埋めるとすれば、 という以上の意味を持たない候補です。ここから先は実装済みの仕組みの説明ではなく、 awaseのコードにはまだ存在しない設計です。

Effectにも観測と同じように生成時点のエポックを持たせるという案がありますが、値として 持たせるだけでは、照合を呼び出す側が書き忘れればそのまま素通りしてしまいます。より強い 案は、dispatchの手前に通過しなければ送信できない関所を置くことです。観測の受理で使った 形を効果の送信にも当てはめ、AcceptedObservationに対応するAcceptedEffectのような型を 用意して、その関所を通った値しか送信関数に渡せないようにします。関所を型で強制しておけば、 送信経路が新しく増えても同じ抜け道は生まれにくくなります。

いずれの案も狙いは一つです。決定からOSへの送信までの間に生じる間隙で、もう一度いまの エポックやgenerationと照合し、一致しなければ送信そのものを取りやめる。取り消せなくなる 直前の地点を、最後の検査点にすることです。もっとも、この検査点にも代償はあります。送信の 直前にもう一度照合すれば、その分だけ送信のタイミングが遅れます。フォーカスが変わる頻度に 比べてこの遅れがどこまで許容できるかは、実装してみるまで分かりません。

この2つの案のうち、値を持たせるだけの案に近い形は、drift correction経路にはすでに 一部入っています。第10章で見たActuation.sent_atという送信時刻が、収束確認の下限を 定める鮮度フェンスとして2026年7月25日に実装されましたが、Windows実機でのソークテストは まだ実施されていません。一方、dispatch_ime_set_openという最終送出の一点には、この2つの 案のどちらも入っていません。第9章の82分とは違い、ここにはまだ答えがありません。

本書のここまでの章は、実際に起きた事故から学んだ工夫を扱ってきました。この章だけは、まだ 起きていない事故を、起きる前に設計で塞ぐという先回り型の指示のしかたです。同じ2026年7月25日に 起票されたADR-082(journalの構造化リプレイ基盤化)も、Claude Fable 5との壁打ちが起点でした (第13章参照)。

他分野への転用

空いた駐車スペースを見つけてから、車を取りに戻るまでの間

空いている駐車スペースを見つけて、少し離れた場所に停めた自分の車を取りに戻る間に、別の車が 先にそのスペースへ入ってしまうことがあります。確認した瞬間には空いていたのに、使おうとする 瞬間には状況が変わっているということです。

この種の間隙は、ソフトウェアの世界では長らく知られてきました。「確認した時点」と「使う 時点」がずれることで起きる不具合は、TOCTOU(Time-Of-Check to Time-Of-Use、確認時点から 使用時点への時間差)と呼ばれ、CWE(Common Weakness Enumeration、既知のソフトウェアの 弱点を分類する体系)にも独立した項目(CWE-367)として登録されています。古典的な例は Unixのファイル操作で、アクセス確認と実際のオープンの間にファイルがシンボリックリンクへ すり替えられると、確認したはずのファイルとは別物が開かれてしまいます。

awaseのExecutor直前の空白は、この古典的なパターンの一変種です。admit()という確認と 実際にOSへコマンドを送信する使用が、非同期のawaitを挟んで離れているために、確認時点で 正しかった前提が送信時点でも正しいとは限らなくなっていました。ファイルがすり替えられるか フォーカスが切り替わるかという違いはあっても、「確認と使用の間に間隙があれば前提が壊れうる」 という形そのものは同じです。

この類似には、テストのしやすさという観点から見て、重要な非対称性もあります。admit()や derive_open()のような純粋関数は、値を入れ替えるだけでテストコードの中に再現できますが、 TOCTOUの間隙そのものは、フォーカス変更とawait再開という二つの非同期な出来事が特定の 順序で重ならなければ発現しないため、狙って再現するのが極めて困難です。テスト容易性と、 間隙の不在は、別の性質です。

そして、この「Executor直前の空白」は、後に調べたロボットランタイムにも存在していました。

設計原則

原則: 鮮度の再照合は、値を使う場所に置くだけでは終わりません。作用が取り消せなくなる直前の場所にも、同じ再照合を置く必要があります。

適用条件: 決定から実行までの間に非同期の間隙があり、かつ実行後に取り消せない作用を伴う経路に当てはまります。間隙のない同期処理や、実行後に取り消せる作用には当てはまりません。

実装の形: 送信を担う関数に、決定時点のエポックやgenerationを引数として持たせます。送信の直前に、その値と現在の値をもう一度照合し、一致しない場合は送信そのものを取りやめます。

限界: この再照合を置いても、判定から送信までの間にさらに間隙が生まれれば、同じ問題は一段深い場所に移るだけです。境界をどこまで遡って検査するかは、有限の選択であり続けます。