これでPromelaでCLH-RW lockをモデル化しようとしています。プロメラのキューをモデル化する方法は？
ロックの仕組みはシンプルです、本当に：
キューは、リーダーとライターの両方が、新しいノードとCAS-INGを作成することによって、彼らがそうする単一bool succ_must_waitを含むノードをエンキューするtail、で構成されていそれはtailです。
これにより、テールがノードの先行ノードpredになります。
次に、でスピンウェイトがfalseになるまで待ちます。
リーダーは、最初にリーダーカウンタncritRをインクリメントしてから、自分のフラグをfalseに設定し、同時にクリティカルセクションの複数のリーダーを許可します。読み取りロックを解除するとは、単にncritRをデクリメントすることを意味します。
ライターはncritRがゼロになるまで待ってから、クリティカルセクションに入ります。ロックが解除されるまで、フラグはfalseに設定されません。
私はプロメラでこれをモデル化するのに苦労しています。
私の現在の試み（下記参照）は、配列を使用しようとします。各ノードは、基本的にいくつかの配列エントリで構成されています。
これは、Aがエンキューしたとすると、B自体がエンキューするため、失敗します。その後、キューは次のようになります。Sは、センチネルリンパ節をある
S <- A <- B
を。今
問題がときA完全性実行され、再エンキュー、キューは実際の実行で
S <- A <- B <- A'
のように見えるだろうということ、であるAとA'が別個のノードオブジェクトであるため、これは絶対に大丈夫です。 Aが最初にロックを解除したときにA.succ_must_waitがfalseに設定されているため、最終的にはBが処理を進めるため、最終的に処理が進まなくなります。
以下のアレイベースのPROMELAモデルでは何が起こる、しかし、誤って（AとA'が、それによってBがあるデッドロックを作成し、Aがロックをリリースしたことを欠場するBを引き起こして、同じ配列位置を占めていることです）A'の代わりにAとA'が待っています（正確にはB）。
この可能性のある「解決策」は、がBが承認を待つまで待つことができます。しかし、それはロックの仕組みには当てはまりません。
もう1つの解決策は、変更が0にリセットされるのではなく、succ_must_waitが増分されるpred.succ_must_waitの変更を待つことです。
しかし、増加バージョンwouldnのようなものを私は（つまり、ノードは、前任者の一部を無視させることができる場合）predが変更される可能性があり、ロックのバージョンをモデル化しようとするんだ、と私は完全に確信していませんこの変更の問題を引き起こしません。
プロメラで暗黙のキューをモデル化する "賢明な"方法は何でしょうか？すべての
/* CLH-RW Lock */
/*pid: 0 = init, 1-2 = reader, 3-4 = writer*/
ltl liveness{
([]<> reader[1]@progress_reader)
&& ([]<> reader[2]@progress_reader)
&& ([]<> writer[3]@progress_writer)
&& ([]<> writer[4]@progress_writer)
}
bool initialised = 0;
byte ncritR;
byte ncritW;
byte tail;
bool succ_must_wait[5]
byte pred[5]
init{
assert(_pid == 0);
ncritR = 0;
ncritW = 0;
/*sentinel node*/
tail =0;
pred[0] = 0;
succ_must_wait[0] = 0;
initialised = 1;
}
active [2] proctype reader()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
succ_must_wait[_pid] = 1;
atomic {
pred[_pid] = tail;
tail = _pid;
}
(succ_must_wait[pred[_pid]] == 0)
ncritR++;
succ_must_wait[_pid] = 0;
atomic {
/*freeing previous node for garbage collection*/
pred[_pid] = 0;
}
/*CRITICAL SECTION*/
progress_reader:
assert(ncritR >= 1);
assert(ncritW == 0);
ncritR--;
atomic {
/*necessary to model the fact that the next access creates a new queue node*/
if
:: tail == _pid -> tail = 0;
:: else ->
fi
}
od
}
active [2] proctype writer()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
succ_must_wait[_pid] = 1;
atomic {
pred[_pid] = tail;
tail = _pid;
}
(succ_must_wait[pred[_pid]] == 0)
(ncritR == 0)
atomic {
/*freeing previous node for garbage collection*/
pred[_pid] = 0;
}
ncritW++;
/* CRITICAL SECTION */
progress_writer:
assert(ncritR == 0);
assert(ncritW == 1);
ncritW--;
succ_must_wait[_pid] = 0;
atomic {
/*necessary to model the fact that the next access creates a new queue node*/
if
:: tail == _pid -> tail = 0;
:: else ->
fi
}
od
}