狠狠撸

Inference

and

Checking

of

Object Ownership

MD 輪講
博?後期課程 1 年

楊　嘉晨

?阪?学?学院コンピュータサイエンス専攻楠本研究室

2013 年 11 ? 20 ?（?）

?阪?学?学院 CS 専攻楊　嘉晨 (楠本研)

Ownership

2013 年 11 ? 20 ?（?）

1 / 46

?次
.
. 背景 Introduction

1

. 所有権型システムの統?されたフレームワーク Uni?ed Framework for
Ownership Type Systems

2

. 型付けのラーキング Heuristic Ranking over Typings

3

. 統合した型推測 Uni?ed Type Inference

4

. 実験結果 Empirical Results

5


Ownership

2013 年 11 ? 20 ?（?）

2 / 46

背景 Introduction


Ownership

2013 年 11 ? 20 ?（?）

3 / 46

出典
Publication

ECOOP 2012
? 26 ページ, B5 サイズ
? European Conference on Object-Oriented Programming

Wei Huang1 ,Werner Dietl2 , Ana Milanova1 , and Michael D. Ernst2
?

1

Rensselaer Polytechnic Institute レンセラー?科?学

?

2

University of Washington

Wei Huang ?最近の論?
?
?
?

Ana Milanova and Wei Huang, “Inference and Checking of Context-Sensitive Pluggable Types”, Proceedings of ACM SIGSOFT Symposium on the
Foundations of Software Engineering(FSE 2012), New Ideas Track, November 2012
Wei Huang, Ana Milanova, Werner Dietl, and Michael D. Ernst, “ReIm & ReImInfer: Checking and inference of reference immutability and
method purity”, Proceedings of Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2012), October 2012
Ana Milanova and Wei Huang, “Composing Polymorphic Noninterference Systems with Reference Immutability”, Proceedings of Formal
Techniques for Java-like Programs (FTfJP 2013), July 2013


Ownership

2013 年 11 ? 20 ?（?）

4 / 46

オブジェクトの所有権
Object Ownership
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

class XStack{
Link top = null;
void push (X d){
Link l = new Link(d);
l.next = top;
top = l;
}
static void main(){
XStack s = new XStack();
X x = new X();
s.push(x);
}
}
class Link {
Link next = null;
X data;
Link(X d) { data = d; }
}


参照 (reference) ?= 所有関係 (ownership)
.
root

.
root
s
l
Ownership

x

s

x

l
2013 年 11 ? 20 ?（?）

5 / 46

所有権を表す型システム
Ownership-like Type Systems
type

quali?er

class type

変数の型は修飾?とクラス型の組み合わせで宣?するもの
1
.

1 public
Object a
2 final
Object b
3 @NotNull Object c

2
.
3
.

ownership

可視性
可変性
Null 可能

type quali?er

今回議論するのは所有権を表す型の修飾?
1 own

Object o


Ownership

2013 年 11 ? 20 ?（?）

6 / 46

背景
Introduction

ownership-like type systems

既存の所有権型システム
owner

as

modi?er

? Universe Types (UT) [8]: 所有者は変更者
[8] Dietl, W., Muller, P. “Universes: Lightweight ownership for JML”. Journal of Object Technology 4(8), 5–32 (2005)

owner

as dominator

? Ownership Types (OT) [4]: 所有者は?配者
[4] Clarke, D., Potter, J.M., Noble, J. “Ownership types for ?exible alias protection”. OOPSLA, vol. 33, pp. 48–64 (1998)

.
型修飾?の?動推測
.
? ?動に付ける苦労を削減
? 価値のある性質を明らかにする
.

Ownership

.
?動推測に難しいのは
.
多数の型が可能の時,
best typing

最適な型付けを決めること
.
2013 年 11 ? 20 ?（?）

7 / 46

この研究の貢献
Contributions
uni?ed framework

? 所有権型システムの統?されたフレームワーク
? UT,OT をインスタンス化した
? 最適な型付けを決めるヒューリスティックな?法
? 統合された型付けの推測?法
? 全?動的な最適 UT 推測
? ?動の型付けで半?動的な OT 推測
? 平均 6/kLOC の?動関与

? 実証的な評価
? 最? 110kLOC の Java プログラム
? UT と OT

Ownership

2013 年 11 ? 20 ?（?）

9 / 46

