Лекция 5. Практические приёмы абстракции. Свойства линейного времени. Спецификация и верификация свойств при помощи Spin (1158558), страница 2
Текст из файла (страница 2)
Допустимые состояния останова mtype = {p, v};semaphoreusers0 s0 chan sem = [0] of {mtype};byte count;active proctype semaphore(){end:do:: sem!p ->sem?vod}active proctype user(){end:do:: sem?p;count++;/*critical section*/count--;sem!vod}sem!psem?psem?vs1 s1 count++s2 count-s3 sem!vНи один из процессов не должен завершаться; допустимое состояние останова для обоих процессов – s0. Верификатор должен искать недопустимые состояния останова, не отвлекаясь на допустимые.
Состояния прогресса mtype = {p, v};semaphoreusers0 s0 chan sem = [0] of {mtype};byte count;active proctype semaphore(){do:: sem!p ->progress: sem?vod}active proctype user(){do:: sem?p;count++;/*critical section*/count--;sem!vod}sem!psem?psem?vs1 s1 count++s2 count-s3 sem!vСистема демонстрирует прогресс всякий раз, когда user получает доступ к критической секции, т.е.
когда процесс semaphore достигает состояния s1. Теперь верификатор будет искать достижимые циклы бездействия. Пример byte x = 2;• x бесконечно варьирует между 2 и 1, • у каждого процесса – одно состояние, • метки progress не используются => по умолчанию всякий цикл рассматривается как потенциально бездейственный active proctype A(){do:: x = 3 - xod}>spin -a fair.pml>gcc -DNP -o pan pan.cactive proctype B() >./pan -lОбнаружение циклов pan: non-progress cycle (at depth 2){бездействия pan: wrote fair.pml.traildo(Spin Version 5.1.4 -- 27 January 2008):: x = 3 - xWarning: Search not completedod+ Partial Order Reduction}Запуск алгоритма Full statespace search for:never claim+проверки assertion violations+ (if within scope of claim)Q1: Что будет, если non-progress cycles+ (fairness disabled)invalid end states- (disabled by never claim) отметить один из do-‐od State-vector 24 byte, depth reached 5, errors: 1 циклов меткой progress? 3 states, storedQ2: А если разметить 0 states, matched3 transitions (= stored+matched) оба цикла? 0 atomic stepshash 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-xA B y = 3-yy = 3-yy = 3-yx = 3-xA x = 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 processes createdобоих процессов (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Свойства правильности • При помощи ассертов можно проверить два простых факта: – должен выиграть процесс с максимальным номером, – должен быть только один победитель.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
