スライド作成ガイドライン

(1)

何故モデル検査が必要なのか？

• 多くのソフトウェアが分散処理・並行処理を基

本としている

– 複数の計算主体が並行動作をしながら共有資源

を用いて機能を実現している

• システム全体が安全な動作をしない可能性が

高い

– 資源を奪い合う競合状態に陥る可能性が高い

– 非決定的な振る舞いについて、誤りがテストなど

では現れない可能性が高い

(2)

非決定的な振舞

• 複数スレッド間の並列動作

• 複数機器間の並列動作

• ネットワーク環境の変化

(3)

複数スレッド間の並列動作

int a;

(ロックは適切にとっているものとする．)

スレッド間共有データ

while (true) {

if (a < 10) { a++; }

}

スレッド1

while (true) {

a--;

}

a = 10;

thread1.run();

thread2.run();

while (true) { b = 100/a; }

スレッド2

スレッド

0

(4)

テストでは．．．

• 実行環境によっては，スレッド

1だけが，非常

に負荷の高いCPUに割り当てられ，スレッド0

や2ばかりが動く，ということもあり得る．

• しかし，テストではそのような環境が再現でき

るとは限らない．

a

10 10 9 9

10

9

8

9 スレッド

1

2 0 1

0

2

1

0

(5)

モデル検査では

• すべての場合を探索するので，エラーがお

こるのなら (原理的には) 必ず見つかる．

10

9 th0,th1

th2

th1

th0

th2

th1

...

1 th2

th1

th0

th2

th1

0 th0

err

(6)

モデル検査

• 状態機械の状態空間を網羅的に探索することにより、与えら

れた性質が正しいかどうかを判定する検証方法

• 従来の形式手法との比較

– モデル検査

• 完全な自動化が可能

– 専門的な知識が必要ない

– 定理証明の手法を応用した検証方法

• 数理論理学の知識が必要

• 取り扱える状態数

–

10

4 から 10

5 （初期）

–

10

120 _（現在）

• 問題点

(7)

古典的モデル検査と

現代的モデル検査

• 古典的モデル検査

– 対象

: 仕様書，プロトコルなど

– 設計段階など，「上流工程」でモデル検査を適用．

– 仕様書などから検査器にかけられるモデルを

(ほと

んどの場合) 手動で構築．

• 現代的モデル検査

– 対象

: プログラムソースコードなど

– テスト段階など，「下流工程」でモデル検査を適用．

ほとんどデバッグの一種．

– ソースコードからモデルを自動的に抽出．

(8)

ソースコードモデル検査:

代表的なツール

• Java

–

Java Pathfinder (NASA)

–

Bandera (Kansas State Uni.)

–

Bogor (Kansas State Uni.)

–

JNuke (ETH)

• C/C++

–

