2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 35
Текст из файла (страница 35)
Представление программы с конечным числом состояний структурой Крипке Известно, что многие синхронизацнонные и коммуннкацмонные протоколы могут быть достаточно точно смоделированы программамн с конечным числом состояний, в которых кюкдое соспиние имеет конечное описание.
Вследствие этого они могут быль адекватно представяены структурой Кринке. В некоторых случаях ирсграмму также удобно задавать визуальна кыг систему переходов. Существует несколько сбласгей, где тыюй вид задания аагоритма активно используется. системы управления, аягорнтмы поведения активных агентов, драйверы внешних устройств н т. п. В частности, диаграммы активности языка ОМ(, (11пгйеб Модейлй Еапйиайе) — это, фактически, модифицированные карты состояний, т. е, системы переходов. Программы, написанные в травишюнном стиле на обычном языке высокого уровня, тоже, конечно, характеризуются своим состоянием. Иапример, в случае прерывания программы ее полное соспмние запоминается дяя того, чтобы в последующем продолжить ее выполнение.
Состояние здесь — это вся ииформашм, необходимая для корректного продолжения выполнения про- гран (стр к со чнкя в но, щеп~ Перз рато лзя з а каз ну ь трам соси Откуз Атом ресук ются дениз соотн сзрук траек подмз Ваяя э Слп Краске иж модели ввэр апжииг граммы. Состояние программы составляют значения жжх ее переменных (структур данных), содержимое регистров, содержимое стека. Кроме того, к состоянию относима и текущая позиция в коде программы (значение счетчика команд). Для параллельной программы с взаимодействием модулей в модель необходимо добавить состояния буферов канвюв (значения сообщений в иих). Переходы между сааза«пнями программы происходвт при выполнении опе.
раторов, изменяющих значения переменных. Рассмотрим слупи(, когда каждая переменная программы может принимать конечное множество значений, а канвы могут хранить конечное число сообщений. В этом случае программу можно описать конечной системой переходов. В литературе такие программы называются/йище-жще ргойтлвм — программы с конечным числом состояний. я( паюиен. х снегином ьный. сита с ции в (ийоа зьных з«ве- вери эьныь ~х мо- умент Пример 6.2 Рассмотрим простой пример: «г е> «:- «+у-зг у: «-бг окопы «чнссанне. турой систе- ваго.
ия акжммм и, ма. :окого в слу>, нога вся г про. Пусть значения переменных до выполнения этого фрагмента таковы: х-з; у в (начвльное состояние фрагмента — пара («-з, у-е)). Первый оператор «г-в переводит это состояние в состояние («в, у-а), второй оператор «: «+у-з— в состояние <«-|з, у-я) и т.д. На рис.5.7,а предащвлен фрагмент системы переходов для этой программы. Дяя того чгобы нз этой системы переходов получить структуру Кринке для верификации, пулею отбросить помене на переходах и в состояния добавить атомарные, предикаты, истинные в этих состояниях.
Откуда беругся атомарные предиквты2 Атомарные преднкатм лзж программы — это логические соотненення, интересующие рюработчика с точки зрения поведения программы. Они назначаются программистом при формулировке специфиющий (требований к повелению программы). Пусть, например, для нас вюкными являются следующие соотношения в этом фрагменте: р м>з"у н ч-у<«. Следующий фрагмент струкгуры Крипке соопвтствуст этой программе (рис.5.7, б).
Фрагментом траектории, соответствующей нашему фрагменту программы. будет цепочка подмножестватомарныхпредиюпов: ... ( )(дЦр,дЦд~..., и н"х в Этот опер туре Подо опер прис~ опер Вопр п1ие моде. верех мм, э М'НЯ если х:=хх про ту Недо или в воой извне ВОДН1 мент, пред( Проб перел деле. е Рис.в.у. Системм пммиодов н струвтуры Кунаке $ра ментов про1рвмм 6.6. СТР Перв 1проп убй Запишем теперь ивпгу програмцу в сдедующец мзде: х: эз х т хчу-1з у: х-Ез Этот фрагмент оглнчаегся от предыдущего тем, что в одной строке стоят двв оператора (рнс. 5.7, в).
Агтклатнв ли соответствующая этой программе структура Кринке (рис. 5.7. г)7 Подобные тзпросы можно продолжить. Является ли неделимым сложный оператор х:-гуып зчхзг, оператор хг «+у-1, оператор хзз, оператор условного присваивания нех:- е>ьз ч г ь, ... 2 Или модель даикна явно предсптлять операции с регистрами? Вопрос не совсем глупый. Сформулированный по-другому, вопрос этот звучит так: насколько сложными могут (должны) быть операторы, определяющие переход в модели программы и изменяющие состояния модели, чтобы модель адекватно огртзжна попедение программы? Ответ на него такой: переходы в модели долэсны нредсннмлянт нм ихненения состояний программы, которые, как это бьыо сказано в разде 5.1, явизются "неделииыыи", нгновеннылш с точки зрения енешниз нроцессов, внеиигей среды.
Например, если х — разделяемав перемениаз, то переход, помеченный оператором х:-х+у-1 на рис. 5.7, а не явлтпся неделимым (см. примеры некорректнмх программ в гл. 1). Неделимыми могут быть операции только относительно другого процесса или внешнего наблюдателя. Поэтому если программа в некотором фрагменте вообще не взаимодействует со средой (т. е. к ее переменным иет обращения извне, программа не посылает и не принимает сообщения, не вводит и не выводит значения и не работает с разделяемыми переменными), то весь фрагмент, каким бы он нн был даниным и долгим в выполнении, может быть представлен в модели одним неделимым переходом. Проблемы, возникающие при представлении с помощью структуры Кринке параллельно функционирующих программ, рассмотрим в сиедувэятм рнг леле.
$.6. Предстааление параллельных программ структурой Крипке Паранлельные программы состоят из нескольких последовательных модулей (процессов), кткдый из которых функционирует независимо, при необходи- Глйея 5 вюр мости (дяя рпження общей задачм) взаимодействуя с другнин процессами через общие переменные илн посылкой сообщений по каналам связи. рассмотрим два процесса, Р, н Рз, парвшельно и независимо выполнающие последовательности простых операций присваивания: Уз:: у2:г ко: :- зг лег уг 21 ЩГ ХГ Уг хм у: х: К2г мхг с2: ево С какими значешшми переменных х н у заюнчиюя выполнение этой прогржамы, если начальные значения х и у ршны 07 Подобный анализ прово. дитсв в примере 5.3, но там мы не рассматриваем состояний процессов. Несмотря на элементарность этих процессов, отвеппь на этот вопрос не так просто.
Анализ этой параллельной программы удобно выполнить с помощью модели. Модель параллельной программы Р, ~~Р2 будем стршць как асинхронную комцознцию моделей процессов Р, н Рз . Пусть состояние Р, 1) Рз состоит из четаерок значений (х, у, Рсн Роз ) . кажлаа операция этих процессов выполняется процессорами неделимо. Поскольку мы не можем делать никаких предполакений о скороешх вмполнення программ, естссзвенно счппць, что в юикдом глобальном соспинин любая из программ может выполнить свой шаг — очередную операцию.
Рис. 5.$ показывает возможные варианты развития вычислений. По окончаНнн ПаРаЛЛЕЛЬНОй ПРОГРаММЫ ПЕРЕМЕННЫЕ х Н у МО1УГ ПРИНЯТЬ тРИ РаЗНЫЕ значения. Какой вариант реализуется при реальном эапусяе программ, зависит от трудно учитываемых соотношений скоростей процессов. Большинство ошибок в разрзГитываемых параллельных программах как раз и являются следствием непрелвнденных перекрмтий операций процессов.
В частности, ошибки, обнаруженные в системе управления аппаратом ОеерЯрзсе! с помощью верификации методом шог(е! сйесЫлй, относшся именно к этому типу. Рассмотрим теперь знаменнзую классическую проблему взаимного нскхючення я параллельном программировании. Заметим, что англоязычный термин этой проблемы — шилаЫ ехс(шюл — почти прижился в русскоязычной среде программистов под именем мьюжекс. Программы в своей работе могуГ Нолсльзовать Общий разделяеммй ресурс. например принтер нли структуру данных (файл лля записи в него новой информации).
Фрагмент программы, в котором этот общий ресурс используется, называется критической секцией (илн критическим интервхеом. гт(лг). Очевидно, что не более чем одна программа может выполнять команды в сво поя ока не олс Для в~ вы сн~ гц вяр, искрит с помо ет, что сами вшие вели. иную ит из г вы- Яких , что свой онча- гюче:рмин среде про- роВО . Нее так взныв зявинство потея мсти, с по.
ипу. нурс, й ин- зуетггглгу щы в своей критической секции, иначе, например. в печатаемом документе мшуг появляться строки, посылаемые на печать другой программой, если кргпнческаз секция — зто обращение к печати на общем принтере. Твк в мультфильме "Каникулы в Простокаашино" в письме дяди Федора иавилнсь строки о лохматости. рис.
%В. йоиаакиые результаты емпоякеиня простой параелеяьиой иргараымы Дяя выполнения требования взаимного исключение прогремим как-го ловлг- ны сиихроиизнроеатьса, т. е. учгпьпмть, что делмот лругне программы. Один из вариантов решения проблемы взаимного исключение представлен нные. Пример б.л Два параллельно фущщионирукицнх процесса Р, и Рг имеют свои критаче- ские секции С, и Сз.
Действия ЛГС, и МСз — зто операцми, находящмеся в некритических секциях процессов. Синхронизвциа пропеаюв осущестышеттл с помощью общей разделяемой переменной г. значение 1 которой опредпиг- ет, что в крцзмческой секции не накоднтси нн одного процымв: Гаева я Яг44 а: исг а4 12(щ-Ы Есес аз ОЗ: Щ-Оз п4( С2( СЗ4 Г;-Т+1( пб4 сосо О14 21:4 и14 НС1 и2: 12(г( 11 СОСО и24 вз4 с: 04 и4: С14 пщ 24 2414 иб: Чесс в14 На рш Спв Р, 40 сос( М4СЛО ( На это ЗОЛЯТС Модель выполнения прош(оса Р, (( Рг строкюя как асинхронная композиция моделей процессов Р, н Рз (см раздел 5.3). состояние Р, ((Рг состоит ю троек значений (рс(, рс2,5'), т.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
