POPL 2008メモ2日目

プログラム http://www.cs.ucsd.edu/popl/08/program.html

POPL 2009のcall for papersがおいてあった（昨日からあったらしいが）。Benjamin (Pierce)がprogram chair。日本からは京大の五十嵐さんと長谷川さんがプログラム委員に（五十嵐さんは二回目。御苦労様です…）。Guy Steeleもいる。今年は（イギリスにいる吉田さん以外に）自分と細谷さんがいたので、二年連続で日本から二人ということに。POPL pearlは継続するらしいが「pearlと明示しなくて良いし、カテゴリも分けない。同様に査読する」(!)らしい。

無線LANがほとんどつながらない。300人もいたら当たり前？（50接続ぐらいが上限とのこと。1000ユーザぐらい同時に接続できるステーションはないのだろうか。あっても高いのか、電波的に不可能？　インターネット接続はないほうが良い:-)というような話も掲示してあるが）

招待講演その2

恥ずかしながらソフトウェアモデル検査はよく知らないので、他の話よりさらに適当です…

抽象解釈によるプログラム解析での"relevance heuristics"の話。一般的問題：解析コストと精度のトレードオフ。整数変数の区間解析や線形等式発見の例。フローの合流が問題。x == yとx == zが合流すると「わからない」か「x == y ∨ x == z」になるが、後者は抽象状態も抽象領域（の高さ）も指数爆発する。

そこで"relevant"な場合分けだけ正確に行う。健全な近似で証明に失敗したところだけ細かくして調べる。Generalization principle: special caseの証明で使われたfactは、証明全体でもrelevantな場合が多い。

SATの例(DPLL)："conflict-based learning"。とりあえず適当に命題変数の一つに真偽を割り当てる。そこから決まる命題変数（の値）は決める。決まらない命題変数の値は、また適当に割り当てる。その「決まる」という依存関係を記憶。偽になったらresolutionをして、どこがまずかった（relevantだった）か学ぶ。例えばbにtrue、cにfalseを割り当てて、(b∨¬c∨d)∧(¬c∨¬d)が偽になったら、b∨¬cをlearning（dはrelevantでない）。

プログラム解析での例：

x = y = 0;
while(...){x++;y++}
while(x!=0){x--;y--}
assert(y==0);

とりあえずちょっとループ展開して、否定を証明しようとしてみる

x = y = 0;
x++;y++;
x++;y++;
assert(x!=0);
x--;y--;
assert(x!=0);
x--;y--;
assert(x==0);
assert(y!=0); // 否定

Interpolation lemmaとpredicate abstractionで証明を生成し、出現する命題からrelevantな命題（の候補）を抽出

POPL 2004の結果：Windows DDK（デバイスドライバ開発キット）のデータ。プリプロセス後12k LOCから138k LOCで4分から77分まで。Relevance heuristicsがないと138k LOCとかは終わらない。

拡張：∀とかのついた命題も生成／証明？（残り20分、その手法の説明だったが、ほとんどわからなかった…）

Conclusionを聞いた限り、（大まかには）上述の理解で良い？

    • [Q] この手法はsyntacticかsemanticか? [A] 「質問のポイントがよくわからない」:-)

セッション5

プログラム解析のセッション。知識不足でよくわかりません。;_;

  • 無限ループバグ（がないこと）の検証。"Failed termination proof ≠ non-termination"。False positiveを検証するため、「止まらないことの証明」を考える。ループしそうな部分(lasso)が本当にループする条件（≒recurrent set）をSAT solverにつっこむ。
  • SubcubicなCFL reachability判定アルゴリズム。関数間フローグラフで関数呼び出し／リターンを(_iとか)_iとかで表す。再帰があるとCFL reachability問題になる。既存アルゴリズムはO(n^3)だが、既存アルゴリズム＋簡単な改良でO(n^3/log n)になる。まずルールの右辺を2記号に。ワークリスト方式で導出可能なfactを列挙していく。ルールをn個とすると、ループ回数（＝factの最大個数）はO(n^2)。ループ内部が従来はO(n)だったが、表を作って、[Rytter 85, 83]みたく集合演算に（アルゴリズムではよくある）"word tricks"を使えばO(n/log n)になる。
  • プログラム解析のためのSMT (satisfiability-modulo-theory) solverの話。リンクリストとかヒープ上のデータ構造があると、∀とか出てきて既存のSMT solverではうまく扱えないので、ヒープを考えて"Btwn_f(t1, t2)"などで論理を拡張した。Btwn_f(t1, t2)は{ x | t1 --f--> x --f--> t2 }の意味。

