slide - POSL

ＳＭＴベースのＣＯＰデバッグ支援
〜ＣＯP：コンテキスト指向プログラミング〜
内尾静
（九州大学）
鵜林尚靖（九州大学）
亀井靖高（九州大学）
２０１１年１１月２４日
概要：
ＳＭＴソルバーによるトレース解析
コンテキスト指向
プログラミング
レイヤ
ＳＭＴ
デバッグ
支援
オブジェクトＢ
オブジェクトＡ
オブジェクトＣ
コンテキストをモジュール化
しかし、デバッグが困難
SMT: Satisfiability Modulo Theories
COP: Context-Oriented Programming
コンテキスト依存グラフ
実行トレース解析を
充足可能性判定問題として扱う
メリット：様々な性質が解析可能
2
発表内容
 コンテキスト指向プログラミングとは
 デバッグにまつわる課題
 CJAdviser: ＳＭＴソルバーによるトレース解析
 関連研究
 まとめと今後の課題
3
コンテキスト指向プログラミング
とは
4
背景
•コンテキストに応じて振る舞いを変え
る Self-* 型アプリケーションが増加
•Self-adaptive, Self-organizing, etc.
プログラム
A
B
B
レイヤA
A
•美術館鑑賞ナビ
•統合開発環境（ＩＤＥ）
•センサーネットワークアプリケーション
•プログラムが複雑化
レイヤB
B
A
A
コンテキスト指向
プログラミング
5
コンテキスト指向プログラミング
 コンテキスト指向プログラミング（ＣＯＰ）では、コンテ
キストそのものをモジュールとして取り扱うことが可能。
 ＣＯＰの種類
 Layer-in-class
 Class-in-layer
 代表的なＣＯＰ言語
 ContextL（Ｌｉｓｐベース）
 ContextJ*（Ｊａｖａベース、フレームワーク）
 ContextJ、JCop（Ｊａｖａベース、構文拡張）
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
問題意識
 コンテキスト指向プログラミングの考え方は適応型
ソフトウェアを開発するのに重要。
 しかし、実行過程がオブジェクトとコンテキストの
間の関係に依存するため、デバッグが従来よりも難
しくなるという課題がある。
全体の振る
舞いは？
レイヤ
オブジェクトＢ
t
レイヤ
レイヤ
オブジェクトA
t
オブジェクトＣ
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レイヤはいつか活性されるか？
 ２つのオブジェクトubayashiとuchioは
同時にレイヤに属することがあるか？
？
？？
12
CJAdviser:
ＳＭＴソルバーによるトレース解析
13
本研究のアプローチ
ＳＭＴ
単体テスト
コンテキスト依存グラフ
SMT: Satisfiability Modulo Theories
トレース解析（実行解析）
充足可能性問題
14
ＳＭＴ（背景理論付きＳＡＴ）
 ＳＭＴはＳＡＴ（Boolean satisfiability）を一般化。
 背景理論




等号と未解釈関数の理論
自然数・整数・有理数・実数
配列の理論
再帰データの理論
 Yices は代表的なＳＭＴソルバーの一つで論理式の充足
可能性を判定する。
Yices: http://yices.csl.sri.com/
15
充足可能性判定（ＳＡＴ）とは？
 命題論理式のうち、連言標準形（ＣＮＦ）で記述さ
れたものについての充足可能性判定問題
 例： (x1 ∨ x2) ∧ (x1 ∨ ¬x2) ∧ (x3 ∨ x4) ∧
(¬x3 ∨ ¬x4) ∧ (x1 ∨ ¬x3) ∧ (¬x2 ∨ ¬x4)
→ ＳＡＴ
割当て (x1, x2, x3, x4) = (1, 1, 1, 0)
井上克巳, 田村直之: ＳＡＴソルバーの基礎, 人工知能学会誌, 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
関連研究
•ＣＯＰに関するデバッグに関する研究はほとんど無い。
•デバッグ一般に関する研究は多い。
 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

Download Report