正确使用 ``progress`` 标签
correct use of ``progress`` label
Progress labels are used to define correctness claims. A progress label states the requirement that the labeled global state must be visited infinitely often in any infinite system execution. Any violation of this requirement can be reported by the verifier as a non-progress cycle.
和
Spin has a special mode to prove absence of non-progress cycles. It does so with the predefined LTL formula:
(<>[] np_)
which formalizes non-progress as a standard Buchi acceptance property.
不过让我们来看看非常原始的promela规范
bool initialised = 0;
init{
progress:
initialised++;
assert(initialised == 1);
}
根据我的理解，assert 应该成立但验证失败，因为 initialised++ 只执行一次，而 progress 标签声称应该可以任意频繁地执行它。
然而，即使使用上面的 LTL 公式，这在 ispin 中验证得很好（见下文）。
如何正确测试语句是否可以任意频繁执行（例如，对于锁定方案）？
(Spin Version 6.4.7 -- 19 August 2017)
+ Partial Order Reduction
Full statespace search for:
never claim + (:np_:)
assertion violations + (if within scope of claim)
non-progress cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 28 byte, depth reached 7, errors: 0
6 states, stored (8 visited)
3 states, matched
11 transitions (= visited+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.293 actual memory usage for states
64.000 memory used for hash table (-w24)
0.343 memory used for DFS stack (-m10000)
64.539 total actual memory usage
unreached in init
(0 of 3 states)
pan: elapsed time 0.001 seconds
No errors found -- did you verify all claims?
更新
仍然不确定如何使用这个...
bool initialised = 0;
init{
initialised = 1;
}
active [2] proctype reader()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
progress_reader:
assert(true);
od
}
active [2] proctype writer()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
(initialised == 0)
progress_writer:
assert(true);
od
}
让我们 select 测试非进度周期。然后是 运行s this as
spin -a test.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DNP -DNOCLAIM -w -o pan pan.c
./pan -m10000 -l
验证无误
所以让我们尝试使用 ltl 属性...
/*pid: 0 = init, 1-2 = reader, 3-4 = writer*/
ltl progress_reader1{ []<> reader[1]@progress_reader }
ltl progress_reader2{ []<> reader[2]@progress_reader }
ltl progress_writer1{ []<> writer[3]@progress_writer }
ltl progress_writer2{ []<> writer[4]@progress_writer }
bool initialised = 0;
init{
initialised = 1;
}
active [2] proctype reader()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
progress_reader:
assert(true);
od
}
active [2] proctype writer()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
(initialised == 0)
progress_writer:
assert(true);
od
}
现在，首先，
the model contains 4 never claims: progress_writer2, progress_writer1, progress_reader2, progress_reader1
only one claim is used in a verification run
choose which one with ./pan -a -N name (defaults to -N progress_reader1)
or use e.g.: spin -search -ltl progress_reader1 test.pml
好吧，我不在乎，我只是想最后 运行，所以让我们保留 progress_writer1 并担心稍后如何将它们拼接在一起：
/*pid: 0 = init, 1-2 = reader, 3-4 = writer*/
/*ltl progress_reader1{ []<> reader[1]@progress_reader }*/
/*ltl progress_reader2{ []<> reader[2]@progress_reader }*/
ltl progress_writer1{ []<> writer[3]@progress_writer }
/*ltl progress_writer2{ []<> writer[4]@progress_writer }*/
bool initialised = 0;
init{
initialised = 1;
}
active [2] proctype reader()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
progress_reader:
assert(true);
od
}
active [2] proctype writer()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
(initialised == 0)
progress_writer:
assert(true);
od
}
用
旋转运行这个
spin -a test.pml
ltl progress_writer1: [] (<> ((writer[3]@progress_writer)))
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000
哪个不会产生错误，而是报告
unreached in claim progress_writer1
_spin_nvr.tmp:3, state 5, "(!((writer[3]._p==progress_writer)))"
_spin_nvr.tmp:3, state 5, "(1)"
_spin_nvr.tmp:8, state 10, "(!((writer[3]._p==progress_writer)))"
_spin_nvr.tmp:10, state 13, "-end-"
(3 of 13 states)
是吗？灿烂！我完全不知道该怎么办。
如何将此内容发送到 运行？
您的代码示例的问题在于它没有任何无限系统执行。
Progress labels are used to define correctness claims. A progress
label states the requirement that the labeled global state must be
visited infinitely often in any infinite system execution. Any
violation of this requirement can be reported by the verifier as a
non-progress cycle.
试试这个例子：
short val = 0;
init {
do
:: val == 0 ->
val = 1;
// ...
val = 0;
:: else ->
progress:
// super-important progress state
printf("progress-state\n");
assert(val != 0);
od;
};
正常检查没有发现错误：
~$ spin -search test.pml
(Spin Version 6.4.3 -- 16 December 2014)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 12 byte, depth reached 2, errors: 0
3 states, stored
1 states, matched
4 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.292 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 init
test.pml:12, state 5, "printf('progress-state\n')"
test.pml:13, state 6, "assert((val!=0))"
test.pml:15, state 10, "-end-"
(3 of 10 states)
pan: elapsed time 0 seconds
然而，检查 进度 会产生错误：
~$ spin -search -l test.pml
pan:1: non-progress cycle (at depth 2)
pan: wrote test.pml.trail
(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (:np_:)
assertion violations + (if within scope of claim)
non-progress cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 20 byte, depth reached 7, errors: 1
4 states, stored
0 states, matched
4 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.292 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
WARNING: 确保在选项-search后写-l，否则不交给验证者
你问：
How do I correctly test whether a statement can be executed arbitrarily often (e.g. for a locking scheme)?
简单写个liveness属性:
ltl prop { [] <> proc[0]@label };
这会检查名称为 proc 且 pid 为 0 的进程是否经常无限执行对应于 label.
的语句
由于您的 edit 大大改变了问题，我写了一个新的答案以避免混淆。此答案仅 新内容。下次，请考虑创建一个新的、单独的问题。
在这种情况下，注意 unreached in ... 警告消息非常重要，因为它会影响验证过程的结果。
警告消息：
unreached in claim progress_writer1
_spin_nvr.tmp:3, state 5, "(!((writer[3]._p==progress_writer)))"
_spin_nvr.tmp:3, state 5, "(1)"
_spin_nvr.tmp:8, state 10, "(!((writer[3]._p==progress_writer)))"
_spin_nvr.tmp:10, state 13, "-end-"
(3 of 13 states)
与编译过程中创建的文件_spin_nvr.tmp内容相关：
...
never progress_writer1 { /* !([] (<> ((writer[3]@progress_writer)))) */
T0_init:
do
:: (! (((writer[3]@progress_writer)))) -> goto accept_S4 // state 5
:: (1) -> goto T0_init
od;
accept_S4:
do
:: (! (((writer[3]@progress_writer)))) -> goto accept_S4 // state 10
od;
} // state 13 '-end-'
...
粗略地说，您可以将其视为 Buchi Automaton 的规范，它接受 writer 进程的执行，其中 _pid 等于 3 其中它不会无限频繁地到达带有标签 progress_writer 的语句， 即它只这样做了有限的次数.
要理解这一点你应该知道，为了验证ltl 属性 φ，spin构建了一个包含原始[=23=中所有路径的自动机] 不满足 φ 的模型。这是通过计算对原始系统建模的自动机的 同步乘积 来完成的，该自动机表示您要验证的 属性 φ 的否定。 在您的示例中，φ 的否定由上面摘自 _spin_nvr.tmp 并标有 never progress_writer1 的代码摘录给出。 然后，Spin 检查是否有可能执行此自动机：
- 如果有，那么 属性
φ 被违反了，这样的执行轨迹是你的 属性 的见证（又名反例）
- 否则，属性
φ 已验证。
警告 告诉您在生成的 同步产品 中，这些状态的 none 是永远可达的。为什么会这样？
考虑一下：
active [2] proctype writer()
{
1: assert(_pid >= 1);
2: (initialised == 1)
3: do
4: :: else ->
5: (initialised == 0);
6: progress_writer:
7: assert(true);
8: od
}
在第 2: 行，您检查 initialised == 1。此语句强制 writer 在 2: 行阻塞，直到 initialised 设置为 1。幸运的是，这是由 init 过程完成的。
在第 5: 行，您检查 initialised == 0。此语句强制 writer 在 5: 行阻塞，直到 initialised 设置为 0。但是，没有进程在代码的任何地方将 initialised 设置为 0。因此，标有 progress_writer: 的代码行实际上无法访问。
(1) /* always executable */
(0) /* never executable */
skip /* always executable, same as (1) */
true /* always executable, same as skip */
false /* always blocks, same as (0) */
a == b /* executable only when a equals b */
A condition statement can only be executed (passed) if it holds. [...]
Progress labels are used to define correctness claims. A progress label states the requirement that the labeled global state must be visited infinitely often in any infinite system execution. Any violation of this requirement can be reported by the verifier as a non-progress cycle.
和
Spin has a special mode to prove absence of non-progress cycles. It does so with the predefined LTL formula:
(<>[] np_)which formalizes non-progress as a standard Buchi acceptance property.
不过让我们来看看非常原始的promela规范
bool initialised = 0;
init{
progress:
initialised++;
assert(initialised == 1);
}
根据我的理解，assert 应该成立但验证失败，因为 initialised++ 只执行一次，而 progress 标签声称应该可以任意频繁地执行它。
然而，即使使用上面的 LTL 公式，这在 ispin 中验证得很好（见下文）。
如何正确测试语句是否可以任意频繁执行（例如，对于锁定方案）？
(Spin Version 6.4.7 -- 19 August 2017)
+ Partial Order ReductionFull statespace search for:
never claim + (:np_:) assertion violations + (if within scope of claim) non-progress cycles + (fairness disabled) invalid end states - (disabled by never claim)State-vector 28 byte, depth reached 7, errors: 0
6 states, stored (8 visited) 3 states, matched 11 transitions (= visited+matched) 0 atomic stepshash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead)) 0.293 actual memory usage for states 64.000 memory used for hash table (-w24) 0.343 memory used for DFS stack (-m10000) 64.539 total actual memory usageunreached in init
(0 of 3 states)pan: elapsed time 0.001 seconds
No errors found -- did you verify all claims?
更新
仍然不确定如何使用这个...
bool initialised = 0;
init{
initialised = 1;
}
active [2] proctype reader()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
progress_reader:
assert(true);
od
}
active [2] proctype writer()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
(initialised == 0)
progress_writer:
assert(true);
od
}
让我们 select 测试非进度周期。然后是 运行s this as
spin -a test.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DNP -DNOCLAIM -w -o pan pan.c
./pan -m10000 -l
验证无误
所以让我们尝试使用 ltl 属性...
/*pid: 0 = init, 1-2 = reader, 3-4 = writer*/
ltl progress_reader1{ []<> reader[1]@progress_reader }
ltl progress_reader2{ []<> reader[2]@progress_reader }
ltl progress_writer1{ []<> writer[3]@progress_writer }
ltl progress_writer2{ []<> writer[4]@progress_writer }
bool initialised = 0;
init{
initialised = 1;
}
active [2] proctype reader()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
progress_reader:
assert(true);
od
}
active [2] proctype writer()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
(initialised == 0)
progress_writer:
assert(true);
od
}
现在，首先，
the model contains 4 never claims: progress_writer2, progress_writer1, progress_reader2, progress_reader1
only one claim is used in a verification run
choose which one with ./pan -a -N name (defaults to -N progress_reader1)
or use e.g.: spin -search -ltl progress_reader1 test.pml
好吧，我不在乎，我只是想最后 运行，所以让我们保留 progress_writer1 并担心稍后如何将它们拼接在一起：
/*pid: 0 = init, 1-2 = reader, 3-4 = writer*/
/*ltl progress_reader1{ []<> reader[1]@progress_reader }*/
/*ltl progress_reader2{ []<> reader[2]@progress_reader }*/
ltl progress_writer1{ []<> writer[3]@progress_writer }
/*ltl progress_writer2{ []<> writer[4]@progress_writer }*/
bool initialised = 0;
init{
initialised = 1;
}
active [2] proctype reader()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
progress_reader:
assert(true);
od
}
active [2] proctype writer()
{
assert(_pid >= 1);
(initialised == 1)
do
:: else ->
(initialised == 0)
progress_writer:
assert(true);
od
}
用
旋转运行这个spin -a test.pml
ltl progress_writer1: [] (<> ((writer[3]@progress_writer)))
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000
哪个不会产生错误，而是报告
unreached in claim progress_writer1
_spin_nvr.tmp:3, state 5, "(!((writer[3]._p==progress_writer)))"
_spin_nvr.tmp:3, state 5, "(1)"
_spin_nvr.tmp:8, state 10, "(!((writer[3]._p==progress_writer)))"
_spin_nvr.tmp:10, state 13, "-end-"
(3 of 13 states)
是吗？灿烂！我完全不知道该怎么办。
如何将此内容发送到 运行？
您的代码示例的问题在于它没有任何无限系统执行。
Progress labels are used to define correctness claims. A progress label states the requirement that the labeled global state must be visited infinitely often in any infinite system execution. Any violation of this requirement can be reported by the verifier as a non-progress cycle.
试试这个例子：
short val = 0;
init {
do
:: val == 0 ->
val = 1;
// ...
val = 0;
:: else ->
progress:
// super-important progress state
printf("progress-state\n");
assert(val != 0);
od;
};
正常检查没有发现错误：
~$ spin -search test.pml
(Spin Version 6.4.3 -- 16 December 2014)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 12 byte, depth reached 2, errors: 0
3 states, stored
1 states, matched
4 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.292 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 init
test.pml:12, state 5, "printf('progress-state\n')"
test.pml:13, state 6, "assert((val!=0))"
test.pml:15, state 10, "-end-"
(3 of 10 states)
pan: elapsed time 0 seconds
然而，检查 进度 会产生错误：
~$ spin -search -l test.pml
pan:1: non-progress cycle (at depth 2)
pan: wrote test.pml.trail
(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (:np_:)
assertion violations + (if within scope of claim)
non-progress cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 20 byte, depth reached 7, errors: 1
4 states, stored
0 states, matched
4 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.292 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
WARNING: 确保在选项-search后写-l，否则不交给验证者
你问：
How do I correctly test whether a statement can be executed arbitrarily often (e.g. for a locking scheme)?
简单写个liveness属性:
ltl prop { [] <> proc[0]@label };
这会检查名称为 proc 且 pid 为 0 的进程是否经常无限执行对应于 label.
由于您的 edit 大大改变了问题，我写了一个新的答案以避免混淆。此答案仅 新内容。下次，请考虑创建一个新的、单独的问题。
在这种情况下，注意 unreached in ... 警告消息非常重要，因为它会影响验证过程的结果。
警告消息：
unreached in claim progress_writer1
_spin_nvr.tmp:3, state 5, "(!((writer[3]._p==progress_writer)))"
_spin_nvr.tmp:3, state 5, "(1)"
_spin_nvr.tmp:8, state 10, "(!((writer[3]._p==progress_writer)))"
_spin_nvr.tmp:10, state 13, "-end-"
(3 of 13 states)
与编译过程中创建的文件_spin_nvr.tmp内容相关：
...
never progress_writer1 { /* !([] (<> ((writer[3]@progress_writer)))) */
T0_init:
do
:: (! (((writer[3]@progress_writer)))) -> goto accept_S4 // state 5
:: (1) -> goto T0_init
od;
accept_S4:
do
:: (! (((writer[3]@progress_writer)))) -> goto accept_S4 // state 10
od;
} // state 13 '-end-'
...
粗略地说，您可以将其视为 Buchi Automaton 的规范，它接受 writer 进程的执行，其中 _pid 等于 3 其中它不会无限频繁地到达带有标签 progress_writer 的语句， 即它只这样做了有限的次数.
要理解这一点你应该知道，为了验证ltl 属性 φ，spin构建了一个包含原始[=23=中所有路径的自动机] 不满足 φ 的模型。这是通过计算对原始系统建模的自动机的 同步乘积 来完成的，该自动机表示您要验证的 属性 φ 的否定。 在您的示例中，φ 的否定由上面摘自 _spin_nvr.tmp 并标有 never progress_writer1 的代码摘录给出。 然后，Spin 检查是否有可能执行此自动机：
- 如果有，那么 属性
φ被违反了，这样的执行轨迹是你的 属性 的见证（又名反例）
- 否则，属性
φ已验证。
警告 告诉您在生成的 同步产品 中，这些状态的 none 是永远可达的。为什么会这样？
考虑一下：
active [2] proctype writer()
{
1: assert(_pid >= 1);
2: (initialised == 1)
3: do
4: :: else ->
5: (initialised == 0);
6: progress_writer:
7: assert(true);
8: od
}
在第 2: 行，您检查 initialised == 1。此语句强制 writer 在 2: 行阻塞，直到 initialised 设置为 1。幸运的是，这是由 init 过程完成的。
在第 5: 行，您检查 initialised == 0。此语句强制 writer 在 5: 行阻塞，直到 initialised 设置为 0。但是，没有进程在代码的任何地方将 initialised 设置为 0。因此，标有 progress_writer: 的代码行实际上无法访问。
(1) /* always executable */ (0) /* never executable */ skip /* always executable, same as (1) */ true /* always executable, same as skip */ false /* always blocks, same as (0) */ a == b /* executable only when a equals b */A condition statement can only be executed (passed) if it holds. [...]