1

我试图弄清楚 SPIN 如何在以下示例中选择执行和终止进程的顺序。我意识到 SPIN 的主要焦点是分析并发进程，但出于我的目的，我只对简单的线性执行感兴趣。在下面的示例中，我只希望 step1() 然后 step2() 以该顺序执行。

int globA;
int globB;

proctype step1() {
  atomic {
    globA = 1;
  }
}

proctype step2() { 
  atomic {
    globB = 2;
  }
}

init { 
  atomic {
    run step1();
    run step2();
  }
}

但是，即使使用原子 {} 声明，进程在执行时也会交错。使用命令spin -p my_pml_code.pml我只得到以下 3 个输出（我运行了很多次，这些是唯一的输出）。

运行 1：

  0:    proc  - (:root:) creates proc  0 (:init:)
Starting step1 with pid 1
  1:    proc  0 (:init::1) creates proc  1 (step1)
  1:    proc  0 (:init::1) pml_testing/transition_testing.pml:16 (state 1)  [(run step1())]
Starting step2 with pid 2
  2:    proc  0 (:init::1) creates proc  2 (step2)
  2:    proc  0 (:init::1) pml_testing/transition_testing.pml:17 (state 2)  [(run step2())]
  3:    proc  2 (step2:1) pml_testing/transition_testing.pml:11 (state 1)   [globB = 2]
  4:    proc  1 (step1:1) pml_testing/transition_testing.pml:6 (state 1)    [globA = 1]
  4:    proc  2 (step2:1)               terminates
  4:    proc  1 (step1:1)           terminates
  4:    proc  0 (:init::1)       terminates
3 processes created

顺序是 proc 0 -> 0 -> 0 -> 0 ->2 -> 1 -> 2 -> 1 -> 0

运行 2：

  0:    proc  - (:root:) creates proc  0 (:init:)
Starting step1 with pid 1
  1:    proc  0 (:init::1) creates proc  1 (step1)
  1:    proc  0 (:init::1) pml_testing/transition_testing.pml:16 (state 1)  [(run step1())]
Starting step2 with pid 2
  2:    proc  0 (:init::1) creates proc  2 (step2)
  2:    proc  0 (:init::1) pml_testing/transition_testing.pml:17 (state 2)  [(run step2())]
  3:    proc  1 (step1:1) pml_testing/transition_testing.pml:6 (state 1)    [globA = 1]
  4:    proc  2 (step2:1) pml_testing/transition_testing.pml:11 (state 1)   [globB = 2]
  4:    proc  2 (step2:1)               terminates
  4:    proc  1 (step1:1)           terminates
  4:    proc  0 (:init::1)       terminates
3 processes created

顺序是 proc 0 -> 0 -> 0 -> 0 -> 1 -> 2 -> 2 -> 1 -> 0

运行 3：

  0:    proc  - (:root:) creates proc  0 (:init:)
Starting step1 with pid 1
  1:    proc  0 (:init::1) creates proc  1 (step1)
  1:    proc  0 (:init::1) pml_testing/transition_testing.pml:16 (state 1)  [(run step1())]
Starting step2 with pid 2
  2:    proc  0 (:init::1) creates proc  2 (step2)
  2:    proc  0 (:init::1) pml_testing/transition_testing.pml:17 (state 2)  [(run step2())]
  3:    proc  2 (step2:1) pml_testing/transition_testing.pml:11 (state 1)   [globB = 2]
  3:    proc  2 (step2:1)               terminates
  4:    proc  1 (step1:1) pml_testing/transition_testing.pml:6 (state 1)    [globA = 1]
  4:    proc  1 (step1:1)           terminates
  4:    proc  0 (:init::1)       terminates
3 processes created

顺序是 proc 0 -> 0 -> 0 -> 0 ->2 -> 2 -> 1 -> 1 -> 0

我试图简单地得到它的输出： proc 0 -> 0 -> 0 -> 0 ->1 -> 1 -> 2 -> 2 -> 0

我意识到 proc 0 在 1 和 2 终止之前无法终止，但是为什么 2 和 1 的终止是不确定的交错的？当 init 函数是原子的并且因此应该按顺序执行时，为什么 SPIN 在执行 proc 1 和 proc 2 之间随机选择？为什么我可以让 proc 2 在 proc 1 之前启动和终止（在 Run 3 中），而不是相反？

