Promela中的原子序列.文档矛盾 [英] atomic sequences in Promela. Contradictory in documentation

问题描述

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

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

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.

那么，什么是真实的?从第一次引用我们可以得知，它不允许以原子方式阻止(不是第一条语句)

So, what is the true? From the first citation we can learn that it is not allowed to block in atomic ( not the first statement)

从第二次引用中我们得知阻止原子是可以的.您只是失去了原子性而已.

From the second citation we learn that it is ok to block in atomic. You just lose the atomicity and that is it.

推荐答案

矛盾性文档:

我的猜测是，矛盾仅是文档的某些部分未更新以反映多年来在 Spin 中发生的更改的结果.

My guess is that the contradiction is merely the result of parts of the documentation not being updated to reflect changes that occurred within Spin over the years.

实际上，在 发行说明 旋转 v. 2.0 ，我们可以找到以下文字(重点是我的文字):

In fact, in the release notes of Spin v. 2.0 we can find the following piece of text (emphasis is mine):

2.3.1阻止原子序列

直到现在，如果包含原子序列，则被视为错误 任何可能阻止序列执行的语句.这 造成了很多混乱，并使建模变得不必要了.开始 在Spin 2版中，阻止原子序列是合法的.如果一个 原子序列块内的过程，控制转移 不确定地用于另一个过程.如果以后再声明 成为可执行文件，控制权可以返回到流程和原子 恢复执行其余序列.

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 中，存在两个原子序列:

In the current version of Promela/Spin there exist two atomic sequences:

• 原子: a href ="http://spinroot.com/spin/Man/atomic.html" rel ="nofollow noreferrer">文档，重点是我的:

说明

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

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.

[...]

d_step: a href ="http://spinroot.com/spin/Man/d_step.html" rel ="nofollow noreferrer">文档，重点是我的:

d_step: from the docs, emphasis is mine:

说明

执行一个 d_step 序列，就好像它是一个单独的不可分割的语句一样.它可与原子序列相提并论，但在以下三点上与此类序列不同:

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:

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

• 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示例来实际测试这种行为.

Of course, one can actually test this behaviour with a simple Promela example.

测试1:使用atomic {}

TEST 1: loss of atomicity with atomic {}

采用以下 Promela模型，其中两个进程pippo和pluto执行atomic {}指令序列，最多执行10次.每个进程在开始执行原子序列时都将其唯一的_pid保存在全局变量p中，然后检查flag变量:

Take the following Promela Model, in which two processes pippo and pluto execute an atomic {} sequence of instructions up to 10 times. Each process saves its unique _pid inside a global variable p when it starts executing the atomic sequence, and then checks a flag variable:

• 如果flag是true，则pippo可以执行，但pluto无法执行，因此pluto应该暂时释放原子性(在某些执行跟踪中)
• 如果flag是false，则pluto可以执行，但pippo无法执行，因此pippo应该暂时释放原子性(在某些执行跟踪中)

• if flag is true, pippo can execute but pluto cannot, therefore pluto should temporarily loose atomicity (in some execution trace)
• if flag is false, pluto can execute but pippo cannot, therefore pippo should temporarily loose atomicity (in some execution trace)

我们通过在pippo的原子序列末尾添加assert(p == _pid)指令来检查最新情况.如果不违反条件，则表示没有执行，其中pippo从原子序列内释放原子性，而pluto开始执行.否则，我们证明链接文档中对atomic {}的描述是正确的.

We check the latest case by adding an assert(p == _pid) instruction at the end of the atomic sequence in pippo. If the condition is not violated, then it means that there is no execution in which pippo looses atomicity from within the atomic sequence and pluto starts executing instead. Otherwise, we proved that the description in the linked documentation for atomic {} is accurate.

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 执行形式验证，则会发现违反该属性的执行跟踪:

If we perform formal verification with Spin, it finds an execution trace that violates the property:

~$ 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

违反了声明，如文档中所述.您可以按以下方式重播无效的执行跟踪:

The assertion is violated, as stated in the documentation. You can replay the invalid execution trace as follows:

 ~$ spin -t -p -l -g test.pml

仔细检查.现在，如果您在pippo中注释了flag:指令并重复了验证过程，您将发现不会有违反断言. 这是因为pippo的原子序列中没有其他指令可以阻塞，因此原子性永远不会丢失.

Double Check. Now, if you comment the instruction flag: inside pippo and you repeat the verification process, you'll see that there won't be any execution trace violating the assertion. This is because no other instruction in the atomic sequence of pippo can block, and therefore atomicity is never lost.

测试2:使用d_step {}

TEST 2: blocking error with d_step {}

现在，以相同的代码示例为例，并将pippo中的atomic关键字替换为d_step:

Now, take the same code example and substitute the atomic keyword inside pippo with 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;
};

如果您正式验证该模型，您会发现它仍然可以找到一个反例，但是这次出现了另一个错误:

If you formally verify this model, you'll see that it still finds a counter-example, but this time with a different error:

~$ 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

与以下执行跟踪相对应:

Which corresponds to the following execution trace:

~$ 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

The problem is that pippo blocks inside the d_step sequence, and this violates the third condition in the synopsis of d_step documentation, exactly as described.

仔细检查.再次，如果您注释flag;指令，您将发现不会有任何错误跟踪.

Double Check. Again, if you comment the flag; instruction you'll see that there won't be any error trace.

这篇关于Promela中的原子序列.文档矛盾的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！