Как SPIN определяет порядок выполнения процессов в атомарных процессах?

Question

Я пытаюсь понять, как SPIN выбирает порядок выполнения и завершения процессов в следующем примере. Я понимаю, что основное внимание в SPIN уделяется анализу параллельных процессов, но для моих целей я просто заинтересован в простом линейном выполнении. В следующем примере я просто хочу, чтобы step1() и step2() выполнялись в этом порядке.

int globA;
int globB;

proctype step1() {
  atomic {
    globA = 1;
  }
}

proctype step2() { 
  atomic {
    globB = 2;
  }
}

init { 
  atomic {
    run step1();
    run step2();
  }
}

Однако даже при использовании атомарных {} объявлений процессы чередуются при их выполнении. Используя команду spin -p my_pml_code.pml Я получаю только следующие 3 выхода (я запускал его много раз, и это были единственные выходы).

Прогон 1:

  0:    proc  - (:root:) creates proc  0 (:init:)
Starting step1 with pid 1
  1:    proc  0 (:init::1) creates proc  1 (step1)
  1:    proc  0 (:init::1) pml_testing/transition_testing.pml:16 (state 1)  [(run step1())]
Starting step2 with pid 2
  2:    proc  0 (:init::1) creates proc  2 (step2)
  2:    proc  0 (:init::1) pml_testing/transition_testing.pml:17 (state 2)  [(run step2())]
  3:    proc  2 (step2:1) pml_testing/transition_testing.pml:11 (state 1)   [globB = 2]
  4:    proc  1 (step1:1) pml_testing/transition_testing.pml:6 (state 1)    [globA = 1]
  4:    proc  2 (step2:1)               terminates
  4:    proc  1 (step1:1)           terminates
  4:    proc  0 (:init::1)       terminates
3 processes created

Порядок: proc 0 -> 0 -> 0 -> 0 -> 2 -> 1 -> 2 -> 1 -> 0

Прогон 2:

  0:    proc  - (:root:) creates proc  0 (:init:)
Starting step1 with pid 1
  1:    proc  0 (:init::1) creates proc  1 (step1)
  1:    proc  0 (:init::1) pml_testing/transition_testing.pml:16 (state 1)  [(run step1())]
Starting step2 with pid 2
  2:    proc  0 (:init::1) creates proc  2 (step2)
  2:    proc  0 (:init::1) pml_testing/transition_testing.pml:17 (state 2)  [(run step2())]
  3:    proc  1 (step1:1) pml_testing/transition_testing.pml:6 (state 1)    [globA = 1]
  4:    proc  2 (step2:1) pml_testing/transition_testing.pml:11 (state 1)   [globB = 2]
  4:    proc  2 (step2:1)               terminates
  4:    proc  1 (step1:1)           terminates
  4:    proc  0 (:init::1)       terminates
3 processes created

Порядок: proc 0 -> 0 -> 0 -> 0 -> 1 -> 2 -> 2 -> 1 -> 0

Прогон 3:

  0:    proc  - (:root:) creates proc  0 (:init:)
Starting step1 with pid 1
  1:    proc  0 (:init::1) creates proc  1 (step1)
  1:    proc  0 (:init::1) pml_testing/transition_testing.pml:16 (state 1)  [(run step1())]
Starting step2 with pid 2
  2:    proc  0 (:init::1) creates proc  2 (step2)
  2:    proc  0 (:init::1) pml_testing/transition_testing.pml:17 (state 2)  [(run step2())]
  3:    proc  2 (step2:1) pml_testing/transition_testing.pml:11 (state 1)   [globB = 2]
  3:    proc  2 (step2:1)               terminates
  4:    proc  1 (step1:1) pml_testing/transition_testing.pml:6 (state 1)    [globA = 1]
  4:    proc  1 (step1:1)           terminates
  4:    proc  0 (:init::1)       terminates
3 processes created

Порядок: proc 0 -> 0 -> 0 -> 0 -> 2 -> 2 -> 1 -> 1 -> 0

На выходе я пытаюсь получить его просто: proc 0 -> 0 -> 0 -> 0 -> 1 -> 1 -> 2 -> 2 -> 0

Я понимаю, что proc 0 не может завершиться, пока не завершатся 1 и 2, но почему окончания 2 и 1 чередуются недетерминированно? Любой, почему SPIN случайно выбирает между выполнением proc 1 и proc 2, когда функция init является атомарной и, следовательно, должна выполняться по порядку? И почему я могу заставить proc 2 запускаться и завершаться до proc 1 (в Run 3), а не наоборот?

Примечание: я также проверил это с помощью dstep вместо atomic и я получаю тот же результат.

Answer 1

Сначала позвольте мне дать краткие ответы на каждый из ваших вопросов:

1. Я понимаю, что proc 0 не может завершиться, пока не завершатся 1 и 2, но почему окончания 2 и 1 чередуются недетерминированно?

