SPINのatomicの使い方

http://spinroot.com/spin/Man/atomic.htmlの和訳です。

名前

atomic - 不可分に実行されるべきコード片を定義する。

文法

atomic { sequence }

効果

意味論的モデル(semantics model)において、atomicシーケンス内では、その最後以外の文が実行されたときの副作用として、グローバルのシステム変数(global system variable)を実行中のプロセスの実体化番号に限定する。これにより、実行の排他的特権を保護する。

説明

もし、文の並びが括弧で囲われていてatomicキーワードが前置されていれば、この文の並びが他のプロセスとインターリーブされない1つの不可分な単位として実行されるべきことを表す。プロセスをインターリーブして実行しようとするとき、atomicシーケンスの最初の文が実行された瞬間から最後の文が完了するまで、他のどのプロセスも文を実行できない。シーケンスは任意のPromela文を含むことができるし、非決定的で構わない。

もしatomicシーケンス内の文がブロック状態になる場合には、アトミック性は失われ、他のプロセスは文を実行し始めることが許される。そのブロックした文が再び実行可能になったとき、そのatomicシーケンスはいつでも実行再開でき、即座に再開される必要はない。プロセスがそのatomicシーケンスの残りを実行再開する前に、まずそのプロセスはシステムの他のすべてのアクティブプロセスと競合してコントロールを得ねばならない。すなわち、まずそのプロセスは実行できるようにスケジューリングしてもらわなければならない。

もしatomicシーケンスが同期(rendezvous)送信の文を含んでいる場合、同期通信(rendezvous)のハンドシェイクが成功したときに送信者から受信者にコントロールが移る。非決定的プロセスインターリーブの通常のルールの下では、コントロールはしばらくしてから送信者に戻り、そしてatomicシーケンスの残りの実行を続けることが許可される。ただし、同期通信(rendezvous)のハンドシェイクがatomicシーケンスの内側で受信されるという特別な場合には、アトミック性も同期通信(rendezvous)のハンドシェイクを通じて渡されることになり、割り込まれない (他のプロセスがそのとき実行の排他的特権を持っている場合を除く)。

atomicシーケンスはPromela文が使えるところならどこでも使うことができる。atomicシーケンスの最初の文は、そのシーケンスの「ガード」と呼ばれ、シーケンスがいつ開始されるかを決定する。よい方法ではないが、goto文を使ってatomicシーケンスの中にジャンプすることもできるし、シーケンスの外にジャンプすることもできる。シーケンスの中にジャンプした後、そのプロセスがコントロールを得たとき、ジャンプした先の文が実行可能な場合には、アトミックな実行が始まる。シーケンスの外にジャンプした後、ジャンプ先もatomicシーケンスの中になければ、アトミック性は失われる。

例示

atomic {	/* swap the values of a and b */
	tmp = b;
	b = a;
	a = tmp
}

この例では、割り込まれずに文の並びが実行され、2つの変数a, bの値が入れ替わる。内部のすべての文が常に無条件に実行可能な文なので、この実行はブロックされない。

次の例は、非決定的なatomicシーケンスである。

atomic {
	if
	:: a = 1
	:: a = 2
	fi;
	if
	:: b = 1
	:: b = 2
	fi
}

この例では、他のプロセスから邪魔され得ない文によって、変数a, bにある単一の値が代入される。このatomicシーケンスの実行のされ方は4通りあり得る。

同期通信(rendezvous)演算を使ってコントロールを渡しあうことによって、2つ以上のプロセスを交互に実行できるので、グローバルでアトミックな実行の連鎖を作ることが可能である。

chan q = [0] of { bool };
active proctype X() { atomic { A; q!0; B } }
active proctype Y() { atomic { q?0 -> C } }

この例では、例えば、プロセスXの、Aというプログラムブロックから実行を始めることができる。同期通信(rendezvous)のハンドシェイクが実行されるとき、アトミック性はプロセスYに移り、Cというブロックが実行開始する。それが終わると、コントロールはXに戻り、そしてBというブロックがアトミックに実行される。

一連のプロセスを開始する際、それらすべてが初期化されるまでどのプロセスでも文が実行され始めないようにしたいとき、atomicシーケンスを使うとうまくいくことが多い。

atomic {
	run A(1,2);
	run B(2,3);
	run C(3,1)
}

注記

atomicシーケンスは検証の複雑さを軽減するために使うことができる。

もし無限ループが誤ってatomicシーケンスに含まれてしまった場合でも、検証器はそのサイクルを常に認識できるとは限らない。デフォルトの深さ優先探索モードでは、そのような無限サイクルがあると最終的には深さの上限を突破してしまい、ループを中断してしまう。だが、幅優先探索モードでは、この種の無限サイクルが検出できる。当然、無限サイクルがatomicシーケンスに現れると、そのatomicシーケンスは現実の実装ではどうやってもアトミックに実行できないので、それはエラーである。

Promelaのd_stepシーケンスは、atomicシーケンスより遥かに効率的に検証器によって実行されうるが、非決定性を許さない。