PROMELA:什么是交织?

PROMELA: What are interleavings?

假设我们有这段代码:

int x = 3;
int y = 5;
int z = 0;

active proctype P(){
   if
      :: x > y -> z = x
      :: else -> z = y
   fi
}

active proctype Q(){
    x++
}

active proctype R(){
    y = y - x
}

我不明白交错是什么。在我上面的示例中,到底什么是交错,交错在哪里,有多少?

Promela 中,可以安排具有 可执行 指令的进程在任何给定时间点执行,前提是没有其他进程当前正在执行 uninterruptible atomic sequence.

单条指令,就其本身而言,它是原子执行的。为了在同一个原子序列中有多个指令,可以使用 atomic { } or d_step { }. I refer you to 来了解两者之间的差异。


对于您的情况,可能的执行跟踪是:

x++           // Q(), x := 4
z = y         // P(), z := 5
y = y - x     // R(), y := 1

另一个完全可以接受的可能执行跟踪是:

y = y - x     // R(), y := 2
x++           // Q(), x := 4
z = x         // P(), z := 4

进程彼此交错,这意味着在某个进程P_i(不在不可中断的原子序列中)的每条指令之后,进程P_i 可以被抢占并且可以安排其他一些进程 P_j 执行(前提是它实际上必须执行某些事情)。

这与多任务 unix 机器中发生的事情没有什么不同,其中进程相互交错并竞争对 CPU 的访问。