2010-01-06 [長年日記]
λ. PLDIr #5
PLDIの論文を読む PLDIr の第五回に参加。 今回はPLDI2001の論文が対象で、私は以下の3本の論文を紹介した。
- Design and Implementation of Generics for the .NET Common Language Runtime (著者版)
- Automatic Predicate Abstraction of C Programs (著者版)
- The Pointer Assertion Logic Engine (著者版)
Design and Implementation of Generics for the .NET Common Language Runtime は、文字通り.NETのCLRにパラメトリック多相を実装する話。 JVMや当時のCLRは多相をサポートしてないので、多相をコンパイルしようとすると性能、プリミティブ型の扱い、コンパイルの複雑さなどの問題がでる。 なので、CLRレベルでちゃんとサポートしようという話。 伝統的なコンパイル・リンク・実行というモデルではなく、CLRの動的なコード生成やJITを活用した設計になっていて、実行時にコードのspecializeを行う。 厳密な実行時型もサポートし、またプリミティブ型によるインスタンス化も性能を低下させずに実現。 vtable内に型パラメータとオープンな型のスロットを用意する点などが面白かった。
Automatic Predicate Abstraction of C Programs はソフトウェア向けモデル検査器SLAMで抽象化を行っているツールC2BPの詳しい話。 C2BPは、CプログラムPと述語の集合Eから、述語抽象化した Boolean program B(P,E) を生成する。 この Boolean program の生成は自明な話だと思っていたけど、元のプログラムのコードに対応して、どの述語の真偽がどう変化するかを判定するのは結構工夫が必要で、面白かった。
The Pointer Assertion Logic Engine は、PALE(the Pointer Assertion Logic Engine)というツールについて。 PALEは、ヒープの構造に関する性質を Pointer Assertion Logic というロジックで、アノテーション(事前条件・事後条件・不変条件)として記述し、プログラムとアノテーションを、WS2S(weak monadic second-order theory of 2 successors)に変換してMONAで検証する。 記述可能な性質は Graph types と呼ばれているもの。
以前にMONAで正規表現にマッチする例を生成したりしたけど、MONAってこんなことも出来るのか、と驚いた。 そういえば、計算機言語で定理証明 (Proof Party.JP) - ヒビルテ(2009-10-24)のときに触ってみたJahobも、決定手続きの一つとしてMONAが利用可能だったけど、同じような感じで使ってるのかなぁ。
発表資料 (PDF):
