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

Question

这是我在 Stack Exchange 上提出的第一个问题，因此如果有任何违反准则的内容，请告诉我。

我有一个用 Promela 编写的程序，用于大学操作系统和并发系统类(class)。有两个正在运行的进程会递增变量 n。我们的任务是编写流程，然后使用 Spin 中的验证工具来证明 n 可以取值 4。我已经阅读了所有命令行参数并搞乱了，但没有任何结果。对我来说，“插入此修饰符后跟变量名以检查所有可能的值。”

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;
}

注意:监控过程中的循环是完全没有必要的，但它让初学者更清楚其目的。

您可以使用以下一行验证此程序:

~$ spin -search -bfs buggy_01.pml

Spin零时间找到反例:

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:重放 spin 生成的 .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属性来帮助验证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，那么您应该考虑一些互斥方法来保护您的关键部分或者，检查 documentation d_step {}。