所有権型システムの
統?されたフレームワーク
Uni?ed Framework for
Ownership Type Systems

Ownership

2013 年 11 ? 20 ?（?）

10 / 46

A-正規形 Java ?法 [26]
A-normal Form Java Syntax

説明するため、この?法を使います. 実装上, 普通の?法に対応できます
cd
fd
md
s

class C extends D{fd md}
τf
τ m(τ x){τ y s; return y}
s; s|x = new τ ()
|x = y|x.f = y|x = y.f|x = y.m(z)
|this.f = y|x = this.f|x = this.m(z)
τ ::= q C
q ∈ Q
::=
::=
::=
::=

クラス
フィルド
メソッド
?

修飾された型
型修飾?

[26] Vaziri M., Tip F., Dolby J., Hammer C., Vitek J. “A Type System for Data- Centric Synchronization”. ECOOP 2010. LNCS, vol. 6183, pp. 304–328.

Ownership

2013 年 11 ? 20 ?（?）

11 / 46

統?されたフレームワーク
Uni?ed Framework

?つの所有権型システムは４つのものに定義されます：{Q, <:, ?, B}
Q 型修飾?の集合
? τ ::= q C q ∈ Q
? 例 (UT): {peer, rep, any}
sub-typing hierarchy

<: サブタイプ階層
? 例 (UT): peer <: any, rep <: any
viewpoint adaptation function

? 視点適応関数 q ? q′ (後述)
B 追加制約集合
? 型システムに特殊な制約

Ownership

2013 年 11 ? 20 ?（?）

12 / 46

視点適応関数: q1 ? q2 = q[8]
Viewpoint Adaptation Function

1 class X{
2
q2 f;
3
void main(){
4
q1 X x;
5
(q) x.f;
6
}
7 }

typeof(x) = q1
typeof(f) = q2
typeof(x.f) = q1 ? q2 = q

型 q1 の x の視点から?る型 q2 の f があるとし, 現在の視点 this から?る
型は q = q1 ? q2
[8] Dietl, W., Muller, P. “Universes: Lightweight ownership for JML”. Journal of Object Technology 4(8), 5–32 (2005)


Ownership

2013 年 11 ? 20 ?（?）

13 / 46

共通する型制約
Uni?ed Typing Rules
.
TWRITE
.

.
TNEW
.

Γ(x) = qx Γ(y) = qy
typeof(f) = qf
qy <: qx ? qf
B(TWRITETHIS) (qx , qf , qy )

Γ(x) = qx q <: qx
B(TNEW) (qx , q)
. Γ ? x = new q C()
.
.
TASSIGN
.

Γ ? x.f = y

.
TWRITETHIS
.

qy <: qx
B(ASSIGN) (qx , q)
.

.
TREAD
.

.

Γ ? this.f = y


typeof(m) = q → q′
Γ(x) = qx Γ(y) = qy Γ(z) = qz
qz <: qy ? q qy ? q′ <: qx
B(TCALL) (m, qy , qx )

typeof(f) = qf
qy ? qf <: qx
B(TREAD) (qx , qf , qy )
.

Γ ? x = y.f

.
TREADTHIS
.

typeof(f) = qf Γ(y) = qy
qy <: qf
B(TWRITETHIS) (qf , qy )

Γ ?x=y

.
TCALL
.

.

.
TCALLTHIS
.
typeof(m) = q → q′
Γ(x) = qx Γ(z) = qz
qz <: q q′ <: qx
B(TCALLTHIS) (m, qx )

typeof(f) = qf Γ(x) = qx
qx <: qf
B(TREADTHIS) (qf , qx )
.

Γ ? x = this.f
.
Ownership

Γ ? x = y.m(z)

Γ ? x = this.m(z)
2013 年 11 ? 20 ?（?）

14 / 46

Universe Types (UT)[8,5]
owner

as

modi?er

owner

peer

所有者は変更者: オブジェクトを変更できるのは所有者と同僚のみ.
.
QUT = {peer, rep, lost, any}
.
peer this と x は所有者が同じのオブ
ジェクト同志
rep this は x の所有者
lost (内部で使う) 制約は確かにあ
るが, 現時点で表せない
any 所有権で表せない
rep <: lost
.

peer <: lost


lost <: any
Ownership

OaM
List

? ? ?

? ??

Node

