4 - Среда верификации SPIN. Описание моделей на языке Promela (К. Савенков - Презентации лекций)

Верификация программна моделяхЛекция №4Среда верификации SPIN. Описаниемоделей на языке Promela.Константин Савенков (лектор)План лекции• Применение SPIN для верификациипрограмм на моделях,• Описание моделей программ на языкеPromela:– основные операторы,– недетерминизм,– синхронизация процессов,– задание потока управления модели.Верификация программы припомощи модели• Нам нужно задавать как система устроена икак она должна быть устроена;• Таким образом, нужны две нотации:– чтобы описать поведение (устройство системы),– чтобы описать требования (свойства правильности);• Программа-верификатор проверяет, чтоустройство системы удовлетворяет свойствамправильности;• Выбранная нотация гарантирует разрешимостьпроверки любого свойства любой модели.Верификация программы припомощи моделидолжно бытьпустоВозможное поведениепрограммыправильное неправильноеSPIN, Promela, LTL• SPIN – Simple Promela INterpreter,• Promela – Process Meta Language,• LTL – Linear Temporal Logic.http://spinroot.comдокументация, дистрибутивы,учебные курсыSPIN, Promela, LTL• SPIN:– моделирование,– верификация;• Promela:– недетерминированный язык с охраняемыми командами,– задача языка – не предотвратить описание моделейплохих программ,– задача языка – разрешить описывать такие модели,которые могут быть верифицированыПроцесс верификацииМодель наPromela-aSPINсвойствоправильности-ipan.cверифицирующийкод на СКомпиляторСисполняемыйверификатор-vслучайное моделированиеинтерактивное моделированиеуправляемое моделирование-tконтрпримерыКлючевые моменты• У моделей – конечное число состояний(потенциально бесконечные элементымоделей в Promela ограничены)– гарантирует разрешимость верификации,– тем не менее, у модели может быть бесконечноечисло вычислений;• асинхронное выполнение процессов– нет глобальных часов,– по умолчанию синхронизация разных процессовотсутствует;Ключевые моменты• Недетерминированный поток управления– абстракция от деталей реализации;• Понятие выполнимости оператора– с любым оператором связаны понятияпредусловия и эффекта,– оператор выполняется (производя эффект),только если предусловие истинно, в противномслучае он заблокирован,– Пример: q?m – если канал q не пуст, читаем изнего сообщение, иначе ждём.Устройство модели на Promelaглобальные данныеТри типа объектов:– процессы,– глобальные илокальныеобъекты данных,– каналысообщений.процесс0процесс1каналысообщенийлокальные данныелокальные данныеHello, world!немедленное инстанцированиеописываем тип процессаactive proctype main(){printf(“Hello, world!\n”)}Имя процесса(не ключевое слово)“;” -- разделитель команд,а не терминальный символрасширение – опциональноДа, это оченьпохоже на С>spin hello.pmlHello, world!1 process createdHello, world!• Основная структурная единица языкаPromela – не функция, а процесс.• Если процесс один, то можно описать егопроще:init {printf(“Hello, world!\n”)}не выделяем определениетипа процесса• Полная форма – с явным инстанцированием:init {run main()}создаём процесс в ходевыполнения моделиПроцессы в Promela• Поведение процесса задаётся в объявлениитипа процесса (proctype),• Экземпляр процесса – инстанцированиеproctype,• Два вида инстанцирования процессов:– в начальном состоянии системы,префикс active– в произвольном достижимом состояниисистемы.оператор runПроцессы в Promelaactive [2] proctype eager(){run eager()run eager();run eager()run eager()}Два процесса инстанцированыв начальном состояниисистемыstopКаждый процесс инстанцируетдве своих копии, а затемзавершает выполнениеПроцессы в Promelaactive [2] proctype eager(){12run eager();run eager()345}67• Почему такая модель остаётся конечной?– run – оператор-выражение,– run либо возвращает pid нового процесса, либо 0, еслиинстанцирование не удалось,– выражение выполняется, только если возвращает не 0,– максимальное число процессов ограничено 255.Оператор runproctype irun(byte x)предопределённая переменная _pid{printf(“it is me %d, %d\n”,x,_pid)}init{pid a,b;a = run irun(1);b = run irun(2);Присваивания и printfвыполняются всегда.Выражения – толькоесли их значение неравно 0.printf(“I created %d and %d”, a, b)}>spin irun.pmlit is me 1, 1I created 1 and 2it is me 2, 23 processes created>Отступ по умолчанию pid+1позиция табуляции1 из 6 возможных чередованийВзаимодействие процессов• Два способа синхронизации процессов:– глобальные (разделяемые) переменные,– обмен сообщениями (буферизованные илисинхронные каналы),– глобальных часов нет;• У каждого процесса есть локальное состояние:– «счётчик команд» (состояние потока управления),– значения локальных переменных;• У модели в целом – глобальное состояние:– значение глобальных переменных,– содержимое каналов сообщений,– множество активных процессов.Почему число состояний моделиконечно?• Число активных процессов конечно,• У каждого процесса – ограниченное числооператоров,• Диапазоны типов данных ограничены,• Размер всех каналов сообщений ограничен.Явная синхронизация процессовbool toggle = true;short cnt;active proctype A() provided (toggle == true){L:./spin provided.pml | moreA: cnt=1B: cnt=0A: cnt=1B: cnt=0...cnt++;printf("A: cnt=%d\n", cnt);toggle = false;goto L}active proctype B() provided (toggle == false){L:cnt--;Процесс выполняется,только если значениеprovided clause равноtrue.printf("B: cnt=%d\n", cnt);toggle = true;goto L}По умолчаниюзначение равно true.Основные операторы Promela• Задают элементарные преобразованиясостояний,• Размечают дуги в системе переходовсоответствующего процесса,• Их немного – всего 6 типов,• Оператор может быть:– выполнимым: может быть выполнен,– заблокированным: (пока что) не может бытьвыполнен.выполнимость может зависетьот глобального состоянияОсновные операторы Promela• 3 типа операторов уже встречались:– оператор печати (printf),– оператор присваивания,всегда безусловно выполним, насостояние не влияетвсегда безусловно выполним, меняет значение толькоодной переменной, расположенной слева от «=»– оператор-выражение.выполним, только есливыражение не равно 0 (истинно)2 < 3 – выполним всегда,x < 27 – выполним, только если значение x < 27,3 + x – выполним, только если x != -3.Чередование операторов(интерливинг)• процессы выполняются параллельно иасинхронно,между выполнением двух последовательных оператороводного процесса может быть сколь угодно длинная пауза• произвольная диспетчеризация процессов,• выполнение операторов разных процессовпроисходит в произвольном порядке,основные операторы выполняются атомарно• в теле одного процесса допускаетсянедетерминированное ветвление.Два уровня недетерминизма• Внутренний (выбор действия в процессе),Чередование(интерливинг)• Внешний (выбор процесса).a1a1b1a2b1 a1b1 a2a2b1b2b2 a1b2b2 a2Выполнимость операторов• Основной инструмент управлениявыполнимостью операторов в Promela –выражения (expressions)Cwhile (x <= y)/* wait*/;y++;Promela(x > y) -> y = y + 1;Псевдо-операторы• Несколько специфических операторов:– skip: всегда выполним, без эффекта, эквивалентвыражения (1),– true: всегда выполним, без эффекта, эквивалентвыражения (1),– run: 0, если при создании процесса превышенлимит, _pid в противном случае.И ещё один тип оператора• assert (выражение)– всегда выполним, не влияет на состояниесистемы,– SPIN сообщает об ошибке, если значениевыражения равно 0 (false),– используется для проверки свойствбезопасности (состояний).int n;active proctype invariant() {assert(n <= 3)}В силу асинхронности выполненияпроцессов, данный оператор можетбыть выполнен в любой момент.Примерint x;proctype A()значение по умолчанию – 0{int y = 1;skip;выполнимо, если получитсясоздать процесс Brun B();x = 2;(x > 2 && y == 1);printf(“x %d, y %d\n”, x, y)}будет выполнено, толькоесли другой процессизменит значение xОператор run• Все выражения без run в Promela не приводят кпобочному эффекту;• в отличие от С, в выражении Promela нельзя изменитьзначение переменной;• в выражении может быть только один оператор run:– run B() && run A() – может быть заблокирован счастичным эффектом,– !(run B()) – эквивалент (_nr_pr >= 255),– run B() && (a>b) – создаёт процессы до тех пор,пока (a <= b);• возврат 0 – как правило, ошибка при разработкемодели.Пример – два процессаmtype = { P, C };перечислимый тип (нумерация с 1)mtype turn = P;active proctype producer(){глобальная переменнаяпо умолчанию – 0, поэтому инициализируемdo:: (turn == P) ->бесконечный циклprintf(“Produce\n”);turn = Cod}последовательность вариантов(option sequence)active proctype consumer()индикатор начала последовательности{do:: (turn == C) ->printf(“Consume\n”);turn = Pod}страж (guard)Пример – два процессаmtype = { P, C };mtype turn = P;active proctype producer(){-uN – ограничение количествашаговdo:: (turn == P) ->printf(“Produce\n”);turn = Cod}active proctype consumer(){do:: (turn == C) ->printf(“Consume\n”);turn = Pod}./spin -u14 pc.pmlProduceConsumeProduceConsume------------depth-limit (-u14 steps) reached#processes: 2turn = C14: proc 1 (consumer) line 17 "pc.pml"(state 3)14: proc 0 (producer) line6 "pc.pml"(state 4)2 processes createdifactive proctype consumer()active proctype consumer(){{doagain: if:: (turn == C) ->:: (turn == C) ->printf(“Consume\n”);printf(“Consume\n”);turn = Pturn = Pfi;odgoto again}}• break – выход из тела do,• :: else – если ни одна из альтернатив не выполняется,• если выполняется несколько альтернатив – внутреннийнедетерминизмwait: if:: (turn == P) -> ...:: else -> goto waitfi(turn == P) ->...или(turn == P);...Пример: взаимное исключениеbool busy;byte mutex;proctype P(bit i){ (!busy) -> busy = true;Показывает, что критическая секциязанятаКоличество процессов в критическойсекцииmutex++;printf(P%d in critical section\n”,i);mutex--;Ждём, пока критическая секция неосвободится, и занимаем еёbusy = false}active proctype invariant(){ assert(mutex <= 1)потенциальная гонка:оба процесса могут вычислить(!busy) до выполненияоператора busy = true}init {Цикл не нуженatomic { run P(0); run P(1)}}Атомарный запуск двух экземпляров PЗапуск верификатора> ./spin -a mutex.pml> gcc -DSAFETY -o pan pan.c> ./panpan: assertion violated (mutex<=1) (at depth 10)pan: wrote mutex.pml.trail(Spin Version 5.1.4 -- 27 January 2008)Warning: Search not completed+ Partial Order ReductionFull statespace search for:never claim- (none specified)assertion violations+cycle checks- (disabled by -DSAFETY)invalid end states+State-vector 24 byte, depth reached 19, errors: 173 states, stored32 states, matched105 transitions (= stored+matched)1 atomic stepshash conflicts:0 (resolved)2.501memory usage (Mbyte)pan: elapsed time 0 secondsМоделирование контрпримера./spin -t -p mutex.pmlStarting invariant with pid 0Starting :init: with pid 1Starting P with pid 21:proc 1 (:init:) line 14 "mutex.pml" (state 1) [(run P(0))]Starting P with pid 32:proc 1 (:init:) line 14 "mutex.pml" (state 2) [(run P(1))]3:proc 3 (P) line4 "mutex.pml" (state 1) [(!(busy))]4:proc 2 (P) line4 "mutex.pml" (state 1) [(!(busy))]5:proc 3 (P) line4 "mutex.pml" (state 2) [busy = 1]6:proc 3 (P) line5 "mutex.pml" (state 3) [mutex = (mutex+1)]P1 in critical section7:proc 3 (P) line6 "mutex.pml" (state 4) [printf('P%d in critical section\\n',i)]8:proc 2 (P) line4 "mutex.pml" (state 2) [busy = 1]9:proc 2 (P) line5 "mutex.pml" (state 3) [mutex = (mutex+1)]P0 in critical section10:proc 2 (P) line6 "mutex.pml" (state 4) [printf('P%d in critical section\\n',i)]spin: line 11 "mutex.pml", Error: assertion violatedspin: text of failed assertion: assert((mutex<=1))11:proc 0 (invariant) line 11 "mutex.pml" (state 1) [assert((mutex<=1))]spin: trail ends after 11 steps#processes: 4busy = 1mutex = 211:proc 3 (P) line7 "mutex.pml" (state 5)11:proc 2 (P) line7 "mutex.pml" (state 5)11:proc 1 (:init:) line 15 "mutex.pml" (state 4) <valid end state>11:proc 0 (invariant) line 12 "mutex.pml" (state 2) <valid end state>4 processes createdВзаимное исключение(другой вариант)bit x,y;byte mutex;Сигнал о входе/выходе из критичесойсекцииactive proctype A(){x = 1;(y == 0) ->mutex++;printf("%d\n", _pid);mutex--;x = 0;}Число процессов в критической секцииactive proctype invariant(){ assert(mutex != 2)}active proctype B(){y = 1;(x == 0) ->mutex++;printf("%d\n",_pid);mutex--;y = 0}!(y == 0) означает, чтоB – в критической секцииВерификация> ./spin -a mutex2.pml> gcc -DSAFETY -o pan pan.c> ./panpan: invalid end state (at depth 3)pan: wrote mutex2.pml.trail(Spin Version 5.1.4 -- 27 January 2008)Warning: Search not completed+ Partial Order ReductionFull statespace search for:never claimassertion violationscycle checksinvalid end states- (none specified)+- (disabled by -DSAFETY)+State-vector 20 byte, depth reached 16, errors: 123 states, stored3 states, matched26 transitions (= stored+matched)0 atomic stepshash conflicts:0 (resolved)2.501memory usage (Mbyte)pan: elapsed time 0 secondsВзаимное исключение(другой вариант)bit x,y;byte mutex;active proctype A(){x = 1;(y == 0) ->mutex++;printf("%d\n", _pid);mutex--;x = 0;}active proctype invariant(){ assert(mutex != 2)}active proctype B(){y = 1;(x == 0) ->mutex++;printf("%d\n",_pid);mutex--;y = 0}гонкаесли эти операторы будут выполненыпоследовательно, процессы заблокируютдруг друга (deadlock, invalid endstate)Моделирование контрпримера> ./spin -t -p mutex2.pmlStarting A with pid 0Starting B with pid 1Starting invariant with pid 21:proc 2 (invariant) line 25 "mutex2.pml" (state 1)[assert((mutex!=2))]2: proc 2 terminates3:proc 1 (B) line 16 "mutex2.pml" (state 1)[y = 1]4:proc 0 (A) line6 "mutex2.pml" (state 1)[x = 1]spin: trail ends after 4 steps#processes: 2x = 1y = 1mutex = 04:proc 1 (B) line 17 "mutex2.pml" (state 2)4:proc 0 (A) line7 "mutex2.pml" (state 2)3 processes created>Алгоритм Петерсона (1981)mtype = {A_Turn, B_Turn};bool x,y;byte mutex;mtype turn = A_Turn;active proctype A(){ x = true;turn = B_Turn;(!y || turn == A_Turn) ->mutex++;/*critical section*/mutex--;x = false;}active proctype invariant(){ assert(mutex <= 1)}Сигнал о входе/выходе из критичесойсекцииЧисло процессов в критической секцииЧей ход?active proctype B(){ y = true;turn = A_Turn;(!x || turn == B_Turn) ->mutex++;/*critical section*/mutex--;y = false;}Вариант алгоритма Лампорта (1981)Чей ход?byte turn[2];byte mutex;active [2] proctype P(){ bit i = _pid;L:turn[i] = 1;turn[i] = turn[i+1];(turn[1-i] == 0) ||(turn[i] < turn[1-i]) ->mutex++;assert(mutex == 1);mutex--;turn[i] = 0;goto L;}Число процессов в критической секцииМожет ли алгоритм достичьмаксимального i = 255?Будет ли алгоритм корректен, если придостижении 255 обнулять i?Основные операторы языка Promela• присваивание:• выражение:• печать:x++, x--, x = x + 1,x = run P();(x), (1), run P(),skip, true,else, timeout;printf(“x = %d\n”, x);• ассерт:assert(1+1 == 2),assert(false);• отправка сообщения: q!m;• приём сообщения:q?m;Последние два типа операторовPromelaотправка и приём сообщенийs2rsenderreceiverr2ss2r!msgs2r?msgr2s!ackr2s?ack! – отправка,? - приёмКаналы сообщений• Сообщения передаются через каналы(очереди/буфера ограниченного объёма),• каналы бывают двух типов:– буферизованные (асинхронные),– небуферизованные (синхронные, рандеву);Каналы сообщений• пример объявления канала:имя типаимя переменнойинициализацияchan x = [10] of {int, short, bit};максимальное числосообщений в канале;0 задаёт рандевуструктура пересылаемыхсообщений(список имён типовполей сообщения)Каналы сообщений• пример объявления канала:неинициализированнаяканальная переменная achanchanchanchanканал c типа «рандеву»a;c = [0] of {bit};toR = [2] of {mtype, bit, chan};line[2] = [1] of {mtype, record};массив издвух каналовпользовательский типканалы можнопередавать поканаламОбъявление mtype(mtype = message type)• способ определить символьные константы(до 255),• объявление mtype: в итоге объявляется 6 константmtype = {foo, bar};mtype = {ack, msg, err, interrupt};• объявление переменных типа mtype:неинициализированная, значение 0mtype a;mtype b = foo;значение всегда отлично от 0Отправка и приём сообщений• отправка: ch!expr1,...,exprn– значения expri должны соответствовать типам вобъявлении канала;– выполнима, если заданный канал не полон;• приём: ch?const1 или var1,…,constn или varn– значения vari становятся равны соотв.