好的，所以我正在尝试在Promela中对CLH-RW锁进行建模。
锁的工作方式很简单，真的：
队列由一个tail组成，读取器和写入器都对包含单个节点的节点进行排队，bool succ_must_wait他们通过创建一个新节点并使用tail对其进行CAS来执行此操作。
因此，尾部成为节点的前身，pred。
然后他们旋转等待pred.succ_must_wait直到它false.
读取器首先递增读取器计数器ncritR，然后将自己的标志设置为false，允许多个读取器同时在关键部分。释放读锁只是意味着再次降低ncritR。
编写器等到ncritR达到零，然后进入关键部分。在释放锁之前，他们不会将标志设置为false。
不过，我有点难以在 promela 中建模。
我目前的尝试(见下文)尝试使用数组，其中每个节点基本上由许多数组条目组成。
此操作失败，因为假设A将自身排队，然后B将自身排队。然后队列将如下所示：
S <- A <- B
其中S是哨兵节点。
现在的问题是，当A运行到完成并重新排队时，队列将看起来像
S <- A <- B <- A'
在实际执行中，这绝对没问题，因为A和A'是不同的节点对象。而且由于A.succ_must_wait在A首次释放锁时就被设置为false，B最终会取得进展，因此A'最终会取得进展。
但是，在下面基于数组的 promela 模型中发生的情况是，A和A'占据相同的阵列位置，导致B错过了A释放锁的事实，从而产生了一个死锁，其中B(错误地)等待A'而不是A，而A'正在(正确)等待B。
对此的一个可能的"解决方案"可能是让A等到B确认发布。但这并不符合锁的工作方式。
另一个"解决方案"是等待pred.succ_must_wait的变化，其中版本将增加succ_must_wait，而不是将其重置为0。
但是我打算对锁的一个版本进行建模，其中pred可能会发生变化(即可以允许节点忽略其某些前辈)，并且我不完全相信像增加版本这样的东西不会导致此更改出现问题。
那么，在 promela 中对这样的隐式队列进行建模的"最聪明"方法是什么？
/* 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
}
首先，一些注意事项：
-
你不需要初始化你的变量来
0，因为：所有变量的默认初始值为零。
请参阅文档。
-
您不需要将单个指令包含在
atomic {}语句中，因为任何基本语句都是以原子方式执行的。为了提高验证过程的效率，应尽可能改用d_step {}。在这里，您可以找到有关该主题的相关堆栈溢出问答。 -
当以下两个条件之一成立时，
init {}保证具有_pid == 0：- 未声明
active proctype init {}在源代码中出现的任何其他active proctype之前声明
活动进程(包括
init {})按源代码中出现的顺序生成。所有其他进程都按相应run ...语句的出现顺序生成。 - 未声明
我在您的模型上发现了以下问题：
-
指令
pred[_pid] = 0是无用的，因为该内存位置仅在分配pred[_pid] = tail之后读取 -
释放节点的后继节点时，
succ_must_wait[_pid]设置为仅0，并且不会使后续节点实例失效。这是您在问题中确定但无法解决的问题。我建议的解决方案是添加以下代码：pid j; for (j: 1..4) { if :: pred[j] == _pid -> pred[j] = 0; :: else -> skip; fi }这应该包含在一个
atomic {}块中。 -
当您发现刚刚离开关键部分的节点也是队列中的
last节点时，您正确地将tail设置回0。您还可以正确地将此操作包含在atomic {}块中。但是，当您即将进入此atomic {}块时，可能会发生以下情况：仍在某种空闲状态下等待的其他进程决定执行初始原子块并将当前值tail(对应于刚刚过期的节点)复制到他自己的pred[_pid]内存位置。如果现在刚刚退出关键部分的节点尝试再次加入它，将自己的值succ_must_wait[_pid]设置为1，您将在进程之间得到另一个循环等待实例。正确的方法是将此部分与发布后续版本的代码合并。
以下内联函数可用于释放给定节点的后继节点：
inline release_succ(i)
{
d_step {
pid j;
for (j: 1..4) {
if
:: pred[j] == i ->
pred[j] = 0;
:: else ->
skip;
fi
}
succ_must_wait[i] = 0;
if
:: tail == _pid -> tail = 0;
:: else -> skip;
fi
}
}
完整模型如下：
byte ncritR;
byte ncritW;
byte tail;
bool succ_must_wait[5];
byte pred[5];
init
{
skip
}
inline release_succ(i)
{
d_step {
pid j;
for (j: 1..4) {
if
:: pred[j] == i ->
pred[j] = 0;
:: else ->
skip;
fi
}
succ_must_wait[i] = 0;
if
:: tail == _pid -> tail = 0;
:: else -> skip;
fi
}
}
active [2] proctype reader()
{
loop:
succ_must_wait[_pid] = 1;
d_step {
pred[_pid] = tail;
tail = _pid;
}
trying:
(succ_must_wait[pred[_pid]] == 0)
ncritR++;
release_succ(_pid);
// critical section
progress_reader:
assert(ncritR > 0);
assert(ncritW == 0);
ncritR--;
goto loop;
}
active [2] proctype writer()
{
loop:
succ_must_wait[_pid] = 1;
d_step {
pred[_pid] = tail;
tail = _pid;
}
trying:
(succ_must_wait[pred[_pid]] == 0) && (ncritR == 0)
ncritW++;
// critical section
progress_writer:
assert(ncritR == 0);
assert(ncritW == 1);
ncritW--;
release_succ(_pid);
goto loop;
}
我向模型添加了以下属性：
P0：
_pid等于4的编写器无限频繁地经历其进度状态，前提是它有机会无限频繁地执行某些指令：ltl p0 { ([]<> (_last == 4)) -> ([]<> writer[4]@progress_writer) };此属性应
true。P1：在关键部分永远不会有多个阅读器：
ltl p1 { ([] (ncritR <= 1)) };显然，我们希望此属性
false在符合您的规范的模型中。P2：在关键部分永远不会有一个以上的作者：
ltl p2 { ([] (ncritW <= 1)) };此属性应
true。P3：没有任何节点同时是另外两个节点的前身，除非该节点是节点
0：ltl p3 { [] ( (((pred[1] != 0) && (pred[2] != 0)) -> (pred[1] != pred[2])) && (((pred[1] != 0) && (pred[3] != 0)) -> (pred[1] != pred[3])) && (((pred[1] != 0) && (pred[4] != 0)) -> (pred[1] != pred[4])) && (((pred[2] != 0) && (pred[3] != 0)) -> (pred[2] != pred[3])) && (((pred[2] != 0) && (pred[4] != 0)) -> (pred[2] != pred[4])) && (((pred[3] != 0) && (pred[4] != 0)) -> (pred[3] != pred[4])) ) };此属性应
true。P4：每当
_pid等于4的编写器尝试访问关键部分时，它最终会到达那里，这是正确的：ltl p4 { [] (writer[4]@trying -> <> writer[4]@progress_writer) };此属性应
true。
验证结果符合我们的预期：
~$ spin -search -ltl p0 -a clhrw_lock.pml
...
Full statespace search for:
never claim + (p0)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 68 byte, depth reached 3305, errors: 0
...
~$ spin -search -ltl p1 -a clhrw_lock.pml
...
Full statespace search for:
never claim + (p1)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 68 byte, depth reached 1692, errors: 1
...
~$ spin -search -ltl p2 -a clhrw_lock.pml
...
Full statespace search for:
never claim + (p2)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 68 byte, depth reached 3115, errors: 0
...
~$ spin -search -ltl p3 -a clhrw_lock.pml
...
Full statespace search for:
never claim + (p3)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 68 byte, depth reached 3115, errors: 0
...
~$ spin -search -ltl p4 -a clhrw_lock.pml
...
Full statespace search for:
never claim + (p4)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 68 byte, depth reached 3115, errors: 0
...