.
視点適応関数
.
peer
rep
_
. q

?
?
?
?

peer
peer
any
q′

=
=
=
=

peer
rep
any
lost otherwise

2013 年 11 ? 20 ?（?）

15 / 46

UT の追加制約
B(TNEW) (ql , qr )
= {qr ?= any}
B(TWRITE) (qr , qf , qo ) = {qr ?= any, qr ? qf ?= lost}
B(TCALL) (m, qr , qo ) = let typeof(m) = q → q′ in
if impure(m)[13] then {qr ?= any, qr ? q ?= lost}
else {qr ? q ?= lost}
下線が付いたのは変更者を規則する部分
[13] Huang W., Milanova A. “A Type System for Reference Immutability”. Technical report, Rensselaer Polytechnic Institute, CS (2011)


Ownership

2013 年 11 ? 20 ?（?）

16 / 46

UT を適?した例
1 class XStack {
2
any Link top;
3
XStack() {
4
top = null;
5
}
6
void push(any X d1) {
7
rep Link newTop;
8
newTop = new rep Link();
9
newTop.init(d1);
10
newTop.next = top;
11
top = newTop;
12
}
13
void main(String[] arg) {
14
rep XStack s;
15
s = new rep XStack();
16
any X x = new rep X();
17
s.push(x);
18
}
19 }


1 class Link {
2
any Link next;
3
any X data;
4
void init(any X d2) {
5
next = null;
6
data = d2;
7
}
8 }

.
root
s

x

l

Ownership

2013 年 11 ? 20 ?（?）

17 / 46

Ownership Types(OT)[4]
owner
as dominator

expose

所有者は?配者: オブジェクトは所有者の外に出せない.
.
OaD
QOT = {?q0 |q1 ?|q0 , q1 ∈ {rep, own, p}}
List
.
rep this を表す
??
? ? ??
own this の所有者を表す
Node
p this に与えた所有関係のパラメーター
.
QOT = {?rep|rep?, ?rep|own?, ?rep|p?, ?own|own?, ?own|p?, ?p|p?}
BOT = ?
OT にサブタイプの階層はない. サブタイプ関係は同値関係になる
[4] Clarke, D., Potter, J.M., Noble, J. “Ownership types for ?exible alias protection”. OOPSLA, vol. 33, pp. 48–64 (1998)

Ownership

2013 年 11 ? 20 ?（?）

18 / 46

OT: 型修飾? ?q0|q1? の意味
1 class L {
2
<q0|q1> x;
3 }

q0 : x の所有者
q1 : x の所有関係のパラメーター

q0 と q1 に以下から選べる：
1 rep を指定して, 　オブジェクト??をさす
.
2 own を指定して, this の所有者をさす
.
3 p を指定して, パラメーターから受け取ったオブジェクトをさす
.
(例) ?rep|own?x: x の所有者は this, パラメーターは this の所有者
パラメーターの数は２つ以上でも可能
? 実験の結果から?ると 1 つは?分
? 増えるほど理解しにくい

Ownership

2013 年 11 ? 20 ?（?）

19 / 46

OT の視点適応関数
?q0 |q1 ? ? ?own|own? = ?q0 |q0 ?
?q0 |q1 ? ? ?own|p?
= ?q0 |q1 ?
?q0 |q1 ? ? ?own|p?
= ?q1 |q1 ?
フィルドの型 (? の右) は rep を含む場合, 静的制約を破ります
1
2
3
4
5
6
7

class L {
<rep|rep> C y;
void main(){ x=y.f }
}
class C{
<own|p> F f;
}


y.f の型修飾?は <rep|rep> になる

Ownership

2013 年 11 ? 20 ?（?）

20 / 46

OT を適?した例
1 class XStack {
2
<rep|p> Link top;
3
XStack() {
4
top = null;
5
}
6
void push( p|p X d1) {
7
<rep|p> Link newTop;
8
newTop = new <rep|p> Link();
9
newTop.init(d1);
10
newTop.next = top;
11
top = newTop;
12
}
13
14
<rep|rep> XStack s;
15
s = new rep|rep XStack();
16
<rep|rep> X x = new <rep|rep> X();
17
s.push(x);
18
}
19 }


1 class Link {
2
<own|p> Link next;
3
<p|p> X data;
4
void init(<p|p> X d2) {
5
next = null;
6
data = d2;
7
}
8 }

