深夜のバッチが動いた。で、それは「予定どおり」か?
監視は「動いたか」を教えてくれる。だが「予定どおりに動いたか」は、実は別の問いである。予定そのものが実行のたびに計算し直され、環境やライブラリの版で揺れるなら、「予定どおり」を証明する土台がない。予実テーブルの追悼で書いたとおり、多くの現場はこれを「予定を DB に保存しておく」ことで解決してきた——予定の複製を作り、複製と実績を突き合わせ、複製の鮮度に悩む。
Kairos の設計はここで一つの賭けをしている。定義と評価窓とデータのスナップショットが同じなら、評価結果の点集合は必ず同じ(評価は純関数)。だから予定は保存しなくていい——いつでも同じものが計算し直せる。理屈はそうだ。では実運用で本当にそうなったか。
今日は、この言語を本番で使っている外部の実装者から届いた実測の報告を紹介する(数値はすべて先方の運用記録からの引用。固有名は伏せる)。数値はいずれも本番環境での実測で、各節気につき1 発火(ベンチマークではない)。
実測 1: 10 日前の予告が、起動 2 回を跨いでそのまま実現した
先方のシステムは二十四節気の通知を配信している。7 月 13 日の稼働開始時、システムは「次の配信は 7 月 23 日(大暑)の 7 時」と予告した。それから 10 日間——日次の再計算が毎日走り、サーバの起動が 2 回(初回起動と再起動)あり、停止中に溜まった未発火 19 点(9 点と 10 点)の回復処理も挟まった。
7 月 23 日、配信は予定比 +0.728 秒(約 0.7 秒)で実行された。10 日間を通じて予定は変わらず——予告が「そのまま実現した」のである。
実測 2: サーバを引っ越しても、予定は動かなかった
8 月、先方はローカル機から VPS へ本番を移した。移行当日が配信日(立秋)である。開発機と本番機、ホスト環境も違えばコンテナの実行既定タイムゾーンは UTC(未設定の既定)——「どこの 9 時」問題がいちばん事故りやすい構図だが、暦計算のtz は定義側に明示してあるので、環境の時計設定に答えが左右されない設計になっている。
引っ越しの前に走った立秋の配信は、+15.958 秒の遅れ(原因は先方でも未特定)で成立した。引っ越した先の新しいサーバは、起動するなり移行前と同じ発火点を再現した——直前の発火(立秋 7 時)を拾い直し、重複は冪等キーで止まり、そのまま次の予定(8 月 23 日 7 時)へ進んだ。次の節気(処暑)では VPS 単独で+0.032 秒、その次の白露(9 月 7 日)は時刻の書き方を新しい形(at)に切り替えた初の配信で+0.037 秒。立秋から処暑までの 16 日間、記録に残る予定の値(分まで)は完全に一致し続け、10 種類の hostname(コンテナの作り直し)を跨いでも予定は不変だった。機械を跨いだ実証はローカル→VPS の 1 回である。同じ定義・同じデータなら、機械を替えても発火点は同じだった——決定性の実証である。
実測 3: 撃ち漏らしの回復と、二重配信ゼロの両立
止まっていた間に何が起きるはずだったかは列挙できる——これも実地で回っている。実測 2 の引っ越し当日、新しいサーバの初回起動は、24 時間の振り返り窓に入っていた立秋 7 時を「取りこぼした発火」として拾い直した。しかしその発火は移行前に送信済みで、冪等キーが一致したため配信は止まり、再送はゼロ(配信記録は 1 行のまま)。同じ起動で別ジョブの未発火の回復も同時に成立している。同じ宛先への二重配信はゼロ——宛先が複数あっても、同じ宛先に同じイベントが 2 度届いた記録は 1 件も無い。
仕組みは分業である。言語側は「この窓の発火点はこれ」を決定的に列挙するだけ。実行系側は発火点から冪等キー(アプリ名・日付・イベント名・宛先・データの観測日で構成)を作り、同じキーの 2 回目以降をスキップする。「列挙は言語・執行は実行系」の分業は仕様に明文があり(spec §7.8)、決定性はこの分業が成立するための土台になっている——列挙が揺れたら、冪等キーも揺れる。
「証明できる」が変えること
- 監査: 「10/23 に走ったのはなぜか」に、定義とデータのスナップショットを添えて答えられる。 再計算すれば同じ答えが出るから、予定の記録は薄くていい(定義とスナップショットがあれば戻る)。 実績——いつ実際に送ったか——の記録は別で、消えれば戻らない
- 移行: 引っ越しの前後で予定の差分を取れば、移行検証が「予定表の突き合わせ」になる
- 障害対応: 停止窓を評価するだけで撃ち漏らしの完全なリストが出る
予定の複製を飼うのをやめて、定義を正とする——予実テーブルの追悼に書いた理屈は、少なくとも一つの本番システムで、夏を越えて実測どおりに回っている。
明日はローンチ週の最後に、この外部実装者との往復書簡が見つけた「あるバグの事件簿」を書く。決定性の話が「言語が正しく動けば」を前提にしていたのに対し、明日はその前提が破れていた日の話である。
Kairos はスケジュール定義言語です。仕様と参照実装はGitHub で公開しています。
コメント