Caduceus : a verification tool for C programs

by syoyo

http://why.lri.fr/caduceus/index.en.html

[En]

TODO…

[Ja]

Haskell
-> QuickCheck 自動テストツール
-> Coq 証明支援ツール
-> Why 検証ツール
-> Caduceus C プログラム用検証ツール(Why を使う)

という感じの流れで見つけたツール。

Caduceus は C 言語用の検証ツールで、たとえば [1] にあるように、
まず以下のようにソースコードにアノテーションで検証のロジックを書きます。


/*@ requires y/2 <= x <= 2*y
  @ ensures
  @   \result == x-y
  @*/

float Sterbenz(float x, float y) {
  return x-y;
}

すると、Caduceus は、この Sterbenz 関数の実装は、
y/2 <= x <= 2 * y な条件を満たすなら(requires)、
結果は x-y と誤差無く一致する(ensures)、
であるとして、それを検証するコードを自動で生成して
テストしてくれるらしい。

まだ使えていないがなんかすごそうだ。

多くのレンダラ野郎どもは、自身のレンダリングアルゴリズムのコードが正しいかどうかを、
そのほとんどは Visual Debug などで行っているのが現状ではないかと思います。
たとえば、

– diagnostic ビューアを作る[法線の色を RGB にマップするとか]
– こいつは間違いない、という画像を作って画像比較
– 目視テスト ^^)
– などなど…

visual debug だと、もし不具合が合ったときに、
検証したり原因を見つけたりするために割く時間というのが、
とても非生産的な時間ではないかと思います
(おかしいことは分かったが、どうおかしいか調べるためにさらに
条件や diagnostic や printf に出す情報を変えてリコンパイルして実行など)。

また、アルゴリズムそれぞれに対して、検証のためにおのおのビューワを作ったりというのも
効率が悪いと思います
(半球上に一様に点を生成するコードが、本当に一様に分布するのか確認するためにビューワを作るなど)。

すくなくとも私の場合はこのような経験が多かったので、
この非生産的で効率の悪い作業をどうにかして解決できないかと
ずーっと考えていたものです。
(そんで、kd-tree が個人的に嫌いなのは、kd-tree というアルゴリズムの
検証しづらさ、デバッグしづらさが原因でした)

最近出てきた、GLSLdevil [2] とか SQL デバッグ [3] のような考え方は、
リアルタイム系には十分 fit するのではないかと思いますが、
アルゴリズムが中心になるオフライン GI 系ではまだまだ物足りない。

Caduceus に限らず、それらを構成する Why, Coq(同類のものに PVS も)、
これらツールが出来る(出来そうな)ことはちらりと見る限りすばらしいもので
(まだ私の頭が追いついていないので使えてはいませんが)、
まさに私がレンダラを書く上でのアルゴリズムの検証•デバッグをどうやるか•どうやればいいか悩んでいたことを、
十分に解決してくれそうです。

たとえば MLT のアルゴリズムを書てちょろちょろっと検証ロジックを書いたら、
コンピュータがいやいやこの perturbation の計算はおかしいよ、って知らせてくれて、
ああわかった、こうだな、かくかくしかじか、、、
でバグフリーで検証済みな MLT コードがポンと gerenate される、みたいな感じができそう。
(出来たコードのパフォーマンスは別な問題ですけどね)

つまりアルゴリズムレベルで物事を考えることに集中できるような仕組みが、これら Caduceus などの
ツールで実現できるのでは?と思っているわけです。
(アルゴリズムが正しいかを確認するために毎度毎度ビューワコードを書いたり printf とかして
ちくちく確認とかやるような開発サイクルはもうやめるべきなのです)

そんなわけで、Haskell に手を出しつつ、これら検証ツール、証明ツールにも手を出してみることにします。

[1] Formal Verification of Floating-Point Programs
http://why.lri.fr/caduceus/

[2] OpenGL GLSL Debugger
http://www.vis.uni-stuttgart.de/glsldevil/

[3] A Relational Debugging Engine for the Graphics Pipeline
http://duca.acm.jhu.edu/research.php

Advertisements