slide - POSL

SMTベースのCOPデバッグ支援
〜 COP: コンテキスト指向プログラミング 〜
内尾 静
(九州大学)
鵜林 尚靖 (九州大学)
亀井 靖高 (九州大学)
2011年11月24日
概要:
SMTソルバーによるトレース解析
コンテキスト指向
プログラミング
レイヤ
SMT
デバッグ
支援
オブジェクトB
オブジェクトA
オブジェクトC
コンテキストをモジュール化
しかし、デバッグが困難
SMT: Satisfiability Modulo Theories
COP: Context-Oriented Programming
コンテキスト依存グラフ
実行トレース解析を
充足可能性判定問題として扱う
メリット: 様々な性質が解析可能
2
発表内容
 コンテキスト指向プログラミングとは
 デバッグにまつわる課題
 CJAdviser: SMTソルバーによるトレース解析
 関連研究
 まとめと今後の課題
3
コンテキスト指向プログラミング
とは
4
背景
•コンテキストに応じて振る舞いを変え
る Self-* 型アプリケーションが増加
•Self-adaptive, Self-organizing, etc.
プログラム
A
B
B
レイヤA
A
•美術館鑑賞ナビ
•統合開発環境(IDE)
•センサーネットワークアプリケーション
•プログラムが複雑化
レイヤB
B
A
A
コンテキスト指向
プログラミング
5
コンテキスト指向プログラミング
 コンテキスト指向プログラミング(COP)では、コンテ
キストそのものをモジュールとして取り扱うことが可能。
 COPの種類
 Layer-in-class
 Class-in-layer
 代表的なCOP言語
 ContextL(Lispベース)
 ContextJ*(Javaベース、フレームワーク)
 ContextJ、JCop(Javaベース、構文拡張)
