ПРОМЕЛА: Что такое чередование?

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 , процесс с исполняемой инструкцией может быть запланирован для выполнения в любой заданный момент времени, при условии, что никакой другой процесс в настоящее время не выполняет непрерывный атомарныйsequence .

Отдельная инструкция сама по себе выполняется атомарно.Чтобы иметь несколько инструкций в одной и той же атомарной последовательности, можно использовать 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, в которой процессы чередуются друг с другом и конкурируют за доступ к процессору.