Syoyo Fujita's Blog

raytracing monte carlo

Month: September, 2007

The pitfalls of verifying floating-point computations

The pitfalls of verifying floating-point computations
David Monniaux
http://hal.archives-ouvertes.fr/hal-00128124

[En]

This is a good article about floating point computation, especially problematic behaviour of x87.
(double-rounding, extended exponent bits, etc…)

Although x87’s extended precision(80bits) is a part of IEEE 754 standard,
this article tells us that we must not use x87 and must use SSE2 as a FPU.

Now days, there are alot of SSE2 capable x86 CPUs(Pentium4 or later) and
gcc uses SSE2 as a FPU on x86_64 environment by default.
Thus we are going to have no scruples about using SSE2 as FPU.

[Ja]

CRlibm [1] のマニュアルのすごさ(誤差を抑える計算のテクニック)に影響されて、
浮動小数点計算をいろいろと調べています。

いくつか調べた中でも、The pitfalls of verifying floating-point computations は例題がいろいろと
取り上げられてまとまっていて役に立ちます(とくに x87 のひどさについて)。

とりあえずの結論:
クロスプラットフォームを考えて、IEEE 754 準拠の他 CPU との浮動小数点計算と
結果を合わせるためにも、SSE2 を使い、x87 は使わないようにしましょう.

[1] http://lipforge.ens-lyon.fr/www/crlibm/index.html
CRlibm, an efficient and proven correctly-rounded mathematical library

Advertisements

Enhanced Motion Blur Calculation with Optical Flow

optical_flow_mb.png
Image from Enhanced Motion Blur Calculation with Optical Flow. [Zheng et al. 2006]

Zheng, Yuanfang ; Köstler, Harald ; Thürey, Nils ; Rüde, Ulrich:
Enhanced Motion Blur Calculation with Optical Flow .
In: Aka GmbH (Hrsg.) : RWTH Aachen (Veranst.) : Proceedings of Vision, Modeling and Visualization 2006 (Vision, Modeling and Visualization Aachen 22. – 24. Nov 2006). Aachen : IOS Press, 2006, S. 253–260. – ISBN Erscheinungsjahr.

http://univis.uni-erlangen.de/formbot/…

[En]

Good motion blur paper from vision researchers.
This paper proposes image based motion blur techniques using optical flow vector field + ray tracer vector field.

The resulting image looks quite nice in overall, but still there seems some artifacts remain
(e.g. see blender monkey’s shadow on right side in fig 9(c)).

Anyway, efficient motion blur computation in ray tracing context is still unresolved research area
and there has been few papers about it ever.
Thus, this optical flow based motion blur paper is much valuable.

[Ja]

書くかもしれない.

Why I’m eager for realtime raytracing and MC based GI.

[En]

In short, it’s simple.
Because I ensures that commoditized realtime raytracing(in short term, within ~ 5 years) and
commoditized Monte Carlo raytracing based Global Illumination(in long term, within ~ 20 years. After realtime rayracing era)
are the most realizable destruptive innovation for realtime/offline graphics.

I forecasts rasterizer based commodity HW graphics technology(such like current GPU)
will hit peak within a couple of years without any (rasterizer based) innovation was found.

Rasterizer based graphics scales with O(N), but I don’t think semiconductor technology
can not catch with it anymore.

On the other hand, raytracing based graphics scales with O(logN) thanks to efficient spatial data structure.
Algouth, raytracing based graphics suffers from heavy random acceessness for
traversing the scene data structure, but recent RTRT(RealTime RayTracing) techniques shows
that it could be overcomed(e.g. see Reshetov’s Vertex Culling paper).

[Ja]

今日は、なぜ私がリアルタイムレイトレとモンテカルロベースの GI(大域照明) に
こだわっているのかについてお話したいと思います。
(ここ 1,2 年はそんな思いを持って lucille(+angelina) を開発してきていました)

ここから数年くらい先は、lucille をリアルタイムレイトレで高速化しつつ、モンテカルロ GI で
数学的な美しさを保ってきれいな CG 画像をレンダリングすることを目指しています。
lucille ではカネをとることはまったく考えていませんが( 196 年後の完成後はどうしようかな )、
コア技術としてのリアルタイムレイトレと GI の
技術と知見はそれなりに転売することは可能だと思っています。

正直なところ、今はやっとリアルタイムレイトレがコモディティ化(e.g. HW でリアルタイム化)されそうか?という
状況であり、リアルタイムレイトレはすぐにはビジネスとしては成り立たないでしょう。
GI はレイトレよりさらにハードルが高いので、さらにまだまだコモディティ化は難しいです。

ではなぜ RTRT(リアルタイムレイトレ)をやるか、というと、

– 今のうちに RTRT で有名になっておいて 10 年後に権威になるため
(さらにその次の波となるであろう GI で有名になっておいて 20 年後に権威になるため)

– ラスタライザベースドグラフィックスはもはや頭打ち感がある。
N や A や I がグラフィックス方面で生き残るには、
今最も可能性がある distruptive innovation であるレイトレにシフトするしかないだろう。
そこで先手をうって RTRT をやっておく。
(I は最近リアルタイムレイトレに結構投資しているみたいですが、これは正しい判断だと思います。
ただ、大企業が distruptive innovation に投資しても失敗することが多いんですよね…)

