model-checking - Peterson 算法的这个模型是错误的吗？

Question

我编写了以下 Peterson 算法模型:

bool want[2], turn

ltl { []<>P[0]@cs }

active [2] proctype P() {
    pid me = _pid
    pid you = 1 - me

    do
    :: want[me] = true
       turn = you
       !want[you] || turn == me
cs:    want[me] = false
    od
}

据我了解，该算法提供了免于饥饿的自由，正如线性时序逻辑声明中所表达的那样。那为什么我分析模型的时候会报错呢？

ltl ltl_0: [] (<> ((P[0]@cs)))
pan:1: acceptance cycle (at depth 2)
pan: wrote peterson.pml.trail

(Spin Version 6.4.8 -- 2 March 2018)
Warning: Search not completed
    + Partial Order Reduction

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

State-vector 36 byte, depth reached 9, errors: 1
        5 states, stored
        0 states, matched
        5 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000   equivalent memory usage for states (stored*(State-vector + overhead))
    0.291   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage



pan: elapsed time 0 seconds

Answer 1

你是对的，Peterson 算法应该不会出现饥饿问题，而且确实如此。

饥饿发生在进程请求一些资源但永久拒绝时。因此，进度公式的更好编码将是:

ltl p1 { [] (P[0]@req -> <> (P[0]@cs) }

哪里req是一个标签，放置如下:

    do
    :: true ->
req:   want[me] = true
       turn = you
       !want[you] || turn == me
cs:    want[me] = false
    od

<小时/>

不幸的是，发现之前的公式仍然是false .

其原因是，您正在检查模型的系统的进程调度程序一般来说并不公平。事实上，它允许执行 _pid 的进程。等于 0永远不会被选择执行。

spin model-checker 为您提供了一个正好适合这种情况的反例:

~$ spin -t -g -l -p t.pml
ltl ltl_0: [] (<> ((P[0]@cs)))
starting claim 1
using statement merging
Never claim moves to line 3 [(!((P[0]._p==cs)))]
  2:    proc  1 (P:1) t.pml:10 (state 1)    [want[me] = 1]
        want[0] = 0
        want[1] = 1
  <<<<<START OF CYCLE>>>>>
Never claim moves to line 8 [(!((P[0]._p==cs)))]
  4:    proc  1 (P:1) t.pml:11 (state 2)    [turn = you]
  6:    proc  1 (P:1) t.pml:12 (state 3)    [((!(want[you])||(turn==me)))]
  8:    proc  1 (P:1) t.pml:13 (state 4)    [want[me] = 0]
        want[0] = 0
        want[1] = 0
 10:    proc  1 (P:1) t.pml:10 (state 1)    [want[me] = 1]
        want[0] = 0
        want[1] = 1
spin: trail ends after 10 steps
#processes: 2
        want[0] = 0
        want[1] = 1
        turn = 0
        cs = 0
 10:    proc  1 (P:1) t.pml:11 (state 2)
 10:    proc  0 (P:1) t.pml:9 (state 5)
 10:    proc  - (ltl_0:1) _spin_nvr.tmp:7 (state 10)
2 processes created

<小时/>

解决方法。

此问题基本上有两种解决方法:

• 第一个只是询问，如果某个进程尝试进入临界区，那么某个进程最终会进入它:

  ltl p2 { [] ((P[0]@req || P[1]@req) -> <> (P[0]@cs || P[1]@cs) }
  

  这确保了整个系统的进展，但并不能保证 P[0] 中的任何一个。和P[1]具体来说不会导致饥饿。

• 第二个是引入一个公平条件，该条件要求将模型检查仅集中在那些进程被安排无限频繁执行的执行上:

  ltl p3 { ([]<> (_last == 0)) -> [] (P[0]@req -> <> (P[0]@cs)) }
  

  哪里_last是预定义的内部变量，如 docs 中所述。如下:

  DESCRIPTION _last is a predefined, global, read-only variable of type pid that holds the instantiation number of the process that performed the last step in the current execution sequence. The initial value of _last is zero.

  The _last variable can only be used inside never claims. It is an error to assign a value to this variable in any context.

  不幸的是，在检查模型是否存在饥饿时，这种方法并不是那么好。这是因为需要 [] <> _last == 0不仅会删除 P[0] 中的任何执行由于调度程序的不公平性，并没有无限频繁地调度执行，但也包括 P[0] 的情况。由于实际的饥饿问题而没有安排。

<小时/>

适当的解决方案。

我建议更改您的模型，以便 P[0]执行忙等待，而不是在等待自己的回合时阻塞。这使得使用_last当试图证明不存在饥饿时问题较少。最终模型将是:

bool flag[2], turn

active [2] proctype P() {
    pid i = _pid;
    pid j = 1 - i;

    do
    :: true ->
req:    flag[i] = true
        turn = j;
        do
            :: (flag[j] && (turn == j)) -> skip
            :: else -> break;
        od;
cs:     skip;
        flag[i] = false;
    od
}

ltl p1 { (
            ([]<> (_last == 0)) &&
            ([]<> (_last == 1))
         ) ->
            ([] (P[0]@req -> <> (P[0]@cs)))
       }

并且该属性确实经过验证，而没有丢弃任何可能有趣的执行跟踪:

~$ spin -a t.pml
ltl p1: (! (([] (<> ((_last==0)))) && ([] (<> ((_last==1)))))) || ([] ((! ((P[0]@req))) || (<> ((P[0]@cs)))))
~$ gcc pan.c
~$ ./a.out -a 

(Spin Version 6.4.8 -- 2 March 2018)

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 40 byte, depth reached 97, errors: 0
      269 states, stored (415 visited)
      670 states, matched
     1085 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.017   equivalent memory usage for states (stored*(State-vector + overhead))
    0.287   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage


unreached in proctype P
    t.pml:18, state 16, "-end-"
    (1 of 16 states)
unreached in claim p1
    _spin_nvr.tmp:23, state 33, "-end-"
    (1 of 33 states)

pan: elapsed time 0 seconds

请注意，我们需要 P[0]和P[1]允许无限频繁地执行，否则会发现另一个虚假的反例。

<小时/>

Is this model of Peterson's algorithm incorrect?

因此，为了更直接地回答您的问题，您的模型在功能上并不是不正确，但为了适本地验证不存在饥饿，有必要执行一些小的更改。