.
root
s

x

l

Ownership

2013 年 11 ? 20 ?（?）

21 / 46

型付けのラーキング
Heuristic Ranking over Typings


Ownership

2013 年 11 ? 20 ?（?）

22 / 46

?つのプログラムには多数の有効型付け案が可能
1 class XStack {
2
any Link top;
3
XStack() {
4
top = null;
5
}
6
void push(any X d1) {
7
rep Link newTop;
8
newTop = new rep Link();
9
newTop.init(d1);
10
newTop.next = top;
11
top = newTop;
12
}
13
14
rep XStack s;
15
s = new rep XStack();
16
any X x = new rep X();
17
s.push(x);
18
}
19 }

1 class Link {
2
any Link next;
3
any X data;
4
void init(any X d2) {
5
next = null;
6
data = d2;
7
}
8 }

.
root
s

x

l

Ownership

2013 年 11 ? 20 ?（?）

23 / 46

?つのプログラムには多数の有効型付け案が可能
1 class XStack {
2
peer Link top;
3
XStack() {
4
top = null;
5
}
6
void push(peer X d1) {
7
peer Link newTop;
8
newTop = new peer Link();
9
newTop.init(d1);
10
newTop.next = top;
11
top = newTop;
12
}
13
14
peer XStack s;
15
s = new peer XStack();
16
peer X x = new peer X();
17
s.push(x);
18
}
19 }

1 class Link {
2
peer Link next;
3
peer X data;
4
void init(peer X d2) {
5
next = null;
6
data = d2;
7
}
8 }

.
root
s

l

x

ゆるい型が付けられたら, 平坦なオブジェクト階
層になって, 全てのアクセスは許されてしまう
Ownership

2013 年 11 ? 20 ?（?）

23 / 46

型付けにヒューリスティックなランキングの?的
主観的に：深いツリー構造で表す所有権がほしい

objective function

ランキング：ツリー構造の深さに影響する性質を?標関数o として定義し, そ
の値を最?化する
. valid
typing
有効な型付け
.
P: プログラーム
F: 所有権型システム
TP,F : 型付け案
.


TP,F は有効: 全ての制約を満たす
若しプログラマーに?動でつけた型があると, それも制
約に含まれる

Ownership

2013 年 11 ? 20 ?（?）

24 / 46

UT の?標関数 oUT

.
修飾?のランキング
.
{any} > {rep} > {peer}
.
.
?標関数
.
oUT (T) = (|T?1 (any)|, |T?1 (rep)|, |T?1 (peer)|)
.
.
?標関数のベクトルを辞書順で?較する
.
oUT (T1 ) = (4, 5, 0) > oUT (T2 ) = (3, 5, 0) > oUT (T3 ) = (3, 4, 10)
.
.
UT の最適型付け
.
max{oT | ?T ∈ {有効な型付け案 T}}
.

Ownership

2013 年 11 ? 20 ?（?）

25 / 46

OT の?標関数 oOT
ベース修飾?のランキング {rep} > {own} > {p}
.
辞書順は最適でないの例 oOT (?rep|rep?) ≯ oOT (?rep|p?)
.
.
root
.
root
m

j

i

.
root
j

i

j

i

k
m

.

k
l

m

k

l

l′

l

l′ i → m を rep にした場合

l′

k → l を rep にした場合

oOT (T) = (|T?1 (?rep|_?)|, |T?1 (?own|_?)|, |T?1 (?p|_?)|)

Ownership

2013 年 11 ? 20 ?（?）

26 / 46

統合した型推測 Uni?ed Type
Inference


Ownership

2013 年 11 ? 20 ?（?）

28 / 46

統合した型推測: 集合ベースの推測
Uni?ed Type Inference: Set Based Solution

