Атомные последовательности в промеле. Противоречивость в документации

Question

Здесь, http://spinroot.com/spin/Man/Manual.html, написано, что:

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

И здесь, http://spinroot.com/spin/Man/atomic.html, написано, что:

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

Итак, что является правдой? Из первой цитаты мы можем узнать, что в атомарной блокировке запрещается (не первая инструкция)

Из второй цитаты мы узнаем, что в атомарном блоке все нормально. Вы просто теряете атомарность и все.

Answer 1

Противоречивая документация:

Я предполагаю, что противоречие является просто результатом того, что части документации не обновляются, чтобы отразить изменения, которые произошли в Spin за эти годы.

Фактически, в примечаниях к выпуску Spin v. 2.0 мы можем найти следующий фрагмент текста (выделение мое):

2.3.1 Блокировка атомных последовательностей

До сих пор считалось ошибкой, если атомарная последовательность содержала какое-либо утверждение, которое могло бы заблокировать выполнение последовательности. Это вызвало много путаницы и без необходимости усложняет моделирование. Начиная с версии Spin 2, атомарная последовательность может блокироваться. Если процесс внутри атомарной последовательности блокируется, управление недетерминированно переходит к другому процессу. Если позднее оператор становится исполняемым, управление может вернуться к процессу, и атомарное выполнение оставшейся части последовательности возобновляется.

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

---

Атомные заявления в Промеле:

В текущей версии Promela/Spin существует две атомные последовательности:

• атомный: из документов, акцент мой:

  ОПИСАНИЕ

  Если последовательность операторов заключена в круглые скобки и имеет префикс с ключевым словом atomic, это указывает на то, что последовательность должна выполняться как одна неделимая единица, не чередующаяся с другими процессами. При чередовании выполнения процессов никакой другой процесс не может выполнять операторы с момента, когда первый оператор атомарной последовательности выполняется до последнего. Последовательность может содержать произвольные операторы Promela и может быть недетерминированной.

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

  [...]

• d_step: из документов, акцент мой:

  ОПИСАНИЕ

  Последовательность d_step выполняется так, как если бы это был один неделимый оператор. Он сопоставим с атомарной последовательностью, но отличается от таких последовательностей следующими тремя точками:

  • Перейти в или из последовательности d_step не допускается.
  • Последовательность выполняется детерминистически. Если присутствует недетерминизм, он разрешается фиксированным и детерминированным способом, например, всегда выбирая первого истинного защитника в каждой структуре выбора и повторения.
  • Ошибка, если выполнение какого-либо оператора внутри последовательности может блокироваться. Это означает, например, что в большинстве случаев операторы отправки и получения не могут использоваться внутри последовательностей d_step.

  [...]

Конечно, это можно проверить на простом примере Promela.

---

ТЕСТ 1: потеря атомарности с atomic {}

Возьмите следующую модель Promela, в которой два процесса pippo а также pluto выполнить atomic {} последовательность инструкций до 10 раз. Каждый процесс сохраняет свой уникальный _pid внутри глобальной переменной p когда он начинает выполнение атомарной последовательности, а затем проверяет flag переменная:

• если flag является true, pippo может выполнить, но pluto не может, поэтому pluto должен временно потерять атомарность (в некоторых трассировках выполнения)
• если flag является false, pluto может выполнить, но pippo не может, поэтому pippo должен временно потерять атомарность (в некоторых трассировках выполнения)

Мы проверяем последний случай, добавив assert(p == _pid) инструкция в конце атомной последовательности в pippo, Если условие не нарушено, то это означает, что нет выполнения, в котором pippo теряет атомарность внутри атомной последовательности и pluto начинает выполнять вместо В противном случае мы доказали, что описание в связанной документации для atomic {} это точно.

bool flag;
pid p;

active proctype pippo ()
{
    byte i;
    do
        :: i < 10 ->
            atomic {
                true ->
                p = _pid;
                flag;      /* executable only if flag is true */
                printf("pippo unblocked\n");
                flag = !flag;
                assert(p == _pid);
            };
            i++;
        :: else -> break;
    od;
};

