コマンドキューをもつシステムのAlloyモデル

形式手法 Alloy

とあることがきっかけで、コマンドキューをもつシステムをAlloyでモデル化し検証したので、ここで紹介します。

問題

あるシステムのミドルウェアを修正することになりました。このミドルウェアは整数値をやり取りするオブジェクトを複数所有します。インタフェースは以下の通りです。

  • assign(v) 　　// オブジェクトの値をvに上書きします。
  • copy(obj) 　　// オブジェクトobjの値をコピーします。
  • getValue()　　// オブジェクトの値を取得します。

このミドルウェアを実装するためにライブラリを使用しています。このライブラリはオブジェクトを複数所有しています。各オブジェクトはキューを持ち、コマンドをキューに積んでから実行する必要があります。コマンドは2種類あります。

  • assign(v)コマンドは、値の上書きする。
  • copy(obj)コマンドは、オブジェクトobjの値をコピーする。

キューに積んだコマンドを実行するときはライブラリの関数

  • execute()

を呼びます。executeを呼ぶとキューに積まれた順番にコマンドを実行します。オブジェクトの値は、これまたライブラリの関数

  • get()

でいつでも（同期で）読みだせます。

当初の実装は以下のように、コマンドをひとつ積むたびにexecute()を呼びだすようになっていました。

void assign(int v)
{
    add_command(make_command(assign, v));
    execute();
}

しかしexecuteに時間がかかっていたので、なるべくコマンドをためてからexecuteをするように改良しようとなりました。

はじめは思いついたままに実装してテストをしていたのですが、テストの種類を増やすとうまくいかないものがぽつぽつ見つかるという状態が続いたので、Alloyで検証することにしました。以下では、モデルを検証しながらインクリメンタルに作った過程を再現します。

状態モデル

まずは、値、コマンド、オブジェクトをモデル化します。コマンドキューを表すのには seq を使いました。後々検査で使うために、オブジェクトが保持する値は、実際の値（real）と期待値（expexted）のふたつにします。

module CommandQueue

abstract sig Value {}
one sig Zero, One, Two extends Value {} 

abstract sig Command {}

sig Copy extends Command {
    src : one Object
}

sig Assign extends Command {
    v : one Value    
}

sig Object {
    expected : one Value,
    real : one Value,
    q : seq Command
}

pred show() {}
run show for 3 but exactly 1 Object

オブジェクトの数をひとつに制限して、[Execute]、[Show] の順番に実行します。以下のようなインスタンスが見つかりました。

[Next]を押して次々に出てくるインスタンスを確認します。想定外のインスタンスが見つからないので、ここまでは正しそうです。

assignとcopyを追加する

次に、assignコマンドとcopyコマンドをキューに積む操作を追加します。まずは、状態の変化を表すためにTimeシグネチャのorderingを導入します。

open util/ordering[Time] as to
sig Time {}

時間で変化する属性をTimeとの関係にします。

sig Object {
	expected : Value one -> Time,
	real : Value one -> Time,
	q : (seq Command)-> Time
}

時間変化をTimeを右側に持ってきた関係で表すので、多重度をシグネチャの右側に移動させます。コマンドキューが時間によって変化するので、seq Command 全体を括弧で囲みます。
assignコマンドは述語で表します。t が事前、t' が事後の時点を表します。この時点では期待値（expected）だけ変更し、実際の値は変更しません。

