今年読んだ面白CS論文紹介

今年読んだ面白CS論文紹介カレンダー というリレー形式のイベント用に書いています.

自己紹介

ネット上では cocoatomo という ID で活動してます.

現実ではサラリーマンしてますが, 社会人博士なんてものでもあります. 映画とか学生料金で入れます. まだ全然行ってないけど.「けいおん!」とか「ベルセルク」とか行きたい.

プログラム書く立場で働いてみて色々変えたいと思うところがあり, また研究者生活もしてみたいと思い (こっちが本心?), 博士に入りました. そこで, 静的解析を軸に「リリースされる前に, プログラムの予想外の不本意な動作をできるだけ除去したい」という目標で研究しています (まだ勉強している段階ですが).

この分野は昔からあって, 自分が予想していたよりは進歩しておらず, 計算機科学の先達が死屍累々な印象を受けました. 自分もその死体の山の1つになる可能性は高いですが, その死体の分だけ山が高くなるので, まぁ意味はあるでしょう.

という感じで生活してます.

では, さっそくその周辺の論文紹介をしていきます.

Has the Bug Really Been Fixed?

出会い

こっちの分野の論文を全然読んだことない自分にとって, 疑問文の題名はちと衝撃でした. ただ内容とすごく合っていて, それを思い出すと内容も自然と思い出されて,「こういうふうに題名は付けるのかぁ」と関心しています.

目的

この論文の目的は, バグ修正のときの修正漏れや別のエンバグを効率良く検出することです.

後者は regression test で頑張るので目新しいとこは無いです.

ストーリー

前者の手法が人間的で面白かったのです. この論文では以下のようなストーリーをイメージしています.

  1. ある入力でバグが起きる, というバグチケットが飛んでくる.
  2. バグの原因を修正して, チケットにある入力値でテストする.
  3. 「よっしゃー, テスト通った! コミットーーーー!!」
  4. (...コーヒーでまったり...)
  5. 「しまったー! 他の入力値だとまだバグってるやんけ!!」

バグというのは1匹見たら近くにもまだバグが30匹いるものです. 経験則でだいたい分かってるものと思います. 論文では Ant, AspectJ, Rhino を調査対象としていますが, そういう例が多かったという報告がなされています. (コミットコメントの "Oh, I am sorry I didn’t consider that possibility” とか “Oops, missed one code path” とか)

手法

バグチケットにバグを引き起こす全ての入力値が書いてあるわけもないので, バグが発生する箇所での発生する条件から入力値の条件 (WP=Weakest Precondition) を求める必要があります. しかし, たいていの場合この計算は条件式が膨らんで計算が手に余るようになります.

なのでさっきの経験則を使って, 全ての実行パスについて WP を計算するのではなく,「バグチケットにあった入力値からバグ発生箇所までの実行パスから, Levenshtein 距離である程度の範囲にある実行パスについてのみ WP を考える」という手法で距離で制限された WP (=WP_d) を求めます. この WP_d についてテストなり記号実行すれば良いのですが, 論文では (この記事の後で出てくる) JPF 上での記号実行をしてバグのあるなしを確かめています.

感想

この論文を読む前は,「バグの近くにバグがある」というのは経験則では分かっているものの, どうやって形式的な定義に落とせば良いのか想像も付きませんでした. この論文を読んで, まだ色々試さなきゃいけない静的解析の手法が残っていて, 現場での経験とセンスが必要とされるんだなぁ, という印象を持ちました. kinaba さんの 論文をよもう という素晴しいエントリもありますが, 論文は構えずに気楽に内容を楽しみながら読むもんだなぁ, ということも教わった論文です.

Snugglebug: A Powerful Approach To Weakest Preconditions

一言でまとめると「WP の計算に静的解析を組み合わせた解析手法」です. WP は上で出てきた Weakest Precondition です.

問題

多態 (polymorphism) のある言語 (論文では Java) だと, virtual call のせいで状態爆発が起きてちゃんと計算できなくなりやすいです.

解決策

なので, WP を計算するとき virtual call についてはいったん変数の形で扱っておいて, 後で具体的な実態が判明したときにその値で WP を計算し直すことにします. これを "Directed Call Graph Construction" と呼んでいます.

また関数単位での WP の再利用性を高めるために, generalization と名付けた WP を少し緩めた summary を作る手法もこの論文では紹介されています.

感想

プログラミング言語の能力と静的解析可能性はだいたい相反するところがあります. 通常, インターフェースに対してプログラミングをすることは推奨されています. しかし, 静的解析からするとそれは状態爆発を起こすもので, 正直解析の邪魔になります.

このトレードオフの状況で, プログラマのできることを制限し過ぎず, 停止性などの良い性質を証明できる言語が理想の言語なのかなぁ? という示唆を与えてくれた論文です.

Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software

一言で言うと「NASA では, JPF というモデルチェッカーに記号実行を載せてそれを利用してテストケース作成を行ったり, システムレベルでのテストと (JPF が得意な) ユニットテストを組み合わせたりしてソフトウェアの品質を上げているよ」という話です. 一言と形容するには長いですね^-^;;

JPF は JVM instruction の意味論を入れ替えるプラガブルな仕組みになっているし, listener という実行中の動作の監視や通知の仕組みもあるので, 具体値での実行と記号実行を切り替えることもできます. その意味論を差し替える機能を使って, Java Object の field を遅延初期化する (読み取られるときに初期化する) ことで状態爆発を抑えつつ, テストしなければならない (木などの) 参照構造を組み立てます. 参照ではない primitive な値に対しては記号実行をしておきます. そして, 最後に記号値を具体値に直したらテストケースの出来上がりです.

システムレベルのテストとユニットテストを結び付けるところは, Monte Carlo 法で入力値を作ったり, 業務のエキスパートにお願いして業務的に取り得る値の範囲を設定したりした, という結構現実的なお話でした.

感想

NASA ではこの仕組みを有人飛行のシステムに適用しているので, 伝わってくる本気度が半端無かったです. そして, そういう現場での「自動で計算できるプログラムの性質」と「業務上の常識」の組み合わせが興味深かったです.

なんでもかんでも自動でやるのはやっぱり良くないよね〜, という言葉にするとごく普通な感想になってしまいますが,「全自動」に夢を見がちなので自戒として心に留めておこうと思った論文でした.

まとめ?

ちと時間オーバーしましたが, 17日の分の論文紹介でした. 次は @cocoa_ruto さん, お願いします.

Licenses