注意：我也使用dstep代替测试了这个atomic，我得到了相同的结果。

4

1 回答 1

2

首先，让我尝试对您的每个问题进行简短回答：

1.我意识到proc 0直到1和2终止才能终止，但是为什么2和1的终止是不确定的交错的？

进程总是以确定性方式2终止：在 before 1、1before0和0始终是最后一个终止。然而，进程终止并没有什么特别之处：它只是一个进程进行的最终转换。因此，在任何时间点，只要有多个进程具有（立即）可执行指令，进程​​交错都是可能的。

2.为什么当init函数是原子函数时，SPIN会在执行proc 1和proc 2之间随机选择，因此应该按顺序执行？

尽管确实init以原子方式执行他的两条指令，但要记住的重要事实是step1和step2是独立的进程，并且在init退出其原子块后执行：run不是函数调用，它只是在环境中产生一个绝对的进程不保证该过程会立即执行。这可能会发生也可能不会发生，这取决于生成的进程是否有任何可执行指令、当前正在执行的进程是否处于原子序列以及非确定性调度程序进程选择的结果。

3.为什么我可以让 proc 2 在 proc 1 之前启动和终止（在 Run 3 中），而不是相反？

在Promela中，进程只能以与其创建相反的顺序死亡，如文档中所示：

When a process terminates, it can only die and make its _pid number
available for the creation of another process, if and when it has the
highest _pid number in the system. This means that processes can only
die in the reverse order of their creation (in stack order).

因此，2可以提前终止，1因为它具有更高的_pid价值，而1必须等待2终止才能死亡。

4. SPIN如何决定原子进程中的进程执行顺序？

如果您的系统中有多个，则没有原子进程之类的东西。即使您将整个进程的主体包含在atomic关键字中，终止步骤仍然在atomic块之外。调度程序永远不会中断执行原子序列的进程，除非该进程阻塞在一条不可执行的指令前面。在这种情况下，原子性会丢失，并且可以安排任何其他进程执行，如文档中所述：

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

在您的问题中，您声明您的目标是获得以下执行流程：

proc 0 -> 0 -> 0 -> 0 ->1 -> 1 -> 2 -> 2 -> 0

在您的代码示例中，此执行流程被禁止，因为它使流程1在流程之前终止，2并且这是规则不允许的（请参阅第三个问题的答案）。

注意：我还使用 dstep 而不是 atomic 对此进行了测试，得到了相同的结果。

原子块内的任何语句都不能阻塞，因此在代码中使用d_step或使用绝对没有区别。atomic但是，我邀请您阅读此答案，以了解atomic和d_step之间的异同。

示例执行流程：

其次，让我根据对执行流程的分析，尝试更深层次的答案。

在您的代码示例中，有三个进程。

init是（总是）要创建的第一个进程（如果可用），因此它（总是）被分配_pid等于0并安排在第一个进程。由于init进程的整个主体都包含在一个原子块中，因此该进程在执行run step1();时run step2()不会与其他进程交错。Processstep1被分配_pidequal 1，因为它是要创建的第二个进程，而 processstep2被分配_pidequal 2，因为它是要创建的第三个进程。

在您的示例中，直到进程到达atomicstep1结束时，进程step2才能被安排执行，在您的代码示例中，这与代码的结束一致。initinit

当init到达其主体的末尾时，进程（_pid等于0）还不能死亡，因为在环境中至少有一个进程的_pid值大于他自己的值，即step1和step2。虽然init被阻塞，但两者step1都已step2准备好执行，因此非确定性调度程序可以任意选择其中一个step1或step2执行。

  • 如果step1首先被调度，那么它会执行其唯一的指令globA = 1;而不与step2. 请注意，由于原子块内只有一条指令，并且该指令本身是原子的，因此原子块是冗余的（同样适用于step2）。同样，由于step1已经_pid等于1并且周围还有一个具有更高_pid价值的进程，因此进程step1还不能死亡。此时，唯一可以调度执行的进程是step2，它也可以终止，因为没有更高_pid值的进程。这允许step1终止，这反过来也允许init死亡。这个执行流程对应于您的运行 2。

  • 如果step2首先被调度，那么一旦该进程将值分配2给globB并到达其主体的末尾，即在原子块之外，则有两种可能的执行流程：

    • 情况A）调度器非确定性地选择step2再次执行，并step2终止；现在调度程序唯一可用的选项是step1执行自己的指令，使其终止，然后init也允许终止。此执行流程对应于运行 1。

    • 情况B）调度器非确定性地选择step1执行，step1分配1给globA但不能终止，因为step2还活着；唯一可以调度的进程是step2，因此后者在被调度程序选择后终止，允许step1和init级联终止。此执行流程对应于运行 3。