pred assign [t, t' : Time, obj : Object] {
     some assign : Assign | obj.q.t' = (obj.q.t).add[assign] and obj.expected.t' = assign.v and noChangeRealValue[t, t', obj]
}

述語 noChangeRealValue は以下の通り。いろんなところで使いまわしそうなのでひとつの pred として切りだしました。

pred noChangeRealValue [t, t' : Time, obj : Object] {
	obj.real.t' = obj.real.t
}

copyコマンドもほぼ同様です。

pred copy [t, t' : Time, obj : Object] {
     some cp : Copy | obj.q.t' = (obj.q.t).add[cp] and obj.expected.t' = cp.src.expected.t and noChangeRealValue[t, t', obj]
}

最後にこのシステムがとり得る状態遷移空間をfactで指定します。状態遷移空間は、初期状態から assign または copy コマンドによって遷移できる空間です。

pred init [t : Time] {
	all obj : Object | (no obj.q.t and obj.real.t = obj.expected.t)
}

pred noChangeAll [t, t' : Time, obj : Object] {
	obj.expected.t' = obj.expected.t
	obj.real.t' = obj.real.t
	obj.q.t' = obj.q.t
}

fact step {
	init[to/first[]]
	all t : Time - to/last[] | let t' = to/next[t] |
		one obj : Object |     // (a)
			(assign[t, t', obj]
			or copy[t, t', obj])
			and (all obj' : Object | obj' != obj => noChangeAll[t, t', obj'])  // (b)
}

fact step の (a) で one obj : Object、および (b) で (all obj' : Object | ...) としているのは、1ステップで状態遷移するオブジェクトをひとつに限定するためです。そうしておくとVisializeしたときに何が起きたか分かりやすくなります。ただし、同じTimeインスタンス数では、同時に複数遷移するモデルに比べて探索できる空間が狭くなるので、見つかってほしい反例が見つかりにくくなります。
今度はObjectのインスタンス数を 2 にして[Show]してみます。

pred show() {}
run show for 3 but exactly 2 Object

妙なインスタンスが見つからないので、ここまでは正しそうです。

executeを追加する

execute も述語で表します。

pred execute [t, t' : Time, obj : Object] {
     isEmpty[obj.q.t']
     let command = last[obj.q.t] {
		(command in Assign) => (obj.real.t' = command.v and obj.expected.t' = obj.expected.t)
		(command in Copy) => (obj.real.t' = command.src.real.t and  obj.expected.t' = obj.expected.t)
	}
}

これは、「キューは空で、キューの最後に積まれているのが assign だったら execute 後の real は expexted と同じ。copy だったら src の real と同じ。かつ、expected は変化しない。」です（察しのいい人は気付くと思いますが、これは間違っています）。
次に、fact step に execute を追加します。

fact step {
	init[to/first[]]
	all t : Time - to/last[] | let t' = to/next[t] |
		one obj : Object | 
			(assign[t, t', obj]
			or copy[t, t', obj]
			or execute[t, t', obj])
			and (all obj' : Object | obj' != obj => noChangeAll[t, t', obj'])
}

最初のモデル ー get前にexecuteする ー

一応、これで準備は整いました。では、executeの回数を減らした新しいミドルウェアの振る舞いを考えて、それを検証したいと思います。最初に考えたのは、以下のようにassignやcopyのメソッド内でexecuteを一切呼ばないことにして、getValueが呼ばれたときにgetする前にexecuteするようにしたらどうかと考えました。

void assign(int v)
{
    add_command(make_command(assign, v));
//    execute(); // <- 毎回呼ぶのを止める
}

int getValue()
{
    execute(); // <- get前に一度だけ呼ぶように。
    return get();
}

これはいつでもexecuteを呼べば、そのあとは正しい値を取得できるということを根拠にしています。よって、このことをアサートで検査してみます。execute 後は期待値と実際の値が一致するというアサートは以下のように書けます。

assert RealValueEqualsExpectedAfterExecute {
	all t : Time - to/last[] | let t' = to/next[t] |
		all obj : Object | 
			execute[t, t', obj] => obj.real.t' = obj.expected.t'
}
check RealValueEqualsExpectedAfterExecute for 3 but exactly 1 Object, 4 Time, 4 seq

まずはオブジェクト1個に限定して、[Execute]メニューからアサートを選んで実行します。そうすると以下のような反例が見つかります。

  1. 初期状態は、Object.real = Object.expected = Two
  2. Object.assgin(Zero). Object.real = Two, Object.expected = Zero
  3. Object.copy(Object). Object.real = Two, Object.expected = Zero
  4. Object.execute. Object.real = Two, Object.expected = Zero

これは、初期状態から、assign, copy(自分自身), execute と進んだ場合、assign で代入した値が無視されて期待値と実際の値が異なることを示しています。実際のシステムは execute した場合、キューのコマンドを順番に実行するわけですから、キューの先頭に入っている assign を実行した時点で期待値と実値が一致します。よって、そのあとに copy を実行すれば、copy 後も期待値と実値は一致します。ということは、execute のモデルが間違っていると言えます。

executeを修正する

では、executeを修正しましょう。今回は素朴にキューのすべてのコマンドをひとつずつ実行するように修正します。「ひとつずつ実行する」といっても、Alloyではループや再帰呼び出しを書けません。そこで、コマンドひとつを実行するたびにひとつ時点を進めるようにします。つまり、ある時点 t でコマンドキューに assign, copy と積まれていた状態で execute すると、t の次の時点(これを t' とします)ではassign実行後の状態、t' の次の時点ではcopy実行後の状態に遷移するとします。実際のシステムでは、execute はアトミックに実行されます。よって、モデル上でも execute しはじめたらキューが空になるまでの間はコマンドの追加できないようにします。これを実現するためにモデルに状態を表す変数を追加します。

sig State {}
one sig InitDone, AssignAdded, CopyAdded, Executing, ExecuteDone extends State {}

sig Object {
	expected : Value one -> Time,
	real : Value one -> Time,
	q : (seq Command)-> Time,
	state : State one -> Time
}

noChangeAll にも state の項を追加します。

pred noChangeAll [t, t' : Time, obj : Object] {
	obj.expected.t' = obj.expected.t
	obj.real.t' = obj.real.t
	obj.q.t' = obj.q.t
	obj.state.t' = obj.state.t
}

初期状態を InitDone にします。

pred init [t : Time] {
	all obj : Object | (no obj.q.t and obj.real.t = obj.expected.t and obj.state.t = InitDone)
}

Executing状態の間は assign, copy コマンドが実行できないように pred に事前条件を追加します。加えて、事後の状態をそれぞれAssignAdded, CopyAddedにします。

pred assign [t, t' : Time, obj : Object] {
     no obj' : Object | obj'.state.t = Executing // pre-condition 
     some assign : Assign { 
     	  obj.q.t' = (obj.q.t).add[assign]
	  obj.expected.t' = assign.v
	  noChangeRealValue[t, t', obj]
	  obj.state.t' = AssignAdded
     }
}

pred copy [t, t' : Time, obj : Object] {
     no obj' : Object | obj'.state.t = Executing // pre-condition 
     some cp : Copy { 
     	  obj.q.t' = (obj.q.t).add[cp]
	  obj.expected.t' = cp.src.expected.t
	  noChangeRealValue[t, t', obj]
	  obj.state.t' = CopyAdded
    }
}

次にキューの先頭にあるコマンドをひとつだけ実行する pred を書きます。

pred executeCommand [t, t' : Time, obj : Object] {
     let command = first[obj.q.t] {
		(command in Assign) => (obj.real.t' = command.v and obj.q.t' = rest[obj.q.t] and obj.expected.t' = obj.expected.t)
		(command in Copy) => (obj.real.t' = command.src.real.t and obj.q.t' = rest[obj.q.t] and obj.expected.t' = obj.expected.t)
		(isEmpty[obj.q.t'] => obj.state.t' = ExecuteDone) and (not isEmpty[obj.q.t'] => obj.state.t' = Executing)
	}
}

executeCommand を使うと execute 時にひとつだけコマンドを実行する pred は以下のように書けます。

pred execute [t, t' : Time, obj : Object] {
	some q.t // pre-condition
	no obj : Object | obj.state.t = Executing // pre-condition 
	executeCommand[t, t', obj]
}

execute 時にキューにふたつ以上のコマンドがある場合は、続けて残りのコマンドをする必要があります。それも pred で表します。

pred executeRest [t, t' : Time, obj : Object] {
  	 obj.state.t = Executing // pre-condition
	 executeCommand[t, t', obj]			    	  
}

あとは fact step に executeRest を追加するだけです。

fact step {
	init[to/first[]]
	all t : Time - to/last[] | let t' = to/next[t] |
		one obj : Object |
			(assign[t, t', obj]
			or copy[t, t', obj]
			or execute[t, t', obj]
			or executeRest[t, t', obj])
			and (all obj' : Object | obj' != obj => noChangeAll[t, t', obj'])
}

アサートはstateを使って以下のように書きなおします。

assert RealValueEqualsExpectedAfterExecute {
	all t : Time |
		all obj : Object | 
			obj.state.t = ExecuteDone => obj.real.t = obj.expected.t
}
check RealValueEqualsExpectedAfterExecute for 3 but exactly 1 Object, 4 Time, 4 seq

再びアサートをチェックします。

No counterexample found. Assertion may be valid. 16ms.

オブジェクトがひとつの場合だと反例は見つからないようです。では少しスコープを広げてみます。

check RealValueEqualsExpectedAfterExecute for 3 but exactly 2 Object, 4 Time, 4 seq

すると、

Counterexample found. Assertion is invalid. 62ms.

今度は反例が見つかりました。[Show]で確認すると以下のシーケンスで違反があることが分かりました。

  1. 初期状態は、Object0.real = Object0.expected = Zero, Object1.real = Object1.expected = Two
  2. Object0.assgin(One). Object0.real = Zero, Object0.expected = One
  3. Object1.copy(Object0). Object1.real = Two, Object1.expected = One (= Object0.expected )
  4. Object1.execute. Object1.real = Zero, Object1.expected = One

これは、Object1 のキューに入っている copy を実行する前にコピー元となっている Object0 の assgin を実行していないためです。どうやらget前にexecuteするだけでは不十分なようです。

2番目のモデル ー コピー元をexecuteする ー

上記の反例では、コピー時のコピー元の値が期待値と実値で一致していないことが原因だったので、以下のような、copyコマンドをキューに積むときには、コピー元のオブジェクトをexecuteする実装を考えました。

void copy(Object obj)
{
    obj->execute();  // <- コピー元のexecuteを呼ぶ
    add_command(make_command(copy, obj));    
}

fact を使って copy コマンドをキューに積む前に execute するようにします。こうするとcopyコマンドを積む前にexecuteが実行するパスしか検査しません。

fact ExecuteCopySrc {
	all t' : Time - to/first[] | let t = to/prev[t'] |
		all obj : Object | 
			(obj.state.t != CopyAdded && obj.state.t' = CopyAdded) => let command = last[obj.q.t'] {
				((command.src).state.t = ExecuteDone or (command.src).state.t = InitDone)
			}
}

では検査してみましょう。

assert RealValueEqualsExpectedAfterExecute {
	all t : Time |
		all obj : Object | 
			obj.state.t = ExecuteDone => obj.real.t = obj.expected.t
}
check RealValueEqualsExpectedAfterExecute for 3 but exactly 2 Object, 5 Time, 5 seq

以下のような反例が見つかりました。

  1. 初期状態は、Object0.real = Object0.expected = Two, Object1.real = Object1.expected = Zero
  2. Object1.copy(Object0). Object1.real = Zero, Object1.expected = Two (= Object0.expected )
  3. Object0.assgin(One). Object0.real = Two, Object0.expected = One
  4. Object0.execute. Object0.real = One, Object0.expected = One
  5. Object1.execute. Object1.real = One, Object1.expected = Two

これは、Object1 のキューに入っている copy を実行する前にコピー元となっている Object0 の値が 3, 4 で Object1 が execute する前に変更されたために起きた違反です。

3番目のモデル ー キューイングするのをひとつずつ ー

上記の反例は、キューに入ったコピー元がそのあとで値を変えてしまうために起きていました。そこで、上記の反例のシーケンスの 2 と 3 の間にも execute する方法を考えました。思いついたのは、新しくコマンドをキューに積むときに、最後にコマンドを積んだオブジェクトを異なる場合はキューに積む前に execute したらどうかというものです。コードにすると以下のような実装です。

void assign(int v)
{
    if (last != this) {
        last->execute(); // <- 最後にキューに積んだオブジェクトのexecuteを呼ぶ
    }
    add_command(make_command(assign, v));
    last = this;
}

そこでこれを fact で表して検証してみました。

pred addCommandAtThatTime [t : Time, obj : Object] {
	let before = to/prev[t] | #(obj.q.before) < #(obj.q.t)
}

fact ExecuteDoneBeforeChangingTarget {
	all disj obj1, obj2 : Object {
		all disj t1, t2 : Time - to/last[] {
			(to/lt[t1, t2] and addCommandAtThatTime[t1, obj1] and addCommandAtThatTime[t2, obj2]) implies {
				obj1.state.t2 = ExecuteDone
			}
		}
	}
}

これで検証すると反例は見つかりません。以下のように

check RealValueEqualsExpectedAfterExecute for 3 but exactly 9 Time, 7 seq

スコープを広げて検査してみましたが、反例が見つからないのでこのモデルは正しそうだと言えます。

おわりに

上記を実装して計測したところなかなかのパフォーマンスだったので以上で設計を終えることにしました。まだまだ改善の余地はありますが、必要十分ということで終えることにしました。

さて、どうだったでしょうか。テストでは自分が思いつくケースしかテストすることはできませんが、Alloyならば（限られたスコープですが）網羅的に検査してくれます。これがテストとモデル検査との大きな違いです。

Alloyの威力が少しでも伝えればいいのですが。

※今回使用したモデルはgithubにあります。
https://github.com/masateruk/blog/tree/master/20111020