Apollo 11 の誘導コンピュータコードに、文書化されていないバグがあることが判明しました。

Japanese Translation:

以前は見落とされていたアポロ・ガイダンスコンピュータ（AGC）のジャイロ制御コードにおけるリソース・ロックリークが発見された。57年間検出されなかったこのバグは、トルク操作中に慣性計測装置（IMU）が「カゲット」されるときに起こり、BADEND ラウトインが LGYRO ロックを解除せずに終了するため、後続のジャイロ操作がハングする。AGC の 130k 行のアセンブリコードを 12.5k の Allium 行動仕様に抽出した結果、エラー経路での未解放が明らかになった。この欠陥は、従来のコードレビュー、エミュレーション、転写検証では捕捉されなかった。というのも、不良パスはほとんど実行されず、可視的なエラー信号を生成しないためである。アポロ 11 では、ミッション・コントロールの「1202 アラーム」が LGYRO をクリアするハードリセットを必要としており、通常運用中に問題がマスクされた。AGC の 74 KB コアロープメモリはボランティアによって物理的に織られ、回収されたソースとバイト単位で検証された。マーガレット・ハミルトンのチームは、優先度スケジューリング、非同期マルチタスク化、再起動保護、およびソフトウェアベースのエラー回復をアポロ計画に導入した。この欠陥は CWE‑772（「有効寿命後のリソース解放が不足」）を示し、レガシー飛行検証済みシステムでもロックリークが残存できることを示している。Allium の仕様モデルは、すべての実行パスにわたってリソースライフサイクル（取得・保持・解放）を扱い、こうした静かな失敗を検出可能にする。現代のプログラミング言語は defer、try‑with‑resources、所有権システムなどの構文でロックリーク防止を試みるが、多くのドメインではクリーンアップがプログラマ駆動であるため問題は残る。バグはその後のアポロミッション（コマンドモジュール COMANCHE とルナモジュール LUMINARY）に継続して伝搬し、発見も修正もされなかった。

この改訂要約はすべての主要ポイントを完全に反映し、根拠のない推測を排除し、読者に明確で簡潔な物語を提示する。

アポロ誘導コンピュータ（AGC）は、歴史上最も精査されたコードベースの一つです。
数千人の開発者がそのコードを読み、学術研究者は信頼性について論文を書き、エミュレータは命令単位で実行しています。その中で、57 年もの間見逃されていたバグを発見しました――ジャイロ制御コードにあるリソースロックがエラー経路でリークし、誘導プラットフォームの再整合機能を静かに停止させる問題です。

私たちは Claude と Allium（オープンソースの行動仕様言語）を使い、130,000 行の AGC アセンブリを 12,500 行の仕様へと凝縮しました。仕様はコード自体から派生したもので、そのプロセスが直接欠陥に導きました。

コードを図式化する

AGC のソースコードは 2003 年以来公開されており、ロン・バークリーとボランティアチームが MIT の Instrumentation Laboratory で印刷されたリストから手作業で転写しました。2016 年には元 NASA インターンのクリス・ガーリーによる GitHub リポジトリが流行し、1 KRAM と 1 MHz クロックを持つ機械のアセンブリ言語を数千人が閲覧しました。

AGC のプログラムは 74 KB のコアロープに保存されていました。銅線を手で微小磁性核に通すことで 1（線を通す）と 0（線を外す）が決まりました。この作業者たちは社内で「Little Old Ladies」と呼ばれ、メモリ自体は LOL メモリと呼ばれていました。プログラムはハードウェアに物理的に織り込まれていたのです。ケン・シリフは個々のゲートまで解析し、Virtual AGC プロジェクトはソフトウェアをエミュレーションで動かし、回収したソースをコアロープダンプとバイト単位で照合しています。

飛行コードに対して正式な検証・モデルチェッキング・静的解析は公開されていません。精査は深くても特定の種類（コード読取、エミュレーション、転写確認）に限られていました。

私たちは別のアプローチを取りました。Allium を使って慣性測定ユニット（IMU）サブシステムから行動仕様を抽出し、ジャイロベースのプラットフォームが宇宙船の向きを示す仕組みをモデル化しました。この仕様は共有リソースのライフサイクル（取得・保持・解放）を表します。

この手法で、読み取りとエミュレーションでは見逃されていた欠陥を発見できました。

参照を失う

AGC は IMU を共有リソースロック LGYRO で管理しています。コンピュータがジャイロをトルク（傾きを補正）する際、開始時に LGYRO を取得し、3 軸すべてのトルク完了後に解放します。このロックは同時に複数のルーチンがジャイロハードウェアを操作しないようにします。

