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

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

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

'''Диктофонная запись:''' http://esyr.org/lections/audio/verification_2008_summer/verification_08_02_29.ogg <br />
'''Оригинальная презентация:''' 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 марта.

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://esyr.org/wiki/%D0%92%D0%9F%D0%BD%D0%9C%2C_04_%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F_%28%D0%BE%D1%82_29_%D1%84%D0%B5%D0%B2%D1%80%D0%B0%D0%BB%D1%8F%29

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

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

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 90: / Строка 90: @@
 * переменные объявл. в любом месте.
-В промела нет действ. чисел, числе с плав. запятой, указателей. Массивы поддерж. только одномерные. Предусмотрена иниц. массивов тем числом, которые указали. Можно вводить свои ТД как структуры. Доступ к полям осущ. через точку. Если хочется использовать массивы большей размерности, то можно использовать макросы. Перед обработкой спином файлы препроцессируются, но при этом мсылки на номера строк могут поплыть.
+В промела нет действ. чисел, числе с плав. запятой, уаазтелей. Массивы поддерж. только одномерные. Предусмотрена иниц. массивов тем числом, которые указали. Можно вводить свои ТД как структуры. Доступ к полям осущ. через точку. Если хочется использовать массивы большей размерности, то можно использовать макросы. Перед обработкой спином файлы препроцессируются, но при этом мсылки на номера строк могут поплыть.
 Все типы отображаются на int, и выражения тоже отображаютсяна int. При выч. сначала в инт, потом в целевой тип. В парсере есть контроль типов, но он контроллирует только грубые ошибки. При сужении размера ТД выдаётся предупреждеение.