 This slide was a material for the “Reading PLDI Papers (PLDIr)”study group written by Kazuhiro Inaba ( www.kmonos.net ),under my own understanding of the papers
published at PLDI
 So, it may include many mistakes etc

 For your correct understanding, please

consult the original paper and/or the authors’presentation slide!

k.inaba (稲葉 一浩), reading:

PLDIr #14
Jul 26, 2010
paper written by K. R. M. Leino A. P.-Heffter Y. Zhou
(PLDI 2002)

USING DATA GROUPS TO SPECIFY
AND CHECK SIDE EFFECTS

Using Data Groups to Specify and Check Side Effects

概要 オブジェクト指向プログラムの副作用解析をやりたい ここでは、副作用 ≒ フィールドの破壊的書換

 全自動でやるのは
 無理
 modular でない ライブラリも含め対象アプリの全ソースコードがな
いと丌可能。現実的でない。

 ということで、プログラマによるアノテーションに頼る
 どういうアノテーションをもらうのが良いか？

基本的なアイデア
 対象言語 “OOLONG” という多分この論文のためだけに設計された、仮想の副作用解析専用言語
 untyped
 class とかの概念もない
 object とその field access があるだけ JavaScript (-prototype) や Lua みたいなの アノテーション 関数を modifies で修飾
proc push(stk, e) modifies stk.contents
impl push(stk, e) { stk.contents << e }むずかしい点 （class があった方が説明しやすいのでJava風の謎言語で説明）
interface Stack{ void push(e); }void useStack(Stack s) { s.push(“hoge”); } Q: このコードはどういう副作用をおこす？

 A: Stack の実装によるので、上のinterface宣言

だけでは解析のしようがない
class ArrayStack implements Stack {Object[] contents;
void push(e) modifies this.contents{ contents << e; }}

むずかしい点＆解決策
 かといって、interface のアノテーションに、実装詳細を書くわけにも…
interface Stack {void push(e) modifies this.contents;} そりゅーしょん：グループ宣言
interface Stack {group impl_data;
void push(e) modifies imple_data;}class ArrayStack implements Stack {field contents in impl_data;
void push(e) { contents.add(e); }}フォーマルに言うと “グループ” を宣言できる グループには階層構造を定義できる

 各 “フィールド” はどのグループに属すか宣言できる
 同時に複数のグループに所属できる
 maps ： メンバオブジェクトのフィールドをグループ宣言

class java.util.ArrayList { Object[] __data; … }class ArrayStack implements Stack {{ ArrayList elems;
field elems maps __data to impl_data; }さらに色々とややこしい問題
Stack {
 実は未だあまり interface
group contents

解決してない 上半分をみただけでは
assert 通りそうに見える でもダメvoid push(e)modifies this.contents;
Object hoge();}void q( Stack s ) {vd = s.hoge().__data;s.push(42);assert( vd == s.vec.__data );} Pivot Uniqueness Owner Exclusion // NO “return vec;”

みたいなのは
Oolongでは禁止

class HogeStack implements Stack {field vec maps __data to contents;
void push(e) { vec.__data << e; }Object hoge() { return vec; }}アノテーションを使って
 これを

 こんな論理式に変換する導出規則を定義

 あとは論理式のChekcerで検査する(のだと思う)k.inaba (稲葉 一浩), reading:

PLDIr #14
Jul 26, 2010
paper written by A. S.-Lezama R. Rabbah, R. Bodik, and K.
Ebcioglu (PLDI 2005)

PROGAMMING BY SKETCHING FORBIT-STREAMING PROGRAMS

問題
 wビットの整数を、3の倍数番目のビットを消して左に詰めて下さい 単純な実装 ： w/3 回のシフト演算等（右はこの研究の提案言語で書いたコード）

速い実装
 なんか並列っぽく、まとめてシフト
 log2 w/3 回のシフト等

 「なんか並列っぽく、まとめて」まで思いついたとしても、この格好いい実装をきちんと正しく作るのは結構大変 各ステップで何ビットずつまとめればいい？
 各ステップでどのくらいシフトすれば？
 動かしちゃいけない部分はどこだろう？

提案言語 StreamBit 「遅いけど正しい実装」と

 「だいたいこんな感じでまとめてシフトを何回かやればできる巧い実装があるはず！」というスケッチを不えると高速な実装を自動合成

どんな感じに書くか (16bitの例)
細かいことはわからん (*) けどビットによってコピーしたりシフトしたりする！

まとめてシフトする
幅はわからん (*) けどなんか適当にまとめてビットずらすはず！

16bit なら、3回もやればできるはず！

 と書くと、* をうまく埋めて完全な実装を作ってくれるそうです。
 実装は探索でみつける （+ 様々なヒューリスティクス）
 push/pop による記述は、AND, OR, XOR, LSHIFT,RSHIFT の組み合わせにうまくコンパイラが展開してくれるらしい評価 こんな計算をするストリーム暗号を いろんな人に実装してもらう かかった時間

 できた実装の速度 などで比較（C言語と勝負）

 論文のグラフ参照

その後
 APLAS 2009 Invited Talk
 ビット以外でも色々できるように発展しているらしい

リストの逆転なんて、なんかループして終了条
件チェックして適当に代入を繰り返してればどうにかなるのでは！！！！