PROMELA：什么是交织？

Question

假设我们有这段代码：

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
}

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

Answer 1

在 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 的访问。

PROMELA：什么是交织？

PROMELA: What are interleavings?

model

model-checking

promela

spin