ВПнМ, 04 лекция (от 29 февраля)

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

Диктофонная запись: http://esyr.org/lections/audio/verification_2008_summer/verification_08_02_29.ogg
Оригинальная презентация: http://savenkov.lvk.cs.msu.su/mc/lect4.pdf

Третье задание --- будет дана функция из minix, нужно будет построить модель,

Последнее задание --- будет дана распр. система, нужно будет смоделировать макромир.

Всего будет заданий 4

Следующей лекции не будет.

Как считать количество достижимых состояний --- можно посчитать при помощи SPIN.

[править] Основные операторы

[править] Взаимодействие через каналы сообщений

Начнём мы с примера на взаимное исключение. Это неправильный алгоритм. Идея такая: есть переменная busy, которая показывает, что крит. переменная занята. Есть мьютекс, который показывает количество процессов. Мы описываем инвариант через этот мьютекс, мьютекс никогда не больше 1. Описываем процесс: если критю.ю секция не знанята, то выставляем, что она занята, что-то делаем, уменьшаем количество процессов, освобождаем крит. секцуию. Соответственно, цикл здесь не нужен, здесь работает внешний недетерминизм, провепрка может быть выполнена в любой момент. Запускаем мы процессы при помощи конструкции atomic, что означает, что они выполнены за один переход. Если не будет, то мы сначала запустим один процесс, потом второй, внесём опередлённость. Запустим верификацию: компилируем gcc'ой, запускаем, инвариант нарушается на глубине 10. Действительно, если мы запустим моделирование контрпримера при помощи ключа -t, то мы получим трассу модели, которая привела к нарушению ассерта. Потом можно вернуться к модели, и заметить, что есть гонка. Если оба процесса проверят, не занятяа ли крит. секция, а потом её займут, то они оба окажутся в ней. Улучшим этот алгоритм. Пусть будет две переменных, по одной на процесс, буждет мьютекс, используемый для проверки инварианта. Процесс А выставляет флаг о том, что хочет занять крит. секцию, проверяет, находится ли в ней процесс В, потом увеличивает мьютекс, уменьшает, и говорит, что вышел. Процесс В аналогичный. Запускаем и видим, что этот алгоритм тоже неправильный. Мы вошли в дедлок. Если дальше сгенерируем трейс, то увидим, что оба процесса в дедлоке, и действительно, если они синхронно выполнят флаг о захвате крит секции, то потом они будут бесконечно долго ждать. На самом деле, такие алгоритмы придумывались в 60-х годах, и очень часто, что алгоритм обсуждался годами, и бывало так, что какая-то ошибка оставалась и вскрывалась через гооды эксплуатации. Далее идут несколько примеров правильных алгоритмов --- алгоритм Петерсона (см РОСы). Алгоритм Лампорта: используется массив переменных, говорящих о том, чей ход, в том виде, в котором здесь приведён, корректен, но в спине количество процессов не может превышать 256, соотвтетсвенно, возникает вопрос, что будет, если эта переменная будет больше 255. Но это не задание, но 4 задание будет на это похоже.

[править] Последние два типа операторов Промела --- отправка и приём сообщений

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

[править] Каналы сообщений

Каналы огр. объёма.

Двух типов:

• Асинхронные ---
• Синхронные --- ёмкость канала равна 0

Канал в промела объявл след образом: есть тип переменной канал, далее записываем размер канала, тип сообщений, которые могут находиться в этом канале. В данном примере могут передаваться сообщения, состоящие из трёх полей.

Примеры:

• Неинициализированный канал
• Канал типа рандеву

mtype --- не только перечисл. тип, это тип, предн. для передачи сообщ. Он принимает знач. от 0..255, 0 только по умолч. При этом можно сопост этому итпу символьные константы. Им последовательно будут присваиваться номера.

[править] Отправка и приём

Отправка сообщений запиывется через воскл. знак.

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

Пример:

При помощи макроса вводим константую

...

[править] Асинхронная передача

Отпр. блокируется, если канал полон, получатель --- если пуст.

[править] Синхр. передача

С точки зрения системы переходов передача выполняется за один переход.

Пример: моделирование семафора.

[править] Другие операции с каналами

Можно проверить длину, пустоту, полноту. Вместо отрицаний данных выражений есть nempty, nfull. Это сделано в целях оптимизации.

[править] Продвинутые операции работы с каналами

• Можно написать приём сообщения, сообщ. в квадратных скобках.
• Можно записать в угловых скобках. Выполнимо, если ... . При этом сообщение удалено не будет.
• Круглые скобки можно писать произв. образом. Обычно ограничение вне, переменные внутри.

[править] Видимость канала

Каналы глобальные. Это позволяет делать разные интересные вещи.

Пример иллюстрирует то, что каналы с точки зрения передачи сообщ. такие же объекты.

В конце b стоит 0, чтобы канал не исчез.

[править] Особые случаи: Упорядоченначя отправка и случайный приём

[править] Основные типы данных Promela

Неочевидные вещи: тип unsigned, для которого указывается количество занимаемых бит.

• По умолчанию все объекты иниц. нулём, но не для каждого типа это корректно.
• Переменные объявл. до первого исп. Если каналы все глобальные, то обыекты бывают двух уровней видимости --- локальные и глобальные.
• переменные объявл. в любом месте.

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

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

В отличие от С, переменные видны во всём процессе.

[править] Поток управления

• Использовать послед. композицию (оператор ""), метки и goto
• Использовать макросы и inline. Используются те же самые операторы, но структурированно описывается программа.
• Использование атомарных посл., но в программе в распр. системах это же не фикс.
• Недетерм. выбор и итерации
• escape-последовательности, когда говорим, что некотороая посл. операторов выполняется до того, как быдет выполнено опр. условие.

[править] Макросы

Используются за тем же, зачем в С.

Минусы ---- имена макросов не видны в парсере. Для замены констр. лучше исп. инлайн.

[править] If

else работает не так, как в С. Если элс отсутствует, то выполнение блокируется. То есть, надо явно описыать все варианты ифа.

[править] Специальные выражения и переменные

Есть timeout --- true, если невыполним ни один из операторов модели. То есть, модель находится в дедлоке.

_ --- /dev/nul

[править] do

do --- оператор if в цикле. Из такого цикла можно выйти только по break или goto.

Пример: ждём, пока не наступит a == b

Последние две лекции дали информацию, которой достаточно для построения модели. Пока нет данных для проверки сложных свойств, но моделировать можно всё. Соответственно, можно выполнять моделирование. Второе задание --- описать полученную программу в виде модели, посмотреть, сколько состояний, прислать на почту модель и то, что выдаёт верификатор в консоли. Это до 14 марта.