1

在这里，http ://spinroot.com/spin/Man/Manual.html ，写着：

在 Promela 中，还有另一种避免测试和设置问题的方法：原子序列。通过在花括号中加上关键字 atomic 前缀语句序列，用户可以指示该序列将作为一个不可分割的单元执行，与任何其他进程不交错。如果除第一条语句之外的任何语句在原子序列中阻塞，则会导致运行时错误。这就是我们如何使用原子序列来保护对前面示例中的全局变量状态的并发访问。

在这里，http ://spinroot.com/spin/Man/atomic.html写着：

如果原子序列中的任何语句阻塞，则原子性丢失 如果原子序列中的任何语句阻塞，则原子性丢失，然后允许其他进程开始执行语句。当被阻塞的语句再次变为可执行时，原子序列的执行可以随时恢复，但不一定立即恢复。在进程可以恢复序列剩余部分的原子执行之前，该进程必须首先与系统中的所有其他活动进程竞争以重新获得控制权，也就是说，它必须首先被调度执行。

那么，什么是真实的？从第一个引用我们可以了解到它不允许在 atomic 中阻塞（不是第一个语句）

从第二个引文中，我们了解到可以在 atomic 中阻塞。你只是失去了原子性，就是这样。

4

1 回答 1

0

矛盾的文件：

我的猜测是，这种矛盾仅仅是由于部分文档没有更新以反映多年来Spin内部发生的变化。

事实上，在Spin v. 2.0的发行说明中，我们可以找到以下一段文字（重点是我的）：

2.3.1 阻塞原子序列

到目前为止，如果原子序列包含任何可能阻止序列执行的语句，则被认为是错误的。这引起了很多混乱并使建模变得不必要地复杂化。从 Spin 版本 2 开始，原子序列阻塞是合法的。如果原子序列中的进程阻塞，控制将不确定地转移到另一个进程。如果该语句稍后变为可执行，则控制可以返回到进程，并恢复序列其余部分的原子执行。

这种语义上的变化使得建模变得相对容易，例如，控制不会从一个进程传递到另一个进程的协同例程，除非正在运行的进程阻塞。

Promela 中的原子语句：

在当前版本的Promela/Spin中存在两个原子序列：

  • atomic：来自文档，重点是我的：

    描述

    如果一系列语句括在括号中并以关键字 atomic为前缀，则表示该序列将作为一个不可分割的单元执行，与其他进程不交错。在进程执行的交错中，从原子序列的第一条语句执行到最后一条语句完成的那一刻，没有其他进程可以执行语句。该序列可以包含任意 Promela 语句，并且可能是不确定的。

    如果原子序列中的任何语句阻塞，则原子性丢失，然后允许其他进程开始执行语句。当被阻塞的语句再次变为可执行时，原子序列的执行可以随时恢复，但不一定立即恢复。在进程可以恢复序列剩余部分的原子执行之前，该进程必须首先与系统中的所有其他活动进程竞争以重新获得控制权，也就是说，它必须首先被调度执行。

    [...]

  • d_step：来自文档，重点是我的：

    描述

    执行d_step序列就好像它是一个不可分割的语句。它与原子序列相当，但在以下三点上与此类序列不同：

    • 不允许 goto 跳入或跳出 d_step 序列。
    • 该序列是确定性地执行的。如果存在非确定性，则以固定和确定性的方式解决，例如，始终在每个选择和重复结构中选择第一个真正的守卫。
    • 如果序列内的任何语句的执行都可以阻塞，则这是一个错误。这意味着，例如，在大多数情况下，发送和接收语句不能在 d_step 序列中使用。

    [...]

当然，实际上可以通过一个简单的Promela 示例来测试这种行为。

测试 1：原子性丢失atomic {}

以下面的Promela 模型为例，其中两个进程pippo并最多pluto执行atomic {}一系列指令10。每个进程在开始执行原子序列时将其唯一性保存_pid在一个全局变量p中，然后检查一个flag变量：

  • 如果flag是true，pippo可以执行但pluto不能，因此pluto应该暂时松散原子性（在某些执行跟踪中）
  • 如果flag是false，pluto可以执行但pippo不能，因此pippo应该暂时松散原子性（在某些执行跟踪中）

assert(p == _pid)我们通过在原子序列的末尾添加一条指令来检查最新情况pippo。如果不违反条件，则意味着不存在pippo从原子序列中丢失原子性并pluto开始执行的执行。否则，我们证明链接文档中的描述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

再检查一遍。现在，如果您注释flag:里面的指令pippo并重复验证过程，您会看到不会有任何违反断言的执行跟踪。这是因为原子序列中没有其他指令pippo可以阻塞，因此原子性永远不会丢失。

测试 2：阻塞错误d_step {}

现在，以相同的代码示例并将atomic里面的关键字pippo替换为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

再检查一遍。同样，如果您评论flag;指令，您将看到不会有任何错误跟踪。

于 2017-03-31T10:31:28.333 回答