Verifying Safety Property of Concurrent Java Programs Using 3-Valued Logic (popl’01) Eran Yahave Available at http://www.math.tau.ac.il/~yahave 　　　　or ~iwama/popl/3vl-java.ps　 ミーティング資料 : 岩間　太

背景 Java 言語は、コンパイル時にも、実行時にも、プログラムの並行的な振る舞い（並行プリミティブなどの動作）に対しては、安全性の検証を何も行っていない。 卒業論文で、Javaの並行プログラム（の実行コード）の安全性（主にロックについて）を検証するするTypeシステムを構築した。

概要 この論文では、 Javaの並行プログラムのconcurrentモデルの部分に対して、いろいろな安全性の検証を行うためのフレームワークを、3-valued logic を使って与えている。 Model checking の一種 相互費序的な実行 実行時エラーになるようなスレッド間のアクション などの安全性

Java の並行モデル （マルチスレッドモデル） synchronized(expr){S}　ステートメント expr を評価した結果のオブジェクトのロックを獲得し、（できなかったらblock-setへ）ステートメント S を実行、その後、ロックを開放 o.wait()　命令 オブジェクト o 上のロックに関連づけられた、wait-set で 待機 o.notify(), o.notifyall ()命令 オブジェクト o 上のロックに関連づけられた、wait-set で待機しているスレッドを起こす

Representing Configuration (1) programの状態(program configuration)、またそこで成り立っている性質(properties of configuration)を first order logic をベースとしたメタ言語で記述　 解析するプログラムに対して、predicatesの集合　P　があると仮定 そのpredicate を使った論理式で、configuration, properties を表現

Representing Configuration (2) Predicates for partial Java semantics (1) is_thread(t)　　 オブジェクト t はスレッド {at[lab](t): lab ∈Labels}　　 スレッド t は、ラベルlabを実行しようとしている {rvalue[fld](o1,o2): fld ∈Field} オブジェクト o1 の field または functional parameter が、オブジェクト o2 を指している held_by(l,t) ロック l は、スレッド t に獲得されている

Representing Configuration (3) Predicates for partial Java semantics (2) blocked(t,l) スレッドt は、ロック l 上でブロックされている、つまり、スレッド t は、ロック l に関連づけられた、block-set の中にいる。 Synchronized 文 で、ロックが獲得できない状態 waiting(t,l) スレッド t は、ロック l 上で待機している

Representing Configuration (4) Program configuration は、 2-valued logical structure CN で定義される CN=<UN,ιN> 　　　　　　　　　　　　　　　　　　　 UN ：CN の universe UN は individual の 集合 ιN：CN の interpretation function 各 predicate に対して、 UN の中の各 individual を代入した際の、 真偽値 （0 または 1) を返す解釈関数

Representing Configuration (5) UN ：CN の universe UN の中の各 individual は heap に割り当てられている オブジェクト の 一つを表す UN 全体として、heap上のすべてのオブジェクトを指す ιN：CN の interpretation function 各 arity k の predicate　p　に対して ιN(p): UN →{0,1}　 k

Configuration グラフ Configuration CN=<UN,ιN> を有効グラフとして表現できる UN の中の各 individual を、ノードとして表現 成り立っている predicate を書く arity 1 の predicate なら、ノードの中に arity 2 の predicate p(u1,u2) なら、u1 から u2 へ有効辺を引き、その有向辺に

