Promela 中的原子序列。文档中自相矛盾
atomic sequences in Promela. Contradictory in documentation
这里，http://spinroot.com/spin/Man/Manual.html，是这样写的：
In Promela there is also another way to avoid the test and set
problem: atomic sequences. By prefixing a sequence of statements
enclosed in curly braces with the keyword atomic the user can indicate
that the sequence is to be executed as one indivisible unit,
non-interleaved with any other processes. It causes a run-time error
if any statement, other than the first statement, blocks in an atomic
sequence. This is how we can use atomic sequences to protect the
concurrent access to the global variable state in the earlier example.
这里，http://spinroot.com/spin/Man/atomic.html，写着：
If any statement within the atomic sequence blocks, atomicity is lost
If any statement within the atomic sequence blocks, atomicity is lost,
and other processes are then allowed to start executing statements.
When the blocked statement becomes executable again, the execution of
the atomic sequence can be resumed at any time, but not necessarily
immediately. Before the process can resume the atomic execution of the
remainder of the sequence, the process must first compete with all
other active processes in the system to regain control, that is, it
must first be scheduled for execution.
那么，什么是真的？从第一个引用我们可以知道它是不允许在原子中阻塞的（不是第一条语句）
从第二个引用中我们了解到在原子中阻塞是可以的。你只是失去了原子性，仅此而已。
矛盾的文档：
我的 猜测 矛盾仅仅是因为文档的部分内容没有更新以反映 Spin 中发生的更改多年来。
其实在Spin的release notesv。 2.0我们可以找到如下一段文字（重点是我的）：
2.3.1 Blocking Atomic Sequences
Until now it was considered an error if an atomic sequence contained
any statement that could block the execution of the sequence. This
caused much confusion and complicates modeling needlessly. Starting
with Spin version 2, it is legal for an atomic sequence to block. If a
process inside an atomic sequence blocks, control shifts
non-deterministically to another process. If the statement later
becomes executable, control can return to the process and the atomic
execution of the remainder of the sequence resumed.
This change in semantics makes it relatively easy to model, for
instance, co-routines where control does not pass from one process to
another until and unless the running process blocks.
Promela 中的原子语句：
在当前版本的Promela/Spin中存在两个原子序列:
-
DESCRIPTION
If a sequence of statements is enclosed in parentheses and prefixed with the keyword atomic, this indicates that the sequence is to be executed as one indivisible unit, non-interleaved with other processes. In the interleaving of process executions, no other process can execute statements from the moment that the first statement of an atomic sequence is executed until the last one has completed. The sequence can contain arbitrary Promela statements, and may be non-deterministic.
If any statement within the atomic sequence blocks, atomicity is lost, and other processes are then allowed to start executing statements. When the blocked statement becomes executable again, the execution of the atomic sequence can be resumed at any time, but not necessarily immediately. Before the process can resume the atomic execution of the remainder of the sequence, the process must first compete with all other active processes in the system to regain control, that is, it must first be scheduled for execution.
[...]
-
DESCRIPTION
A d_step sequence is executed as if it were one single indivisible statement. It is comparable to an atomic sequence, but it differs from such sequences on the following three points:
- No goto jumps into or out of a d_step sequence are allowed.
- The sequence is executed deterministically. If non-determinism is present, it is resolved in a fixed and deterministic way, for instance, by always selecting the first true guard in every selection and repetition structure.
- It is an error if the execution of any statement inside the sequence can block. This means, for instance, that in most cases send and receive statements cannot be used inside d_step sequences.
[...]
当然，实际上可以用一个简单的 Promela 示例.
来测试这一行为
测试 1：atomic {}
失去原子性
采用以下 Promela 模型，其中两个进程 pippo 和 pluto 执行一个 atomic {} 指令序列，直到 10 次。每个进程在开始执行原子序列时将其唯一的 _pid 保存在一个全局变量 p 中，然后检查一个 flag 变量：
- 如果
flag 是 true，pippo 可以执行但 pluto 不能，因此 pluto 应该暂时松散原子性（在某些执行跟踪中）
- 如果
flag 是 false，pluto 可以执行但 pippo 不能，因此 pippo 应该暂时松散原子性（在某些执行跟踪中）
我们通过在pippo中的原子序列末尾添加一条assert(p == _pid)指令来检查最新的情况。如果不违反条件，则意味着没有执行 pippo 从原子序列中失去原子性，而是 pluto 开始执行。否则，我们证明 linked documentation 中对 atomic {} 的描述是准确的。
bool flag;
pid p;
active proctype pippo ()
{
byte i;
do
:: i < 10 ->
atomic {
true ->
p = _pid;
flag; /* executable only if flag is true */
printf("pippo unblocked\n");
flag = !flag;
assert(p == _pid);
};
i++;
:: else -> break;
od;
};
active proctype pluto ()
{
byte i;
do
:: i < 10 ->
atomic {
true ->
p = _pid;
end:
!flag; /* executable only if flag is false */
printf("pluto unblocked\n");
flag = !flag;
};
i++;
:: else -> break;
od;
};
如果我们用Spin进行形式验证，它会发现违反属性:
的执行轨迹
~$ spin -search -bfs test.pml # -bfs: breadth-first-search, results in a
# shorter counter-example
pan:1: assertion violated (p==_pid) (at depth 6)
pan: wrote test.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 20 byte, depth reached 6, errors: 1
15 states, stored
10 nominal states (stored-atomic)
0 states, matched
15 transitions (= stored+matched)
5 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.001 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 -l -g test.pml
Double Check. 现在，如果您在 pippo 中注释指令 flag: 并重复验证过程，您会看到 won不会是任何违反 断言 的执行跟踪。 这是因为pippo的原子序列中没有其他指令可以阻塞，因此原子性永远不会丢失。
测试 2：d_step {}
出现阻塞错误
现在，使用相同的代码示例，将 pippo 中的 atomic 关键字替换为 d_step:
bool flag;
pid p;
active proctype pippo ()
{
byte i;
do
:: i < 10 ->
d_step {
true ->
p = _pid;
flag; /* executable only if flag is true */
printf("pippo unblocked\n");
flag = !flag;
assert(p == _pid);
};
i++;
:: else -> break;
od;
};
active proctype pluto ()
{
byte i;
do
:: i < 10 ->
atomic {
true ->
p = _pid;
end:
!flag; /* executable only if flag is false */
printf("pluto unblocked\n");
flag = !flag;
};
i++;
:: else -> break;
od;
};
如果你正式验证这个模型，你会发现它仍然找到了一个反例，但这次有不同的错误：
~$ spin -search -bfs test.pml
pan:1: block in d_step seq (at depth 2)
pan: wrote test.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 20 byte, depth reached 2, errors: 1
4 states, stored
4 nominal states (stored-atomic)
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.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 -l -g test.pml
using statement merging
1: proc 1 (pluto:1) test.pml:26 (state 1) [((i<10))]
2: proc 0 (pippo:1) test.pml:8 (state 1) [((i<10))]
3: proc 0 (pippo:1) test.pml:9 (state 8) [(1)]
3: proc 0 (pippo:1) test.pml:11 (state 3) [p = _pid]
spin: trail ends after 3 steps
#processes: 2
flag = 0
p = 0
3: proc 1 (pluto:1) test.pml:27 (state 7)
3: proc 0 (pippo:1)
2 processes created
问题是 pippo 块在 d_step 序列中，这违反了 概要 [=] 中的 第三个条件 d_step documentation 的 133=]，与描述的完全一致。
仔细检查。 同样，如果您注释 flag; 指令，您会发现不会有任何错误跟踪。
这里，http://spinroot.com/spin/Man/Manual.html，是这样写的：
In Promela there is also another way to avoid the test and set problem: atomic sequences. By prefixing a sequence of statements enclosed in curly braces with the keyword atomic the user can indicate that the sequence is to be executed as one indivisible unit, non-interleaved with any other processes. It causes a run-time error if any statement, other than the first statement, blocks in an atomic sequence. This is how we can use atomic sequences to protect the concurrent access to the global variable state in the earlier example.
这里，http://spinroot.com/spin/Man/atomic.html，写着：
If any statement within the atomic sequence blocks, atomicity is lost If any statement within the atomic sequence blocks, atomicity is lost, and other processes are then allowed to start executing statements. When the blocked statement becomes executable again, the execution of the atomic sequence can be resumed at any time, but not necessarily immediately. Before the process can resume the atomic execution of the remainder of the sequence, the process must first compete with all other active processes in the system to regain control, that is, it must first be scheduled for execution.
那么，什么是真的？从第一个引用我们可以知道它是不允许在原子中阻塞的（不是第一条语句）
从第二个引用中我们了解到在原子中阻塞是可以的。你只是失去了原子性，仅此而已。
矛盾的文档：
我的 猜测 矛盾仅仅是因为文档的部分内容没有更新以反映 Spin 中发生的更改多年来。
其实在Spin的release notesv。 2.0我们可以找到如下一段文字（重点是我的）：
2.3.1 Blocking Atomic Sequences
Until now it was considered an error if an atomic sequence contained any statement that could block the execution of the sequence. This caused much confusion and complicates modeling needlessly. Starting with Spin version 2, it is legal for an atomic sequence to block. If a process inside an atomic sequence blocks, control shifts non-deterministically to another process. If the statement later becomes executable, control can return to the process and the atomic execution of the remainder of the sequence resumed.
This change in semantics makes it relatively easy to model, for instance, co-routines where control does not pass from one process to another until and unless the running process blocks.
Promela 中的原子语句：
在当前版本的Promela/Spin中存在两个原子序列:
-
DESCRIPTION
If a sequence of statements is enclosed in parentheses and prefixed with the keyword atomic, this indicates that the sequence is to be executed as one indivisible unit, non-interleaved with other processes. In the interleaving of process executions, no other process can execute statements from the moment that the first statement of an atomic sequence is executed until the last one has completed. The sequence can contain arbitrary Promela statements, and may be non-deterministic.
If any statement within the atomic sequence blocks, atomicity is lost, and other processes are then allowed to start executing statements. When the blocked statement becomes executable again, the execution of the atomic sequence can be resumed at any time, but not necessarily immediately. Before the process can resume the atomic execution of the remainder of the sequence, the process must first compete with all other active processes in the system to regain control, that is, it must first be scheduled for execution.
[...]
-
DESCRIPTION
A d_step sequence is executed as if it were one single indivisible statement. It is comparable to an atomic sequence, but it differs from such sequences on the following three points:
- No goto jumps into or out of a d_step sequence are allowed.
- The sequence is executed deterministically. If non-determinism is present, it is resolved in a fixed and deterministic way, for instance, by always selecting the first true guard in every selection and repetition structure.
- It is an error if the execution of any statement inside the sequence can block. This means, for instance, that in most cases send and receive statements cannot be used inside d_step sequences.
[...]
当然，实际上可以用一个简单的 Promela 示例.
来测试这一行为测试 1：atomic {}
采用以下 Promela 模型，其中两个进程 pippo 和 pluto 执行一个 atomic {} 指令序列，直到 10 次。每个进程在开始执行原子序列时将其唯一的 _pid 保存在一个全局变量 p 中，然后检查一个 flag 变量：
- 如果
flag是true，pippo可以执行但pluto不能，因此pluto应该暂时松散原子性（在某些执行跟踪中） - 如果
flag是false，pluto可以执行但pippo不能，因此pippo应该暂时松散原子性（在某些执行跟踪中）
我们通过在pippo中的原子序列末尾添加一条assert(p == _pid)指令来检查最新的情况。如果不违反条件，则意味着没有执行 pippo 从原子序列中失去原子性，而是 pluto 开始执行。否则，我们证明 linked documentation 中对 atomic {} 的描述是准确的。
bool flag;
pid p;
active proctype pippo ()
{
byte i;
do
:: i < 10 ->
atomic {
true ->
p = _pid;
flag; /* executable only if flag is true */
printf("pippo unblocked\n");
flag = !flag;
assert(p == _pid);
};
i++;
:: else -> break;
od;
};
active proctype pluto ()
{
byte i;
do
:: i < 10 ->
atomic {
true ->
p = _pid;
end:
!flag; /* executable only if flag is false */
printf("pluto unblocked\n");
flag = !flag;
};
i++;
:: else -> break;
od;
};
如果我们用Spin进行形式验证，它会发现违反属性:
的执行轨迹~$ spin -search -bfs test.pml # -bfs: breadth-first-search, results in a
# shorter counter-example
pan:1: assertion violated (p==_pid) (at depth 6)
pan: wrote test.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 20 byte, depth reached 6, errors: 1
15 states, stored
10 nominal states (stored-atomic)
0 states, matched
15 transitions (= stored+matched)
5 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.001 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 -l -g test.pml
Double Check. 现在，如果您在 pippo 中注释指令 flag: 并重复验证过程，您会看到 won不会是任何违反 断言 的执行跟踪。 这是因为pippo的原子序列中没有其他指令可以阻塞，因此原子性永远不会丢失。
测试 2：d_step {}
现在，使用相同的代码示例，将 pippo 中的 atomic 关键字替换为 d_step:
bool flag;
pid p;
active proctype pippo ()
{
byte i;
do
:: i < 10 ->
d_step {
true ->
p = _pid;
flag; /* executable only if flag is true */
printf("pippo unblocked\n");
flag = !flag;
assert(p == _pid);
};
i++;
:: else -> break;
od;
};
active proctype pluto ()
{
byte i;
do
:: i < 10 ->
atomic {
true ->
p = _pid;
end:
!flag; /* executable only if flag is false */
printf("pluto unblocked\n");
flag = !flag;
};
i++;
:: else -> break;
od;
};
如果你正式验证这个模型，你会发现它仍然找到了一个反例，但这次有不同的错误：
~$ spin -search -bfs test.pml
pan:1: block in d_step seq (at depth 2)
pan: wrote test.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 20 byte, depth reached 2, errors: 1
4 states, stored
4 nominal states (stored-atomic)
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.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 -l -g test.pml
using statement merging
1: proc 1 (pluto:1) test.pml:26 (state 1) [((i<10))]
2: proc 0 (pippo:1) test.pml:8 (state 1) [((i<10))]
3: proc 0 (pippo:1) test.pml:9 (state 8) [(1)]
3: proc 0 (pippo:1) test.pml:11 (state 3) [p = _pid]
spin: trail ends after 3 steps
#processes: 2
flag = 0
p = 0
3: proc 1 (pluto:1) test.pml:27 (state 7)
3: proc 0 (pippo:1)
2 processes created
问题是 pippo 块在 d_step 序列中，这违反了 概要 [=] 中的 第三个条件 d_step documentation 的 133=]，与描述的完全一致。
仔细检查。 同样，如果您注释 flag; 指令，您会发现不会有任何错误跟踪。