ロックはエントリで取得し、出口で解放されます。しかし第三の経路が存在し、ロックを解放しません。

Caging は緊急措置です。IMU のジンバルを物理的に固定してジャイロを保護するクランプで、乗組員はコックピット内のガード付きスイッチで作動させることができます。

正常終了時は

STRTGYR2

を通じて LGYRO がクリアされます。IMU がトルク中に cage された場合は

BADEND

と呼ばれるルーチンを経由し、ロックをクリアしません。次の二つの命令が欠けています。

CAF  ZERO
TS   LGYRO

合計四バイトです。

LGYRO が固まると、以降にジャイロをトルクしようとするすべての試みはロック保持中としてスリープし、復帰信号が来ないため永遠にハングします。微調整、漂移補正、手動ジャイロトルク：すべてブロックされます。

1969 年 7 月 21 日、ネイル・アームストロングとバズ・オールドリンが月面を歩く間、マイケル・コリンズはコマンドモジュール「コロンビア」で単独で軌道を維持していました。彼は毎 2 時間ごとに月の背後へ消え、地球との無線通信が途絶えていました。「私は今、本当に孤立し、何も知らない存在から切り離されている」と Carrying the Fire に書きました。

各通過時に彼は星見合わせプログラム 52（P52）を実行し、誘導プラットフォームが正しい方向を指しているか確認していました。もしプラットフォームが漂移すれば、帰還用のエンジン点火は誤った方向へ向きます。

無線沈黙

バグがどのように現れたかを示します。

コリンズは光学ステーションで星見合わせを終え、最終指令を入力しました。コンピュータはジャイロをトルクしてすべての軸に補正を適用しています。彼は狭いコックピット内でメインパネルへ戻り、flip‑up カバーで保護された cage スイッチに手首が触れます。

コードは

CAGETEST

ルーチンで cage を検知し、トルクを中止して終了します。P52 は失敗し、彼は原因を理解します：cage が補正を妨げたのです。IMU をアンケージし、光学ステーションへ戻って再整合します。

新しい P52 を開始するとプログラムがハングします。

警告もなく、プログラムランプも点灯せず、DSKY（ディスプレイ・キーボード）が入力を受け付けても何もしません。

V41

（手動ジャイロトルク）も同様です。他のすべてが機能します。ジャイロ操作だけが停止しています。

最初の失敗は cage イベントによる既知の回復可能なケースに見えます。二度目は何が問題かを示さず、訓練された対応策（アンケージして再整合）は適用されませんでした。コリンズはコンピュータを再起動するよう訓練されていましたが、この失敗では必要性が示唆されません。入力は受け付けられ、他の機能は正常です。これはハードウェア障害に見えるでしょう。

「最後 6 ヶ月間の私の秘密の恐怖は、彼らを月面に残し地球へ帰ることでした」とコリンズは後に書きました。月面でアームストロングとオールドリンが誘導打ち上げを待つ間、ジャイロシステムが停止している状況です。

ハードリセットが解決しました。しかし 1202 アラームが月降下中に発生し、ミッション・コントロールのラインでストレスが高まっていたため、彼は自らの判断で再起動を行わなければならない場面でした。

知るべきマイルストーン

「rope mother」として知られるマーガレット・ハミルトンは LUMINARY の最終フライトプログラムをコアロープに織り込む前に承認しました。MIT Instrumentation Laboratory のチームは、現在当たり前になった優先度スケジューリング、非同期マルチタスク、再起動保護、ソフトウェアベースのエラーレカバリを開発しました。「software engineering」という用語自体が彼女のものです。

その優先度スケジューリングは 1202 アラームが降下中に発火した際に、低優先度タスクを削除し、設計どおりに動作させました。多くの現代システムは過負荷時にこのような挙動を行いません。

最も深刻なバグは仕様エラーであり、コードミスではありませんでした。月面着陸誘導コードを書いたドン・イェイルズは数例を文書化しました。例えば、レゾナンスレーダーの ICD には 800 Hz の電源が周波数ロックされると記載されていますが、位相同期については言及していませんでした。その結果、位相ドリフトでアンテナがちらつき、1 秒あたり約 6,400 回の偽割り込みを発生させ、アポロ 11 の降下時にコンピュータ容量の約 13% を消費しました。これが 1202 アラームの根本原因です。

今回の欠陥も同じ形状です。

BADEND

は IMU モード切替操作で共有される一般的な終了ルーチンです。

MODECADR

（スタールレジスター）をクリアし、スリープ中のジョブを復帰させて終了します。しかし LGYRO はジャイロ専用のロックであり、トルクコードのみが取得し、通常完了経路