Hirschfeld, R., Costanza, P., and Nierstrasz, O.: Context-oriented Programming,
In Journal of Object Technology (JOT), vol. 7, no. 3, pp.125-151, 2008.
6
具体例: ContextJ* コード
Employer
Person
Name: UchioShizuka; Address: Arae1
public class
Employer
ubayashi
Employer
public
= new
implements
class
Employer("Ubayashi",
Person
IEmployer
implements
{ "Motooka");
IPerson { Arae1;
Name:
UchioShizuka;
Address:
Person uchio = newlayers.define(Layers.Address,new
layers.define(Layers.Address,new
Person("UchioShizuka",
IEmployer()
"Arae1",
{ Ubayashi;
ubayashi);
IPerson()
{
[Employer]
Name:
Address:
Motooka
public String toString()
public
{ String toString() {
with(Layers.Address).eval(
return layers.next(this)
return
+new
"; layers.next(this)
Address:
Block()" {+ address;}});
+ "; Address: " + address;}});
public void eval() { System.out.println(uchio); }});
layers.define(Layers.Employment,new IPerson() {
with(Layers.Address, Layers.Employment).eval(
public String toString() {
newBlock() {
public void eval() { System.out.println(uchio);
return layers.next(this) + }});
"; [Employer] " + employer;}});
7
デバッグにまつわる課題
8
問題意識
 コンテキスト指向プログラミングの考え方は適応型
ソフトウェアを開発するのに重要。
 しかし、実行過程がオブジェクトとコンテキストの
間の関係に依存するため、デバッグが従来よりも難
しくなるという課題がある。
全体の振る
舞いは?
レイヤ
オブジェクトB
t
レイヤ
レイヤ
オブジェクトA
t
オブジェクトC
t
9
実行トレースを見ると...
10
プログラマの悩み?
結果出力
Name: UchioShizuka; Address: Arae1;
[Employer] Name: Ubayashi; Address: Motooka
ubayashi
はどこ?
with(Layers.Address,
public
class Employer
Person implements
Layers.Employment).eval(
implements
IPerson
IEmployer
{
{ newBlock() {
ここかあ。。。
layers.define(Layers.Address,new
public void eval() { System.out.println(uchio);
IPerson() { {}});
IEmployer()
Employerクラス
public String toString() {
あれ?
を見ないと?
return layers.next(this) + "; Address: " + address;}});
Emplymentレイヤ
が無いぞ!
layers.define(Layers.Employment,new IPerson() {
そうか、今、
public String toString() {
ubayashiは
似たようなものが
return layers.next(this) + "; [Employer] " + employer;}});
Addressレイヤに
沢山あって
入っているの
よく分からな
か。。。
い。。。
11
他にもあるデバッグ時の関心事
 AddressレイヤとEmploymentレイヤが
同時に活性化する可能性はあるのか?
 Addressレイヤはいつか活性されるか?
 2つのオブジェクトubayashiとuchioは
同時にレイヤに属することがあるか?
?
? ?
12
CJAdviser:
SMTソルバーによるトレース解析
13
本研究のアプローチ
SMT
単体テスト
コンテキスト依存グラフ
SMT: Satisfiability Modulo Theories
トレース解析(実行解析)
充足可能性問題
14
SMT(背景理論付きSAT)
 SMTはSAT(Boolean satisfiability)を一般化。
 背景理論




等号と未解釈関数の理論
自然数・整数・有理数・実数
配列の理論
再帰データの理論
 Yices は代表的なSMTソルバーの一つで論理式の充足
可能性を判定する。
Yices: http://yices.csl.sri.com/
15
充足可能性判定(SAT)とは?
 命題論理式のうち、連言標準形(CNF)で記述さ
れたものについての充足可能性判定問題
 例: (x1 ∨ x2) ∧ (x1 ∨ ¬x2) ∧ (x3 ∨ x4) ∧
(¬x3 ∨ ¬x4) ∧ (x1 ∨ ¬x3) ∧ (¬x2 ∨ ¬x4)
→ SAT
割当て (x1, x2, x3, x4) = (1, 1, 1, 0)
井上 克巳, 田村 直之: SATソルバーの基礎, 人工知能学会誌, Vol. 25, No. 1, 2010.
16
CJLogger: 実行ログの収集
ContextJ*
プログラム実行
(単体テスト)
オブジェクト
収集するContextJ*イベント
コンテキスト
ログ収集
(AspectJ)
レイヤへの
入場
退場
入場
退場
(Period)
コンテキスト
オブジェクト
Environment
Address
•オブジェクトの生成
•メソッドの起動
•レイヤの生成
•レイヤメソッドの定義
•レイヤメソッドの起動
•ベースメソッドの起動
•レイヤへの入場
•レイヤからの退出
Address
CXDG: Context dependence graph
(コンテキスト依存グラフ)
Period
Period
1
2
Person オブジェクト
17
Yices エンコーディング -- CXDG
Scheme に類似した構文
グラフを配列で表現(現在は手動)
グラフ探索を充足可能性判定問題に帰着
: ; Type definitions
(define-type obj (scalar Employer Person))
(define-type layer (scalar Address Employment))
(define-type with-period (subrange 1 2))
(define-type log-count (subrange 0 4))
(define-type obj-with-layer (tuple with-period obj layer))
(define-type logging (-> int obj-with-layer))
(define log::logging)
: ; Log data (CXDG: Context dependence graph)
(define test-run::logging
(update (update (update (update (update (update
log (0) (mk-tuple 1 Person Address))
(1) (mk-tuple 1 Employer Address))
(2) (mk-tuple 2 Person Address))
(3) (mk-tuple 2 Employer Address))
(4) (mk-tuple 2 Person Employment))))
配列
18
CJQuery:トレース解析
デバッグの
関心事
コンテキスト
問い合わせ
オブジェクト
(Period)
コンテキスト
SAT or UNSAT
19
Case 1:
person と employer は同時にAddress
レイヤに属することがあるか?
(define i::log-count)
(define j::log-count)
(define t::with-period)
(assert (and
(/= i j)
(= (test-run i) (mk-tuple t Person Address))
(= (test-run j) (mk-tuple t Employer Address))))
(check)
SAT
i = 2, j = 3, and t = 2
20
Case 2:
person と employer は同時に同じレイ
ヤに属することがあるか?
(define i::log-count)
(define j::log-count)
(define t::with-period)
(define l::layer)
(assert (and
(/= i j)
(= (test-run i) (mk-tuple t Person l))
(= (test-run j) (mk-tuple t Employer l))))
(check)
SAT
i = 2, j = 3, t = 2, and
l=Address.
21
Case 3:
person は、いつかは Employment レイ
ヤに属するか?
(define i::log-count)
(define t::with-period)
(assert (= (test-run i) (mk-tuple t Person
Employment)))
(check)
SAT
i = 4 and t = 2
22
関連研究
23
関連研究
•COPに関するデバッグに関する研究はほとんど無い。
•デバッグ一般に関する研究は多い。
 Whyline [Ko, A. J. et al. ICSE2008]
 プログラマは、バグに関して “Why did” および “Why didn‘t” と
いう質問をツールに投げかけることができる。
 ツールはその原因を返答する。
 DebugAdvisor [Ashok, B. et al. FSE2009]
 プログラマがツールにバグの状況を伝えると、自然言語のテキス
トやコアダンプなど様々なデータを検索してくれる。
24
まとめと今後の課題
25
まとめと今後の課題
 CJAdviserを提案
 SMT ベースのデバッグサポート
 今後の課題





JCop のサポート
COP 自身によるログ収集(class-in-layer 型 COP)
ユーザインタフェースの改良(cf. Whyline)
スケーラビリティ
実用的な事例への適用
26
ご清聴ありがとうございました
27