Процессы всегда заканчиваются детерминированным способом: 2 заканчивается до 1, 1 до 0 а также 0 всегда последний. Однако в завершении процесса нет ничего особенного: это просто последний переход, который выполняет процесс. В результате чередование процессов возможно в любой момент времени, когда существует более одного процесса с (немедленно) исполняемой инструкцией.

2. Любой, почему SPIN случайным образом выбирает между выполнением proc 1 и proc 2, когда функция init является атомарной и, следовательно, должна выполняться по порядку?

Хотя это правда, что init выполняет обе его инструкции атомарно, важно помнить, что step1 а также step2 являются независимыми процессами и выполняются после init выходит из своего атомного блока: run это не вызов функции, он просто порождает процесс внутри среды без какой-либо гарантии, что такой процесс будет выполнен немедленно. Это может произойти или не произойти в зависимости от того, имеет ли порожденный процесс какую-либо исполняемую инструкцию, находится ли выполняемый в данный момент процесс в атомарной последовательности и от результата недетерминированного выбора процесса планировщика.

3. И почему я могу заставить proc 2 запускаться и завершаться раньше, чем proc 1 (в Run 3), а не наоборот?

В Promela процессы могут умирать только в обратном порядке их создания, как указано в документах:

When a process terminates, it can only die and make its _pid number
available for the creation of another process, if and when it has the
highest _pid number in the system. This means that processes can only
die in the reverse order of their creation (in stack order).

Следовательно, 2 может прекратить раньше 1 потому что у него выше _pid значение, тогда как 1 должен ждать 2 быть прекращенным, прежде чем он может умереть.

4. Как SPIN определяет порядок выполнения процессов в атомарных процессах?

Нет такого понятия, как атомарный процесс, если в вашей системе их больше одного. Даже если вы заключите все тело процесса в ключевое слово atomic, шаг завершения все еще находится за пределами атомарного блока. Планировщик никогда не прерывает процесс, выполняющий атомарную последовательность, если только процесс не блокируется перед командой, которая не является исполняемой. В таком случае атомарность теряется, и любой другой процесс может быть запланирован для выполнения, как описано в документации:

Если какой-либо оператор внутри атомарной последовательности блокируется, атомарность теряется, и тогда другим процессам разрешается начинать выполнение операторов. Когда заблокированный оператор снова становится исполняемым, выполнение атомарной последовательности может быть возобновлено в любое время, но не обязательно немедленно. Прежде чем процесс сможет возобновить атомарное выполнение оставшейся части последовательности, процесс должен сначала конкурировать со всеми другими активными процессами в системе, чтобы восстановить управление, то есть сначала он должен быть запланирован для выполнения.

---

В своем вопросе вы утверждаете, что ваша цель - получить следующий поток выполнения:

proc 0 -> 0 -> 0 -> 0 ->1 -> 1 -> 2 -> 2 -> 0

В вашем примере кода этот поток выполнения запрещен, потому что он делает процесс 1 прекратить до процесса 2 и это не разрешено правилами (см. ответ на третий вопрос).

---

Примечание: я также проверил это, используя dstep вместо atomic, и я получил тот же результат.

Никакое утверждение внутри вашего атомарного блока не может блокировать, поэтому нет никакой разницы между использованием d_step или же atomic в вашем коде. Тем не менее, я предлагаю вам прочитать этот ответ, чтобы понять сходства и различия между атомарными и d_step.

---

ПРИМЕР ИСПОЛНИТЕЛЬНОГО ПОТОКА:

Во-вторых, позвольте мне попробовать более глубокий уровень ответа, основанный на анализе потока выполнения.

В вашем примере кода есть три процесса.

init (всегда) первый процесс, который будет создан (когда доступен), и по этой причине он (всегда) назначен _pid равно 0 и запланировано на первое. Так как все тело init процесс заключен в атомарный блок, этот процесс выполняется run step1(); а также run step2() без чередования с другими процессами. Процесс step1 назначен _pid равный 1потому что это второй процесс, который будет создан, тогда как процесс step2 назначен _pid равный 2, поскольку это третий процесс, который будет создан.

В вашем примере процессы step1 а также step2 не может быть запланировано к исполнению до тех пор, пока init процесс достигает конца атомарного, который в вашем примере кода совпадает с концом init код.

когда init достигает конца своего тела, процесс (с _pid равно 0) пока не может умереть, потому что внутри окружающей среды есть хотя бы один процесс с _pid ценность больше его собственной, а именно step1 а также step2, Хотя init заблокирован, оба step1 а также step2 готовы к выполнению, поэтому недетерминированный планировщик может произвольно выбрать либо step1 или же step2 для выполнения.

• Если step1 сначала планируется, затем выполняется единственная инструкция globA = 1; без чередования с step2, Обратите внимание, что, поскольку внутри атомарного блока есть только одна инструкция, и эта инструкция сама по себе является атомарной, атомарный блок является избыточным (то же самое относится и к step2). Опять же, так как step1 имеет _pid равно 1 и есть еще процесс с более высоким _pid ценность вокруг, процесс step1 не может умереть еще. На данный момент, единственный процесс, который может быть запланирован для выполнения, step2, который также может завершиться, потому что нет процесса с более высоким _pid значение. Это позволяет step1 прекратить, что в свою очередь позволяет init умереть также. Этот поток выполнения соответствует вашему прогону 2.

