SPIN如何确定原子流程中流程执行的顺序? [英] How does SPIN decide the order of process execution in atomic processes?

问题描述

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

I am trying to figure out how SPIN chooses the order in which to execute and terminate processes in the following example. I realize that a main focus of SPIN is analyzing concurrent processes, but for my purposes I am just interested in simple linear execution. In the following example I just want step1() then step2() to be executed in that order.

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个输出(我运行了很多次，这是唯一的输出).

However, even with the atomic {} declarations, the processes become interleaved in their execution. Using the command spin -p my_pml_code.pml I get the following 3 outputs only (I ran it many times and these were the only outputs).

运行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

The order is 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

The order is 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

The order is proc 0 -> 0 -> 0 -> 0 ->2 -> 2 -> 1 -> 1 -> 0

我想简单地获得输出:proc 0-> 0-> 0-> 0-> 1-> 1-> 2-> 2-> 0

The output I am trying to get it simply: 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之前(在运行3中)开始和终止，却不能反过来呢?

I realize that proc 0 can't terminate until 1 and 2 have terminated, but why are the terminations of 2 and 1 being interleaved non-deterministicly? Any why is SPIN randomly choosing between executing proc 1 and proc 2 when the init function is atomic and therefore should be executed in order? And why can I get proc 2 to start and terminate before proc 1 (in Run 3) but not the other way around?

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

Note: I have also tested this using dstep instead of atomic and I get the same result.

推荐答案

首先，让我尝试为您的每个问题提供简短答案:

First, let me try give short answers to each of your questions:

1..我知道proc 0直到1和2终止后才能终止，但是为什么2和1的终止不确定地交错?

1. I realise that proc 0 can't terminate until 1 and 2 have terminated, but why are the terminations of 2 and 1 being interleaved non-deterministically?

进程始终以确定性方式终止:2在1之前终止，1在0之前终止，并且0始终是最后一个终止.但是，进程终止并没有什么特别的:进程执行的只是最终转换.结果，在有多个进程使用(立即)可执行指令的任何时间点，都可以进行进程交织.

The processes always terminate in a deterministic fashion: 2 terminates before 1, 1 before 0 and 0 is always the last one. However, there is nothing special about process termination: it is simply the final transition that is taken by a process. As a result, process interleaving is possible at any point in time in which there are more than one process with an (immediately) executable instruction.

2.为什么当init函数为atomic时，SPIN为什么在执行proc 1和proc 2之间随机选择?

2. Any why is SPIN randomly choosing between executing proc 1 and proc 2 when the init function is atomic and therefore should be executed in order?

虽然init是原子执行的，但确实要记住的重要事实是step1和step2是独立的进程，并且在init退出其原子后执行块:run不是函数调用，它只是在环境内部生成一个进程，绝对不能保证立即执行该进程.这可能会或不会发生，这取决于产生的进程是否具有任何可执行指令，当前正在执行的进程是否处于原子顺序以及非确定性调度程序选择的结果./p>

Although it is true that init executes both of his instructions atomically, the important fact to keep in mind is that step1 and step2 are independent processes and are executed after init exits its atomic block: run is not a function call, it just spawns a process inside the environment with absolutely no guarantee that such process is executed immediately. That might or might not happen depending on whether the spawned process has any executable instruction, whether the process that is currently executing is in an atomic sequence and on the outcome of the non-deterministic scheduler process selection.

3.为什么为什么要让proc 2在proc 1之前(在运行3中)启动和终止，却不能反过来呢?

3. And why can I get proc 2 to start and terminate before proc 1 (in Run 3) but not the other way around?

在 Promela 中，进程只能按照其创建的相反顺序终止，如文档:

In Promela, processes can only die in reverse order of their creation, as indicated in the docs:

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终止才能终止.

Therefore, 2 can terminate before 1 because it has higher _pid value, whereas 1 must wait upon 2 to be terminate before it can die.

4..SPIN如何确定原子流程中流程执行的顺序?

4. How does SPIN decide the order of process execution in atomic processes?