(OT 等の型システムに対し) 全?動で型推測は不可能
→ 協?的に半?動で型を推測
.
キーアイデア: 集合ベースの推測
.
各
. 変数宣?に型修飾?の有効集合を求める
.
集合のマッピング
.
SP,F は各変数宣?の型修飾?の有効集合
{
{q} プログラーマーが v に?動つけた型修飾?
S0 (v) =
QF 型修飾?の最?集合
.

Ownership

2013 年 11 ? 20 ?（?）

29 / 46

統合した型推測の?法
Architecture of Uni?ed Type Inference

?動で型付け

.
統合制約

集合ベース
のソルバー

{Q, <:, ?, B}

最適型付
けを抽出

型の制約
をチェック

ソースコード
最適型付け


Ownership

2013 年 11 ? 20 ?（?）

30 / 46

伝達関数と不動点まで繰り返し
Transfer Function and Fixpoint Iteration

.
伝達関数 fs : S → S′
.
伝
. 達関数 fs は S に s ?の制約を破った型付けを削除
.
不動点まで繰り返し
.
全ての伝達関数を以下の状況がでるまで S にかけて繰り返す
1 S は変わらない, 解に導いた
.
. 2. S にある変数の型集合は空, プログラームに型が?盾している


Ownership

2013 年 11 ? 20 ?（?）

31 / 46

UT の型推測例
1 class XStack {
2
{any,rep,peer} Link top;
3
XStack() {
4
top = null;
5
}
6
void push({any,rep,peer} X d1) {
7
{any,rep,peer} Link newTop;
8
newTop = new {any,rep,peer} Link();
9
newTop.init(d1);
10
newTop.next = top;
11
top = newTop;
12
}
13
14
{any,rep,peer} XStack s;
15
s = new {any,rep,peer} XStack();
16
{any,rep,peer} X x = new {any,rep,peer} X();
17
s.push(x);
18
}
19 }

Ownership

初期状態
1 class Link {
2
{any,rep,peer} Link next;
3
{any,rep,peer} X data;
4
void init({any,rep,peer} X d2) {
5
next = null;
6
data = d2;
7
}
8 }

2013 年 11 ? 20 ?（?）

32 / 46

UT の型推測例
1 class XStack {
2
3
XStack() {
4
top = null;
5
}
6
7
{any,rep,peer} Link newTop;
8
newTop = new {
rep,peer} Link();
9
newTop.init(d1);
10
newTop.next = top;
11
top = newTop;
12
}
13
14
15
16
17
s.push(x);
18
}
19 }

Ownership

BTNEW = {qr ?= any}
1 class Link {
2
3
4
void init({any,rep,peer} X d2) {
5
next = null;
6
data = d2;
7
}
8 }

2013 年 11 ? 20 ?（?）

32 / 46

UT の型推測例
1 class XStack {
2
3
XStack() {
4
top = null;
5
}
6
7
{
rep,peer} Link newTop;
8
newTop = new {
rep,peer} Link();
9
newTop.init(d1);
10
newTop.next = top;
11
top = newTop;
12
}
13
14
15
16
17
s.push(x);
18
}
19 }

Ownership

BTCALL = {qr ?= any, qr ? q ?=
lost}
1 class Link {
2
3
4
void init({any
,peer} X d2) {
5
next = null;
6
data = d2;
7
}
8 }

2013 年 11 ? 20 ?（?）

32 / 46

UT の型推測例
1 class XStack {
2
3
XStack() {
4
top = null;
5
}
6
void push({any
,peer} X d1) {
7
{
rep,peer} Link newTop;
8
newTop = new {
rep,peer} Link();
9
newTop.init(d1);
10
newTop.next = top;
11
top = newTop;
12
}
13
14
{
rep,peer} XStack s;
15
s = new {
rep,peer} XStack();
16
{any,rep,peer} X x = new {
rep,peer} X();
17
s.push(x);
18
}
19 }

Ownership

イテレーション 1 がおわった時点
1 class Link {
2
{any,
peer} Link next;
3
{any,
peer} X data;
4
void init({any,
peer} X d2) {
5
next = null;
6
data = d2;
7
}
8 }

2013 年 11 ? 20 ?（?）

32 / 46

UT の型推測例
1 class XStack {
2
any
Link top;
3
XStack() {
4
top = null;
5
}
6
void push( any
X d1) {
7
rep
Link newTop;
8
newTop = new
rep
Link();
9
newTop.init(d1);
10
newTop.next = top;
11
top = newTop;
12
}
13
14
rep
XStack s;
15
s = new
rep
XStack();
16
any
X x = new
rep
17
s.push(x);
18
}
19 }

最適化に選ばれた型
1 class Link {
2
any
Link next;
3
any
X data;
4
void init( any
X d2) {
5
next = null;
6
data = d2;
7
}
8 }
X();

Ownership

OT の推測例を省略
2013 年 11 ? 20 ?（?）

