代码之家 › 专栏 › 技术社区 › isekaijin

彼得森算法的这个模型不正确吗?

spin promela model-checking

3

isekaijin · 技术社区 · 6 年前

我编写了彼得森算法的以下模型:

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

1 回复 | 直到 6 年前

1

3

Patrick Trentin 6 年前

你说得对,孩子们应该免于饥饿,事实上,的确如此。

饥饿当进程 请求一些资源 但确实如此 一直拒绝他们 . 因此,更好地编码进步公式为:

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 具体如下:

当前执行序列中的步骤。初始值是

这个变量只能在never声明中使用。它是一个在任何上下文中为此变量赋值时出错。

不挨饿 在你的模型上。这是因为 [] <> _last == 0 P[0] 由于调度器的不公平性,常常不能无限地调度执行,而且在那些情况下 P[0] 由于实际的问题而没有安排 .

一个合适的解决方案。

我建议你换个型号执行 忙着等待 而不是 等待轮到自己时阻挡 _最后 当试图证明没有饥饿 . 最终模型为:

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] 被允许无限频繁地执行,否则会发现另一个虚假的反例。

彼得森算法的这个模型不正确吗?