线性执行：

实现线性执行的最简单和最明显的方法是在模型中只包含一个进程。很容易看出为什么会这样。所以你的例子会变成：

int globA;
int globB;

inline step1()
{
    globA = 1;
}

inline step2()
{
    globB = 2;
}

init
{
    step1();
    step2();
}

不再需要在此代码中包含原子块，因为只有一个进程。当然，你可能会对这样一个微不足道的解决方案感到不满，所以让我们看看另一个基于全局变量的解决方案：

int globA;
int globB;
bool terminated;

proctype step1()
{
    globA = 1;
    terminated = true;
}

proctype step2()
{
    globB = 2;
    terminated = true;
}

init
{
    run step1();
    terminated -> terminated = false;
    run step2();
    terminated -> terminated = false;
}

与您的代码示例不同，由于同步变量，这里globB = 2永远不能在执行之前执行。但是，与您的代码示例类似，进程的实际终止并受到交错的影响。即如果立即终止，那么只有在完全释放它拥有的资源之后才创建，然后分配等于; 否则，分配等于。globA = 1terminatedstep1step2step1step2step1step2_pid1step2_pid2

我能想到的最佳解决方案是基于消息传递的概念。基本上，这个想法是只允许在任何给定时间点调度当前持有令牌的进程，并以所需的调度顺序传递此类令牌：

int globA;
int globB;

mtype = { TOKEN };

proctype step1(chan in, out)
{
    in ? TOKEN ->
        globA = 1;
        out ! TOKEN;
}

proctype step2(chan in, out)
{
    in ? TOKEN ->
        globB = 2;
        out ! TOKEN;
}

init
{
    chan token_ring[2] = [0] of { mtype };

    run step1(token_ring[0], token_ring[1]);
    run step2(token_ring[1], token_ring[0]);

    token_ring[0] ! TOKEN;

    token_ring[0] ? TOKEN;
}

请注意，此解决方案仅强制执行一种可能的调度。这可以通过运行交互式模拟来验证：

~$ spin -i ring.pml 
Select a statement
    choice 2: proc  0 (:init::1) ring.pml:25 (state 2) [(run step2(token_ring[1],token_ring[0]))]
Select [1-2]: 2
Select a statement
    choice 3: proc  0 (:init::1) ring.pml:27 (state 3) [token_ring[0]!TOKEN]
Select [1-3]: 3
Select a statement
    choice 2: proc  1 (step1:1) ring.pml:9 (state 2) [globA = 1]
Select [1-3]: 2
Select a statement
    choice 2: proc  1 (step1:1) ring.pml:10 (state 3) [out!TOKEN]
Select [1-3]: 2
Select a statement
    choice 1: proc  2 (step2:1) ring.pml:16 (state 2) [globB = 2]
Select [1-3]: 1
Select a statement
    choice 1: proc  2 (step2:1) ring.pml:17 (state 3) [out!TOKEN]
Select [1-3]: 1
Select a statement
    choice 1: proc  2 (step2:1) ring.pml:18 (state 4) <valid end state> [-end-]
Select [1-3]: 1
Select a statement
    choice 1: proc  1 (step1:1) ring.pml:11 (state 4) <valid end state> [-end-]
Select [1-2]: 1
3 processes created

如您所见，用户永远没有机会做出任何选择，因为只有一种可能的执行流程。这显然是因为A)我没有在前后放置任何指令in!TOKENB out!TOKEN )所需的调度顺序与创建进程的顺序一致。

于 2017-07-25T09:07:36.257 回答