使用远程 varrefs 时，自旋模型检查器未发现错误

Question

我正在尝试在以下Promela 模型 上正式验证互斥：

/* Mutex with (bugged) Peterson algorithm */

bool flag[2];
int turn = -1;

active [2] proctype agent() {
    bool in_cs;
    int other = 1 - _pid;

    do
        :: true ->

            /* trying section */
            turn = other;
            flag[_pid] = true;
            !( flag[other] && (turn == other));

            /* critical section */
            in_cs = true;
            printf("Agent %d in CS\n", _pid);
            in_cs = false;

            /* exit section */
            flag[_pid] = false;
    od;
}

ltl mutex { [] ! (agent[0]:in_cs && agent[1]:in_cs) }

为了验证它，我使用以下命令链：

~$ spin -a test.pml ; gcc -o run pan.c -DNOREDUCE ; ./run -a -N p1

打印以下输出：

...
Full statespace search for:
    never claim             + (mutex)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states      - (disabled by never claim)

State-vector 40 byte, depth reached 53, errors: 0
...

问：我知道 Promela 模型 不满足互斥，但 Spin 声称确实如此。为什么会这样？

注意： 我在使用 gcc 编译时添加了选项 -DNOREDUCE 因为 Spin 6.4.8 会打印一条警告消息，要求我这样做，如果我不要：

~$ spin -a test.pml ; gcc -o run pan.c ; ./run -a -N p1
...
pan.c: In function ‘main’:
pan.c:9478:3: warning: #warning p.o. reduction not compatible with remote varrefs (use -DNOREDUCE) [-Wcpp]
  #warning p.o. reduction not compatible with remote varrefs (use -DNOREDUCE)
   ^~~~~~~
...

Answer 1

解决方法如下：

The problem here is that to disable partial order reduction you not only have to compile with -DNOREDUCE but also generate the model while disabling statement merging (merging of subsequent local actions) -- which is also a partial order reduction strategy. So, for the second example you also get the counter-example if you do:
spin -o3 -a test.pml; gcc -DNOREDUCE -o pan pan.c; ./pan -a
[G. H., private communication]

建议解决方案的输出符合我们的预期：

~$ spin -o3 -a test.pml ; gcc -o run pan.c -DNOREDUCE ; ./run -a -N p1
...
pan:1: assertion violated  !( !( !((agent[0].in_cs&&agent[1].in_cs)))) (at depth 55)
pan: wrote test.pml.trail

...

Full statespace search for:
    never claim             + (mutex)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 40 byte, depth reached 69, errors: 1
...

或者，可以通过使用标签远程引用而不是变量远程引用来解决这个问题，例如:

/* Mutex with (bugged) Peterson algorithm */

bool flag[2];
int turn = -1;

active [2] proctype agent() {
    int other = 1 - _pid;

    do
        :: true ->

            /* trying section */
            turn = other;
            flag[_pid] = true;
            !( flag[other] && (turn == other));

            /* critical section */
cs:
            printf("Agent %d in CS\n", _pid);

            /* exit section */
            flag[_pid] = false;
    od;
}

ltl mutex { [] ! (agent[0]@cs && agent[1]@cs) }

有了这个模型，我们找到了一个反例，正如预期的那样：

~$ spin -search test.pml
...
pan:1: assertion violated  !( !( !(((agent[0]._p==cs)&&(agent[1]._p==cs))))) (at depth 28)
pan: wrote test.pml.trail
...

使用远程 varrefs 时，自旋模型检查器未发现错误

Spin Model Checker does not find a bug when using remote varrefs

model-checking

spin

promela