如果系统中有多个进程，则没有 atomic 进程.即使将整个过程包含在 atomic 关键字内，终止步骤仍然位于 atomic 块的 outside 外.调度程序永远不会中断执行原子序列的进程，除非该进程在不可执行的指令之前阻塞.在这种情况下，原子性丧失，并且可以安排执行任何其他过程，如文档:

There is no such thing as an atomic process if you have more than one in your system. Even if you enclose the whole body of a process inside the atomic keyword, the termination step is still outside the atomic block. The scheduler never interrupts a process executing an atomic sequence, unless the process blocks in front of an instruction that is not executable. In such a case atomicity is lost and any other process can be scheduled for execution, as described in the docs:

如果原子序列中的任何语句被阻止，则原子性会丢失， 然后允许其他进程开始执行语句. 当阻塞的语句再次变为可执行文件时，将执行 原子序列可以随时恢复，但不一定 立即地.在该流程可以恢复原子的执行之前 在序列的其余部分中，该过程必须首先与所有人竞争 系统中其他活动进程以重新获得控制权，即 必须先安排执行时间.

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.

---

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

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

在您的代码示例中，此 execution-flow 被禁止，因为它使进程1在进程2之前终止，并且规则不允许这样做(请参阅第三个问题的答案.

In your code example, this execution-flow is forbidden because it makes process 1 terminate before process 2 and this is not allowed by the rules (see the answer to your third question).

注意:我也使用dstep而不是atomic进行了测试，并且得到了相同的结果.

Note: I have also tested this using dstep instead of atomic and I get the same result.

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

No statement inside your atomic block can block, therefore there is absolutely no difference among using d_step or atomic in your code. However, I invite you to read this answer to get an insight of similarities and differences among atomic and d_step.

示例执行流:

第二，让我根据执行流的分析尝试更深的答案.

Second, let me try a deeper answer level based on the analysis of the execution-flow.

在您的代码示例中，共有三个过程.

In your code example there are three processes.

init是(总是) 第一个要创建的过程(如果可用)，因此，它是(总是)分配的_pid等于0，并排在第一位.由于init进程的整个主体都包含在 atomic 块中，因此该进程执行run step1();和run step2()而不与其他进程交织.为进程step1分配了_pid等于1，因为它是要创建的第二个进程，而为进程step2分配了_pid等于2，因为它是要创建的第三个进程.

init is (always) the first process to be created (when available), and for this reason it is (always) assigned _pid equal to 0 and scheduled for first. Since the whole body of the init process is enclosed in an atomic block, this process executes run step1(); and run step2() without interleaving with other processes. Process step1 is assigned _pid equal 1, because it's the second process to be created, whereas process step2 is assigned _pid equal 2, since it's the third process to be created.

在您的示例中，只有当init进程到达 atomic 的末尾(在您的代码示例中与该末尾重合)时，才能安排进程step1和step2的执行时间. init代码.

In your example, processes step1 and step2 cannot be scheduled for execution until when the init process reaches the end of the atomic, which in your code example coincides with the end of the init code.

当init到达其主体末端时，该进程(_pid等于0)仍不能消失，因为在环境中至少有一个进程的_pid值大于自己的值，即step1和step2.尽管init被阻止，但step1和step2都可以执行，因此非确定性调度程序可以任意选择step1或step2来执行.

When init reaches the end of its body, the process (with _pid equal to 0) cannot die yet because inside the environment there is at least one process with a _pid value greater than his own, namely step1 and step2. Although init is blocked, both step1 and step2 are ready for execution, so the non-deterministic scheduler can arbitrarily select either step1 or step2 for execution.

• 如果首先调度了step1，则它将执行其唯一的指令globA = 1;，而不会与step2进行交织.请注意，由于 atomic 块内只有一条指令，而该指令本身是原子的，因此 atomic 块是多余的(step2也是一样) .同样，由于step1的_pid等于1，并且仍然有一个具有更高_pid值的进程，因此进程step1仍然无法消失.此时，可以安排执行的唯一进程是step2，因为没有_pid值更高的进程，该进程也可以终止.这允许step1终止，进而允许init死亡.此执行流程对应于您的运行2 .

• If step1 is scheduled first, then it executes its only instruction globA = 1; without interleaving with step2. Notice that, since there is only one instruction inside the atomic block and this instruction is atomic on his own, the atomic block is redundant (the same holds for step2). Again, since step1 has _pid equal to 1 and there is still a process with higher _pid value around, process step1 cannot die yet. At this point, the only process that can be scheduled for execution is step2, which can also terminate because there is no process with higher _pid value. This allows step1 to terminate, which in turn allows init to die as well. This execution-flow corresponds to your run 2.

如果首先安排了step2，则此过程将2的值分配给globB并到达其主体的末尾，即 outside > atomic 块，有两种可能的执行流程:

If step2 is scheduled first, then once this process has assigned the value 2 to globB and reaches the end of its body, which is outside the atomic block, there are two possible execution flows:

• 情况A)，调度程序不确定地选择step2重新执行，并且step2终止；现在，调度程序唯一可用的选项是使step1执行其自己的指令，使其终止，然后也允许init终止.此执行流程对应于运行1 .