セッション6

プログラム解析の続き。

  • Javaで、初期化以降は一定になる"stationary"フィールド（finalの拡張）を検出するプログラム解析。アクセスが「書き込みのみ→読み込みのみ」の形。44-59%が該当。finalは11-17%。Whole-program analysisになるが、「初期化」はわりと「生成」直後（ownershipをloseする以前）に来るので、比較的容易に検出できる。SourceForgeからとってきた現実のプログラムで実験。
    • [Q] finalに「すればできる」のはどれぐらい？ [A] かなりある（グラフあり、30%前後）
    • [Q] finalだけどstationaryでない例？ [A] コンストラクタ内でowernshipを失うとき
  • エイリアス解析の話。Points-to setの計算が不要。Demand-driven, whole-program, flow-insensitive analysis。軽い＆わりと正確(95% precision, 0.5 ms, 65 KB)。xとか&yとか*pとかの式の間のグラフを考える。Assignment edgeとdereference edgeを描く。alias(p, q)?とかsame(*s, *t)?などのqueryを考える。CFLで表現して、CFL rechabilityに還元。速いので「IDEでクリックしたらmayエイリアスを表示」などに使える。Crystal projectの一部。
    • [Q] mallocと関数ポインタは？ [A] mallocは呼び出しごとに新しいメモリ。関数ポインタは保守的に近似。
  • C言語プログラムの移植性バグを検出するための形式的モデル（意味論）とツール。lintとか-Wpaddedとか-Wcast-alignとかより完全。"Layout portability constraint" Sをeffectのように考える。「Γ |- e : τ ; SかつΠ |- SならばΠ |- e → e'」が成立。キャストはメモリレイアウトが物理的部分型になっているかどうかで安全性を判定。実装ではfalse positiveを減らすためにmay-alias解析を行い、さらに"host"と"target"の2プラットフォームで食い違いがあるときのみ警告。実在のコード（Spreadメッセージングライブラリ）で、既知のバグだけでなく、未知のバグも発見。structの要素のintとsize_tの食い違いなど。

セッション7

仕事がたまっていたのでパスしてメール処理

セッション8

  • PrefixとchoiceしかないCCS（ともいえないが）でweb serviceの仕様(contract)を記述。Subtyping (subcontract relation)を成り立たせるための制限"filters"を定義。
    • [Q (というかコメント) by 自分] Igarashi & Kobayasi, POPL 2001等を読め（意訳） [A] Thanks
    • 実はホテルが一緒で、出発直前の朝食で出くわした（やはりGoogle Mapで安ホテルを探したらしい）。「我々は言語を特定していないのでcompletely different」と言い残して去っていった。日本語勉強中らしいので、ここでも迂闊なことはいえない:-)が、小林さんの型システムの（言語は忘れて）型とsubtypingだけsubsetすれば、その部分はやはり同じではなかろうか。もちろん、filterの話がメインなので、そこはoriginalと思われるし、そもそもfilterの部分以外は普通のCCS（のsubset）のsimulationの一種っぽいが。
  • セッションタイプの多者拡張。
    • [Q by 自分] （またすみませんが）小林さんの型システムとの関係は？ [A] Global type（全体の動作を表す型）から各参加者の型を取り出して(projection)チェックするための単純なnotation (?)を与えている

Chair report

  • 212本投稿、35本採択、査読レポート合計1100ページ、外部査読者340人
  • 参加者合計320人（過去最高）、内訳USA: 173, France & UK: それぞれ31, Japan & Germany: それぞれ15
  • $170,000
  • Most influential POPL 1998 paper award: MorrisettらのTAL (typed assembly language)の論文