lect_all (1161275), страница 9

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 9)

Выигрывает процессс максимальнымномером.2. Должен быть толькоодин победитель.3. Оператор отправкисообщения недостижим.out!one(mynumber);do:: in?one(nr) ->if:: Active ->if:: nr != maximum ->out!two(nr);neighbourR = nr:: else ->know_winner = 1;out!winner,nr;fi:: else ->out!one(nr)fi:: in?two(nr) ->if:: Active ->if:: neighbourR > nr && neighbourR > maximum ->maximum = neighbourR;out!one(neighbourR):: else ->Active = 0fi:: else ->out!two(nr); assert(false)fi:: in?winner,nr -> assert(nr == N) ;if:: nr != mynumber:: else -> nr_leaders++; assert(nr_leaders == 1)fi;if:: know_winner:: else -> out!winner,nrfi;breakod312Циклыбездействия• Свойство:– Программа эффективноработает, покаувеличиваетсязначение переменнойmaximum.• Проверяем:> ./spin -a leader2.pml> gcc -DNP -o pan pan.c> ./pan -l...(циклов бездействия ненайдено)out!one(mynumber);do:: in?one(nr) ->if:: Active ->if:: nr != maximum ->out!two(nr);neighbourR = nr:: else ->know_winner = 1;out!winner,nr;fi:: else ->out!one(nr)fi:: in?two(nr) ->if:: Active ->if:: neighbourR > nr && neighbourR > maximum ->progress:maximum = neighbourR;out!one(neighbourR):: else ->Active = 0fi:: else ->out!two(nr)fi:: in?winner,nr;if:: nr != mynumber:: else -> nr_leaders++fi;if:: know_winner:: else -> out!winner,nrfi;breakodКонструкции never(отрицание свойств)Never say never(народная пословица)Рассуждения о вычисленияхпрограммы• Существует несколько вариантов формализациивычислений распределённой системы:– последовательность состояний,– последовательность событий (переходов),– последовательность значений высказываний всостояниях (свойства состояний) – трассы.bit x,y;byte mutex;x = 1 (y==0) mutex++ printf mutex-- x = 0active proctype A(){x = 1;x==1x==1x==1x==1x==1x==0x==0(y == 0) ->y==0y==0y==0y==0y==0y==0y==0mutex++;printf(“%d\n”, _pid); mutex==0 mutex==0 mutex==0 mutex==1 mutex==1 mutex==0 mutex==0mutex--;x = 0p!p!ppp!pp}p: (x == mutex)q: (x != y)!qqqqqq!qПример• «не существует вычисления, в котором за pследует q»active proctype invariant(){assert(!p || !q);}НЕПРАВИЛЬНО!Свойства только дляодного состоянияactive proctype invariant(){p;do::assert(!q);od}НЕПРАВИЛЬНО!Асинхронноевыполнениеnever claims(утверждения о невозможности)• выполняются синхронно с моделью,• если достигнут конец, то – ошибка,• состоят из выражений и конструкцийзадания потока управления,• фактически, описывают распознающийавтомат.Пример• «не существует вычисления, в котором за pследует q»never{p;q}never{do:: p -> breakoddo:: q -> breakod}НЕПРАВИЛЬНО!Синхронное выполнение– будет работать только дляпервых двух состоянийПРАВИЛЬНО!Конструкция never• может быть как детерминированной, так и нет;• содержит только выражения без побочных эффектов(соотв.

булевым высказываниям на состояниях);• используются для описания неправильного поведениясистемы;• прерывается при блокировании:– блокируется => наблюдаемое поведение не соответствуетописанному,– паузы в выполнении тела never должны быть явно заданыкак бесконечные циклы;• never нарушается, если:– достигнута закрывающая скобка,– завершена конструкция accept (допускающий цикл);• бездействие может быть описано как конструкция neverили её часть (для обнаружения циклов бездействия естьтело never «по умолчанию»).Пересечение множеств трасс(языков)Описаниеповедения наPromelaКОНТРПРИМЕРЫОграничениясправедливостиСпецификация припомощи never(отрицание свойств)Проверка инварианта системы припомощи конструкции nevernever{do:: invariant:: else -> breakod}never{do:: assert(invariant)od}never{do:: atomic{ !invariant ->assert(invariant)}od}Ссылки на точки процессовиз тела never• из тела never можно сослаться на точку (состояниеуправления) любого активного процесса;• синтаксис такой ссылки:– proctypename[pidnr]@labelname• это выражение истинно только если процесс с номеромpidnr находится в точке описания типа процессаproctypename, размеченной меткой labelname;имя типа процессаuser[1]@critномер экземпляра процессаимя метки• если существует только один процесс типа user, то можноопустить часть *pidnr]:user@critСсылки на точки процессов(пример)never{do:: user[1]@crit && user[2]@crit -> break:: elseod}Используемметкиуправлениявместосчётчикапроцессовmtype = {p, v};chan sem = [0] of { mtype };active proctype semaphore(){do sem!p ; sem?v od}active [2] proctype user(){ assert(_pid == 1 || _pid == 2);do:: sem?p ->crit:/*критическая секция*/sem!vod}Проверяем, что процесс завершилсяactive proctype runner(){do:: ...

...:: else -> breakod;L:(false)}active proctype runner(){do:: ... ...:: else -> breakod}runner@LКонструкции never:• могут содержать любые конструкции потока управления:– if, do, unless, atomic, d_step, goto;• должны содержать только выражения:– т.е. q?[ack] или nfull(q), но не q?ack или q!ack;• не должны содержать меток progress и end;• нужно аккуратно использовать never вместе с метками progress;• могут использоваться для фильтрации интересующего насповедения:never{do:: atomic {(p || q) -> assert(r)}od}Проверяем assert(r) накаждом шаге, но лишь длятех вычислений, гдеодновременно выполняютсяp и q.Видимость• все конструкции never – глобальны;• тем самым, в них можно ссылаться на– глобальные переменные,– каналы сообщений,– точки описания процессов (метки),– предопределённые глобальные переменные,– но не локальные переменные процессов;• нельзя ссылаться на события (действия),только на состояния.

