💬 自然言語処理

CrossTL: Hub-Based Translation of GPU Programs and the Preservation of Source Rules

本論文は、ルールを保持する中間言語（CrossGL）を介して10のGPU言語を11のターゲットへとルーティングする、ハブ型のオープンソース・トランスレータであるCrossTLを紹介するものであり、ソース固有のセマンティックなルールを明示的に保持することが、構文のみに依存するアプローチと比較して翻訳の乖離を大幅に減少させることを実証しているが、基盤となる実装の非適合性により完全な正当性を保証することはできず、大規模なサードパーティ製コードに対するユーザビリティの向上もわずかなものにとどまっている。

原著者： NRIPESH NIKETAN, VAATSALYA SHRIVASTVA, BHUSHAN SRIVASTAVA, SUSHANT MISHRA

公開日 2026-10-20✓ Author reviewed ⓘ

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： NRIPESH NIKETAN, VAATSALYA SHRIVASTVA, BHUSHAN SRIVASTAVA, SUSHANT MISHRA

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

現代のビデオゲーム、科学シミュレーション、そして人工知能はすべて、グラフィックス・プロセッサ上で動作する特殊な種類のコンピュータ・プログラムに依存しています。これらのチップは、一度に大量の計算を行うことに非常に長けていますが、数値の扱い方については非常に好みが分かれます。Apple、NVIDIA、AMDといったこれらのチップを製造する各社は、これらのプログラムを記述するために異なる言語を使用しています。これらの言語は表面上は似ていますが、算術の最も基本的なルールにおいて意見が食い違うことがよくあります。例えば、ある言語では、ある数値を自分自身に加えた結果が大きすぎる場合に、結果が小さな負の数へと「ラップアラウンド（回り込み）」すると規定している一方で、別の言語では、その操作は未定義であり、何が起こるかわからないと規定している場合があります。開発者があるタイプのチップ向けにプログラムを書き、それを別のタイプのチップへ移行しようとする際、翻訳ツールはそのどのルールに従うべきかを決定しなければなりません。もしこの判断を誤れば、プログラムはコンパイルされ実行はされるものの、誤った答えを導き出し、ゲームのクラッシュや科学データの破損を引き起こす可能性があります。

研究チームは、これらのグラフィックス・プログラムのための「ユニバーサル・トランスレーター（汎用翻訳機）」を構築することで、この問題の解決に取り組みました。彼らは、中心的なハブとして機能するCrossTLと呼ばれるシステムを開発しました。あらゆる言語の組み合わせに対して個別の翻訳機を作る代わりに、彼らのシステムは10種類の異なるソース言語からコードを受け取り、それを単一の中立的な形式に変換してから、11種類の異なるターゲット言語へと送り出します。彼らが直面した核心的な課題は、この中立的な形式自体には、特定のコードがどの特定のルールに従うべきであったかという記憶がないことでした。それは単純な加算記号を見ても、その記号が「ラップアラウンド」を意味するのか、それとも「停止してエラーを出す」ことを意味するのかを判別できないのです。この記憶がなければ、翻訳機は意図せずプログラムの意味を変えてしまい、コードは実行されるものの計算結果が誤っているという「サイレント・フェイラー（静かな失敗）」を招く恐れがあります。

これを解決するために、研究者たちは「ルール・キャリング（ルール運搬）」と呼ばれる手法を開発しました。彼らは、遭遇するすべての数学的演算に対して、特定の「メモ」を付与するように翻訳機を改良しました。このメモは、元の言語がその演算に対してどのルールを使用したかを正確に記録します。コードがハブを経由して新しいターゲット言語へと向かうとき、翻訳機はこのメモをチェックします。もしターゲット言語が同じルールに従っている場合は、その演算をそのまま通過させます。もしターゲット言語が異なるルールに従っている場合は、翻訳機はその演算を、ターゲットにソースと全く同じ挙動を強制させるためのカスタムメイドのコードへと置き換えます。これにより、基礎となる言語の違いに関わらず、プログラムが新しいハードウェア上でも旧来のハードウェアと同じ結果を算出できることが保証されます。