STRTGYR2

でのみ解放されます。エラー経路が

BADEND

を通ると、一般リソースは正しく処理されますがジャイロ専用ロックはクリアされません。

AGC は防御的に設計されており、再起動ロジック（全消去可能メモリ初期化時の副作用）で LGYRO が自動的にクリアされるようになっています。バグをトリガーした後に再起動が発生すれば、システムは無事復旧します。

防御的なコード設計は問題を隠しましたが消し去ったわけではありません。cage イベントで再起動が行われない場合、ジャイロはロックされたままであり、コリンズは誘導プラットフォームを再整合できず、診断手掛かりも得られませんでした。

星見合わせ

Allium を使って IMU サブシステムの行動仕様を抽出し、欠陥を発見しました。仕様では共有リソースは「取得」「保持」「解放」のエンティティとしてモデル化されます。

IMU エンティティは

gyros_busy

フィールドで LGYRO を表します。二つのルールが定義されています。

rule GyroTorque {
    -- ジャイロトルクパルスコマンドを送信し、ジャイロを予約、
    -- 電源供給を有効化し、軸ごとにパルスを発行。
    when: GyroTorque(command: GyroTorqueCommand)

    requires:
        imu.mode != caged
        imu.gyros_busy = false

    ensures:
        imu.gyros_busy = true
        GyroTorqueStarted()
}

rule GyroTorqueBusy {
    -- 既に別のトルク操作でジャイロが予約されている。
    -- 呼び出し側は LGYRO がクリアされるまでスリープ。
    when: GyroTorque(command: GyroTorqueCommand)

    requires: imu.gyros_busy = true

    ensures:
        JobSleep(job: calling_job())
}

GyroTorque

は

gyros_busy = false

を要求し、実行後に

true

に設定します。つまりロックを取得しました。コードのすべての経路で必ずロックが解放される必要があります。仕様はコード内で解放がどこで起きるか示さないものの、その義務を明確にしています。

Claude は

gyros_busy

が

true

に設定された後に実行されるすべての経路を追跡しました。正常終了パス（

STRTGYR2

）ではクリアされますが、cage で中断された経路（

BADEND

）では解放されません。

MODECADR

は

BADEND

内で正しくクリアされていますが LGYRO は欠けています。

仕様は IMU モード切替コード全体を通じてこの質問を投げかけます。レビュワーは

BADEND

を検証するとき、設計されたすべてのリソースが完全にクリーンアップされることを確認できます。

逆方向からアプローチします：LGYRO から始め、解放しない経路が存在するかどうか尋ねます。テストは「コードが書かれた通りに動作するか」を検証しますが、行動仕様は「コードが何をすべきか」を問いかけます。

Allium によって抽出された仕様は、誰もテストしなかった経路を含めてリソースライフサイクルをモデル化しています。GitHub で Allium の仕様とバグ再現を見ることができます。

コース・コレクション

ハミルトンのチームはリソースを解放する際、定数ゼロをアキュムレータにロードし（

CAF ZERO

）、ロックレジスタに格納しました（

TS LGYRO

）。すべての解放は手作業で実装され、プログラマが到達可能なすべてのパスを覚えていました。

現代言語はロックリークを構造的に不可能にしようとしています。Go の

defer

、Java の try‑with‑resources、Python の

with

、Rust の所有権システムはコンパイル時エラーとしてロックリークを検出します。

しかしロックリークは依然存在します。MITRE はこのパターンを CWE‑772：「有効ライフタイム後のリソース解放漏れ」と分類し、悪用の可能性が高いと評価しています。すべてのリソースが言語ランタイムによって管理されるわけではありません。データベース接続、分散ロック、シェルスクリプトのファイルハンドル、インフラストラクチャは依然としてプログラマの責任です。プログラマがクリーンアップを書く必要がある場所なら、同じバグが潜んでいます。

すべてのアポロ乗組員は無事帰還しました。しかし IMU モード切替ルーチンは Command Module ソフトウェア（COMANCHE）と Lunar Module ソフトウェア（LUMINARY）の両方に継承され、欠陥は未発見・未修正のままでした。

57 年前から存在するバグが飛行実証されたアセンブリに潜んでいます。あなたのコードにも隠れているものは何でしょうか？話し合いませんか？

Farzad “Fuzz” Pezeshkpour が独自にバグを再現したこと、Danny Smith と Prashant Gandhi がこの記事の初稿をレビューしてくれたことに感謝します。

Apollo 11 の誘導コンピュータコードに、文書化されていないバグがあることが判明しました。