32 / 46

実験結果 Empirical Results


Ownership

2013 年 11 ? 20 ?（?）

33 / 46

実装と実験対象
既存ツールの Checker Framework[20,6] で実装した
実験対象
Benchmark
JOlden
tinySQL
htmlparser
ejc
javad
SPECjbb
jdepend
classycle

#Lines
6223
31980
62627
110822
4207
12076
4351
8972

#Meths
326
1597
1698
4734
140
529
328
440

Description
Benchmark suit of 10 small programs
Database engine
HTML parser
Compiler of the Eclipse IDE
Java class ?le disassembler
SPEC?s benchmark for evaluating server side Java
Java package dependency analyzer
Java class and package dependency analyzer

[20] Papi, M.M., Ali, M., Correa Jr., T.L., Perkins, J.H., Ernst, M.D. “Practical pluggable types for Java.”ISSTA, pp. 201–212 (2008)
[6] Dietl, W., Dietzel, S., Ernst, M.D., Muslu, K., Schiller, T.W. “Building and Using Pluggable Type-Checkers. ” ICSE, pp. 681–690 (2011)


Ownership

2013 年 11 ? 20 ?（?）

34 / 46

UT の実験結果
any

rep

peer

100%

90%
80%
70%
60%

50%
40%
30%
20%

10%
0%


Ownership

2013 年 11 ? 20 ?（?）

35 / 46

UT の実験結果
Benchmark
JOlden
tinySQL
htmlparser
ejc
javad
SPECjbb
jdepend
classycle

Pure
175
965
642
1701
60
195
102
260

Ref
685
2711
3269
10957
249
1066
542
946

any
227 (33%)
630 (23%)
426 (13%)
1897 (17%)
31 (12%)
295 (28%)
95 (18%)
87 ( 9%)

rep
71 (10%)
104 ( 4%)
153 ( 5%)
122 ( 1%)
11 ( 4%)
74 ( 7%)
14 ( 3%)
11 ( 1%)

387
1977
2690
8938
207
697
433
848

peer
(56%)
(73%)
(82%)
(82%)
(83%)
(65%)
(80%)
(90%)

Time
11.3
18.2
22.9
119.7
4.1
13.6
7.2
9.9

(ちなみに私のツールで htmlparser の Stateful+Stateless の純粋関数は 543)


Ownership

2013 年 11 ? 20 ?（?）

36 / 46

UT の実験結果と既存研究 [7] の?較
既存研究 [7] の結果より, any をつけた変数の割合が?きくなった. 原因
? 純粋関数の測定?法は違う
? 既存研究で javad の内 40 個の関数は?動で純粋関数であることを検証した
? 本研究で 60 個の関数は?動で推測した, 増えたの 20 個は確かに純粋関数

であることを検証した
? ヒューリスティックで最適修飾?を選ぶ?法が違った
? 本研究で {any,rep} の場合に any にする
? 既存研究では両?ありえる
[7] Dietl, W., Ernst, M.D., Müller, P. “Tunable Static Inference for Generic Universe Types. ”ECOOP 2011. vol. 6813, pp. 333–357. Springer


Ownership

2013 年 11 ? 20 ?（?）

37 / 46

OT の実験結果
<rep|_>

<own|_>

<p|_>

100%
90%
80%

70%
60%
50%
40%
30%
20%
10%
0%


Ownership

2013 年 11 ? 20 ?（?）

38 / 46

OT の実験結果
Benchmark
Ref
<rep|_>
<own|_>
<p|_> <norep|_>
JOlden
685
67(10%/10%)
497(73%)
24(4%)
97(14%)
tinySQL
2711
224(8%/11%)
530(20%)
5(0%) 1952(72%)
htmlparser
3269 330(10%/11%)
629(19%)
36(1%) 2274(70%)
ejc
10957
467(4%/4%) 1768(16%)
50(0%) 8672(79%)
javad
249
44(18%/19%)
27(11%)
74(30%)
104(42%)
SPECjbb
1066 166(16%/16%)
141(13%)
71(7%)
688(65%)
jdepend
542 130(24%/25%)
156(29%) 128(24%)
128(24%)
classycle
946 153(16%/20%)
173(18%)
28(3%)
592(63%)
<rep|_> 列の２つ?の割合は理論上限, パラメーター数を増えても超えない