チームは、このシステムを「ハザード・カーネル」として設計された66種類の厳密に設計されたテストプログラムを用いて徹底的に検証しました。これらのテストは、ゼロ除算や数値の加算によるオーバーフローなど、言語間でルールが食い違う箇所を誘発するように設計されています。彼らは、Appleのグラフィックス・プロセッサやいくつかのオープンソース・ドライバーを含む、さまざまな実世界のハードウェアおよびソフトウェア環境でこれらのテストを実行しました。その結果、彼らの新しい手法を用いない場合、既存の翻訳ツールは多くのケースで正しいルールを見失い、誤った出力を生成することが示されました。研究者たちがルール・キャリング機能を有効にすると、システムはほぼすべての事例において正しい挙動を維持することに成功しました。数百回のテスト走行のうち、エラーの数は劇的に減少しましたが、残ったわずかな失敗は、翻訳ロジック自体の欠陥ではなく、特定のドライバーによるコードの処理における特有の癖に起因するものでした。

また、この研究では、機械学習ライブラリからグラフィックス・エンジンに至るまで、サードパーティによって書かれた数千の現実世界のプログラムにおけるこの新手法の性能についても調査しました。研究者たちは、この新システムは、既存のツールと比較してコンパイラが受理できるコードを生成する確率がわずかに低いものの、コンパイルされたコードが実際に正しく動作するという点においては、はるかに信頼性が高いことを発見しました。実際、この新手法によるコードの成功率の変化は1パーセント未満であり、既存のワークフローを壊すことなく導入できることが証明されました。研究者たちは、翻訳機が真に忠実であるためには、単に構文を別の言語へ移動させるだけでなく、ソース言語の「意味論的なルール（セマンティック・ルール）」を道連れにして、プログラムの意味が旅の間も損なわれることなく維持されるようにしなければならないと結論付けました。

技術要約: CrossTL: GPUプログラムのハブベース翻訳とソース言語規則の保存

1. 問題提起

GPUプログラムは、ベンダー固有の言語（例：GLSL、HLSL、Metal Shading Language (MSL)、CUDA、OpenCL C）で記述されているが、これらは共通の構文的語彙を持ちつつも、意味論的な規則において大きく乖離している。これらの相違点には以下が含まれる：

整数オーバーフロー: GLSLおよびWGSLは符号付きオーバーフローをラップ（wrapping）として定義するが、C++ベースの言語（MSL、CUDA、OpenCL C）や現代的なHLSLコンパイラ（DXC）は、これを未定義動作（UB）またはポイズンとして扱う。
ゼロ除算: ルールは、特定の値を返す（例：レガシーなDirect3Dにおける0xFFFFFFFF）もの、不定値を返すもの、あるいは未定義動作となるものなど、多岐にわたる。
浮動小数点収縮（Floating-Point Contraction）: 融合積和演算（FMA）に関するデフォルトの挙動や、NaN/無限大に関する仮定が、言語やコンパイラの設定によって異なる。
データレイアウト: バッファのストライド（例：Metalにおけるfloat3とHLSLの差異）やメモリ配置の規則が一貫していない。

核心となる課題: ハブベースの翻訳アーキテクチャ（ $M$ 個のソースを $N$ 個のターゲットに接続する一つの中間言語）において、操作の構文のみを記録する翻訳器は、ソースのラップ規則とターゲットの未定義規則を区別することができない。その結果、翻訳されたプログラムはターゲット上で正常にコンパイルされるものの、計算結果が誤る（意味論的な乖離）可能性がある。既存のツールは、多くの場合単一の中間言語（例：WGSLのラップ規則）のセマンティクスを継承するか、あるいは記録・強制されていないターゲット固有のフラグに依存しており、その結果、「潜在的なドロップ（latent drops）」、すなわち義務が静かに失われる現象を引き起こしている。

2. 手法

著者らは、10種類のGPU言語をテキストベースのハブ言語であるCrossGLにインポートし、11種類のターゲット言語を出力するオープンソースのソース・トゥ・ソース翻訳器、CrossTLを研究している。

