Противоречивая документация:
Я предполагаю, что это противоречие является просто результатом того, что части документации не обновлялись, чтобы отражать изменения, которые произошли в Spin на протяжении многих лет.
Фактически, в примечаниях к выпуску Спин v. 2.0 мы можем найти следующий фрагмент текста (выделено мной):
2.3.1 Блокировка атомарных последовательностей
До сих пор считалось ошибкой, если атомарная последовательность содержала оператор, который мог заблокировать выполнение последовательности. Это вызывало много путаницы и излишне усложняло моделирование. Начиная с версии Spin 2, атомарная последовательность разрешена для блокировки. Если процесс внутри атомарной последовательности блокируется, управление недетерминированным образом переходит к другому процессу. Если оператор позже становится исполняемым, управление может вернуться к процессу, и атомарное выполнение оставшейся части последовательности возобновится.
Это изменение в семантике позволяет относительно легко моделировать, например, сопрограммы, в которых управление не переходит от одного процесса к другому до тех пор, пока работающий процесс не заблокируется.
Атомные операторы в Promela:
В текущей версии Promela/Spin существуют две атомарные последовательности:
atomic: из документы, выделение мое:
ОПИСАНИЕ
Если последовательность операторов заключена в круглые скобки и снабжена префиксом ключевое слово atomic, это означает, что последовательность должна выполняться как одна неделимая единица, не чередующаяся с другими процессами. При чередовании выполнения процессов ни один другой процесс не может выполнять операторы с момента выполнения первого оператора атомарной последовательности до завершения последнего. Последовательность может содержать произвольные операторы Promela и может быть недетерминированной.
Если какой-либо оператор внутри атомарной последовательности блокируется, атомарность теряется, и другим процессам разрешается начинать выполнение операторов. Когда заблокированный оператор снова становится исполняемым, выполнение атомарной последовательности может быть возобновлено в любой момент. время, но не обязательно немедленно. Прежде чем процесс сможет возобновить атомарное выполнение оставшейся части последовательности, он должен сначала конкурировать со всеми другими активными процессами в системе, чтобы восстановить контроль, то есть сначала он должен быть запланирован для выполнения.
[...]
d_step: из документы, выделение мое:
ОПИСАНИЕ
Последовательность d_step выполняется так, как если бы это был один неделимый оператор. Она сравнима с атомарной последовательностью, но отличается от такой последовательности в следующих трех моментах:
- No goto jumps into or out of a d_step sequence are allowed.
- Последовательность выполняется детерминировано. Если присутствует недетерминизм, он разрешается фиксированным и детерминированным способом, например, всегда выбирая первую истинную защиту в каждой структуре выбора и повторения.
- Это ошибка, если выполнение любого оператора внутри последовательности может быть заблокировано. Это означает, например, что в большинстве случаев операторы отправки и получения нельзя использовать внутри последовательностей 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;, вы увидите, что трассировки ошибок не будет.
person
Patrick Trentin
schedule
31.03.2017
