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.

Slides:



Advertisements
Similar presentations
ソフトウェア工学 知能情報学部 新田直也. オブジェクト指向パラダイムと は  オブジェクト指向言語の発展に伴って形成され てきたソフトウェア開発上の概念.オブジェク ト指向分析,オブジェクト指向設計など,プロ グラミング以外の工程でも用いられる.  ソフトウェアを処理や関数ではなくオブジェク.
Advertisements

プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
なぜ今Pythonか? Pythonをお薦めする18の理由
This slide was a material for the “Reading PLDI Papers (PLDIr)” study group written by Kazuhiro Inaba ( ), under my own understanding of.
SHA-1の高速化tips 2007/9/15
英語勉強会.
稲葉 一浩 (k.inaba) Python と プログラミングコンテスト 稲葉 一浩 (k.inaba)
2008/03/01 D-BOF k.inaba はじめての initial D 2008/03/01 D-BOF k.inaba
Javaのための暗黙的に型定義される構造体
実行時のメモリ構造(1) Jasminの基礎とフレーム内動作
Handel-C基礎 および 7セグとマウスのハンドリング
LMNtalからC言語への変換の設計と実装
Myoungkyu Song and Eli Tilevich 発表者: 石尾 隆(大阪大学)
LMNtalからC言語への変換の設計と実装
読んだもの1 P0145R1: Refining Expression Evaluation Order for Idiomatic C++
Object Group ANalizer Graduate School of Information Science and Technology, Osaka University OGAN visualizes representative interactions between a pair.
Paper from PVLDB vol.7 (To appear in VLDB 2014)
アルゴリズムとデータ構造 2011年6月13日

①データ構造 ②アルゴリズム ③プログラム言語 ④マークアップ言語
社会人学習講座 「Javaプログラミング概論」
の まとめ 2007/04/02 (Mon) / d;id:hzkr
Licensing information
Flyingware : バイトコード変換による 安全なエージェントの実行
CGと形状モデリング 授業資料 長井 超慧(東京大学)
コンパイラの解析 (2) GCJのデータ構造 - 1.
C 言語について 補足資料 資料および授業の情報は :
細かい粒度でコードの再利用を可能とするメソッド内メソッドのJava言語への導入
プログラミング言語入門 手続き型言語としてのJava
Session 8: How can you present your research?
識別子の命名支援を目的とした動詞-目的語関係の辞書構築
細かい粒度で コードの再利用を可能とする メソッド内メソッドと その効率の良い実装方法の提案
0からわかるF# Part1 中 博俊 F# September 2008 CTP Base.
0からわかるF# Part1 中 博俊 F# September 2008 CTP Base.
暗黙的に型付けされる構造体の Java言語への導入
50年前のプログラミング言語 50年後のプログラミング言語
0からわかるF# Part1 中 博俊 F# September 2008 CTP Base.
プログラミング言語入門.
0からわかるF# Part1 中 博俊 F# September 2008 CTP Base.
Javaプログラムの変更を支援する 影響波及解析システム
依存型で型付けされた 副作用のある関数のための 型保存コンパイラ
0からわかるF# Part1 中 博俊 F# September 2008 CTP Base.
0からわかるF# Part1 中 博俊 F# September 2008 CTP Base.
第5章 計算とプログラム 本章で説明すること ・計算の概観と記述法 ・代表的な計算モデル ・プログラムとプログラム言語.
アルゴリズムとデータ構造 2011年7月8日課題の復習
コンパイラ 2011年10月20日
This slide was a material for the “Reading PLDI Papers (PLDIr)” study group written by Kazuhiro Inaba ( ), under my own understanding of.
ソフトウェア工学 知能情報学部 新田直也.
プログラミング言語論 第十一回 理工学部 情報システム工学科 新田直也.
オブジェクト指向言語論 第三回 知能情報学部 新田直也.
アルゴリズムとデータ構造 2012年6月11日
This slide was a material for the “Reading PLDI Papers (PLDIr)” study group written by Kazuhiro Inaba ( ), under my own understanding of.
アルゴリズムとデータ構造1 2009年6月15日
This slide was a material for the “Reading PLDI Papers (PLDIr)” study group written by Kazuhiro Inaba ( ), under my own understanding of.
統合開発環境のための プログラミング言語拡張 フレームワーク
発表者: 稲葉 一浩 複雑ネットワーク・地図グラフ セミナー 2017/1/19
オブジェクト指向言語論 第十一回 知能情報学部 新田直也.
エイリアス関係を考慮した Javaプログラム用静的スライシングツール
オブジェクト指向言語論 第九回 知能情報学部 新田直也.
コンパイラ 2012年10月11日
アルゴリズムとデータ構造 2010年6月17日
フレンド関数とフレンド演算子.
プログラミング入門2 第6回 関数 情報工学科 篠埜 功.
オブジェクト指向言語論 第六回 知能情報学部 新田直也.
情報処理Ⅱ 2005年11月25日(金).
識別子の読解を目的とした名詞辞書の作成方法の一試案
GluonJ を用いたビジネスロジックからのデータベースアクセスの分離
This slide was a material for the “Reading PLDI Papers (PLDIr)” study group written by Kazuhiro Inaba ( ), under my own understanding of.
オブジェクト指向言語論 第九回 知能情報学部 新田直也.
計算機プログラミングI 第2回 2002年10月17日(木) 履習登録 複習 ライブラリの利用 (2.6-7) 式・値・代入 (2.6-8)
Presentation transcript:

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!