active proctype pluto ()
{
    byte i;
    do
        :: i < 10 ->
            atomic {
                true ->
                p = _pid;
end:
                !flag;     /* executable only if flag is false */
                printf("pluto unblocked\n");
                flag = !flag;
            };
            i++;
        :: else -> break;
    od;
};

Если мы выполняем формальную проверку с помощью Spin, он находит трассировку выполнения, которая нарушает свойство:

~$ spin -search -bfs test.pml    # -bfs: breadth-first-search, results in a 
                                 # shorter counter-example

pan:1: assertion violated (p==_pid) (at depth 6)
pan: wrote test.pml.trail

(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
    + Breadth-First Search
    + Partial Order Reduction

Full statespace search for:
    never claim             - (none specified)
    assertion violations    +
    cycle checks            - (disabled by -DSAFETY)
    invalid end states      +

State-vector 20 byte, depth reached 6, errors: 1
       15 states, stored
          10 nominal states (stored-atomic)
        0 states, matched
       15 transitions (= stored+matched)
        5 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001   equivalent memory usage for states (stored*(State-vector + overhead))
    0.290   actual memory usage for states
  128.000   memory used for hash table (-w24)
  128.195   total actual memory usage

pan: elapsed time 0 seconds

Утверждение нарушено, как указано в документации. Вы можете воспроизвести неверную трассировку выполнения следующим образом:

 ~$ spin -t -p -l -g test.pml

Двойная проверка. Теперь, если вы прокомментируете инструкцию flag: внутри pippo и вы повторите процедуру проверки, вы увидите, что не будет никаких следов выполнения, нарушающих утверждение. Это потому, что нет другой инструкции в атомарной последовательности pippo может блокировать, и поэтому атомарность никогда не теряется.

---

ТЕСТ 2: ошибка блокировки с d_step {}

Теперь возьмите тот же пример кода и подставьте atomic ключевое слово внутри pippo с d_step:

bool flag;
pid p;

active proctype pippo ()
{
    byte i;
    do
        :: i < 10 ->
            d_step {
                true ->
                p = _pid;
                flag;      /* executable only if flag is true */
                printf("pippo unblocked\n");
                flag = !flag;
                assert(p == _pid);
            };
            i++;
        :: else -> break;
    od;
};

active proctype pluto ()
{
    byte i;
    do
        :: i < 10 ->
            atomic {
                true ->
                p = _pid;
end:
                !flag;     /* executable only if flag is false */
                printf("pluto unblocked\n");
                flag = !flag;
            };
            i++;
        :: else -> break;
    od;
};

Если вы формально подтвердите эту модель, вы увидите, что она все еще находит контрпример, но на этот раз с другой ошибкой:

~$ spin -search -bfs test.pml 
pan:1: block in d_step seq (at depth 2)
pan: wrote test.pml.trail

(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
    + Breadth-First Search
    + Partial Order Reduction

Full statespace search for:
    never claim             - (none specified)
    assertion violations    +
    cycle checks            - (disabled by -DSAFETY)
    invalid end states      +

State-vector 20 byte, depth reached 2, errors: 1
        4 states, stored
           4 nominal states (stored-atomic)
        0 states, matched
        4 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000   equivalent memory usage for states (stored*(State-vector + overhead))
    0.290   actual memory usage for states
  128.000   memory used for hash table (-w24)
  128.195   total actual memory usage

pan: elapsed time 0 seconds

Что соответствует следующей трассировке выполнения:

~$ spin -t -p -l -g test.pml
using statement merging
  1:    proc  1 (pluto:1) test.pml:26 (state 1) [((i<10))]
  2:    proc  0 (pippo:1) test.pml:8 (state 1)  [((i<10))]
  3:    proc  0 (pippo:1) test.pml:9 (state 8)  [(1)]
  3:    proc  0 (pippo:1) test.pml:11 (state 3) [p = _pid]
spin: trail ends after 3 steps
#processes: 2
        flag = 0
        p = 0
  3:    proc  1 (pluto:1) test.pml:27 (state 7)
  3:    proc  0 (pippo:1) 
2 processes created

Проблема в том, что pippo блоки внутри d_step последовательность, и это нарушает третье условие в кратком изложении d_step документация, точно так, как описано.

Двойная проверка. Опять же, если вы прокомментируете flag; инструкция вы увидите, что не будет никаких ошибок.