彼得森算法的这个模型不正确吗？
Is this model of Peterson's algorithm incorrect?
我写了下面的 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
你是对的，Peterson 算法 应该没有饥饿，确实如此。
饥饿 当一个进程请求一些资源 但被永久拒绝 时发生。因此，progress 公式的更好编码是：
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 模型检查器为您提供了一个恰好属于这种情况的反例：
~$ 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?
因此，为了更直接地回答您的问题，您的模型在功能上并非不正确，但要适当地验证不存在饥饿，有必要进行一些小的更改。
我写了下面的 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
你是对的，Peterson 算法 应该没有饥饿，确实如此。
饥饿 当一个进程请求一些资源 但被永久拒绝 时发生。因此，progress 公式的更好编码是：
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 模型检查器为您提供了一个恰好属于这种情况的反例：
~$ 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
_lastis 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_lastis zero.The
_lastvariable 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?
因此，为了更直接地回答您的问题，您的模型在功能上并非不正确，但要适当地验证不存在饥饿，有必要进行一些小的更改。