2.1 ハブ・アーキテクチャ

CrossGL: RustやWGSLの拡張機能を備えたCファミリー言語。これはテキストベースの中間表現（IR）として機能する。
インポーター/エミッター: 10種類のインポーターがネイティブの構文木を解析してCrossGLダイアレクトを出力し、11種類のエミッターがCrossGLの構文木を走査してターゲットコードを生成する。
制限事項: ハブはテキストベースであり、意味論的な規則に関して型付けされていない。そのため、ある操作（例：x + 1）がGLSLのラップ規則に従うのか、それともMSLの未定義規則に従うのかを本質的に区別できない。

2.2 形式的フレームワーク：忠実な翻訳（Faithful Translation）

論文では、忠実な翻訳を、コンパイル構成および記録された状態エンコーディングの下での「拒絶までの精緻化（refinement up to rejection）」と定義している。

義務（Obligations）: ある構成が、修正なしにターゲットの同名構成へとマッピングされた場合に、不忠実な挙動（すなわち、ターゲットのルールがソースのルールを精緻化しない場合）をもたらすとき、その構成は「義務」を伴う。
処置（Treatments）: 翻訳器は、以下の方法で義務に対処しなければならない：
1. 解消（Discharging）: ターゲットのルールがソースのルールを精緻化する構成または設定を出力する。
2. 検証（Checking）: 義務が満たされない場合にローダーに拒絶させる。
3. 仮定（Assuming）: 入力空間または実装の仮定を制限する。
4. 拒絶（Refusing）: 診断と共に停止する。
5. 破棄（Dropping）: 上記のいずれも行わない（不忠実）。

2.3 ルール保持型翻訳（CrossTL-R）

ハブがルールを区別できない問題に対処するため、著者らは**ルール保持（rule carrying）**を提案している：

アノテーション: アノテーション・パスが操作の発生箇所を特定し、それらを特定のソースルールを表す個別のイントリンシック・コール（例：__cgl_wrap_add）へと書き換える。
ローリング（Lowering）: 1つのターゲットごとのルールテーブルが、これらのイントリンシックを以下にマッピングする：
- ネイティブ（Native, N）: ターゲットの同名構成（ソースのルールを精緻化する場合）。
- ポリフィル（Polyfill, P）: 「信頼できる基盤（trusted base）」となる操作（例：ビット再解釈、無符号算術）を用いたCrossGLによる実装。
- 拒絶（Refusal, Ref）: ターゲットがそのルールを表現できない場合。
健全性（Soundness）: 論文では、アノテーションが健全かつ完全であり、かつルールテーブルのエントリが健全であれば、翻訳は忠実であるという定理を提示している。

2.4 評価

評価には以下を用いる：

ハザード・スイート（Hazard Suite）: 6つのソース言語にわたる18クラスのセマンティクスの差異をカバーする66個のカーネル。
コーパス: 12のプロジェクト（MLX、Vulkanサンプル、ggmlを含む）から得られた2,585個のサードパーティ製翻訳ユニット。
ランタイム: AppleのMetalコンパイラ、MoltenVK、KosmicKrisp（適合性のあるVulkanドライバ）、Mesaのlavapipe/llvmpipe、およびDXC。
機械的検証: SMTソルバ（Z3）を用いて、ルールテーブルのエントリの健全性を言語仕様に対してチェックする。

3. 主な貢献

セマンティクス・カタログ: 8つのGPU言語における操作の差異の18クラスを仕様から導出したカタログ（表1）。
忠実性の形式モデル: 忠実な翻訳を「拒絶までの精緻化」として定義し、解消、検証、仮定、拒絶の可能な義務を区別した。
ルール保持メカニズム: ハブを通じてソースのルールを記録するモデルと実装（CrossTL-R）。アノテーションが健全かつ完全であり、ルールテーブルが健全であれば、ルール保持が意味を保存することを証明している。また、単一の「最強のセマンティクス」が十分である場合と、特定のソースルールを記録しなければならない場合を特徴付けている：厳密なフレームが与えられたとき、すべてのターゲット構成はソースのルールを精緻化しなければならず、拒絶を行わないハブは、定義が衝突している場合に操作のソースを正確に記録しなければならない。
実装と分析: MetalのC++テンプレートのモノモーフィナイザー（monomorphiser）を含むCrossTLの記述、およびSMTソルバを用いたルールテーブルの機械的チェック（131個中13個の不健全なエントリを特定）。

