Лекция 5. Практические приёмы абстракции. Свойства линейного времени. Спецификация и верификация свойств при помощи Spin (1158558), страница 3

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

Текст из файла (страница 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;breakodБолее осмысленная верификация >./spin -a leader.pml>./gcc -DSAFETY -o pan pan.c>./pan(Spin Version 5.1.4 -- 27 January 2008)+ Partial Order ReductionFull statespace search for:never claimassertion violationscycle checksDSAFETY)invalid end states- (none specified)+- (disabled by -memory usage (Mbyte)unreached in proctype nodeline 40, state 26, "out!two,nr"line 40, state 27, "assert(0)"(2 of 47 states)unreached in proctype :init:(0 of 11 states)pan: elapsed time 0.01 secondsПоявились ассерты +State-vector 196 byte, depth reached 112, errors: 04819 states, stored1824 states, matched6643 transitions (= stored+matched)12 atomic stepshash conflicts:5 (resolved)3.379Проверяем простейшие свойства безопасности Ошибок не найдено! Число состояний увеличилось: ассерты Действительно, недостижимое состояние Alterna•ng Bit Protocol (с потерей сообщения и таймаутом) mtype = {msg, ack};chan to_s = [1] of {mtype, bit};chan to_r = [1] of {mtype, bit};chan from_s = [1] of {mtype, bit};chan from_r = [1] of {mtype, bit};active proctype sender(){ bit a;do:: from_s!msg,a ->if:: to_s?ack,eval(a) ->a = 1 - a:: timeoutfiod}active proctype receiver(){ bit a;do:: to_r?msg,eval(a) ->from_r!ack,a;progress:a = 1 - aodactive proctype channel(){ mtype m; bit a;do:: from_s?m,a ->if:: true -> to_r!m,a:: skipfi:: from_r?m,a ->to_s!m,aod}Теряем сообщение Повторная отправка Будет ли алгоритм эффективно работать при потере сообщений? Проверяем! > ./spin -a abp_lossy.pml> gcc -DNP -o pan pan.c> ./pan -lpan: non-progress cycle (at depth 4)pan: wrote abp_lossy.pml.trailХорошо бы рассмотреть и другие сценарии! В найденном сценарии мы бесконечно часто теряем сообщение ./spin -t -c abp_lossy.pmlproc 0 = senderproc 1 = receiverproc 2 = channelspin: couldn't find claim (ignored)q\p011from_s!msg,01..from_s?msg,0<<<<<START OF CYCLE>>>>>1from_s!msg,01..from_s?msg,0spin: trail ends after 12 steps------------final state:------------#processes: 3queue 1 (from_s):12:proc 2 (channel) line 33 "abp_lossy.pml" (state 4)12:proc 1 (receiver) line 21 "abp_lossy.pml" (state 4)12:proc 0 (sender) line 11 "abp_lossy.pml" (state 5)3 processes createdУточняем свойство active proctype channel(){ mtype m; bit a;do:: from_s?m,a ->if:: true -> to_r!m,a:: skip; progress: skipfi:: from_r?m,a ->to_s!m,aod}active proctype receiver(){ bit a;do:: to_r?msg,eval(a) ->from_r!ack,a;progress:a = 1 - aod}Размечаем цикл потери сообщений меткой прогресса, исключая из поиска Уточнённая проверка > ./spin -a abp_lossy2.pml> gcc -DNP -o pan pan.c> ./pan -l(Spin Version 5.1.4 -- 27 January 2008)+ Partial Order ReductionFull statespace search for:never claim+assertion violations+ (if within scope of claim)non-progress cycles+ (fairness disabled)invalid end states- (disabled by never claim)State-vector 60 byte, depth reached 53, errors: 073 states, stored (98 visited)64 states, matched162 transitions (= visited+matched)0 atomic stepshash conflicts:0 (resolved)2.501memory usage (Mbyte)unreached in proctype senderline 17, state 10, "-end-"(1 of 10 states)unreached in proctype receiverline 27, state 7, "-end-"(1 of 7 states)unreached in proctype channelline 40, state 12, "-end-»(1 of 12 states)Единственный цикл бездействия связан с бесконечной потерей сообщений Пример: протокол голосования #define N#define I#define L5 /* nr of processes (use 5 for demos)*/3 /* node given the smallest number*/10 /* size of buffer (>= 2*N) *//* file ex.8 */mtype = { one, two, winner };chan q[N] = [L] of { mtype, byte};byte nr_leaders = 0;proctype node (chan in, out; byte mynumber){bit Active = 1, know_winner = 0;byte nr, maximum = mynumber, neighbourR;...}init {byte proc;atomic {proc = 1;do:: proc <= N ->run node (q[proc-1], q[proc%N],(N+I-proc)%N+1);proc++:: proc > N ->breakod}}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)fi:: in?winner,nr;if:: nr != mynumber:: else -> nr_leaders++;fi;if:: know_winner:: else -> out!winner,nrfi;breakСвойства правильности •  Кое-­‐что мы уже проверили при помощи ассертов: 1.  Выигрывает процесс с максимальным номером.

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;breakod3 1 2 Циклы бездействия •  Свойство: –  Программа эффективно работает, пока увеличивается значение переменной 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;breakСпасибо за внимание!Вопросы?.

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

Список файлов лекций