6 - Практические приёмы абстракции. Свойства линейного времени. Спецификация и верификация свойств при помощи Spin (1161370), страница 2

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

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

когдапроцесс semaphore достигаетсостояния s1.Теперь верификатор будет искатьдостижимые циклы бездействия.Примерbyte x = 2;active proctype A(){do:: x = 3 - xod}• x бесконечно варьирует между 2 и 1,• у каждого процесса – одно состояние,• метки progress не используются => поумолчанию всякий цикл рассматриваетсякак потенциально бездейственный>spin -a fair.pml>gcc -DNP -o pan pan.cactive proctype B() >./pan -l{Обнаружение цикловpan: non-progress cycle (at depth 2)dopan: wrote fair.pml.trailбездействия:: x = 3 - x(Spin Version 5.1.4 -- 27 January 2008)Warning: Search not completedod+ Partial Order Reduction}Full statespace search for:Запуск алгоритмаnever claim+assertion violations+ (if within проверкиscope of claim)non-progress cycles+ (fairness disabled)Q1: Что будет, еслиinvalid end states- (disabled by never claim)State-vector 24 byte, depth reached 5, errors: 1отметить один из do-od3 states, storedциклов меткой progress?0 states, matchedQ2: А если разметить3 transitions (= stored+matched)0 atomic stepsоба цикла?hash conflicts:0 (resolved)2.501memory usage (Mbyte)Какой цикл мы обнаружили?>spin -t -p fair.pmlStarting A with pid 0Starting B with pid 1spin: couldn't find claim (ignored)2:proc 1 (B) line 13 "fair.pml"<<<<<START OF CYCLE>>>>>4:proc 1 (B) line 13 "fair.pml"6:proc 1 (B) line 13 "fair.pml"spin: trail ends after 6 steps#processes: 2x = 16:proc 1 (B) line 12 "fair.pml"6:proc 0 (A) line5 "fair.pml"2 processes created(state 1)[x = (3-x)](state 1)(state 1)[x = (3-x)][x = (3-x)](state 2)(state 2)Мы не знаем относительной скорости выполненияпроцессов:• возможно, что процесс B выполнит бесконечно больше шагов,чем процесс A;• цикл бездействия, обнаруженный Spin – это не обязательносправедливый цикл.Справедливые циклы• Часто мы ожидаем конечного прогресса:– если процесс может сделать шаг, он в конце концов егосделает.• Существует два основных варианта справедливости:1) слабая справедливость:– если оператор выполним бесконечно долго, то он вконце концов будет выполнен;2) сильная справедливость:– если оператор выполним бесконечно часто, то он вконце концов будет выполнен.• Справедливость применима как к внешнему, так и квнутреннему недетерминизму.выбор оператораvs.

выбор процессаbyte x = 2, y = 2;active proctype A(){do:: x = 3 – x;:: y = 3 - yod}active proctype B(){do:: x = 3 – x;:: y = 3 - yod}x = 3-xx = 3-xABy = 3-yy = 3-yy = 3-yx = 3-xAx = 3-xy = 3-ySPIN поддерживает один из вариантов слабойсправедливости (>pan -f):«если процесс содержит хотя бы один оператор,который бесконечно долго остаётся выполнимым,то этот процесс рано или поздно сделает шаг».Это касается только потенциально бесконечных вычислений(циклов).Поиск слабо справедливыхциклов бездействия>./pan -l -fpan: non-progress cycle (at depth 6)pan: wrote fair.pml.trail>./spin -t -p fair.pmlStarting A with pid 0Starting B with pid 1spin: couldn't find claim (ignored)2:proc 1 (B) line 13 "fair.pml"4:proc 1 (B) line 13 "fair.pml"6:proc 0 (A) line6 "fair.pml"<<<<<START OF CYCLE>>>>>8:proc 1 (B) line 13 "fair.pml"10:proc 0 (A) line6 "fair.pml"spin: trail ends after 10 steps#processes: 2x = 110:proc 1 (B) line 12 "fair.pml"10:proc 0 (A) line5 "fair.pml"2 processescreatedТеперьв цикле естьшагиобоих процессов(state 1)(state 1)(state 1)[x = (3-x)][x = (3-x)][x = (3-x)](state 1)(state 1)[x = (3-x)][x = (3-x)](state 2)(state 2)Указываем полезные действияbyte x = 2, y = 2;active proctype A(){do:: x = 3 – x;:: y = 3 – y; progress: skipod}ВОПРОСЫ:active proctype B(){do:: x = 3 – x;:: y = 3 – y; progress: skipod}• А справедливые циклы?• Будут ли циклы бездействияс меткой progress в одномпроцессе?• А если метки есть в обоихпроцессах?Использование условийсправедливости• Любой тип справедливости можно описатьпри помощи формулы LTL (позже)• добавление предположения осправедливости всегда увеличиваетсложность верификации• использование сильной справедливостисущественно дороже слабой:– слабая: сложность (по времени и памяти) растётлинейно от числа активных процессов,– сильная: сложность растёт квадратично.Пример: протокол голосования#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;breakodЗапускаем моделирование>spin -cproc 0 =proc 1 =proc 2 =proc 3 =proc 4 =proc 5 =q\p05.3.2.4.2.4.1.3.1.5.2.1.5.3.5.4.1.4.leader.pml:init:nodenodenodenodenode12345...out!one,5.out!one,2out!one,3..out!one,1.in?one,3...in?one,1....out!one,4..in?one,2in?one,4....in?one,5out!two,4....out!two,5...out!two,1.out!two,3....in?two,1..out!two,2in?two,5...in?two,21.....out!one,53...in?two,32..in?two,41.in?one,52.out!one,52..in?one,53..out!one,53...in?one,54...out!one,54....in?one,55....out!one,55.....in?one,51.....out!winner,51.in?winner,52.out!winner,52..in?winner,53..out!winner,53...in?winner,54...out!winner,54....in?winner,55....out!winner,55.....in?winner,5------------final state:------------6 processes createdВерификация по умолчанию>./spin -a leader.pml>./gcc -o pan pan.c>./pan(Spin Version 5.1.4 -- 27 January 2008)+ Partial Order ReductionFull statespace search for:never claim- (none specified)assertion violations+acceptancecycles- (not selected)invalid end states+State-vector 200 byte, depth reached 106, errors: 04813 states, stored1824 states, matched6637 transitions (= stored+matched)12 atomic stepshash conflicts:13 (resolved)Stats on memory usage (in Megabytes):0.991equivalent memory usage for states (stored*(State-vector + overhead))1.070actual memory usage for states (unsuccessful compression: 107.92%)state-vector as stored = 217 byte + 16 byte overhead2.000memory used for hash table (-w19)0.305memory used for DFS stack (-m10000)Ошибок нет, но мы ещё3.282total actual memory usageunreached in proctype nodeне сказали, что долженline 40, state 26, "out!two,nr"делать алгоритм(1 of 44 states)unreached in proctype :init:(0 of 11 states)pan: elapsed time 0.03 secondsПохоже, в модели естьpan: rate 160433.33 states/secondнедостижимый кодСвойстваправильности• При помощиассертов можнопроверить двапростых факта:– должен выигратьпроцесс смаксимальнымномером,– должен быть толькоодин победитель.• Правда ли операторотправки сообщениянедостижим?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Проверяем простейшиесвойства безопасностиОшибок не найдено!Число состоянийувеличилось: ассертыДействительно,недостижимое состояниеAlternating 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 - aod}active 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;breakodСвойстваправильности• Кое-что мы ужепроверили припомощи ассертов:1.

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

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