これは、Axivion for CUDA に関する共同エキスパートシリーズの第1回です。
「コンピュータが普及するにつれ、安全性が求められる用途にも使われるようになった。そうしたコンピュータ上で動くソフトウェアではリスクが高く、より慎重な設計と構築が求められる。」
数週間前、Qt Group から、新たに CUDA をサポートしたコード解析ツール Axivion について記事を書いてほしいと連絡をもらった。Axivion は、熟練開発者が従う MISRA、AUTOSAR、NVIDIAの ガイダンス などのコーディング標準を置き換えるのではなく、補完するよう設計されたコード解析ツールだ。
コード解析ツールには長い歴史がある。1970年代、K&Rの「The C Programming Language」が出た頃、ベル研究所の Stephen C. Johnson が lint というプログラムを開発した。自体は、言語設計で解決された機能(例: 引数型の不一致)や、コンパイラに取り込まれた機能(例: 移植性に関する慎重な警告)によって役目を終えた歴史的な遺物だが、コンパイラの本来の仕事であるソースコードから機械語への変換を補うツールの役割は残り、起源へのオマージュとしてこうしたツールは linter (リンター)と呼ばれている。
本番でリンターを使った最初の経験は1990年代のMicrosoftだった。そこで同社は、コンパイラよりずっと厳しくコードを検査する静的コード解析ツール PREfast を買収した。経営陣はバッファオーバーフローによる脆弱性などを懸念しており、PREfast はソースコードを俯瞰的に解析してそうしたバグを検出するよう設計されていた。チームは Windows のコードベース全体を PREfast にかけ、見つかった問題ごとにバグを起票した。
この作業は、私の開発者人生の中で、コードの書き方に最も大きな影響を与えた――なぜなら、その中にはリグレッショリスクなしにはほとんど直せないバグがあったからだ。
もし関数が malloc() の戻り値を検査せず、結果のポインタを呼び出しスタックに渡し、一部のコードパスだけがその不正なポインタを参照していたとしたら… PREfast はそのバグを検出し、再現に必要な条件を正確に示してくれる。しかし、そのバグを直すには多くの箇所に手を入れる必要があり、修正がコードレビューで正しいと確認するのが難しくなることもあった。
PREfast が起票したバグは、概ね次の三つに分類できた。
ほとんどの場合、PREfast はソースコードを最小限の変更で修正できる正当なバグを報告した。
ときには、PREfast が誤検知を挙げたことを証明できた。
そして時折、釈然としない結末もあった。バグがありそうに見えるが再現ケースがなく、問題のコードがソースに広く散らばっている場合、試みた「修正」がリグレッション(デグレ)を招きそうに思えた。
Microsoft はエンジニアを信頼しており、PREfast の指摘を調査した人が修正済み(あるいはバグではない)と認めればバグはクローズされた。誤検知と判断したバグについては、PREfast が再度同じ指摘をしないよう印を付ける仕組みがあり、記憶が正しければその印付けにはコードレビューのように複数人のサインオフが必要だった。
こうしたバグの分類、修正、修正確認、そしてテストカバレッジをどう改善するかを考える経験は、私の開発アプローチに大きな影響を与えた。特に後ろの二つのカテゴリは、1) 静的コード解析ツールに誤検知を挙げさせないコードの書き方、そして 2) よりローカルにバグ修正を行えるようなコードの書き方――例えば呼び出し元でリソース確保の失敗を処理し、統一されたコードパスからエラーを伝搬させる――を考える動機づけとなった。
コンピュータが普及するにつれ、安全性が求められる用途にも使われるようになった。そうしたコンピュータ上で動くソフトウェアではリスクが高く、より慎重な設計と構築が求められる。医療機器、航空機、兵器システム、自動車向けのソフトウェアを、コンピュータゲームやECサイトのソフトウェアと同じようには作れない。NASA は古くから、開発スピードより堅牢性を優先するコーディング標準や開発手法を守ってきた。悪名高い Therac-25 放射線治療装置1 のような著名な失敗は、社内で交渉された勧告的なコーディング標準よりも形式的で拘束力の強い標準の策定を促した。
1990年代後半、自動車業界は、製品のあらゆる箇所でコンピュータが活用され続けることを見越し、Motor Industry Software Reliability Association (MISRA) を設立してコーディング標準を整備した。現在第3版となるMISRAは、Joint Strike Fighter (JSF) C++ コーディング標準2 など他の分野にも取り入れられている。さらに、Electronic Control Unit (ECU) の標準化に向けて AUTOSAR (AUTomotive Open System ARchitecture) が策定され、国際標準化機構 (ISO) は道路車両の機能安全規格 ISO 26262 におけるセクション6「ソフトウェアレベルの製品開発」として組み込んだ。
MISRA が存在するだけでは、あるいは遵守を謳うだけでは、従業員がベストプラクティスを守らない限り企業を守れない。約15年前、安全性の標準をリードしていた自動車業界がなぜそうしていたのかを示すかのように、トヨタ自動車は UA(意図せぬ急加速)事案で調査を受けた。2010年5月時点で89人が死亡したと推定されている。関連の集団訴訟は2012年12月に16億ドルで和解し、2014年にはトヨタは安全欠陥を隠したとしてさらに12億ドルの罰金を科された。専門家証人 Michael Barr は20カ月以上トヨタのソースコードをレビューし、その品質について証言した。内部文書で「スパゲッティコード」と評されていたことまで引用し、Barr と評価を請け負ったNASAのチームはいずれもコードを MISRA に照らしてチェックし、数千件の違反を見つけた。興味があれば、この記事に長い要約と、専門家 Koopman と Barr の数百ページに及ぶ証言へのリンクがある。
「『静的解析やコード検証ツール』は、熟練エンジニアの判断を代替するのではなく補完することを意図している。」
なぜ Axivion のようなツールへの需要があるのか、ここまでで明らかだろう。Axivion はソースコードを解析し、各種安全基準の違反の可能性を章節付きで指摘する。これらは熟練エンジニアの判断を代替するのではなく補完することを意図している。PREfast の指摘に対処する開発者を信頼した Microsoft のリーダーたちと同様に、これらのコーディング標準の策定者は、説教するより現実的である方が好ましいと認識していた。もし私が安全性が求められるシステムを開発する企業のエンジニアリングディレクターなら、Axivion を CI/CD ワークフローに慎重に組み込むことを検討するだろう。
そして私の知る限り、Axivion は C/C++ と C# に加えて CUDA C++ コードに対してもこの機能を提供する初めてにして唯一のツールだ3。つい最近、NVIDIA は CUDA C++ Guidelines for Robust and Safety Critical Programming を公開し、Qt Group はその文書のガイダンスを自社ツールに取り込んだ。CUDA がロボティクス、自動運転車、その他安全性が求められる領域で使われ続ける中、こうしたサポート拡張が求められている。
As a first exercise, the Qt folks ran the source code for The CUDA Handbook through their tool, and sent a report summarizing its findings. The CUDA Handbook isn’t intended for safety-critical applications, per se, but it’s an open source code base we can usefully examine to get a sense of the error reporting and how a developer would triage and address the issues raised by the tool.
最初の取り組みとして、Qt のメンバーは「The CUDA Handbook」のソースコードをツールにかけ、検出結果をまとめたレポートを送ってくれた。「The CUDA Handbook」は安全性を求める用途向けのものではないが、エラーレポートの様子や、開発者がツールの指摘をどのように分類して対処するかを把握するうえで役立つオープンソースのコードベースだ。
次回の記事では、Axivion を実際に試し、その検出結果を見ていく。
1) 皮肉なことに、リンク先の論文「An Investigation of the Therac-25 Accidents」の冒頭は「コンピュータはますます安全性が求められるシステムに導入され、それに伴い事故に関与するようになっている」で始まる。この論文が発表されたのは1993年7月だ。
2) 1987年から1997年にかけて、米国防総省は、1970年代に乱立していたプログラミング言語を標準化する目的で国防総省自身が開発したオブジェクト指向言語 Ada で全ソフトウェアを記述するよう有名な要件を課していた。Lockheed Martin は、Joint Strike Fighter の開発中に C++ を認めるよう国防総省を再考させる役割を果たしたと言われている。
3) 少なくとも現時点では、CUDA Python をサポートする静的コード解析ツールは存在しない。