А если очень хочется?Ассерты на трассы• Используются для описания правильных и неправильныхпоследовательностей выполнения операторов send и receive.mtype = {a, b };chan p = [2] of mtype;chan q = [1] of mtype;trace {do:: p!a; q?bod}Если в ассерте упоминаетсяхотя бы одна операцияотправки сообщения вканал q, ему должнысоответствовать всеподобные операцииЭтот ассерт фиксирует лишь взаимный порядоквыполнения операций посылки сообщенийв канал p и приёма сообщений по каналу q.Он утверждает, что каждая отправкасообщения a в канал p сопровождаетсяполучением сообщения b из канала q.Отклонение от этой схемы приветётк сообщению об ошибке.В ассертах на трассы могу использоваться лишьоператоры отправки и получения сообщений.Не могут использоваться переменные, толькоконстанты, mtype или _q?_ используется для обозначения приёмалюбого сообщенияПримерВерно ли, что в протоколе голосования типы сообщенийone, two и winner приходят в строгом порядке, так чтоникто не увидит сообщение one после сообщения two?trace {do:: q[0]?one,_:: q[0]?two,_ -> breakod;do:: q[0]?two,_:: q[0]?winner,_ -> breakod}Верификация(неправда!)> ./spin -a leader_trace.pml> gcc -o pan pan.c> ./panpan: event_trace error (no matching event) (at depth 64)pan: wrote leader_trace.pml.trail(Spin Version 5.1.4 -- 27 January 2008)Warning: Search not completed+ Partial Order ReductionFull statespace search for:trace assertion+never claim- (none specified)assertion violations+acceptancecycles- (not selected)invalid end states+State-vector 200 byte, depth reached 63, errors: 152 states, stored0 states, matched52 transitions (= stored+matched)12 atomic stepshash conflicts:0 (resolved)2.501memory usage (Mbyte)pan: elapsed time 0 secondsКак же так?Ассерт нарушен!> ./spin -t -c leader_trace.pmlproc 0 = :init:proc 1 = nodeproc 2 = nodeproc 3 = nodeproc 4 = nodeproc 5 = nodeq\p0123451.....out!one,45....out!one,55.....in?one,51.....out!two,54...out!one,14....in?one,15....out!two,15.....in?two,11.....out!one,53..out!one,23...in?one,24...out!two,24....in?two,22.out!one,32..in?one,33..out!two,33...in?two,31.in?one,42.out!two,42..in?two,41.in?two,51.in?one,5spin: trail ends after 64 stepsАссерты notrace• обратное утверждение: ассерт notraceутверждает, что описанный шаблон поведенияневозможенmtype = {a, b };chan p = [2] of mtype;chan q = [1] of mtype;notrace {do:: p!a; q?b:: q?b; p!aod}Этот ассерт утверждает, что не существуетвычисления, в котором отправкасообщения a в канал p сопровождаетсяполучением сообщения b из q, и наоборот.Сообщение об ошибке генерируется, еслидостигнута закрывающая фигурная скобкаассерта notrace.О невозможном и неизбежном• ассерт формализует утверждение:– указанное выражение не может принимать значение ложь,если достигнут ассерт;• метка end формализует утверждение:– система не может завершить работу без того, чтобы всеактивные процессы либо завершились, либо остановились вточках, помеченных метками end;• метка progress формализует утверждение:– система не может выполняться бесконечно без того, чтобыпроходить через точку, помеченную меткой progressбесконечно часто;• конструкция never формализует утверждение:– система не может демонстрировать поведение (конечноеили бесконечное), полностью совпадающее с описанным втеле never;• ассерт на трассах формализует утверждение:– система не может демонстрировать поведение, отличное отописанного шаблона.Спасибо за внимание!Вопросы?Верификация программна моделяхЛекция №7Практические приёмы абстракции.Спецификация и верификация свойств припомощи автоматов Бюхи.Константин Савенков (лектор)План лекции••••Практические приёмы абстракцииПроверка свойств правильностиАвтоматы БюхиПроверка свойств при помощи автоматовБюхиПрактические приёмы абстракцииОбщая схемаПрограмма на СМодель наPromela• Неправильный подход!– Если строить модель без оглядки на проверяемыесвойства, то она получится слишком детальной.– Скорее всего, не хватит ресурсов на верификацию.Общая схемаПрограмма на СМодель наPromelaПроверяемыесвойства• Модель должна моделировать только то,что влияет на выполнимость проверяемыхсвойств.Примерvoid f(int x){while(x < 10){if(x < 3){printf(“Case 1\n”);}else{printf(“Case 2\n”);}x++;}}• Модель точная, но у неёслишком многодостижимых состояний.• Давайте посмотрим назаданные свойства.proctype f(int x){do:: x < 3 ->printf(“Case 1\n”);x = x + 1:: x >= 10 ->break;:: else ->printf(“Case 2\n”);x = x + 1od}init {int x;do:: x++;:: x--;:: break;od;run f(x)}Примерvoid f(int x){while(x < 10){if(x < 3){printf(“Case 1\n”);}else{printf(“Case 2\n”);}x++;}}«Проверить, что передпечатью “Case 2”всегда была выполненапечать “Case 1”.»proctype f(int x){do:: x < 3 ->printf(“Case 1\n”);x = x + 1:: x >= 10 ->break;:: else ->printf(“Case 2\n”);x = x + 1od}init {int x;do:: x++;:: x--;:: break;od;run f(x)}Примерvoid f(int x){while(x < 10){if(x < 3){printf(“Case 1\n”);}else{printf(“Case 2\n”);}x++;}}«Проверить, что передпечатью “Case 2”всегда была выполненапечать “Case 1”.»mtype {X1, X2, X3};proctype f(mtype x){do:: x == X1 ->printf(“Case 1\n”);incr(x);:: x == X3 ->break;:: x == X2 ->printf(“Case 2\n”);incr(x);inline incr(x){odif}:: x += 1;init{:: skipmtype x;fiif}:: x = X1:: x = X2:: x = X3fi;run f(x)}Не загромождаеммодельПриёмы абстракции•••••Абстракция предикатовАбстракция типов данныхАбстракция наблюдаемых переменныхАбстракция от «лишнего» кодаАбстракция от функций и системныхвызововАбстракция предикатовif(x < 0){printf (“Case 1”);}else{printf (“Case 2”);}…if:: printf (“Case 1”);:: printf (“Case 2”);fi• В модели увеличивается количество возможныхвычислений– если формула не нарушается ни на одном вычислении модели,то на исходной программе она также будет выполнима,– если формула нарушается на одном из «добавленных»вычислений, необходимо увеличить уровень детализациимоделиАбстракция типов данныхint x;…if(x < 0) {…}else {if(x < 3) {…}else {…}…}mtype { X1, /*x < 0*/X2, /*0 <= x < 3*/X3 /*x >= 3*/};if:: x == X1 -> …:: x == X2 -> …:: x == X3 -> …fi• Диапазон типа данных разбивается на классыэквивалентности относительно конструкций организациипотока управления и проверяемых свойств.• Необходимо корректно моделировать:– предикаты в операторах ветвления,– операторы, изменяющие значения переменных этого типа.Абстракция наблюдаемыхпеременных• Из модели удаляется переменные, значениякоторых не влияют на выполнимость заданныхсвойств:– не используются при формулировке свойства,– не влияют на поток управления модели.• Операторы модели могут быть связаныдостаточно сложными зависимостями поданным и управлению, поэтому в ходе удаленияпеременных допускается только расширениемножества возможных вычислений моделиАбстракция наблюдаемыхпеременныхint x;…while (x != 0){x = get_value();}…printf (“Something\n”);printf (“Something\n”);do:: skip:: breakod;printf(“Something\n”)• Свойство – операция печати будет выполнена один раз,• Если абстрагируемся от цикла – теряем возможностьбесконечного зацикливания (сужаем множествовозможных вычислений).Абстракция «лишнего» кода…some_func();printf(“Func called!\n”)……some_func: skip;…• Свойство – some_func() будет вызвана.• Можно абстрагироваться от:– кода, не влияющего на проверяемое свойство (printf),– реального выполнения операторов, если нас интересует лишьфакт его выполнения («функция была вызвана»).• Здесь также необходимо следить за допустимымивычислениями.…int x;x = some_func();if (x)……int x;some_func: skip;if:: x -> ……Абстракция от функций и системныхвызововff(){sys_call();}sys_callcallres• Выполнение реальной функции заменяется наобмен сообщениями с процессом-«заглушкой»,• Обмен сообщениями должен корректномоделировать вызов функции:– синхронное взаимодействие, гарантированный отклик.От чего не стоит абстрагироваться• Поток управления:– ветвление, циклы;• Можно добавлять новые ветви и пути выполнения:– см.

Характеристики

Список файлов лабораторной работы