Spin Verification，验证变量达到某个值

Question

这是我在 Stack Exchange 上的第一个问题，所以如果有任何违反准则的地方请告诉我。

我有一个用 Promela 为大学 OS 和并发系统 class 编写的程序。有两个进程运行递增变量 n。我们的任务是编写流程，然后使用 Spin 中的验证工具来证明 n 可以取值 4。我已经阅读了所有命令行参数并弄乱了但没有任何内容对我来说 "insert this modifier followed by a variable name to check all it's possible values."

byte n;

proctype p()
{
    byte countp = 0;
    byte temp;
    do
    :: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1;
    :: countp >= 2 -> break;
    od
}

proctype q()
{

    byte countq = 0;

    do
    :: countq != 2 -> n = n + 1; countq = countq + 1;
    :: countq >= 2 -> break;
    od
}

init
{
    run p();
    run q();
}

Answer 1

有几种方法可以做到这一点，但作为一名教师，我更喜欢基于 ltl 的方法，因为至少它表明你了解如何使用它。

监控进程。

从概念上讲，这是迄今为止最简单的：您只需添加一个随时断言 n != 4 的进程，然后检查该断言最终是否失败。

byte n;

active proctype p()
{
    byte countp = 0;
    byte temp;
    do
    :: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1;
    :: countp >= 2 -> break;
    od
}

active proctype q()
{

    byte countq = 0;

    do
    :: countq != 2 -> n = n + 1; countq = countq + 1;
    :: countq >= 2 -> break;
    od
}

active proctype monitor()
{
    do
        :: true -> assert(n != 4);
    od;
}

注意：monitor进程中的循环是完全没有必要的，但初学者更清楚其目的。

你可以用下面的一行来验证这个程序：

~$ spin -search -bfs buggy_01.pml

自旋在零时间找到反例：

Depth=10 States=56 Transitions=84 Memory=128.195    
pan:1: assertion violated (n!=4) (at depth 19)
pan: wrote buggy_01.pml.trail

(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
    + Breadth-First Search
    + Partial Order Reduction

Full statespace search for:
    never claim             - (none specified)
    assertion violations    +
    cycle checks            - (disabled by -DSAFETY)
    invalid end states      +

State-vector 28 byte, depth reached 19, errors: 1
      215 states, stored
             215 nominal states (stored-atomic)
      181 states, matched
      396 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.011       equivalent memory usage for states (stored*(State-vector + overhead))
    0.290       actual memory usage for states
  128.000       memory used for hash table (-w24)
  128.195       total actual memory usage

pan: elapsed time 0 seconds

您实际上可以检查违反断言的执行跟踪：

~$ spin -t -p -g -l buggy_01.pml

选项含义如下：

-t：重放自旋

.trail

-p: 打印所有语句
-g: 打印所有全局变量
-l: 打印所有局部变量

这是输出：

using statement merging
  1:    proc  2 (monitor:1) buggy_01.pml:27 (state 1)   [(1)]
  2:    proc  1 (q:1) buggy_01.pml:19 (state 1) [((countq!=2))]
  3:    proc  0 (p:1) buggy_01.pml:8 (state 1)  [((countp!=2))]
  4:    proc  1 (q:1) buggy_01.pml:19 (state 2) [n = (n+1)]
        n = 1
  5:    proc  1 (q:1) buggy_01.pml:19 (state 3) [countq = (countq+1)]
        q(1):countq = 1
  6:    proc  1 (q:1) buggy_01.pml:19 (state 1) [((countq!=2))]
  7:    proc  1 (q:1) buggy_01.pml:19 (state 2) [n = (n+1)]
        n = 2
  8:    proc  1 (q:1) buggy_01.pml:19 (state 3) [countq = (countq+1)]
        q(1):countq = 2
  9:    proc  1 (q:1) buggy_01.pml:20 (state 4) [((countq>=2))]
 10:    proc  0 (p:1) buggy_01.pml:8 (state 2)  [temp = n]
        p(0):temp = 2
 11:    proc  0 (p:1) buggy_01.pml:8 (state 3)  [temp = (temp+1)]
        p(0):temp = 3
 12:    proc  0 (p:1) buggy_01.pml:8 (state 4)  [n = temp]
        n = 3
 13:    proc  0 (p:1) buggy_01.pml:8 (state 5)  [countp = (countp+1)]
        p(0):countp = 1
 14:    proc  0 (p:1) buggy_01.pml:8 (state 1)  [((countp!=2))]
 15:    proc  0 (p:1) buggy_01.pml:8 (state 2)  [temp = n]
        p(0):temp = 3
 16:    proc  0 (p:1) buggy_01.pml:8 (state 3)  [temp = (temp+1)]
        p(0):temp = 4
 17:    proc  0 (p:1) buggy_01.pml:8 (state 4)  [n = temp]
        n = 4
 18:    proc  0 (p:1) buggy_01.pml:8 (state 5)  [countp = (countp+1)]
        p(0):countp = 2
 19:    proc  0 (p:1) buggy_01.pml:9 (state 6)  [((countp>=2))]
spin: buggy_01.pml:27, Error: assertion violated
spin: text of failed assertion: assert((n!=4))
 20:    proc  2 (monitor:1) buggy_01.pml:27 (state 2)   [assert((n!=4))]
spin: trail ends after 20 steps
#processes: 3
        n = 4
 20:    proc  2 (monitor:1) buggy_01.pml:26 (state 3)
 20:    proc  1 (q:1) buggy_01.pml:22 (state 9) <valid end state>
 20:    proc  0 (p:1) buggy_01.pml:11 (state 11) <valid end state>
3 processes created

如您所见，它报告了导致断言违规的（一个）可能执行跟踪。

LTL.

可以想出几个 ltl 属性 来帮助验证 n 是否最终等于 4。其中一个属性是 [] (n != 4)，它显示为：

starting from the initial state, in every reachable state along all outgoing paths it is always true that n is different from 4.

新模型是这样的：

byte n;

active proctype p()
{
    byte countp = 0;
    byte temp;
    do
    :: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1;
    :: countp >= 2 -> break;
    od
}

active proctype q()
{

    byte countq = 0;

    do
    :: countq != 2 -> n = n + 1; countq = countq + 1;
    :: countq >= 2 -> break;
    od
}

ltl p0 { [] (n != 4) }

您验证此属性的方式与您验证断言的方式几乎相同。为了使这个答案简短，我不会在此处复制并粘贴整个输出，而只是列出使用的命令：

~$ spin -search -bfs buggy_02.pml
ltl p0: [] ((n!=4))
Depth=10 States=40 Transitions=40 Memory=128.195    
pan:1: assertion violated  !( !((n!=4))) (at depth 15)
pan: wrote buggy_02.pml.trail

...

Full statespace search for:
    never claim             + (p0)
    ...
State-vector 28 byte, depth reached 15, errors: 1
...

~$ spin -t -p -g -l buggy_02.pml
...

如果你想保证 n 最终总是等于 4，那么你应该研究一些互斥方法来保护你的 临界区 或者，检查 d_step {} 的 documentation。

Spin Verification，验证变量达到某个值

Spin Verification, verifying a variable reaches a certain value

concurrency

verification

model-checking

spin

promela