SPIN如何决定原子流程中流程执行的顺序?

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

在下面的示例中,我试图弄清楚 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 的终止非确定性地交错?为什么 SPIN 运行domly 在执行 proc 1 和 proc 2 之间进行选择,而 init 函数是原子的,因此应该按顺序执行?为什么我可以让 proc 2 在 proc 1 之前开始和终止(在 运行 3 中)而不是相反?

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

首先,让我试着简短回答你的每个问题:

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?

进程总是以确定性方式终止:21之前终止,10和[之前终止=19=]永远是最后一个。然而,进程终止并没有什么特别之处:它只是进程进行的 final transition。因此,进程交错在任何时间点都是可能的,其中有多个进程具有 (立即) 可执行指令。

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 确实以原子方式执行了他的两条指令,但要记住的重要事实是 step1step2 是独立的进程,并且在 init 退出其 atomic 块:run 不是函数调用,它只是 spawns 环境中的进程不保证立即执行此类过程。这可能发生也可能不发生取决于 spawned process 是否有任何可执行指令,当前正在执行的进程是否在原子序列中以及非确定性调度程序进程的结果select离子.

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 中,进程只能以其创建的相反顺序死亡,如 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 在它之前终止可以死

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

如果您的系统中有多个进程,就没有 atomic 进程这样的东西。即使您将进程的整个主体包含在 atomic 关键字内,终止步骤仍然 outside atomic块。调度程序从不中断执行原子序列的进程,除非进程阻塞在不可执行的指令前面。在这种情况下 原子性丢失 并且可以安排任何其他进程执行,如 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

在您的代码示例中,这个执行流程禁止的,因为它使进程1在进程[=之前终止16=] 而这是规则所不允许的(参见第三个问题的答案)。


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

atomic 块中的任何语句都不能阻塞,因此在代码中使用 d_stepatomic 绝对没有区别。但是,我邀请您阅读 以了解 atomicd_step 之间的异同。


示例执行流程:

其次,让我根据对执行流程的分析尝试一个更深入的答案级别。

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

init(总是) 第一个 要创建的进程 (可用时),因此 (总是) 分配 _pid 等于 0 并排在第一位。由于 init 进程的整个主体包含在 atomic 块中,因此该进程执行 run step1();run step2() 时不会与其他进程交错。进程 step1 被分配 _pid 等于 1,因为它是要创建的第二个进程,而进程 step2 被分配 _pid 等于 2,因为这是要创建的第三个进程。

在您的示例中,进程 step1step2 无法安排执行,直到 init 进程到达 atomic,这在您的代码示例中与 init 代码的末尾一致。

init到达其主体的末尾时,进程(_pid等于0)还不能结束,因为在环境中至少有一个进程具有_pid值大于自己的,即step1step2。虽然 init 被阻塞了,但是 step1step2 都准备好执行了,所以 non-deterministic scheduler 可以任意 select 或者step1step2 执行。

  • 如果 step1 首先被调度,那么它会执行它唯一的指令 globA = 1; 而不会与 step2 交错。请注意,由于 atomic 块中只有一条指令,并且该指令本身是原子的,因此 atomic 块是冗余的(相同适用于 step2)。同样,由于 step1_pid 等于 1 并且周围仍然存在具有更高 _pid 值的进程,因此进程 step1 还不能结束。此时,唯一可以安排执行的进程是 step2,它也可以终止,因为没有更高 _pid 值的进程。这允许 step1 终止,这反过来又允许 init 死亡。这个 execution-flow 对应你的 运行 2.

  • 如果先调度step2,那么一旦这个进程将值2分配给globB并到达其主体的末尾,即outside atomic 块,有两种可能的执行流程:

    • 情况 A) 调度程序非确定性地 selects step2 再次执行,并且 step2 终止;现在调度程序唯一可用的选项是让 step1 执行它自己的指令,让它终止,然后允许 init 也终止。这个执行流程对应运行1.

    • 情况 B) 调度程序非确定性地 selects step1 执行,step1 分配 1globA 但无法终止,因为 step2 还活着;唯一可以调度的进程是 step2,因此后者在被调度程序 select 编辑后终止,从而允许 step1init 以级联方式终止。这个执行流程对应运行 3.


线性执行:

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

int globA;
int globB;

inline step1()
{
    globA = 1;
}

inline step2()
{
    globB = 2;
}

init
{
    step1();
    step2();
}

不再需要此代码中的 atomic 块,因为只有一个进程。当然,您可能会对这种微不足道的解决方案不以为然,那么让我们看看另一个基于全局变量的解决方案:

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

与您的代码示例不同,由于 同步 变量 terminated,这里的 globB = 2 永远不会在 globA = 1 执行之前执行。但是,与您的代码示例类似,进程 step1step2 的实际终止会交错。 如果step1立即终止,使得step2仅在step1完全释放其拥有的资源后才创建,则step2被分配 _pid 等于 1;否则,step2 被分配 _pid 等于 2.

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

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!TOKEN 之前和 out!TOKEN B)[=235= 之前放置任何指令] 所需的调度顺序与创建进程的顺序一致。