ВПнМ, 05 лекция (от 14 марта)

Материал из eSyr's wiki.

Вторая задача: спин не позволдяет автоматически перебрать все значения переменной, можно вручную, можно разбить на классы эквивалентности и ручками посчитать, но это необязательно, достаточно посчитать для конкретных значений переменных

Пример. Alternating Bit Protocol

• Есть отправитель и получатель
• Отправитель хочет убедиться в доставке сообщения, поэтому посылает дополнительный бит, который получатель должен вернуть
• Если бит вернули, то всё хорошо, иначе повторяется посылка

(модель на Promela)

Единственный момент, который здесь выглядит, диаграмма взаимодействия, выглядит примерно так: ...

Действия по сохранению и игн. сообще здесь не присутствуют, ибо это модель. Елинственный момент --- eval, мы его рассмотрим.

Далее моделируем первые 20 шагов.

Если запустить xspin, то помимо всего прочего, можно будет увидеть диагармму взаимодействия процессов. Сейчас она неинтресна, но при выполнении следующих заданий она пригодится.

Функция eval()

Основная идея этой функции --- отображаем некое значение наконстану, и используем это как ограничитель. В этом случае, приёма не будет, пока ограничитель не выполнится.

Графы программ

Когда строим модель, работаем не с системой переходов, работаем с моделью, система переходов есть, но мы её не рассм. на этом этапе. И, чтобы описать сист. переходов (?), нужно хадать ... , после чего можно сформулировать свойство корректной абстракции.

Напоминание: система переходов задаёт граф, где вершины --- состояния, рёбра --- переходы.

Формально система переходов задаётся следующей сигнатурой: ...

Вспомогательные определения

• D_p --- единый абстрактный домен данных в нашей программе
• P --- программа, эта программа определена, описана на нек-ром множестве переменных
• ...
• ...
• Cond(V_p) --- набор булевых условий V_p

Графы программ

Такой граф можно построить практически для любой импер. программы.

Пример

Такое представление помогает избавиться от синтаксического сахара. Если возьмём программу на промеле, то переходы по метке, while, do, то они будут представлены более-менее унифицированно.

Переход от PG к TS

Далее надо определить, как мы от графа перейдём к системе переходов.

• Основная идея --- раскрутка

Это достаточно формально определение, но не достаточно строгое. Строго это делается через правила вывода.

Параллелизм

Интерливинг

• Абстрагируемся от того, что у нас программа из нескольких процессов
• Есть один процессор и несколько независимых процессов
• Порядок выполнения процессов произволен
• Обоснование чередования: если есть два действия, которые независимо изм. сост. программы, то их параллельное применение равносильно посл. применению в произвю порядке

Пример

x = x + 1 ||| y = y - 2

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

Чередование систем переходов

Чередование графов программ

Если общих переменных нет, то TS(PG_1) ||| TS(PG_2) достоверно описывает композицию двух программ.

Если переменная общая есть, то получим полную лажу, следовательно, надо как-то по-другому описывать.

...

Если мы будем следовать этим правилам, то получим более достоверную систему переходов. Можно заметить, что TS(PG_!) ||| TS(PG_@) != TS(PG_1 ||| PG_2)

Параллелизм и рандеву

Если расм. программы, вып. на нескольких системах, общих перпеменных там нет, надо предложить другие механизмы. Есть предача сообщений. Синхронная (рандеву, хэндшейкинг) и асинхронная (каналы сообщений). В спине, если ёмкость канала равна 0, то это синхр. передача, иначе асинхр.

Рандеву

Пример рандеву: ...

Чтобы можно было удобно записывать попарную композицию, определим попарное рандеву: ...

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