4. 結果

ルールの保存:
- 標準的な翻訳器（SPIRV-Cross、naga、Tint、Slang、および修正なしのCrossTL）は、様々なランタイム上でソースのルールを失う。例えば、SPIRV-CrossとCrossTLは、Metalにおいて、Metalコンパイラが未定義のオーバーフロー仮定の下で x + 1 > x を true と畳み込むため、ラップのセマンティクスを保持できない。
- CrossTL-Rは、保持されたルールにおける37個の差異のうち32個を取り除いた。残りの5個の差異は、ランタイムスタックの失敗（例：MoltenVKやKosiskrispが、符号付き加算として扱うことで正しいSPIR-Vを誤コンパイルしたこと）に起因する。
- 462個のホールドアウト・ランダムカーネルにおいて、修正されたカタログの下で、CrossTL-Rはゼロの差異を示したが、修正なしのCrossTLは120回の実行で差異が生じた。
健全性チェック: SMTチェックにより、記録された131個のルールテーブルエントリのうち、13個が不健全であることが判明した（例：特定のデバイスプロパティなしでのSPIR-V上のNaN処理）。
サードパーティ製コードの妥当性:
- 確立された翻訳器は、コーパスにおける39件の比較のうち31件において、CrossTLよりも多くの有効なグラフィックスコードを生成した。
- CrossTLの利用可能な翻訳率は約31%である。
- ルールを保持すること（CrossTL-R）による、ターゲットの許容シェアの変化は最大でも0.2パーセントポイントであり、ルール保持が構文的な妥当性を著しく損なわないことを示している。
コスト:
- ほとんどの操作において、ルール保持によるMetalでの実行時コストの増加は無視できる（ポリフィルはハードウェア操作へとコンパイルされるため）。
- しかし、すべてのソースに対して単一の「最強のセマンティクス」を使用する場合、保持された特定のソースルールを使用する場合よりも、約9倍多くの書き換え（ポリフィル）が必要となる（特に、符号付きオーバーフローが未定義であるCUDAやHIPのような言語において）。

5. 意義と主張

本論文は、ソース言語のルールを各操作に対して記録することが、アノテーションが健全かつ完全であり、かつルールテーブルが健全である限り、ハブベースの翻訳器において意味を保存するために十分であることを主張している。

必要性: ソースのルールが衝突する場合（例：ラップ vs 未定義）、かつ共通の精緻化が存在しない場合、拒絶を行わないハブは特定のソースルールを記録しなければならない。単一の「最強のセマンティクス」は不十分であり、不必要な書き換えや拒絶を招く。
十分性: アノテーションが健全かつ完全であり、テーブルが健全であれば、忠実性は保証される。
実用的影響: 「適合している」とされるドライバ（KosmicKrisp）であっても、ランタイムスタックが仮定（ラップなど）を強制していない場合、正しいコードを誤コンパイルする可能性があることを本研究は強調している。したがって、忠実な翻訳器は、ルールを保持するだけでなく、特定のルールを記録し、かつ使用者の特定のランタイムスタック上でテストされる必要がある。

著者らは、自身の実装は形式的に検証されたものではなく、偏差のカウントはテストされた入力に対する下限値であり、評価は特定のハードウェア（Apple Silicon）およびCPUドライバに限定されていることを認め、控えめな姿勢を保っている。本研究は、ルール保持なしではハブが重要な意味論的区別を失うという事実を認めることで、CrossGLがすべての言語のセマンティクスを捉えているという先行研究の主張を精査するものである。