时间戳

首页 > 解决方案 > PROMELA：什么是交错？

model - PROMELA：什么是交错？

问题描述

假设我们有这段代码：

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
}

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

标签： modelmodel-checkingpromelaspin

解决方案

在Promela中，可以安排具有可执行指令的进程在任何给定时间点执行，前提是当前没有其他进程正在执行不可中断的原子序列。

一条指令，就其本身而言，它是原子执行的。为了在同一个原子序列中有多个指令，可以使用atomic { }或d_step { }。我建议您参考有关该主题的另一个问题，以了解两者之间的区别。

在您的情况下，可能的执行跟踪是：

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

推荐阅读