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
}

Я не понимаю, что такое чередование. Что именно является чередованием и где и сколько их в моем примере выше?


model promela spin model-checking
person jdoe    schedule 10.12.2018    source источник

Ответы (1)


arrow_upward
0
arrow_downward

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

person Patrick Trentin    schedule 10.12.2018