• Если step2 сначала планируется, а затем этот процесс назначил значение 2 в globB и достигает конца своего тела, которое находится за пределами атомарного блока, существует два возможных потока выполнения:

  • случай А) планировщик недетерминированно выбирает step2 выполнить снова и step2 заканчивается; теперь единственная доступная опция для планировщика - сделать step1 выполнить свою собственную инструкцию, заставить ее завершиться и затем разрешить init прекратить тоже. Этот поток выполнения соответствует прогону 1.

  • случай B) планировщик недетерминированно выбирает step1 выполнить, step1 правопреемники 1 в globA но не может прекратить, потому что step2 все еще жив; единственный процесс, который может быть запланирован, step2, так что последний заканчивается после выбора планировщиком, что позволяет step1 а также init завершить также в каскаде. Этот поток выполнения соответствует прогону 3.

---

ЛИНЕЙНОЕ ИСПОЛНЕНИЕ:

Самый простой и очевидный способ достижения линейного выполнения - это иметь только один процесс внутри вашей модели. Нетрудно понять, почему это так. Таким образом, ваш пример станет:

int globA;
int globB;

inline step1()
{
    globA = 1;
}

inline step2()
{
    globB = 2;
}

init
{
    step1();
    step2();
}

Наличие атомарных блоков в этом коде больше не требуется, поскольку существует только один процесс. Конечно, вы можете не одобрить такое тривиальное решение, поэтому давайте посмотрим на другое решение, основанное на глобальной переменной:

int globA;
int globB;
bool terminated;

proctype step1()
{
    globA = 1;
    terminated = true;
}

proctype step2()
{
    globB = 2;
    terminated = true;
}

init
{
    run step1();
    terminated -> terminated = false;
    run step2();
    terminated -> terminated = false;
}

В отличие от вашего примера кода, здесь globB = 2 никогда не может быть выполнен раньше globA = 1 выполняется благодаря переменной синхронизации terminated, Однако, как и в вашем примере кода, фактическое завершение процессов step1 а также step2 подлежит чередованию. т.е. если step1 заканчивается немедленно, так что step2 создается только после step1 полностью высвободил имеющиеся у него ресурсы, затем step2 назначен _pid равно 1; иначе, step2 назначен _pid равно 2,

Лучшее решение, которое я могу придумать, основано на концепции передачи сообщений. По сути, идея состоит в том, чтобы позволить планировать только процесс, который в настоящее время содержит токен, в любой заданный момент времени, и передавать такой токен в желаемом порядке планирования:

int globA;
int globB;

mtype = { TOKEN };

proctype step1(chan in, out)
{
    in ? TOKEN ->
        globA = 1;
        out ! TOKEN;
}

proctype step2(chan in, out)
{
    in ? TOKEN ->
        globB = 2;
        out ! TOKEN;
}

init
{
    chan token_ring[2] = [0] of { mtype };

    run step1(token_ring[0], token_ring[1]);
    run step2(token_ring[1], token_ring[0]);

    token_ring[0] ! TOKEN;

    token_ring[0] ? TOKEN;
}

Обратите внимание, что это решение вызывает только одно возможное планирование. Это можно проверить, запустив интерактивное моделирование:

~$ spin -i ring.pml 
Select a statement
    choice 2: proc  0 (:init::1) ring.pml:25 (state 2) [(run step2(token_ring[1],token_ring[0]))]
Select [1-2]: 2
Select a statement
    choice 3: proc  0 (:init::1) ring.pml:27 (state 3) [token_ring[0]!TOKEN]
Select [1-3]: 3
Select a statement
    choice 2: proc  1 (step1:1) ring.pml:9 (state 2) [globA = 1]
Select [1-3]: 2
Select a statement
    choice 2: proc  1 (step1:1) ring.pml:10 (state 3) [out!TOKEN]
Select [1-3]: 2
Select a statement
    choice 1: proc  2 (step2:1) ring.pml:16 (state 2) [globB = 2]
Select [1-3]: 1
Select a statement
    choice 1: proc  2 (step2:1) ring.pml:17 (state 3) [out!TOKEN]
Select [1-3]: 1
Select a statement
    choice 1: proc  2 (step2:1) ring.pml:18 (state 4) <valid end state> [-end-]
Select [1-3]: 1
Select a statement
    choice 1: proc  1 (step1:1) ring.pml:11 (state 4) <valid end state> [-end-]
Select [1-2]: 1
3 processes created

Как видите, пользователю никогда не предлагается возможность сделать какой-либо выбор, потому что существует только один возможный поток выполнения. Это, очевидно, связано с тем, что а) я не ставил никаких инструкций до in!TOKEN и после out!TOKEN Б) желаемый порядок планирования совпадает с порядком, в котором создаются процессы.