No Such Blog or Diary

とりあえず，会場がダメすぎて困る．椅子しかない，ものすごく密集している，質問にマイクの位置まで出るのすら大変，そもそも人が邪魔でスクリーンの下半分が完全に見えない．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++のオブジェクトレイアウトの検証．多重継承時のオブジェクトレイアウトのアルゴリズムとかのをちゃんと検証したと．確かにこれも面倒な話だね…　なんとなく実用的な言語の検証は力技で押し切れる体力がないと駄目だなぁという印象．

以下略．

ホテルに Wi-Fi があるかなと探してみたら（PCは有線接続できるがiPodは無線が必要なので），COA_MESH とかいう SSID のネットワークが無料で使えることを見つけた．調べてみると City of Austin - The City of Austin is deploying a Wireless Mesh Wi-Fi Network とかいうことで，オースティン市が提供しているらしい．

行政が屋外でも使えるワイヤレスネットワークを提供してくれるってのはいろいろと便利でいいなぁと．一応，最初にネットワークにつなげると「ブラウジングとメール以外に使わないでね」とかあるけれど，これらを使わせてもらえるだけでありがたい．市民税とかで強制的に使用料を取られると思うと微妙だけれど．

でもまあ，まだまだメッシュが限定的なので欲しいところで繋がらないという罠が待っていたりする．ちょうど泊まっているホテルはメッシュ内なので接続可能だが，会議の開かれているホテルはメッシュ外なので繋がらなかった．外を歩きながら google map 使おうと思ったら繋がらなかったとかも．

風邪引くのも嫌なのでスーパーマーケットで新鮮な食糧をゲット．ホテルから歩いて15分の Whole Foods Market というお店．なにやら Austin 発祥の巨大なチェーンでかつ有機栽培に拘った有名なお店らしい．日本語のウィキペディアにも載ってるっぽいし．

んで，総菜コーナーでサラダやらなんやらを好きなように容器に詰めてお持ち帰り．野菜のあまりないホテルの食事とかもう嫌だ．お値段も$7.99/1lbなので換算して100g145円程度とオリジン弁当よか安いし．惣菜以外にも色々とものすごく何でもあるので不健康な食事もいくらでも可能．普通に鳥の丸焼きが紙袋入りでドカドカおかれていたのはアメリカっぽいというかなんというか．

Bostonに行ったときには Trader Joe's にお世話になったけど，近くに大きなスーパーがあるって便利だなぁ．というか，海外行ったら現地のスーパーで現地の食糧を調達して食べるってのが半ばパターン化している気がする．お金の節約＆体へのダメージ減少というメリットは捨てがたい．今回の Whole Foods Market は若干お値段高めっぽいのでなんともだけど．

そういや Whole Foods Market の（エコ）バッグとか土産になるのかね？　Google の suggestions に出てくるし楽天で800円とかで売ってるし．

今日は主にツールと並列と．

最初の Particle systems 記述用のライブラリ in SML3d を作ったぜという話は…　使えそうだけど実際問題としてどの程度実用なのかよくわからず．とりあえず particle-particle interaction はまだできないらしい．世の中でパーティクル間の相互作用ってどれくらい必要になっているのか知らんけど，それを GPU でどうやってうまくやるんだろうとかいう興味はある．それはさておき，3Dグラフィックスには宣言的なアプローチが必要だというのは大いに納得．命令的に3Dやるのは面倒すぎて過去何度やる気が無くなったことか．まあ，パフォーマンスが気になるところではあるけれど．次の Xpath クエリを functional logic な言語 TOY に実装したぜ(XPath = non-deterministic higher-order expression で)の話は…　forward-axes の実装は普通なのでさておき，reverse-axes の filter への変換が高階マッチングでダイナミックにできてしまうという点に感動した．ついでに XPath のデバッグに現在の XPath にマッチするインスタンスを生成させりゃいいとかいう考え方も論理型言語ならではだなぁと感心．Curry でも勉強しようかね．そんで3つ目の話は strictness を排除してメモリ効率を上げましょうという話で…　strict にして効率を上げようという普通の考え方と逆を行く結果で興味深い．不必要に評価しなければメモリを無駄に消費しないで済むよねと言われれば確かにその通りな気もするけれど，最適な strict 具合を見極めるのも大変そうだなぁ．

で，午後１は並列．とりあえず F♯ に async 入れたよ（というか，既存言語に容易に機能追加する方法論？）という話で…　英語が速すぎて…　実際のところ数年前にテクレポか何かで出ていた話をちゃんと学会で話しましたよという宣伝でしかなかったような．んで，その次は HPC のために通信を明示的に書きましょう，でも宣言的に，という話．ぶっちゃけ何処が宣言的なのかとかいう疑問というかただのマクロの展開じゃんというツッコミが Launchbury から飛んでいたのだけど…　代数規則とかは無いんかいという．ぶっちゃけ使い物になるのかどうかわからない．そして3つ目でまたF＃に戻って，こんどは reactive programming 用の拡張を入れたよと．まあ自然．Manticore の pcase と同じ．

どうでもいいけど並列系の人間はしゃべる時間も勿体ないくらいにせっかちなのかね？　3件中2件が喋るの速かった．特に2件目とか無駄に時間が余ってたんだけど…

以下略．

朝一でレジストレーションしてPADL'11で話を聞く．

初っ端の招待公演は Core i7 の formal verification の話．どうやら Pentium Pro のころから FV をやっていたらしい．仕様とか検証器とかをlazyなMLで書いてるとかいう話で，まあ手続型言語で仕様書くとか検証に関する無駄な計算を省かせるとかはしたくないから遅延評価な関数型言語でやるのは筋が良いねという．質問でロジック言語でいいんじゃねーのとか出てたけど，そこらへんは歴史的事情と現場的事情があるのでしょう．

次いで，メッセージパッシングとかネットワークの話．Erlang で，お前にはメッセージが絶対来ないよとか，お前のメッセージは絶対に受け取ってもらえないよとか，そういうメッセージのやり取りの不備を静的に解析する話．大半の発表スライドが「スライド一枚に説明したいことを連想する画像一枚」とかいう構成だったのが印象的．しゃべっていた内容は納得．パイ計算などとの関連や，セッションタイプとかとの関係があるのかないのか良くわからなかった．その次はチャネルを使ったプロセス通信なプログラムを簡単に書くコンビネータライブラリの話で，type class 使いまくると綺麗に書けるとという話．とりあえず type class を使ったプログラムは細かいことを考えなければ読みやすいのだけど，細かいことを考え出すと「この部分式の型はこれだからこのインスタンスの関数が実行されて…」とか追わなければならないので理解が大変な気がしなくもない．最後のはProbLog (Probabilistic extension of Prolog) でモバイルアドホックネットワークのプロトコルの解析を解析的にやるとか．新に解析的なのかどうかはさておき，ProbLogはプログラムに対して何かの確率をうまく計算してくれるらしい．シミュレーションとは違うのだよシミュレーションとは，と言っていたけれど，ProbLogでやってることって確率モデル（プログラム）のシミュレーションなんじゃないかなぁとか思ってみたり．まあ，よくわからん．

以下略．

オースティン到着．空港から街中までのバスが1ドルとか素晴らしすぎる．街中のバス全部が1回乗車1ドルで，一日パスでも2ドルとか．東京のバスも半額になってほしいなぁ．

さて，今日はもうレジストレーションに行ってもしょうがないので明日の朝に行くことにする．さっさと寝ないと風邪ひきそう．