サンプル プログラム（１） class approver class Producer implements Runable { protected Queue q; …… public void run() { q.approveHead(); } class Producer implements Runable { protected Queue q; …… public void run() { q.put(val1); } class Consumer implements Runable { protected Queue q; …… public void run() { val2 = q.take(); } //QueueItem.java class QueueItem { private QueueItem next ; private int value ; …… public void approve() { …….} }

サンプル プログラム（２） // Queue.java class Queue { private QueueItem head; private QueueItem tail; …… public void put(int value) { QueueItem x_i = new QueueItem(value); lp1 synchronized(this) { lp2 if (tail == null) { lp3 tail = x_i; lp4 head = x_I ; lp5 } else { tail.next = x_i; lp6 tail = x_i ; lp7 } lp8 } lp9 ラベル

public void take() { synchronized(this) { lt1 QueueItem x_d ; if (head != null) { lt2 newHwad = head.next; lt3 x_d = head ; lt4 x_d.next = null ; lt5 head = newHead ; lt6 if (newHead == null) { lt7 tail = null; lt8 } } lt9 return x_d ; lt10 public void approveHead() { synchronized(this) { la1 if (head != null) ; la2 head.approve(); la3 } la4

サンプル プログラム（３） ラベル class Main { public static void main(String[] args) { Queue q = new Queue(); lm1 Thread prd = new Thread(new Producer(q)); lm2 Thread cns = new Thread(new Consumer(q)); lm3 for (int i=0; i<3; i++) { lm4 new Thread(new Approver(q).start(); lm5 } prd.start(); lm6 cns.start(); lm7

Configurationグラフの例 rvalue[next] rvalue[head] rvalue[next] <u1> r_by[next] <u2> r_by[next] <u0> r_by[head] <q> r_by[this] rvalue[tail] rvalue[next] rvalue[this] rvalue[this] <m1> r_by[x_i] <u3> r_by[next] <prd> is_thread at[lp_6] held_by rvalue[this] <a2> is_thread at[la_1] rvalue[next] blocked <cns> is_thread at[lt_1] <u4> r_by[next] r_by[tail] <a1> is_thread at[la_1] <a1> is_thread at[la_1] rvalue[this]

Extracting Properties of Configuration (1) Configuration の性質は、その性質を表した first order logic の式を評価することで調べることができる。 式の評価結果が 0 なら、その性質（式が表している性質，状態）は成り立っていない 式の評価結果が 1 なら、その性質は成り立っている。

Extracting Properties of Configuration (2) ∃t : is_thread(t)∧held_by(l,t) この式は、ロック l があるスレッドによって獲得されていることを示している ∀t1,∀t2 (t1≠t2)→￢(at[l_crit](t1)∧at[l_crit](t2)) クリティカルセクション中のラベルをl_critで表しているとすると、この式は、クリティカルセクションの相互排除的な実行要求を表している

Semantics (1) Java の statement 実行は、actionによるconfigurationの書き換え、によってモデル化される。 Synchronized(expr){S} 文 ( blockLock(v) ) 　： S に入れなかったとき lock(v) S と対応する action unlock(v) Javaのステートメントが実行されていくと、ヒープ内の状態も変わっていくので、対応して、configurationも変わっていく。

Semantics (2) Java の statement実行は、actionによるconfigurationの書き換え、によってモデル化される。 o.wait 文 wait(v) o.notify 文 notify(v) 　または　ignoredNotify(v) o.notifyall notifyAll(v)　または　ignoredNotifyAll(v) Javaのステートメントが実行されていくと、ヒープ内の状態も変わっていくので、対応して、configurationも変わっていく。

Semantics (3) Action ac によって、 CN =<UN,ιN> が CN’ =<UN,ιN’> に 書き換えられる(CN ⇒ac CN’) とは CN において、ac の precondition を満たす代入Zが存在する。 すべての　predicate∈P, u1,…,uk∈UN について、ιN’(p)(u1,…uk)= 【Φp_ac(v1,…vk)】 (Z[v1 →u1,.., vn→un]) Φp_ac(v1,…vk) は、 action ac の predicate-update の式 CN 2

Semantics (4) action の precondition とは、action を起こすために成り立っていなければならない、論理式 action の predicate-update とは、actionを起こした後の、各predicate の値を変化，更新させる式 at[lab](t) については、適切に更新されるとする

Semantics (5) lock(v) Action を起こすスレッドを ts とおく precondition : ￢∃t≠ts:rvalue[v](ts,l)∧held_by(l,t) predicate-update held_by’(l1,t1)=held_by(l1,t1)∨(t1=ts ∧ l1=l) blockd’(l1,t1)=blockd(t1,l1)∧((t1≠ts)∨(l1≠l))

Semantics (6) blockLock(v) unlock(v) precondition predicate-update ￢∃t≠ts:rvalue[v](ts,l)∧held_by(l,t) predicate-update bolocked’(t1,l1)=blocked(t1,l1)∨(t1=ts ∧ l1=l) unlock(v) rvalue[v](ts,l) held_by’(l1,t1)=held_by(l1.t1)∧(t1≠ts ∨ l1≠l) blocking action (ラベルを進めない action)

Semantics (7) ある action ac について CN ⇒ac CN’ のとき CN ⇒ CN’ と書く 以下のような列があるとき　 CNは CN’ に推移的に書き換えられるという( CN ⇒* CN’ ) CN =CN1, CN2,…, CNn= CN’ such that for each 0≦i＜n, CNi ⇒CN’(i+1)

Safety properties of Java programs(1) 初期状態の集合として、initial configurations CI を考える。 Initial configurations から，推移的に書き換えられて作られる configuration の集合として reachable configurations CR を定義する Cr ∈CR iff ∃Ci ∈CI : Ci ⇒*Cr

Safety properties of Java programs(2) Reachable configurations CR のなかのすべての configuration について、安全ではないような性質を表した論理式を、満たすようなものを探し出すことにより、プログラムの安全性について検証できる。

Safety properties of Java programs(3) RW Interference 2つのスレッドが同時に、あるオブジェクトに書き込み，読み出し、しようとしている状態 ∃(tr,tw)∃o: is_thread(tr)∧is_thread(tw) ∧ at[lr](tr)∧at[lw](tw) ∧ rvalue[xw](tw,o)∧rvalue[xr](tr,o) lr は、読み出しを行う文のラベル、lwは、書き込みを行う文のラベルを表す

Safety properties of Java programs(4) WW Interference 2つのスレッドが同時に、あるオブジェクトに書き込み，読み出し、しようとしている状態 ∃(tw1,tw2)∃o: is_thread(tw1)∧is_thread(tw2) ∧ at[lw1](tw1)∧at[lw2](tw2) ∧rvalue[tw1](tw1,o)∧rvalue[tw2](tw2,o) lw1,lw2は、書き込みを行う文のラベルを表す

Configurationグラフの例 rvalue[next] rvalue[head] rvalue[next] <u1> r_by[next] <u2> r_by[next] <u0> r_by[head] <q> r_by[this] rvalue[tail] rvalue[next] rvalue[this] rvalue[this] <m1> r_by[x_i] <u3> r_by[next] <prd> is_thread at[lp_6] held_by rvalue[this] <a2> is_thread at[la_1] rvalue[next] blocked <cns> is_thread at[lt_1] <u4> r_by[next] r_by[tail] <a1> is_thread at[la_1] <a1> is_thread at[la_1] rvalue[this]

State space exploration Initial configurations CI から reachable configurations CR を求めながら、安全性を検証していくアルゴリズムは、次のような形になる explore() { while stack is not empty { C = pop(stack) if not member(C,stateSpace) { verify(C) stateSpace’ = stateSpace∪{C} for each C’ such that C⇒C’ push(stack,C’) } initialize(CI) { for each C ∈CI push(stack, C) }

Representing Abstract configuration (1) Configuration を 2-valued structure で表したのでは、柔軟な解析ができないし、何より、先の initialize, explore のアルゴリズムがとまらないことがある（オブジェクトやスレッドの数などに制限がない場合とか）

Representing Abstract configuration (2) そこで、プログラムの状態を、 　　　　　　　　　　　　　3-valued structure で表す 　　　　　　(これを、abstract configuration という) universe の中の individual のいくつかをまとめて 一つの individual に predicate p ∈ P 　の評価結果を　 0 -- 成り立たない　 1 -- 成り立つ 1/2 -- それ以外、不明

Representing Abstract configuration (3) Abstract program configuration は、 3-valued logical structure C で定義される C=<U,ι> U ：C の universe individual の集合 ι：C の interpretation function 各 predicate に対して、 U の中の各 individual を代入した際の、 真偽値 （0 または 1　または 1/2) を返す解釈関数

Representing Abstract configuration (４) U ：C の universe U の中の各 individual は、heap に割り当てられた、一つ以上のオブジェクトを表す （重なりはないものとする） 一つ以上のオブジェクトを表す individual を summery node という U 全体としてheap上のすべてのオブジェクトを指す ι：C の interpretation function 各 arity k の predicate　p　に対して ι(p): Uk →{0,1/2,1}　

Representing Abstract configuration (5) arity k の predicate p(v1,…,vk) に対して、individual u1,…uk ∈ U を代入したときの値 p(u1,…uk) = 0 individual u1,…uk が表す、全てのオブジェクト に対して、p が成り立たない、ということを表す p(u1,…uk) = 1 individual u1,…uk が表す、全てのオブジェクト に対して、p が成り立つ、ということを表す p(u1,…uk) = 1/2 individual u1,…uk が表すあるオブジェクトに対しては、p は成り立ち、また他のあるオブジェクトに対しては、p は成り立たない,もしくは、不明 を表す

Abstract Configuration グラフ Abstraction Configuration C=<U,ι> も有効グラフとして表現できる Uの中の各 individual を、ノードとして表現 summery node は点線で 成り立っている predicate を書く arity 1 の predicate なら、ノードの中に (1/2ならそれを明記） arity 2 の predicate p(u1,u2) なら、u1 から u2 へ有効辺(1/2なら点線で）を引き、その有向辺に

Configurationグラフの例 rvalue[next] rvalue[head] rvalue[next] <u1> r_by[next] <u2> r_by[next] <u0> r_by[head] <q> r_by[this] rvalue[tail] rvalue[next] rvalue[this] rvalue[this] <m1> r_by[x_i] <u3> r_by[next] <prd> is_thread at[lp_6] held_by rvalue[this] <a2> is_thread at[la_1] rvalue[next] blocked <cns> is_thread at[lt_1] <u4> r_by[next] r_by[tail] <a1> is_thread at[la_1] <a1> is_thread at[la_1] rvalue[this]

Abstract Configurationグラフの例 rvalue[next] <u> r_by[next] rvalue[next] rvalue[head] <u0> r_by[this] rvalue[next] <q> r_by[this] rvalue[tail] <u4> r_by[next] r_by[tail] rvalue[this] held_by <prd> is_thread at[lp_6] rvalue[this] rvalue[this] ここからでも　RW　WW　がわかるということを述べる blocked rvalue[this] <m1> r_by[x_I] <cns> is_thread at[lt_1] <a> is_thread at[la_1]

Embedding (1) Configuration(concrete configuration) CN と abstract configuration C の関係 CN の universe のなかの individual の幾つかをまとめて、C のなかの一つの individual にする。 しかし、そうすることで、各 predicate の評価があいまいになっていく(1/2 と評価されるものが多くなっていく）

Embedding (2) C=<U,ι>, C’=<U’,ι’> に対して 　全射 f : U → U’ が次の条件を満たすとき、 f は、C を C’ に埋め込む、埋め込み写像という 全ての predicate p(v1,…,vk), u1,…,uk ∈ U に対して，次のどちらかが成り立っている。 ι(p(u1,…,uk )) = ι’(p(f(u1),…,f(uk)) ι’(p(f(u1),…,f(uk)) = 1/2

Embedding (3) C=<U,ι>, C’=<U’,ι’> に対して、埋め込み写像 f : U → U’ が存在するとき、C’ は C を表すといい、次のように記す 　　 C ⊂ C’

Abstract semantics (1) Action ac によって、 C =<U,ι> が C’ =<U,ι’> に 書き換えられる(C ⇒ac C’) とは、以下を満たすようなconcrete configuration CN,CN’ が存在することを言う C ⇒ac C’ ∪　　　　∪ CN ⇒ac CN’

Abstract semantics (2) 実装上では、focus,coerce というオペレーションによって、次のような形で、abstract configuration の書き換えを行う (M. Sagiv, T. Reps, and R. willhelm. Parametric shape analysis via 3-valued logic.In Sympo. On Popl 99) {C} ⇒ac 　 {C’} ↓focus　　　　 　　　　　∪ ↓focus　　　 {C’1,..,C’k} ↓focus　　　　 ↑coerce {Cf1,..,Cfk} ⇒ac {Co1,..,Cok}　　 canonical abstraction

Abstract semantics (3) Abstract configuration を 必要なところまで、concretization するのには focus というオペレーションを使う abstract configuration の集合 XS に対して maximal(XS) = XS-{C∈XS|∃C’∈XS:C⊆C’ and C’⊆C} focus_{φ}(C) = maximal({C’|C’は3-value logical structure, C’⊆C, 全ての代入 Z に対して 【φ】 (Z)≠1/2} C’ 3

Abstract semantics (4) focus_{φ}(C) は、式φをどのような代入に関しても必ず確定した値（0,1）で評価する、C が表すconfigurationの中で、他のそのようconfigurationのどれかで表されないもの(configuration)の集合 action の precondition, predicate-update をφ として適用、φに関して確定値をとるので、 ⇒ac が定義できる

Abstract semantics (5) coerce オペレーション は、forcus オペレーションの結果得られた configuration の集合に対して、修正をおこなう 抽象化されている部分（値1/2 とか summary node) を、論理的に決定できることがある、それを決定して、値0,1 などにする

Abstract semantics (6) 実装上では、focus,coerce というオペレーションによって、次のような形で、abstract configuration の書き換えを行う {C} ⇒ac 　 {C’} ↓focus　　　　 　　　　　　∪ ↓focus　　　 {C’1,..,C’k} ↓focus　　　　 ↑coerce {Cf1,..,Cfk} ⇒ac {Co1,..,Cok}　　 canonical abstraction

Abstract semantics (7) unbounded number の スレッドが、オブジェクト u を指し、ロックしようとしている状態のconfiguration は次のように表すことができる <s_t> at[la_1] is_thread rvalue[this] <u>

Abstract semantics (8) あるスレッドが lock(v) action を起こそうとすると forcus オペレーションによって，次が得られる <s_t> at[la_1] is_thread <u> rvalue[this] <u> <s_t_0> at[la_1] is_thread rvalue[this] <s_t_1> at[la_1] is_thread rvalue[this]

Abstract semantics (9) 各 configuration で action lock(v) v→u をおこして held_by <s_t> at[la_2] is_thread <u> rvalue[this] rvalue[this] <u> <s_t_0> at[la_1] is_thread rvalue[this] <s_t_1> at[la_2] is_thread held_by

Abstract semantics (１０) Embedding を行って(arity 1 の predicate が同じindividual　をまとめるかたちで) action の結果のconfiguration として次を得る <s_t> at[la_1]=1/2 at[la_2]=1/2 is_thread rvalue[this] <u> held_by

まとめ Java の concurrent モデル の部分に対して、安全性を検証するための フレームワークを与えている このフレームワークではunbound number の スレッドやオブジェクトを扱うことができる

Reference (1) M. Sagiv, T. Reps, and R. willhelm. Parametric shape analysis via 3-valued logic.In Symp.on Princ. of Prog.Lang 99 P. Couston and R. Cousot Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fix point .In Symp.on Princ. of Prog.Lang., page238-252, New york, NY, 1977.ACM press

Reference (2) T. Lev-Ami and M. Sagi. TVLA: A framework for Kleene based static analysis . In SAS’00, static analysis Symposium. Springer, 2000. Available at http://www.math.tau.ac.il/~tau