Solving Shape-Analysis Problems in Languages with Destructive Updating

Presentation on theme: "Solving Shape-Analysis Problems in Languages with Destructive Updating"— Presentation transcript:

1 Solving Shape-Analysis Problems in Languages with Destructive Updating
増山 (米澤研究室) 小野 (西田研究室)

2 参考文献 Mooly Sagiv et al , Solving Shape-Analysis Problems in Languages with Destructive Updating ACM Transactions on Programming Languages and Systems , 1998

3 概要 Shape-Analysisとは? 理論 / 解析アルゴリズム 解析の利点、欠点 解析の安全性(safety) 応用 / まとめ
DSG SSG 変換関数 / interpretation 解析の利点、欠点 解析の安全性(safety) 応用 / まとめ

4 Shape-Analysisとは?

5 Shape-Analysisとは? データの形を静的に解析 入力が
リストならば出力もリストを保証 木ならば出力も木を保証 Pointer-Analysis , Alias-Analysis , Type Checking の問題を解くことができる

6 用途 デバッグツールとして使用 並列化に使用 共有されないデータを見つける

7 簡単な例: リストのreverse

8 簡単な例: リストのreverse

9 簡単な例: リストのreverse

10 理論 / 解析アルゴリズム

11 対象言語 破壊的代入を伴うimperativeな言語 Cons-cell を扱う x : = nil
x.sel := nil (sel ∈ { car, cdr }) x := new x := y x.sel := y x := y.sel kill generate

12 プログラムの形式化 プログラムはControl-flow Graph (V,A)で表現 (V.. vertex, A .. arc)
制御の流れを示す

13 Shape Graph <Ev,Es>
ノード 変数 PVar メモリのセルを表す shape_node car,cdrというセレクタを持つ 枝 変数から出る枝　variable-edge (Ev) shape_nodeから出る枝　selector_edge (Es)

14 DSG: deterministic shape-graph
定義 |Ev(x)| ≦ (x ∈ PVar) |Es(n,sel)| ≦ 1 (n ∈ shape_nodes) DSGのクラスをDSGと書く 実行時のメモリ状態を表現する

15 Concrete Semantics [] : DSG → DSG

16 DSGとControl-Flow Graphの 関係

17 Collecting Semantics 定義　cs: V → 2DSG あるプログラムポイントでの実現しうるメモリ状態全ての集合

18 SSG: Static Shape-Graph
定義 Shape-Graph(SG#)と、shape_nodeの共有状態を表す真偽値関数(is#)とのペア(<SG#, is#>) shape_nodeは変数の集合で名前付けされている　(例 n{x,y,z}) SSGのクラスをSSGと書く あるプログラムポイントでのメモリ状態を抽象化している

19 DSGとSSGとControl-Flow Graphの関係

20 DSGからSSGへの変換 定義 β: DSG → SSG β(l) : shape_node間の変換
DSG上でlを指す変数集合で名前付け is#(n) : SSGのshape_node→{true,false} iis[Es](l) = |{<*,*,l>∈Es}| ≧ 2 is#(n) =

21 変換の例 x y z w n{w,y} n{z} nφ n{x}

22 複数のDSGのマージ α: 2DSG→SSG

23 DSGのマージの例

24 Concrete and Abstract Properties

25 Safe Approximation 定義 DSGでpが成り立つならば、SSG上でもp#が成り立つ
compatible , = などはSafe Approximationである その対偶である!p# ⇒ !pが重要

26 Abstract Interpretation
DSG SSG Abstract Interpretation DSG SSG Abstract Interpretation SSG

27 Abstract Semantics 定義 []#: SSG → SSG x := nil x.sel := nil x := new
x := y x.sel := y x := y.sel それぞれの文について定義する

28 x := nil {v7 : t1 := nil}

29 x.sel := nil {v11 : y.cdr := nil}

30 x := new 新しく共有されていないshape_nodeを作成 Evに新たな枝 [x,n{x}]を加える

31 x := y {v6 : y := x}

32 x.sel := y {v12 : y.cdr := t}

33 x := y.sel {v8 : t1 := x.cdr}

34 Shape-Analysis Algorithm
　Control-Flow Graphの各頂点に対して上の式から計算 できるleast fixed pointを求める 　反復法 　SSGのshape_nodeは2|Pvar|で抑えられ、反復によって、 枝数は単調に増加する　⇒　解析は停止する

35 データタイプを表すSSG

36 Concretization Function
定義 γ: SSG → 2DSG SSGから実現されうるDSGの集合

37 この解析の利点、欠点

38 Strong nullification

39 e.cdr := t iis#(n{t}) = true n{y,z},n{x,y}からn{t}へ の枝が消せる ⇒ iis#(n{t}) = false ⇒ is#(n{t}) = false

40 この解析の問題点 nφが多くのノードを抽象化 ノード数がプログラムの変数の数の指数オーダー 精度を落とす原因 nφをより詳しく分類する
分岐が多いプログラムでは特に問題 精度は落ちるがノード数を減らした解析は可能

41 解析の安全性 (safety)

42 安全性 Local Safety ∀SG∈DSG,st Grobal Safety ∀v ∈ V
(vはControl-Flow Graphのvertex) の定義 SGi# = <<Evi#,Esi#>,isi#>

43 安全性の証明の流れ

44 応用 / まとめ

45 応用 Aliasesの発見 共有されうるデータの発見 あるプログラムポイントvで、2つのアクセスパスe1,e2が
同じcons-cellを指すような実行があるか?　(may) 必ず同じcons-cellを指すか? (must) 共有されうるデータの発見

46 まとめ Shape-Analysis ヒープの状態を静的に解析 変数のaliasingを正確に追うことである程度正確な解析が可能
状態数の抑制と精度のトレードオフあり