lect06 (К. Савенков - Верификация программ на моделях (2010)), страница 2

Выигрывает процессс максимальнымномером.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;• ассерт на трассах формализует утверждение:– система не может демонстрировать поведение, отличное отописанного шаблона.Спасибо за внимание!Вопросы?.