Using Data Groups to Specify and Check Side Effects    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風の謎言語で説明) Q: このコードはどういう副作用をおこす? A: Stack の実装によるので、上のinterface宣言  だけでは解析のしようがない interface Stack { void push(e); } void useStack(Stack s) { s.push(“hoge”); } 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; }

さらに色々とややこしい問題 実は未だあまり 解決してない Pivot Uniqueness Owner Exclusion interface Stack { group contents void push(e) modifies this.contents; Object hoge(); } void q( Stack s ) { vd = s.hoge().__data; s.push(42); assert( vd == s.vec.__data ); // NO class HogeStack implements Stack { field vec maps __data to contents; void push(e) { vec.__data << e; } Object hoge() { return vec; } 実は未だあまり 解決してない 上半分を みただけでは assert 通りそう に見える でもダメ Pivot Uniqueness Owner Exclusion “return vec;” みたいなのは Oolongでは禁止

アノテーションを使って これ             を こんな論理式に変換する導出規則を定義 あとは論理式のChekcerで検査する(のだと思う)

Programming by Sketching for Bit-Streaming Programs    k.inaba (稲葉 一浩), reading: PLDIr #14 Jul 26, 2010 paper written by A. S.-Lezama R. Rabbah, R. Bodik, and K. Ebcioglu (PLDI 2005) Programming by Sketching for Bit-Streaming Programs

問題 wビットの整数を、 3の倍数番目のビットを消して 左に詰めて下さい

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

提案言語 StreamBit 「遅いけど正しい実装」 と 「だいたいこんな感じでまとめてシフトを何回 かやればできる巧い実装があるはず!」とい うスケッチを与えると 高速な実装を自動合成

どんな感じに書くか (16bitの例) 細かいことは わからん (*) けど ビットによって コピーしたりシフト したりする! まとめてシフトする 幅はわからん (*) けど なんか適当にまとめてビットずらすはず! 16bit なら、 3回もやれば できるはず!

と書くと、* をうまく埋めて完全な実装を作っ てくれるそうです。 実装は探索でみつける (+ 様々なヒューリスティクス) push/pop による記述は、AND, OR, XOR, LSHIFT, RSHIFT の組み合わせにうまくコンパイラが 展開してくれるらしい

評価 こんな計算をするストリーム暗号を いろんな人に実装してもらう 論文のグラフ参照 かかった時間 できた実装の速度 などで比較(C言語と勝負) 論文のグラフ参照

その後 APLAS 2009 Invited Talk ビット以外でも色々できるように 発展しているらしい リストの逆転なんて、 なんかループして終了条件チェックして適当に代入を繰り返してればどうにかなるのでは!!!!