PROMELA: What are interleavings?

Question

Lets say we have this piece of code:

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
}

I don't understand what interleavings are. What exactly are interleaving and where and how many are there in my example above?

Answer 1

In Promela, a process with an executable instruction can be scheduled for execution at any given point in time, provided that no other process is currently executing a uninterruptible atomic sequence.

A single instruction, on its own, it is executed atomically. In order to have multiple instructions in the same atomic sequence, one can use either atomic { } or d_step { }. I refer you to this other question on the topic for learning the difference among the two.

---

In your case, a possible execution trace is:

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

Another, totally admissible, possible execution trace is:

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

The processes are interleaved with one another, meaning that after each instruction of some process P_i (which is not in an uninterruptible atomic sequence), the process P_i can be preempted and some other process P_j can be scheduled for execution (provided that it actually has to execute something).

It is is nothing different from what happens in a multi-tasking unix machine, in which processes are interleaved one another and compete for access to the CPU.