– ついでにいうと最近の話題ですが、メリケンがついに FF rate を 0.5% 下げました。
ついに米国経済 recession 突入が確実なものになってきました。
N や A や I などの米系企業はこれからもっと経営が難しくなるでしょう。
明日の利益になるネタにもっとリスクを賭けて貪欲になっていかなざるを得なくなると踏んでいます。
その中でもっとも可能性があるものの一つが、RTRT なのです。

# と経営が厳しくなるかなと思ったけど、
# メリケン衰退&ドル安 -> BRICs 発展で、BRICs マーケット拡大でうはうはの期待がありました。
# 今や I の売り上げの 50% はアジアです(日本除く. 日本は 11%)

– さらにいうと、Prof. Hanazawa の提唱する、真の仮想世界である unreal ワールド構想を再現できるのは、
RTRT と GI しかありません(本当は AI と五感デバイスも必要ですが…)。
日本人として、2015 年までに unreal ワールド構想を再現しないことには、
死んでも死にきれません。
なので 2015 までに頑張って RTRT を発展させたい。

そんな訳でそのような状況を見越して、私のような個人が出来ることと言えば、
今のうちに先攻して特許とか論文とか書いたりデモ作ったり名前をうっておいて、
N や A や I などの会社にライセンスしてうはうはになったり、権威になることである。

この先数年はリアルタイムレイトレがついにコモディティ化されるかも知れない、
というとても面白い時期にあるかと思います。このような大きなチャンスは 10 年に一度到来するかしないか
だと思います。
そして、ラスタライザベースドグラフィックスに振り回されてきたひとびとが、
一転、レイトレベースドグラフィックスで支配する側に回れるようになるかもしれないというチャンスでもあります。 

2010 年が、RTRT のためのプロセッサパワー、レイトレ技術進歩、GPU の衰退(?)で、
RTRT がグラフィックスのキー技術になれるかもしれないかが判断できるよい区切りの時期になると思います。
このあと 3 年以内までに、RTRT とかレイトレ言語とかで、
いんご、ゔぁちゃー、じゃっこ、れしぇとふとかと並んでイニシアティブを取っておきたいところ。

そして RTRT の次の10 年後はこのリアルタイムレイトレのコモディティ化を踏み台とした、
リアルタイム GI になると予想します。

おまけ

あ、ちなみに私が GI というときは、モンテカルロレイトレベースの GI です。
radiosity も GI 手法の一つですが、radiosity was dead ですので、radiosity に投資する価値はないです。

Cell

http://www.cell.com/content/issue?volume=130&issue=5

おぉ、ブラボー!!!
こんなことがあっていいのか!?

僕も SIGGRAPH に論文を通して、表紙を書いてもらう!

Gappa : automatic proof generation of arithmetic properties

http://lipforge.ens-lyon.fr/www/gappa/

[En]

Gappa is a cool program which validates your floating-point code.

Here is an example of gappa code(Cauculates x * (1-x) in [0, 1]. Taken from gappa’s site).


{ x in [0,1] -> float(x * float(1 - x)) in ? }

Then, gappa automatically computes it’s error bound,


$ echo "{ x in [0,1] -> float(x * float(1 - x)) in ? }" | src/gappa

[rounding_float,ne,24,149](x * [rounding_float,ne,24,149](1 - x)) in [0 {-0}, 1 {1}]

It’s quite nice!

Gappa code format is almost similar to C expression, thus it would be easy to
translate your floating point C code to gappa code.

Gappa is successfully used for CRlibm [1] and CGAL.

[Ja]

Gappa は浮動小数点計算の error bound を自動で計算してくれちゃうらしい。これもすげー。
CRlibm[1] や CGAL の浮動小数点計算の妥当性の検証に gappa が使われているとのこと。
CGAL はグラフィックスのひとなら聞いたことはあるかと思います。有名な幾何計算ライブラリですね。

Gappa はあくまで存在するコードに対して誤差を測定するようなので、
たとえば誤差ターゲットと定義域を指定して最適な sin の多項式近似コードを自動で見つける、
というところまではできないらしい。
CRlibm では多項式近似コードは maple で生成したとのこと。
# Intel’s libm のスライドに CRlibm ってのがあって、これってなんだろうって思っていたのですが、
# Correctly-Rounded libm のことだったのですね。

gappa, caduceus でロバストな floating point 計算コードと C プログラムを書くことができそうです。
あとは GI レンダリングの場合は数値積分やモンテカルロ法などもあるので、
それらも自動で検証できるようなツールもないか探してみたいと思います.
(PVS とかは積分も検証できるみたいですが、GI の場合は discontinuity やら singularity の問題があるので、
まじめに(連続)積分で考えない方がいいと思うので)

[1] CRlibm, an efficient and proven correctly-rounded mathematical library
http://lipforge.ens-lyon.fr/www/crlibm/

Caduceus : a verification tool for C programs

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