Static Driver Verifier (Microsoft）

–

ZING (Microsoft）

–

BLAST (U. of Berkeley)

–

MAGIC (CMU)

(9)

Java Path Finder (JPF)

• NASA Ames Research Center

–

W. Visser らによって開発された

• 2005 年 4 月以降は sourceforge.net で公開

• Java のバイトコードから状態を生成してモデル検査

• 反例を出力

– 全ての実行系列について探索するので、違反が発見されるまで

の経路を出力できる

• 拡張可能

– プロパティクラス、リスナークラスによりユーザが定義する特性の

検証が可能

• 独自の VM

– 初期の

JPF は PROMELA/SPIN に変換していたが、独自の VM に

より実行するように改良された。 Java.awt、java.net には非対応

(10)

JPFの動作原理 (1)

• Javaのクラスファイルは，Java Virtual

Machine （ＪＶＭ）によって解釈され，実

行される．

*.class

*.jar

Java Virtual Machine

....

x ++;

....

(実際にはバイトコード)

a: 0

b: 3

x: 4

5 y: -2

(11)

JPFの動作原理 (2)

• JPFは，自分のJVMを持っている．通常の

JVMと同様に，クラスファイルを解釈できる．

• さらに，後戻り

(backtrack) したり，スレッド

スケジュールを外から与えることもできる．

*.class

*.jar

Java Virtual Machine

for JPF

....

x ++;

....

(実際にはバイトコード)

a: 0

b: 3

x: 4

5 y: -2

(12)

JPFの動作原理 (3)

• JPFの中心は，サーチエンジン．これが，JVM for JPF を駆

動する．

サーチエンジン

_{for JPF}

JVM

次のバイトコードを実行せよ

このような状態になった．

これは以前の

状態と同じだ．

後戻りして，スケジューリングを変えよ

次のバイトコードを実行せよ

(13)

JPFの動作原理 (4)

• 実際には，状態量が増えすぎないように

様々な工夫が行われている．

– 同定可能な範囲でできるだけコンパクトな状態

– スレッド相互間に干渉のない部分は一気に実

行 (半順序簡約)

• サーチエンジン，

JVMも含め，すべてjavaで

書かれている．

(14)

(15)

最上位構造

• 2つの中心的な概

念: SearchとJVM

• JVM: 状態生成 (右

図)

• Search: JVMのドラ

イバ+性質の評価

(16)

JPFの入手とバージョン

• 入手可能なバージョン

: v3 と v4

–

v3: 安定版．ソースで配布．配布サイトではv1.0aと書

かれている．

J2SE1.4 に対応．(Java5では動作しない．)

–

v4: 開発版．ソースで配布．頻繁に更新．v3と比べ，

基本的な構成は同じ．使い勝手が向上している．

Java5に対応．(J2SE1.4では動作しない．)

• ここでは

v3 を使用する．

http://sourceforge.net/projects/javapathfinder/ から

javapathfinder‐src‐libs‐1.0‐7‐oct‐05.zip をダウンロードして展開．(イ

ンストール指示書参照)

(17)

JPF の利用方法についての注意

• Java のバージョン

–

J2SE 1.4 のみに対応．

–

J2SE 1.5 (Java5.0）以降は使わないので注意すること

• Cygwin を用いる．(http://www.cygwin.com/)

• JPF のインストール先

–

C:¥JPF¥jpf release

• 設定方法

(次スライド以降)

– 環境変数の設定

–

jpf (C:¥JPF¥jpf release¥bin)

(18)

環境変数の設定

• 以下のディレクトリからファイル

bashrcをダウンロードする．

http://hagi.is.s.u‐tokyo.ac.jp/pub/staff/hagiya/kougiroku/0521JPF_tanabe/

• 以下の

2つの行の内容を確認し，必要なら書き直す．

• 次のコマンドを実行

(先頭のドットに注意)．

• bashrcファイルの内容を ~/.bashrc に追記しておけば，次回

から以上の操作は不要．(他の講義の設定と衝突しないかど

JAVA_HOME="C:¥usr¥local¥java¥j2sdk1.4.2_12"

JPF_HOME="C:¥JPF¥jpf release"

$

. bashrc

(19)

# bashrc file for JPF

#

# Set appropriate directories

#JAVA_HOME="C:¥usr¥local¥java¥j2sdk1.4.2_12"

JAVA_HOME="C:¥j2sdk1.4.2_14"

#JPF_HOME="C:¥JPF¥jpf release"

JPF_HOME="C:¥jpfv3¥release"

# Do not edit the following

JAVA_HOME_UNIX=`cygpath -u "${JAVA_HOME}"`

JPF_HOME_UNIX=`cygpath -u "${JPF_HOME}"`

export

CLASSPATH="${JPF_HOME}¥build¥jpf;${JPF_HOME}¥lib;${JPF_HOME}¥e

xamples;."

export

PATH="${JPF_HOME_UNIX}/bin:${JAVA_HOME_UNIX}/bin:/bin:/usr/bin:/

usr/local/bin:${PATH}”

(20)

スクリプト jpf の置き換え

• スクリプト

${JPF_HOME}/bin/jpf を，

以下のディレクトリにある jpf で置き換える．念のた

め，オリジナルの jpf は保存しておく．

http://hagi.is.s.u‐tokyo.ac.jp/pub/staff/hagiya/kougiroku/0521JPF_tanabe/

$ diff jpf jpf‐original‐ 7d6 < JPF_HOME_UNIX=`cygpath ‐m "${JPF_HOME}"` 37,38c36,37 < # JAVA_HOME=`cygpath ‐‐path ‐‐windows "$JAVA_HOME"` < # CLASSPATH=`cygpath ‐‐path ‐‐windows "$CLASSPATH"` ‐‐‐ > JAVA_HOME=`cygpath ‐‐path ‐‐windows "$JAVA_HOME"` > CLASSPATH=`cygpath ‐‐path ‐‐windows "$CLASSPATH"` 59,60c58 < # echo java $JVM_FLAGS ‐classpath "$CP" gov.nasa.jpf.JPF +jpf.basedir="$JPF_HOME_UNIX" $@ < java $JVM_FLAGS ‐classpath "$CP" gov.nasa.jpf.JPF +jpf.basedir="$JPF_HOME_UNIX" $@

(21)

JPFの基本機能

配布された (何もカスタマイズしない) 状態で

できること

• デッドロックの検出

• アサーション違反の検出

• 捕捉されない例外の検出

(22)

最初の例（Deadlock.java)

‐ デッドロックの検出

$

cd "${JPF_HOME}"

$

javac examples/deadlock/Deadlock.java

$

java deadlock.Deadlock

…

途中でプログラムが停止

$

jpf deadlock.Deadlock

…

エラー出力については後のスライドで説明

(23)

1 package deadlock; /**

* This example shows a simple deadlock. 5 */

public class Deadlock implements Runnable { /**

* A name for the thread. */

10 String name; /**

* A reference to the other Deadlock object running as a separate thread. */

15 Deadlock other;

public Deadlock (String name) { this.name = name;

} 20

public static void main (String[] args) { Deadlock o1 = new Deadlock("A"); Deadlock o2 = new Deadlock("B"); 25 o1.other = o2;

(24)

Thread t1 = new Thread(o1); Thread t2 = new Thread(o2); 30

t1.start(); t2.start();

}

35 public void run () { while (true) {

System.out.println(name + " cycle start");

synchronized (this) {

other.foo();

40 }

System.out.println(name + " cycle end"); }

} 45

synchronized void foo () {

System.out.println(name + ".foo() was called"); }

(25)

プログラムの説明

• プログラムの並列実行

_31, 32

• 自分自身のロックを獲得

38 • 相手オブジェクトのメソッド

_{foo() を呼ぶ}

₃₉

• ロックを開放する前に相手オブジェクトからメ

ソッドを呼ばれるとデッドロックに陥る

(26)

1 C:¥jpf deadlock.Deadlock A cycle start

B.foo() was called A cycle end

5 A cycle start A cycle start

A cycle start 10 B.foo() was called

A cycle end A cycle start

15 B cycle start A cycle start

B.foo() was called A cycle end A cycle end 20 A cycle start --- thread stacks Thread: Thread-0 at deadlock.Deadlock.run(deadlock¥Deadlock.java:57) Thread: Thread-1 at deadlock.Deadlock.run(deadlock¥Deadlock.java:57)

スレッド＃０

スレッド＃１

行番号

other.foo()

(27)

1

Deadlock

--- path to error (length: 88) Transition #0 Thread #0

5 deadlock¥Deadlock.java:40 Deadlock o1 = new Deadlock("A"); deadlock¥Deadlock.java:35 public Deadlock (String name) { deadlock¥Deadlock.java:36 this.name = name;

deadlock¥Deadlock.java:37 }

deadlock¥Deadlock.java:40 Deadlock o1 = new Deadlock("A"); 10 deadlock¥Deadlock.java:41 Deadlock o2 = new Deadlock("B");

deadlock¥Deadlock.java:35 public Deadlock (String name) { deadlock¥Deadlock.java:36 this.name = name;

deadlock¥Deadlock.java:37 }

deadlock¥Deadlock.java:41 Deadlock o2 = new Deadlock("B"); 15 deadlock¥Deadlock.java:43 o1.other = o2;

deadlock¥Deadlock.java:44 o2.other = o1;

deadlock¥Deadlock.java:46 Thread t1 = new Thread(o1); deadlock¥Deadlock.java:46 Thread t1 = new Thread(o1); deadlock¥Deadlock.java:47 Thread t2 = new Thread(o2); 20

(snipped)

deadlock¥Deadlock.java:56 synchronized (this) { Transition #86 Thread #1

25 deadlock¥Deadlock.java:56 synchronized (this) {

deadlock¥Deadlock.java:57 other.foo();

Transition #87 Thread #2

deadlock¥Deadlock.java:57 other.foo();

--- end error path

===================================

1 Error Found: Deadlock

(28)

デッドロックとなる理由

synchronized (this) { other.foo() }

スレッド

1 t2

スレッド

2 #85,86

#69,80

t1

#86

#87

(29)

(比較) デッドロックとはならない場合

スレッド

1

synchronized (this) { other.foo(); }

t2

スレッド

2 t1

t2

t1

(30)

Javaアサーション

• 指定した

boolean式の値がtrueになるべきである

という表明．

• 実行時に式の値が

_{falseになると，実行時エラー}

(java.lang.AssertionError)になる．

• 形式

_{: assert p : m}

–

p : チェック対象のboolean型の式

–

m : エラーメッセージ

「: m」の部分は省略可能．

• コンパイルオプション

: javac -source 1.4

• 実行時オプション

: java -ea

(31)

JPFとアサーション

• 通常の実行時には，アサーションの位置に制

御が渡ったときに，チェックが行われる．

→ その実行によって通らないパスでは，

チェックが行われない．

• _{JPFによる実行時には，すべてのパスでチェッ}

クが行われる．

(32)

例: AssertionTest1.java

• _{2つのスレッド a1 と a2}

• _{a1 が先に start. a2が後から start}

• _{run の内容: 自分自身を「登録する」}

• 登録の内容

_{: at1 が空いていたら at1 に，そう}

でなかったらat2に代入．

• 両方登録が終わったとき，

_{a1 == at1 になる}

(33)

AssertionTest1.java

at1 = null; at2 = null;

AssertionTest a1 = new AssertionTest(10); AssertionTest a2 = new AssertionTest(20); a1.start(); a2.start();

assert at1.getVal() < at2.getVal();

スレッド

0

at1 = a1;

at2 = a2;

スレッド

1 スレッド

2 null pointer exception

テストで検出できる．

(34)

JPFエラートレース

--- path to error (length: 3) Transition #0 Thread #0

(略)

egs¥AssertionTest1.java:31 a1.start(); egs¥AssertionTest1.java:32 a2.start(); Transition #1 Thread #0

egs¥AssertionTest1.java:33 assert at1.getVal() < at2.getVal() : "unexpected order"; Transition #2 Thread #0

egs¥AssertionTest1.java:33 assert at1.getVal() < at2.getVal() : "unexpected order"; --- end error path

--- thread stacks Thread: Thread-0

at egs.AssertionTest1.run(egs¥AssertionTest1.java:25) Thread: Thread-1

at egs.AssertionTest1.run(egs¥AssertionTest1.java:25) --- end thread stacks

=================================== 1 Error Found: uncaught exception

(35)

AssertionTest2.java (1)

AssertionTest a1 = new AssertionTest(10); AssertionTest a2 = new AssertionTest(20); a1.start(); a2.start(); if (at2 != null) { ... } if (at2 != null) {

assert at1.getVal() < at2.getVal(); }

スレッド

0

at1 = a1;

// at1.getVal() == 10 at2 = a2;

// at2.getVal() == 20

スレッド

1 _スレッド

₂

assertion は成功

1CPUマシンでは，こうなることが多い(?)

しかし，状況によっては

...

(36)

AssertionTest2.java (2)

AssertionTest a1 = new AssertionTest(10); AssertionTest a2 = new AssertionTest(20); a1.start(); a2.start(); if (at2 != null) { ... } if (at2 != null) {

assert at1.getVal() < at2.getVal(); }

スレッド

0

at2 = a1; // at2.getVal() == 10 at1 = a2; // at1.getVal() == 20

スレッド

1 _スレッド

₂

assertion は失敗

テストでは検出できるとは限らない．

(37)

JPFエラートレース

--- path to error (length: 20) Transition #0 Thread #0 (略) egs¥AssertionTest2.java:31 a1.start(); egs¥AssertionTest2.java:32 a2.start(); (略) Transition #7 Thread #2

egs¥AssertionTest2.java:12 if (at1 == null) {at1 = at; } egs¥AssertionTest2.java:11 synchronized(lockObj) {

(略)

egs¥AssertionTest2.java:13 else {at2 = at; } egs¥AssertionTest2.java:11 synchronized(lockObj) {

(略)

egs¥AssertionTest2.java:18 public int getVal() { return val; }

egs¥AssertionTest2.java:36 assert at1.getVal() < at2.getVal() : "unexpected order"; (略)

--- end error path

=================================== 1 Error Found: uncaught exception