Ownership

?動
13(2)
215(7)
200(3)
592(5)
46(10)
73(6)
26(6)
90(10)

Time
10.3
18.4
33.6
122.4
5.5
17.1
13.7
11.7

2013 年 11 ? 20 ?（?）

39 / 46

OT の実験結果に対する議論
? UT の結果に?べて rep の割合は?きいが, ?較は無意味 (後述)
? ?動で付ける型は 6 個/kLOC, 実?的
? 表での時間は?動で付ける必要がある型が与えた後、ツールをかける

時間のみ. ?動で選ぶ時間を計算すると,JOlden は約 10 分
間,SPECjbb は約 2 時間を掛かりました.
既存研究との?較は?われてない


Ownership

2013 年 11 ? 20 ?（?）

40 / 46

UT と OT の?較: 所有権の割合
OT:rep
UT&OT:rep
31%

9%

UT:rep

5%

.
55%

Other

Ownership

2013 年 11 ? 20 ?（?）

41 / 46

UT と OT の?較
OT:
<rep|_> <rep|_> not <rep|_> not <rep|_>
UT:
rep
peer
rep
not rep
JOlden
26 (22%)
8 ( 7%)
19 (16%)
66 (55%)
tinySQL
32 ( 6%) 123 (24%)
13 ( 2%)
355 (68%)
htmlparser 27 ( 2%) 234 (20%)
16 ( 1%)
926 (77%)
ejc
44 ( 2%) 336 (12%)
81 ( 3%) 2321 (83%)
javad
6 (10%) 38 (66%)
0 ( 0%)
14 (24%)
SPECjbb
75 (26%) 84 (29%)
25 ( 9%)
110 (37%)
jdepend
13 ( 7%) 71 (41%)
1 ( 1%)
90 (51%)
classycle
1 ( 0%) 109 (45%)
5 ( 2%)
128 (53%)

Ownership

2013 年 11 ? 20 ?（?）

42 / 46

オブジェクト所有権構造で OT は UT より深い例
オブジェクト図
.
root
i

k

OT のツリー
.
root
i

UT のツリー
.
root

k
i

j


j

k

j

Ownership

2013 年 11 ? 20 ?（?）

43 / 46

オブジェクト所有権構造で UT は OT より深い例
オブジェクト図
.
root

UT のツリー
.
root

OT のツリー
.
root

x

x
x
c

c

i
c

i

e

e

e

Ownership

i

2013 年 11 ? 20 ?（?）

44 / 46

結論
Conclusion

? 所有権型システムを推測と検証するための統?されたフレームワークを
?
?
?
?

提案した
UT と OT の２つ既存の所有権型システムにインスタンス化した
有効な型付けのランキングを決めるヒューリスティックの?法
最?型付けの?動?半?動推測?法
実装して, 規模がある対象に UT と OT を実験した


Ownership

2013 年 11 ? 20 ?（?）

45 / 46

論?を読んだ感想
上から?線で

? 「既存研究に対するメソット抽出リファクタリング」?たいな研究は初?
? 若?無理?理感をした
? 追加制約 B は UT のみ
? 型修飾?のサブタイプルールも UT のみ
? 純粋関数判定に依存するのも UT のみ

? と関わらず (書いてない

が)UT の?が優れる感
? 理解しやすい
? 最適解が保証される
? ?動関与は要らない

? ２つの?法を組み合わせによって, 既存研究より良い結果が期待され

ているが, そうでもなかった


Ownership

2013 年 11 ? 20 ?（?）

46 / 46

集合ベースの?法の性質
Properties of Set-Based Solution

.
命題 1
.
若し q ∈ S(v) なら, T(v) = q に成り?てる有効型付け T ∈ S0 は存在しない
/
.
.
命題 2
.
P の全て変数宣? v に対し T(v) = max(S(v)) なら, T は P の最?型付け
.
.
性質 1: 最適化性質
.
全ての変数宣? v に型集合の最?修飾?は有効である場合に限り, 型付けは最適化さ
れた
.
.
時間複雑度
.
集合ベースのアルゴリズムの時間複雑度は O(n2 ), そのうち n はプログラムの?の数.
.

Ownership

2013 年 11 ? 20 ?（?）

47 / 46

狠狠撸

Inference and Checking of Object Ownership

More Related Content

Inference and Checking of Object Ownership