形式手法が使われる意外な分野

ゲームプログラミング界の巨人、Tim Sweeneyが「未来のゲーム開発テクノロジー」を語る on CEDEC 2008
これからはレイトレーシングをするようになるそうな。

その計算力で実現可能になるリアルタイムのレンダリング処理は、これまでのポリゴンベースのラスタライザの考えとは大きく異なったものになる。ひとつの可能性はレイトレーシング。各ピクセルに対して、ゲームシーン内の光の動きをトレースする方法である。物理学的に正しいライティングが得られるものの膨大な計算量が必要であり、これまではリアルタイム処理が難しかった手法だ。

レイトレーシングっていえば、確か昔持っていたFM-77AVでOh!FMにのっていたプログラムを入力して、円柱とか球とかのレイトレーシングを10分以上かかって書くっていうのをやっていた気がする。

で、この人によると、ゲームでのマルチスレッドプログラミングにおける生産性に関して言えば、「指数的に予算が増やせない以上、ハードウェアがいくら指数的に高性能化してもゲームの生産量には限界がある」ということがあるとのこと。なるほど。これを解決するには、「性能を犠牲にしてでもマルチスレッドプログラミングの生産性をあげていく」手段を提供していかなければならないということだそうな。そのひとつがC++のような手続き型プログラミングではなく、スレッドセーフを保証している純粋関数型プログラム言語によるゲームプログラムという手法であるということだそうな。Haskelなんかを例に挙げている。

　しかし、現状でさえマルチスレッドプログラミングは開発の困難さが指摘されている分野である。同時並列的に動作するプログラムがモデルデータやゲーム内状態などの共有情報にアクセスしようとするとき、そこには必ずデータ競合によるバグの発生や、デッドロックによるプログラムの停止というリスクがつきものである。しかも、それを効率的にデバッグすることは非常に難しく、開発規模の拡大や期間の長大化を招いているのだ。
　Sweeney氏は、これは現在主流の開発言語であるC++の手続き型言語としての特性に由来すると指摘する。マルチスレッドにおける問題を避けるためのテクニックは各種あるが、Sweeney氏に言わせるとそれは「シングルスレッドのプログラムをアセンブラで書くようなもの」であり、生産性が悪いのである。
Sweeney氏が注目する純粋関数型言語は、並列処理を安全に実行でき、メニーコア時代の生産性に寄与するという 　ややプログラマ向けの説明となってしまうが、ここでの議論を簡単にご紹介しよう。Sweeney氏は、この問題を解決するためには、ゲーム開発言語として純粋関数型の言語が必要になるだろうと言う。純粋関数型言語とは、プログラム中の関数が、戻り値のみによって作用する構造の処理系だ。
　この種の処理系では、C++のような共有メモリのアクセスや、I/O操作は基本的に行なえない。その引き替えとして、各関数のアトミック性が構造的に保証されており、安全に並列実行できるのだ。しかも、コンパイラが対応さえすれば、関数を自動的に多数のコアに分散処理させることができるというスケーラブルな実行バイナリを作り出せる。
　Sweeney氏は純粋関数型言語のもつ並列処理安全性に着目しており、将来的にゲームプログラミングはそういった処理系に移行していくべきだとした。Sweeney氏はそのひな形として言語“Haskel”を挙げているが、ゲーム開発のメインストリームたり得る言語はまだ登場しておらず、将来に期待しているという。

この記事を見ていると、形式手法って実はゲームプログラミングで使えるのではと漠然と思った。ゲームの世界の安全性を保証する手段としてね。