- 2011-01-27 (Thu) 10:24
- 一般
とりあえず，会場がダメすぎて困る．椅子しかない，ものすごく密集している，質問にマイクの位置まで出るのすら大変，そもそも人が邪魔でスクリーンの下半分が完全に見えない．ACMの会議の発表はあとでオンラインでビデオが見れるので，この会場だったらビデオで見るだけでも十分，というかビデオのほうがスクリーンをちゃんと見れる分より良いのではなかろうか？
んで，招待公演は certified compiler の話で… 確かに飛行機のプログラムにもコンパイラが関与していると思うと certified compiler がないと怖すぎて飛行機乗れないなぁと．とはいえ，飛行機の制御とかは floating point 使っているわけで，そいつの検証とか大変だよねと．常識的に考えて合っているだろう前提条件が floating point だと正しくないことが多々ある（結合性とか，同値判定とか）のでなんとも．いっそのこと制御機を綺麗な構造の体の上に構築すればいいんじゃねとか思ったりするのだけど，そういったものは理論的にもあるのだろうか？ それはさておき，肝心の検証器自体の検証をどうやるのかとか考え出すと非常に悩ましい気になるのだけど，そこらへんどうなっているのやら．何を信じていいのかわからない気もしなくはない．verified mix とかあれば verified compiler は verified interpreter から作れるんじゃね？
そしてテクニカルセッションは今年から2並列なので… とりあえず Semi-Automated Verification へ．んで，concurrent C の certified compiler という CompCertTSO (TSO = Total Store Ordering) の話が最初．細かいことはわからんが，そもそも certified compiler は逐次でさえ面倒なので，concurrent 用の証明を簡単にするために言語のセマンティクスとメモリのセマンティクスを分けたとかなんとか．確かに，Sequentially Consistent でないことが起こる（最初 0 で初期化された x と y に対し，２つのスレッドが それぞれ mov x 1 と mov y 2 をし，そして其々が mov ax y と mox bx x とやると，ax も bx も 0 ってことがしばしばある．バッファのせいで．）って時点でどんだけ面倒なんだよと．計算機のセマンティクスは x86-TSO という去年あたりに発表されたもの．次いで，c++0xのconcurrentの検証で，実際いくつかの問題を見つけたりしたそうな．これも x86-TSO のセマンティクスを使っている．そしてC/C++言語の検証セッションの最後は，C++のオブジェクトレイアウトの検証．多重継承時のオブジェクトレイアウトのアルゴリズムとかのをちゃんと検証したと．確かにこれも面倒な話だね… なんとなく実用的な言語の検証は力技で押し切れる体力がないと駄目だなぁという印象．
以下略．
- Newer: ことはじめ