modelmodel-checkingpromelaspin

PROMELA: What are interleavings?


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?


Solution

  • 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.