2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 47
Текст из файла (страница 47)
Протокол РАЙ АзОпиш4 мести посла» рован» Процес на рис. 15 рвх 1б 004 в10 и вььс. В первых двух канапах возможна буферизация не более одного сообщения, в остальных четырех — не более двух сообщений. Скобка (псуре, ьусе) в описании каналов указывает, по кюкдый канал может передаыпь сообщения, сооююшне нз двух полей: первое поле — любое данное типа петре, второе — типа ьусе. Данные типа псуре — символьные констанзы аск, пас40 егг — перечислены в строке 1.
В строке 32 одновременно запускаются оба процесса передачи с параметрами, обсузкаенными выше. Заканчиваетсв процесс 10»г передачей ошибочного сообщения для иницнвлизацин про- цсССОВ ПЕрЕдатЧИКОВ (ЧГОЕЫ ОНИ НЕ жаапи бЕСКОНЕЧНО друГ друГа В ЦИКЛЕ 00). Необходимость этого искусспюнного приема обьясюмтся некорректностью протокола, описанного йГ.С.Еупсй — в нем инициализация процессов не описана.
Заметим, что злясь нс моделируются ошибки, возникавшие в реальных канавах перелачи данных. Для испольювания этого описания в качестве модели протокола необходимо построить модели пользователей А и В, юторые в каналм щп и вщ передзввли бы сообщению, содерюащис пару: служебное слово ьекг и произвольное значение типа ьусе (например, символ), н принимвлн бм по каналам аоьг н вгюс соответствующие сообщения.
Этот протокол был приведен в гл. 5 как пример протокола коммуникации, работающего некорректно при редких сочетаниях ошибок в канале связи. Протокол РАЙ является разновидностью классического протокола альтернирующего бита (Айешаг)вб Вй Ргогосо!, АВР). В отличие от протокола АВР, в протоколе РАК подтверлшения, которые посылает приемник о получении сообщений, не нумероввны. Это и является причиной некорректности протокола РАК Подобные некорректности легко выявляются при анализе протокола с помощью системы Бр)л. Протокол АВР— это классический пример протокола. Он часто приводится в учебных курсах для демонстрации асинхронной природы взаимодействия параллельных процессов в распределенной сисгеме. Несмотря на свою простоту, протокол не может быль записан в несколько строю в работе (82) спецнфикацнв этого протокола на юзыке Еме)10 занимает 300 строк кода. В приводимом ниже опшжнии мы покажем, как этот протокол может быть описан на языке Ргоюе1а: это описание, фактически, повторяет спецификацию этого протокола в виде взаимодействующих систем переходов, приведенную на рис.
5.4. Цель приводимого ниже описания этого протокола — демонстрация того, что распределенная системе, каждый модуль которой представлен в виле конечно.автомюмого описанюь практически однозначно может быть представлена системой взвнмолействунпцик процессов на языке Ргоюе1а. Перва занум иодел по ка! тами. синхр сообш перед ннфор Сйаи 04 ргь 05 Об 01 Ш 00 1 оэ 10 рг4х 11 04 12 Ч'. 15 ч, 14 1 диого Ксбка :т пе- ВННОЕ )уска- чива) проч ос). )стью 'Оли ~ьных ИННО реда)ьнос мс и вин, вязи. :рниВр,в енин зсто- юто(нгся таня про. спс- приисаи ЛОГО о на ацня в ви- бьпь оО /* описание Мхнокона глл / О) Сусе-(оа, а,а(к) /* эсмюиме ссюоэээн» е «аналах */ 02 сьаэ с1, с2, сэ, с4, сз, са [0) ос ( исусе ) / Ь.эаэаэоа / ОЗ ЬОО1 эо, э1, Ю, т1 Гэхээз В строке 03 описаны глобальные булевы переменные эо, эз, *о, тз.
Они являются атомарными преднхзтами и будут использоваться прн верификации протокола. Они имеют следующий смысл: 51 псльзОватель А послал данное, занумерОВанное 1( щ — пользователь В принял данное, занумерованное 1. Опишем процессы пользователей протокола. В этих процессах в нумнык местах приписываем атомарным предикатам пушные значеншс эо-с*се, когда посланы ланные, занумерованные О, эзььэсе, когда посланы данные, зануме. рованные 1, и т.д.
04 рэсссуре Овеяв) ( 05 ЧО: сш ОО7 ЬО 06 ЧЫ Щ( 4пз эО- 07 Ч2: оз( Ооз эО 00 ) 09 10 ргостуре пасси() ( и чо: сю оо) то 12 Ч14 с47 О17 сО 13 02: с42 004 то ы ) Сэзмз а1 Га1эез Гаээез э1 Созез том 7 э1 га1эез Оосс ч17 созез *1 саьэе) еэзэе) с1 Симз сэое) Щ тазэез восо ч14 процесс передатчика строится в точнссв по спеийфиквцни, пррйртвапениой на рис. 5.4: 15 РЭОССУРЕ Звжний ( ИСУРЕ Ияез 16 ЧО: с17 Ооз Первая строка описания — определение сообщений в каналах (это данные, .занумерованные О н 1, и подтвермдение аск), хворые улобно представить в модели как константы перечислимого типа.
Хотя сообщения, пераааввемьм по каналам, могут быть произвольными, мы моделируем их просто константами. Порты 1, „б в спецификации проюкола в аа 5 здесь предсгавлмоюя синхронными канавами сз-сь, по которым без буферизации передаютса сообщения типа асуре. Каналы С/)1 н С/)2, по котормм эти сообщения передаются на рнс.
5.4, имеют свое собственное поаеаение (они мшуг терять информацию), и поэтому праасгвалены здесь процессами С/юлией и Сдаллэ(2 соответственно. грг, Гяаяи 7 17 и(1и с2! бог 16 Ч2г 11 ЗВ ги сат ЛСК -> Чоис ЧЗ 20 ии сияя -> Оссс ч1 /* еарелаичяя яе ясаяался яалчяерялеяяя */ 21 117 22 ЧЗи с17 гп! 23 Чи' сг! Сгг ' 24 Ч5и 12 25 7 и сб7 ЛСК -> ЧМс ЧО 26 и: сыв и сосо ч4 /и ияранееаш яе исялаася ясачаеуялемиа */ 27 ты гв ! 23, ЗО р*ссиуре Ляся1чеи(! ( 31 /* ярсяясс Кесе1ияг строятся ясяяссиио аяялсгячяс яргшмсу Мпы» '/ Пршыссы, моделирующие поведение канввов, учитывает воимшкность поте- ри передаваемой инфорищции; 31 ргссиур СШОВМЫП ( ясуре ш 32 чои с27 яис( зз Зг 34 :: *С вЂ” бОг -> 35 За За :: сЗ! бс 37 :и сом -> а(бр За 11 39 гг мо б17 -> 30 Зк 31:: сЗ. бг Зг иг спы -> ЯЩ> зз вг 34 ть 35 Ссис ЧО Зб ! 37 рисесжм СШШИКЬ20 ( жуРе иисг ЗЕ /* цяимсс СЬ~~а32 сиямис» ясяииисич» аяяяспичяс я(яяиссу Сиагям11 '/ 33 ! К атой программе нуикно добавить процесс инициелюации (пьс, эапускыощий( все б пронлссов.
Формально требования спецификации протокола в лв 5 были представлены формулами 1Т(, в которых, в соответствии с нотацией системм Зр(п, темпорвльные операторы С н Г обовначаютсл П и ч~! Анели приме! т.з. Однии данны исто та со!). й кими 1 рам н успсш один ( аборп Л Фк Ме Сои аер вуя ци! об» Л Фк Еш без окс лаи из~ это кои раб ме! Прим строе! Брас!: Ц(эб->(П)Пгб))лЦ(гб->(!г)Пэ1))лД(з! ->(!эббг)))лЦ(г)->(!гОПэб)) Брес2: Ц((эб-><>э1)л(э!-> с>зб)) Анализ с помошью сисшмы Зргп этих требований позволяет найти контр- примеры — ошибочные траектории, на которых требования не выполнаотся.
лены :мпо- 7.3. Протокол двухфазной Фиксации Одним из методов обеспечения целостности данных в распределенных базах данных является подтверждение выполнения обрабогки транзакции в сооэветствии с протоколом двухфазной фиксации (2РС, Тмо РЬше Сошппг Рпиг> со!). Этот протокол используется в случаях обработки транзакции несколькимн серверами в распределенной базе данных (БД). Всем активным серверам нужно принять единое коллективное решение либо о том, что все они успешно завершили обработку транзакции.
либо о неудаче, если хотя бы один сервер не смог довестн обработку до конца и транзакция дошкна быть абортирована. Протокол состоиг нз двух фаз. (2 Фаза!: подготовка Менеджер транзакций (например, М!симой П!зЫЬгиед Тгапиюбоп Соогапашг, МБ ПТС) сначала проверяет готовность всех серверов к завершению транзакции, запрашивая их решение. Каждый сервер, участвующий в обработке транзакции, посылает свой ответ менеджеру транзакций, информируя его либо о безошибочном завершении, либо о необходимости аборта (опглонения) обрабатываемой транзакции вследствие обнаруженной и!я ошибки. П Фаза2: фиксация или откат(сошшй ог гойЬасЫ Если все серверы сосбшнли. что они завершили обработку'трммакцин безошибочно, менеджер транзакций отправляет всем серверам команду окончательной фиксации ягой транзакции, разрешен записать в БД сделанные при обработке транзакции изменения данных.
Если хотя бы один иэ серверов при выполнении транзакции обнаружил ошибку и направил сб этом информацшо менеджеру, менеджер направляет всем серверам команду об аборте транзакции. Все изменения данных, сделанные при обработке этой транзакции, каждым сервером игнорируются (не записываются в БД), и транзакция запускаешя на обработку повторно (используя механизм множественных поколений, нлн реинкврнаций).
Приведем модель протокола 2РС как программу на языке Ргошс(. Прн построении модели абстрапгруемся от несушественных деталей протокола, на- пример, зафиксируем число ш»тинных процессов, решение о том, правильно или неправильно обработана транзакции будем принимать случайно, будем стлать, что передача сообщений синхронна — каждое посланное сообщение полною ожидатьсл получателем. 1 Ие23ле И 6 /' число пктивнмк процессов */ 2 юиуре - (5ТМГТ, ОВВПТ, апорт, НООКСГВПж)! /*сммольньм «онсгвнтм*/ 3 сЬлп исьлп [О) оГ (мсуре), / «вилл от мьнелпч)м к лроцессвм '/ 4 рсьвп (01 оз (мсуре) ! /* кюилл от процессов к менедверу */ 5 >куре 01оЬл10ес1н1оп ИОЮЕС161(ИГ /' нпниектнвнсе реюмние '/ 6 7 рсссюурв Шпшсег() ( Ьусе соплю О! 6 /' соспс счмювет число вювнмолействий с интимнее! прослссюми */ 9 бо /* юнг) ! мпрос «о всем вктнвньм процес<ем прилить рмюение*/ 10 Г! (сош»с < н) -> исьпп ! Ншктю с»кюж ++ 11 ! ! (<оспе И) -> ЬгелК 12 об! 13 14 /* КИГ2! прием рмюеннй ст всем в»шинник процессов */ 15 01оьл1оес1в1оп (хшатю /' сначала полагаем сопев рмюение — Охопт 16 это ремение оствнетсл, если ни один ив процессов не приидет даокт */ 17 юпуре часе! /* тосе — перпмнюмл длл примы реиений процессов "/ 10 бо 19 ГГ (СОЦПС < з*и ) -> РСЬЛП > ЧОСЕГ ССОЛС»Ы 20 12 21 ! Г (ЧОСЕ МОКТ) -> 01аЬа10ЕС1Н1<п ЛПСНТ 22 Г! (тосе (хзж1т) -> юк10 23 /* если котя см скин процесс пришил инсат, то реюршие джх(т / 24 Щ 25 :: (смшс 2*и) -> Ьгевь 26 обю 27 /* ЮВГЗГ РЕССМЛПВ М.'ШЮГО Рвмвиню аааМ ВНЮММВШ МНШЕССЮМ »/ 26 бО 25 ю ! (<»мпю < 3'И) -> НсЬвп ! 61еЬв10в<безол! Ссчпч ++ 30 Г! (сосюж 3'И) -> Ьсеви 31 об 32 ) 33' 34 рсоссуре ассзче рисенв (ьусе зб) /"вммшиюж процесс,с и<»иром зб */ 35 ( мсуре бес1в1оп жхжсзвзсм! 34 /' сивчввв у процессе рмювиию нет */ 37 ис)шп 7 лпи(т -> /» сюврютюм, кожи пшжчеи веиуск от менлвперв */ 36 39 49 (г (З 4 ° / 45 46 47 1п1 49 ( Ь 49 б 50 51 52 о 5З ы Здесь, в стро! ТИННО ЗГОГО ( КОИ ни инфор! зс поз! СГОИТ Г сов ре! цссс п) провер 7.4.: Привел тальн(н ды.
Зт( !Инин ! МНОЖ6( доказал сталин! техник! зв щ, 39 /* спгчеако имен)мем свое ранение к стпреалямг его менепеирг т/, 40 /* потом окиянам сесне реиение от менедьере */ :: гспап . Лжжтг Испяп 2 Сесзщоп4 Сесзяьоп - ИКцт 42:; р . ССНат4 Нове . Мсьщо 4З Г)4 аееесе (Сесзщоп — щопнзОесзеьоп) /* если ьы реиини ввовт, сесне ренские лоякно смть анино квОвт / 45 ) 46 /' ссътниаяся часть щкптьмеяг мопенчкям пргнмссм */ 47 (пгс /* инипиетор ввпэскает к актиннмк пропессов и мененаер '/ 49 ( Ьупе стопе 04 49 Со 50 4: (соаьс < н) -> гоп Вещее рсосеяе (сом14)4 соопсьь (поппе И) -> Ькеах, 52 ос 4 53 счп Иапасег() г 54 кльно будем жение м'/ / '/ */ Здесь для верификации испольюван оператор аяяегс(погическое нщмяение) а строке 43.
Этот оператор всегда вычислмм. Если логическое выражение истинно на всех траекюриях в процессе выполнемия программы, то вычисление >гого оператора нс имеет никакого эффекта (см. пример 5.2). Если же на ш)- кой-нибудь траектории вычисления это вырюкеиие ложно, то Бр)п выдает информацию об ошибке, Использование такого оператора в данном протоколе позволяет его верифицнроаать: корректное поведение протокола 2РС состоит в том, что при всех возможных варищпах поведении щттнвных процессов решение кюкаого процесса совпадает с общим решением, но если процесс принял решение ажжт, то н общее решение будет апскт.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