• case A) the scheduler non-deterministically selects step2 to execute again, and step2 terminates; now the only available option for the scheduler is to make step1 execute its own instruction, make it terminate and then allow init to terminate too. This execution flow corresponds to run 1.

情况B):调度程序不确定地选择step1执行，step1将1分配给globA，但由于step2仍然有效而无法终止；唯一可以调度的进程是step2，因此后者由调度程序选择后终止，从而允许step1和init也以级联方式终止.此执行流程对应于运行3 .

case B) the scheduler non-deterministically selects step1 to execute, step1 assigns 1 to globA but cannot terminate because step2 is still alive; the only process that can be scheduled is step2, so the latter terminates after being selected by the scheduler, allowing step1 and init to terminate as well in cascade. This execution flow corresponds to run 3.

线性执行:

实现线性执行的最简单，最明显的方法是在模型中仅包含一个过程.弄清楚为什么会这样是微不足道的.因此，您的示例将变为:

The simplest and most obvious way to achieve linear execution is to have only one process inside your model. It is trivial to see why this is the case. So your example would become:

int globA;
int globB;

inline step1()
{
    globA = 1;
}

inline step2()
{
    globB = 2;
}

init
{
    step1();
    step2();
}

由于只有一个过程，因此不再需要在此代码中具有 atomic 块的功能.当然，您可能不赞成这种琐碎的解决方案，所以让我们看看基于全局变量的另一种解决方案:

Having atomic blocks in this code is no longer necessary, since there is only one process. Of course, you might frown upon such a trivial solution, so let's see another solution based on a global variable:

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;
}

与您的代码示例不同，由于 synchronization 变量terminated，在这里globB = 2永远无法在执行globA = 1之前执行.但是，与您的代码示例类似，进程step1和step2的实际终止也需要交织. 即，如果step1立即终止，以便仅在step1完全释放其拥有的资源之后创建step2，则将step2分配为等于1的_pid;否则，将为step2分配_pid等于2.

Differently than your code example, here globB = 2 can never be executed before globA = 1 is executed thanks to the synchronisation variable terminated. However, similarly to your code example, the actual termination of processes step1 and step2 is subject to interleaving. i.e. if step1 terminates immediately, so that step2 is created only after step1 has completely released the resources it owns, then step2 is assigned _pid equal to 1; otherwise, step2 is assigned _pid equal to 2.

我能想到的最佳解决方案是基于消息传递的概念.基本上，该想法是仅允许在任何给定时间点调度当前拥有令牌的进程，并按照所需的调度顺序传递此类令牌 :

The best solution I can think of is based on the concept of message passing. Basically, the idea is to allow only the process that currently holds a token to be scheduled at any given point in time, and to pass around such token in the desired scheduling order:

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;
}

请注意，此解决方案仅强制执行一项可能的计划.可以通过运行交互式仿真进行验证:

Notice that this solution forces only one possible scheduling. This can be verified by running an interactive simulation:

~$ 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!TOKEN之前和out!TOKEN B)之后放置任何指令.创建了哪些进程.

As you can see, the user is never offered the chance to make any choice, because there is only one possible execution-flow. This is obviously due to the fact that A) I did not put any instruction before in!TOKEN and after out!TOKEN B) the desired scheduling order coincides with the order in which processes are created.

这篇关于SPIN如何确定原子流程中流程执行的顺序?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！