автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Верификация асинхронных параллельных систем на основе L-программ

Гь од

п ГОСУДАРСТВЕННЫЙ КОМИТЕТ

U fHIR bio РОССИЙСКОЙ ФЕДЕРАЦИИ

ПО ВЫСШЕМУ ОБРАЗОВАНИЮ

РОСТОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

Региональный специализированный совет К.063.52.12. но физико-математическим наукам

На правах рукописи

ПАНКОВ Сергей Владимирович

ВЕРИФИКАЦИЯ АСИНХРОННЫХ ПАРАЛЛЕЛЬНЫХ СИСТЕМ НА ОСНОВЕ L-ПРОГРАММ

05.13.II - Математическое и программное обеспечение вычислительных машин и систем.

05.13.16 - Применение вычислительной техники, математического моделирования и математических методов в научных исследованиях.

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

г.Ростов-на-Дону - 1995 г.

Работа выполнена на кафедре информатики и вычислительного эксперимента РГУ и в Вычислительном центре РТУ.

Научный руководитель - доцент кафедры ИВЭ РГУ, зав.

лабораторией теоретического программирования ВЦ РГУ, кандидат технических наук Крицкнй СЛТс

Официальные оппоненты - зав.кафедрой прикладной математики и програмирования РГУ, профессор, доктор физико- математических наук Горстко А.Б.

зав.лабораториееЯ НИИ многопроцессорных вычислительных систем при Таганрогском радиотехническом университете, доктор технических наук Бабенко Л.К.

Ведущая организация - Институт кибернетики им.В.М.Глуш-

кова академии наук Украины.

Защита состоится а- /1996

час. на заседании специализированного Совета К.063.52.12. Вычислительного центра Ростовского государственного университета по адресу 344104, Ростов-на-Дону, пр.Стачки, 200/1, корп.2, ВЦ РГУ.

С диссертацией можно ознакомиться в библиотеке РГУ (по адресу ул.Пушкинская, 148).

Автореферат разослан " ^ " Кг.

7

Ученый секретарь совета

к.т.н. Щ€>>ьс^> Х.Д.Дженибалаев

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ Актуальность. Одной из основных проблем технологии программирования является проблема обоснования надежности программ на основе математического моделирования и математических методов. Эта проблема приобретает особое значение в связи с внедрением в практику параллельных вычислительных систем, информационно-вычислительных сетей и ввиду большой сложности создаваемых для них параллельных программ. Средства параллельной вычислительной техники активно применяются, в частности, при проведении научных исследований, характеризующихся большим размером обрабатываемых данных, требующих высокой скорости и надежности обработки.

Формальная верификация посредством формального доказательства позволяет устанавливать присутствие требуемых свойств программы для всех допустимых этой программой выполнений. Для асинхронных параллельных систем (АПС) она является почти единственным способом анализа требуемых свойств относительно заданных предусловий, из-за сильной недетерминированности таких систем.

Основным подходом к анализу корректности АПС является подход, при котором верифицируется не сама АПС, а ее спецификация (формальная модель). При этом осуществляется сведение анализа требуемых свойств АПС к исследованию свойств ее формальной модели, для которых уже известны метода анализа. Существует потребность в логической формальной модели, позволяющей верифицировать как трансформационные, так и реагирующие АПС, при этом устанавливать наличие сеойств относительно заданных предусловий, а также исследовать АПС с произвольным числом состояний. Для такой модели должны быть разработаны методы верификации (методы построения логических условий корректности). Наличие таких средств может служить основой для достаточно общего подхода к получению логических условий корректности АПС, т.е. для сведения верификации к доказательству истинности логических формул. Таким образом, проблема разработки подхода к верификации АПС, предполагающего выбор формальной модели и разработку методов ее верификации, является актуальной.

Целью работы является разработка подхода к верификации (к построению логических условий корректности для заданного списка свойств) АПС, использующего в качестве формальной

- 3 -

модели Ь-программы, применявшиеся ранее для описания операционной семантики параллельных языков программирования.

Состояние проблемы. Часто, под верификацией трансформационных АПС понимается формальный анализ следующих свойств: частичная корректность в смысле Хоора; завершав-мость; отсутствие тупиков; а также тотальная корректность, определяемая пересечением всех вышеперечисленных свойств. Верификация реагирующих (реактивных) АПС состоит в исследовании таких их свойств, как свойства достижимости дедлоков и лайвлоков, справедливости, реагирования и родственных им свойств. Фундаментом верификации является логика, формальный язык логики, а также формальные модели и метода. Верификация трансформационных АПС обычно сводит анализ их свойств к доказательству истинности условий корректности в виде логических формул.

В отличие от последовательных программ проблема верификации трансформационных АПС менее изучена, нет достаточно общего подхода к получению условий корректности АПС в связи с большм разнообразием типов АПС. Основой такого подхода для последовательных программ является логика Хоора, с помощью аксиом и правил вывода задающая определение семантики синтаксических конструкций языков программирования и метод генерации условий корректности. Но аксиоматика Хоора в общем случае не может служить основой для генерации условий корректности АПС, так как она ориентирована на семантику последовательных программ.

Основным подходом к обоснованию корректности реагирующих АПС, является подход, при котором исследуется (верифицируется) ее формальная модель. Самой абстрактной из известных формальных моделей являются система переходов. Непосредственное применение систем переходов для анализа свойств АПС в общем случае невозможно из-за алгоритмической неразрешимости таких проблем, как проблема достижимости, проблема останова и др.

Представительными из числа широко распространенных формальных моделей являются сети Петри, взаимодействующие последовательные процессы Хоора, временные логики. Но, к сожалению, сети Петри и взаимодействующие последовательные процессы в общем случае не позволяют анализировать частичную корректность АПС, а также другие свойства относительно заданного предусловия. Это

происходит потому, что предусловие может быть представлено мно-

_ 4 _

жеством наборов данных (возможно бесконечным), а представление данных и их преобразования затруднено в этих моделях. Средства верификации на основе временных логик достаточно сложны в применении и используются для анализа реагирующих АПС (главным образом с конечным числом состояний).

"Научная новизна. В результате проведенных исследований обосновано применение формальной модели L-программ для верификации АПС. При этом имеется в виду верификация, устанавливающая частичную корректность АПС относительно заданных пред- и постусловий, а также присутствие других свойств относительно заданного предусловия. На- основе L-программ разрабатывается единый подход к верификации как трансформационных, так и реагирующих АПС.

Для произвольной L-программы, рассматриваемой как система переходов, предложены алгоритмы построения логических формул, выражающих отношение перехода Т, множества состояний post, непосредственно достижимых из заданного множества состояний, множества состояний pre, непосредственно предшествующих заданному множеству состояний, множества неподвижных точек Их, множества заключительных состояний íln, множества состояний С%, з которых возможен переход t, и другие.

С помощью этих формул, а также таких понятий, как инвариант ж траектория, для L-программ формулируются логические условия корректности АПС.

В отличие от подхода на основе временных логик, который состоит в проверке свойств либо множества вычислений, либо дерева вычислений, предлагаемый подход заключается в проверке свойств пар состояний, связанных отношением перехода.

На основе L-программ, а также формулируемых для них условий корректности, для класса потоковых, аннотированных в смысле Хо-ора АПС получены алгоритмы построения условий корректности (корректность определяется как частичная корректность и нетушжо-вость) в виде логических формул первого порядка.

Практическая ценность. Результата диссертации, полученные для L-программ,могут быть применены к конкретным классам АПС посредством сведения верификации АПС к верификации моделирующей L-программы. На этой основе могут быть получены алгоритмы построения условий корректности конкретных

- 5 -

классов аннотированных АПС. Причем такие условия корректности могут быть значительно упрощены по сравнению с общ™ случаем. Таким образом, эти результата могут применяться при построении блока генерации условий корректности в автоматизированных системах верификации АПС из различных проблемных областей.

Предлагаемые методы позволяют устанавливать свойства не только отдельных АПС, но и целых их классов, а также исследовать АПС с произвольным числом состояний.

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

Публикации и апробация работы. По теме диссертации опубликовано 8 работ. Основные положения и результаты диссертации обсуждались на семинарах в ВЦ РГУ и на международных семинарах "Formal Models оГ Concurrency: Logics and Semantics" (Переславль-Залесский, 1992) и "First Internatl-nal Workshop on High Speed Networks Open Distributed Platforms" (Санкт-Петербург, 1995).

Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения, списка литературы (75 наименовний) и трех приложений. Основной текст занимает 133 стр.

СОДЕРЖАНИЕ РАБОТЫ

Во введении обоснована актуальность проволяжх исследований, сформулированна цель диссертационной работы, показана научная новизна результатов диссертации и аннотировано содержание глав.

В первой главе делается краткий обзор наиболее распространеных представительных формальных моделей параллелизма: сети Петри, взаимодействующие последовательные процессы Хоора, временные логики. Описывается синтаксис и семантика L-программ и проводится сопоставление L-программ и перечисленных формальных моделей с точки зрения возможности их применения для

- 6 -

верификации АПС. В качестве формальной модели, позволяющей исследовать такие свойства АПС, как частичная корректность относительно заданных пред- и постусловий, завершаемость относительно заданного предусловия, а также другие свойства относительно заданного предусловия, предлагается использовать L-npor-раммы. Обосновывается возможность такого применения L-программ, а также делается краткий обзор по верификации АПС на основе формальных моделей.

Множество L-программ определяется заданием многосортного языка L логики предикатов первого порядка. Через Q обозначим класс всех частичных (т.е. с частичными функциями) L-структур, а через П - произвольную L-прогрзмму, П действует на Q и преобразует одну Ь-структуру в другую. Ъ-прогрсшма задается конечной совокупностью правил вида

cond(x)>-act(x),

где conti - условие, act - действие, х=<х.,,... ,хп> - кортеж переменных. В этом правиле сопй - произвольная L-формула, act - формула вида act1&...&act|n, где ас^ - формула вида р(хр). "ф(йр) или f(xf)=y (р - предикат, i - функция из L), причем кортежи переменных х , xf состоят из переменных кортежа j, у - переменная того же сорта, что и значение Функции i, у также из х.

В отличие от обычных логических программ L-программы могут произвольным образом переопределять значения функций и предикатов. Их работа аналогична прямому выводу в логических программах и допускает одновременное исполнение разных правил и различных конкретизации одного и того же правила.

В L различаются изменяемые и неизменяемые программой П функции и предикаты. Под изяететш понимаются функции и предикаты, входящие в действия правил программы П, будем

обозначать их кортежем I.

Перед правилом или группой правил может стоять выражение вида $v, называемое синхронизатором, где v - кортеж переменных из числа переменных, входящих в условия этих правил. Группа правил с синхронизатором называется синхрогруппой. Синхронизатор,до некоторой степени уменьшает недетерминизм Ь-программы.

Операционная семантика L-программ определяется с помощью следующих понятий и обозначений.. Пусть Cq - множество констант для обозначения объектов структуры q. Пусть г(х) обозначает

- 7 -

правило Ir-программы cond(x)Hact(x). Ансамблем на q, пороадаемым правилом г(х), назовем произвольную конкретизацию этого правила на q, т.е. запись вида г(с), где с=<с1,. ...сп>, с^С^. Ансамбль г(с) называется атсавнил на q, если qj-cond(c). (Обычное отношение истинности (■ формул расширяется для частичных структур следующим образом: для атомарной формулы p(t.,,...,tn) отношение <1НР("Ц,...,1;п)1ч] считается ложным, если при оценке 7 на q не определено значение хоть одного терма ti.)

Пусть правило r(z,v) входит в группу с синхронизатором $v и на q активен ансамбль г(с,Б), где с и Б - конкретизация соответствующих наборов переменных z и v. Синхрорасширением активного , ансамбля г(с,Б) назовем множество ансамблей

{г(с,Б')1 г(с,Б') активен на q}.

Лтоларкы&л действиями назовем формулы acti(a1,...,an), где a^-tCq. Активность ансамбля cond(c)i-act(с) может привести к одновременному выполнению всех его атомарных действий. При выполнении на q атомарное действие р(а) устанавливает истинным р на §, -ip(ä) устанавливает ложным р на ä, a f(ä)=b устанавливает значение í на ä равным Ъ.

Коалицией на q называется произвольное непустое множество активных ансамблей М, удовлетворяющее следующим трем условиям:

1. Условие непротиворечивости: объединение всех атомарных действий коалиции образует непротиворечивую совокупность формул.

2. Первое условие синхронизации: если в М входит ансамбль, порожденный некоторым правилом синхрогруппы, то и для любого другого правила этой синхрогруппы в М должен входить хотя бы один порожденный этим правилом активный ансамбль, если такой существует.

3. Второе условие синхронизации: если в М входит ансамбль, порожденный правилом синхрогруппы, то в М также должно входить все его синхрорасширение.

Исполнение коалиции состоит в выполнении всех ее атомарных действий.

Определение I.I. Шаг работы L-программы на заданной структуре состоит в исполнении на ней некоторой коалиции.

Обычно под Q понимается произвольное множество L-структур, замкнутое относительно шага работы L-программы П. Тогда L-npor-рамма задает систему переходов S=(Q,T), где Т={(q,q')!q,a'eQ и

- 8 -

q' получается из q исполнением некоторой коалиции).

Очевидно что, если q-*q', то они имеют общие носитель и неизменяемые функции и предикаты.

Для удобства изложения вводятся некоторые понятия. Коалиция, исполнение которой на q дает q', называется коалицией, переводящей q в q'. Ансамбль на q' cond.(c)»-act(c) не выводит из q, если на q истинна формула act (с). О множестве ансамблей, не выводящих из q, говорят, что оно также не выводит из q.

В этой глаЕе отмечаются прблемы, • возникающие при применении наиболее распространенных формальных моделей для верификации АПС. Это основные проблемы, которые снимаются при верификации АПС на основе L-программ.

Под верификацией трансформационной АПС здесь понимается анализ таких ее свойств, как частичная корректность в смысле Хоора относительно заданных пред- и постусловий, завершаемость и недостижимость дедлоков относительно заданного предусловия. При этом в пред- и постуслоеиях, как правило, формулируются некоторые ограничения на наборы входных и выходных данных АПС. Для того, чтобы формальная модель АПС сохраняла такие свойства, необходимо, что бы данные, а также их преобразования были представлены в зтой модели.

К сожалению, сети Петри не ориентированы на представление данных, в них удобно представлять наличие данных или их количество. Так, например, начальной маркировкой невозможно задать предусловие, когда оно описывает бесконечное число наборов входных данных.

Обратим внимание на то, что здесь речь идет о сетях Петри в их классическом понимании. Их мощность моделирования ограниченна, т.к. отсутствует возможность проверки неограниченной позиции на нуль. Все расширения сетей Петри направлены на создание возможности проверки на нуль и повышение мощности моделирования. Известно, что мощность моделирования сетей Петри с проверкой на нуль совпадает с мощностью моделирования машины Тьюринга. Однако, подобные расширения приводят к понижению разрешающей мощности, т.е. к неприменимости методов анализа классических сетей Петри.

Таким образом, в общем случае сети Петри не могут быть использованы для верификации трансформационных АПС.

- 9 -

Для реагирующих АПС в том случае, когда система начинает работу в одном из состояний некоторого множества начальных состояний (возможно бесконечного), а поведение системы зависит от выбора начального состояния, возникает потребность в верификации, осуществляющей проверку свойств системы относительно заданного предусловия. Такая верификация реагирующих АПС может состоять в исследовании различных аспектов достижимости дедлоков, лайвлоков из заданного предусловия. В этом случае, как и в случае с трансформационными АБС, имеют место проблемы, связанные с представлением данных, предусловия, преобразований, а также проблемы, связанные с мощностью моделирования.

Верификация трансформационных АПС предполагает изучение множества достижимых состояний системы. В формальной модели взаимодействующих последовательных процессов Хоора подход к верификации основан на проверке свойств вычислений, представляемых последовательностями событий. Эта формальная модель не содержит средств представления состояний АПС. По этим причинам она не может быть использована для верификации трансформационных АПС.

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

Другая проблема, возникающая при исследовании свойств АПС средствами этой формальной модели, заключается в необходимости проверять очень большое количество протоколов.

Временные логики используются для верификации реагирующих АПС. Их применение в случае трансформационных АПС было бы излишеством, т.к. в этом случае могут быть найдены более простые средства. Верификация АПС средствами временных логик состоит в проверке свойств либо вычислений, либо дерева вычислений, порождаемых этой АПС. Поэтому сложность верификации АПС зависит как от общего числа состояний системы, так и от количества начальных состояний. Верификация, основанная на вычислении временных операторов как наименьших неподвижных точек уравнений требует, чтобы АПС имела конечное число состояний.

В этой главе строится Ь-программа, моделирующая произвольную сеть Петри. На этой основе показывается, что Ь-программы обладают средствами, необходимыми для моделирования АПС, а также то, что мощность моделирования Ь-программ не ниже мощности моделиро-

- 10 -

вания сетей Петри с проверкой на нуль, а следовательно, и машины Тьюринга.

Верификация АПС на основе L-программ сводит анализ таких свойств АПС, как частичная корректность, завершаемость и т.д. к исследовании одноименных свойств моделирующей L-программы. Это достигается за счет того, что каждому вычислению АПС s0,s.,,..., sm>... в моделирующей L-программе взаимнооднозначно соответствует вычисление q0,q1,... ,q ,..., где q^ - L-структура, представляющая состояние Sj, 1е(0,1,...,п,...}. При этом данные представляются в qif i€tO,1 ,...,п,...}, с помощью функций и предикатов языка L, а их преобразования - посредством правил.

Язык L является языком предметной области исследуемой АПС. Пред- и постусловия формулируются в виде L-формул. Подход к верификации АПС на основе L-программ, предполагает использование знаний о предметной области АПС, которые могут быть представлены в виде системы аксиом.

Стоит отметить, что ранее L-программы использовались для описания операционной семантики языков программирования. Способность L-программ описывать операционную семантику параллельных языков программирования позволяет обобщить метода анализа L-программ на классы программ, порождаемых этими языками.

Во второй .главе для L-программ предлагаются средства анализа частичной корректности, основанные на методе инвариантов. В терминах систем переходов формулируются условия частичной корректности для любых АПС. Эти условия выражаются через семантические понятия, такие как, например, отношение перехода, множество неподвижных точек и др. Для произвольной L-программы, рассматриваемой как система переходов, предлагаются алгоритмы построения логических L-формул, выражающие эти понятия. Тем самым доказательство частичной корректности L-программы сводится к доказательству истинности логически формул, которые фактически оказываются формулами первого порядка. При этом основная роль принадлежит формуле, выражающей отношение перехода, применение которой фактически дает метод вывода инварианта.

Любая АПС определяет систему переходов S=(Q,T), где Q- множество состояний, a I - отношение перехода на множестве Q, т.е. TcQ*Q. Запись q-*q' означает, что (q.q'kT. Пусть P=Q и q.q'eQ-Обозначим через postCS]<Р) множество всех состояний, достижимых

- II -

из Р за один шаг,

posttS](P)={q!3q'(q'€P и q'-*q)).

Множеством состояний, достгшхшшх из Р за конечное число шагов,

называется множество

post*[SJ(P)= U posti[S](P), O^i

где post°[S](P)=P, posti+1[S)(?)=posttS](postitSHP))- Р называется инвариантом системы S, если postfSl(Р)=Р. Множеством неподвижных точен системы S называется множество состояний iixiS], из которых нет переходов в другие состояния: IixCS]={qiVq'(q-^q' — q=q')K Пусть 1,Е с Q. Отношением {I)S{E> выражается корретность (частичная, в смысле Хоора) системы S относительно предусловия I и постусловия Е, т.е. ШБШ » post*[Sl (I)nfixiSl = Е.

Справедливо следующее утверждение о полноте метода инвариантов для доказательства корректности систем. •Ееореыа 2.1.

{I)S(E} » 3P=Q (post[S3 (P)cP & IsP & Pflfix[S]cE) (первый член конъюнкции означает, что Р - инвариант).

Пусть система S аннотирована в смысле Хоора предусловием I, постусловием Е и инвариантом Р. Если множества I, Е, Р, fixfS] и post[S3(P) выражаются логическими формулами I, Е, Р, PIX и POST соответственно, то корректность системы следует из истинности логических формул POST -»- Р, I Р, Р - FIX -»- Е, первая из которых есть условие инвариантности Р.

Дальше описывается метод построения формул POST и PIX для L-програш. Пусть П - произвольная L-программа, a g', g - наборы функциональных и предикатных переменных, взаимнооднозначно соот-

ветствуюшдх набору Г изменяемых в П функциональных к предикатных символов, причем тип g^ и g^ совпадает с типом ii. Через Ь^ обозначим язык логики предикатов второго порядка, полученный из L добавлением переменных g' и g, а через LQ - язык логики предикатов полученный из L удалением изменяемых функций и

предикатов Г. Пусть Р - I- формула , P<g> - это формула, полученная из Р, в которой все функциональные и предикатные символы

из i заменены на соответствующие переменные из g. Пусть qeQ,

тогда ?г - это интерпретации f на а.

- 12 -

Сначала строится -формула T(g',g), выражающая отношение перехода в том смысле, что она удовлетворяет следующей спецификации:

(S.,) Vq\ qeQ ( quq qQ|. T(g>,g) fg'=iq,,§=i ^ ).

Здесь и везде в дальнейшем q0 - структура, являщаяся обеднением структур q и q' до языка LQ.

Построение формулы T(g',g) носит иерархический характер по принципу сверху вниз, слева направо. Каждый шаг построения состоит в определении еще неконкретизированной подформулы (на первом шаге такой подформулой является формула T(g',g)) через формулы вида P<g>, и новые неконкретизированные формулы с помощью обычных логических операций. При этом такой шаг сопровождается спецификацией новых формул и доказательством того, что производимая на этом шаге конкретизация подформулы не нарушает ее спецификацию.

Формула T(g',g) строится в виде:

(2.1) T(g\q): T.,(g\g) - T2(g\g),

где ^(g'.g), T2(g\g) удовлетворяют следующим спецификациям: (S2=

(SgC

(S3-(S3=

— q0H ^(i'.Dtg^Tq.,^],

o. q0f- T, (g* ,g) tg'=fQ, ,g=fq] И qVq,

q'-»q q0b T2(g',g)tg'=iq,,®=Tq], на q' есть коалиция, не выводящая из о

Здесь выпишем только формулу несущую основную се-

мантическую нагрузку в формуле Т(§',§). Формула Т.,¡|',§) строится в виде:

(2.2) ТЛё'.ё): ух Т (ё'.ё.х.),

I Èà г I I

где набор переменных х^ соответствует аргументам 1.

Пусть аг - произвольный набор значений хг. Формула Тг(ё',§,хг) удовлетворяет следующим спецификациям:

(Б4^) на q' есть коалиция, не выводящая из ч и устанэвливаю-

- 13 -

щая значение 1(аг) .совпадающее с I значение

Г (а£) не совпадает с Г , (а£) и ч0|- Т^ё'.ё.а^ё'^,,

ё=тч1).

Пусть переменные 8'её', 8(8 соответствуют X.

В случае когда I - функция, формула Тг(§' ,1Дг) строится в

виде:

(2.3) Тг(ё',ё,хг):(в'(хх)=8(хг)-

■-УУ1(8'(хг)=у') - Уу1(в(х1)=у)--Зу(1(в,(хг)=у) * в(хг)=у - ф£(ё',ё,хг,у))1 где формула фг (§' .ё.Ху.у) для произвольного значения "Ь переменной у удовлетворяет следующим спецификациям:

») Ч'-*<1 и коалиция, переводящая я' в устанавливает

Г(а£)=Ь (в(аг)=Ь - ф^ё'.ё.^.ЬШё'^.ё^].

) на д' есть коалиция, не выводящая из ч и устанавливающая 1(аг)=Ь «=-

я0Ке(а£)=Ь - Ф1(ёМ,аг,Ь))[ё'=Тд,,|=Та]. В случае когда I - предикат, формула з^) строится

в виде:

(2.4) Тг(ё',ё,хг):(ё'(хг) - в(хг) - иг' (х1) -

- 8*(хг) " 18(хг)- фпг(§',ё,хг)),

где формула фрг(ё',ё.х£) удовлетворяет следующим спецификациям: q^—хз и коалиция, переводящая q, в ч, устанавливает

Г(а£) (в(аг) - Фрг(1,.ё,ах))[в'=г(1,,8=Т(1]),

на q, есть коалиция, не выводящая из ч и устанавливающая Х(аг) о- ч0(= (в(ах)- Фрг(1',Ё,а£))[ё'=1С1,,ё=Гч], а формула ФпГ(в',8,хг) удовлетворяет спецификациям (3?-=>), (37=—), совпадающими соответственно с (Б^-^), ) с точностью до замены ф £ на фпГ, 8(хг) на -1£(хг) и 1(хГ) на пГ(хГ).

Пусть 1 - функция. Формула фг(ё'»ёДг.У) строится в виде:

(2.5) Фг(ё',ёДгУ): Ф1Г(ё'»8,хг,у) - фгг(ё',ё,хг,у).

Формула ф11(ё',ё,х£,у) удовлетворяет спецификациям:

q'—и коалиция, переводящая q, в q, устанавливает Г(а^)=Ь и ансамбль этой коалиции, устанавливающий - 14 -

Да£)=Ъ, порожден не синхронизированным правилом

-=» ОоН (8(а1)=Ь - 4>1Г,Ь))[ё'=Т(1, (За«=»-) на q, есть коалиция, не выводящая из д и устанавливающая Г(аг)=Ь

а формула ф2г(б'.8.аг,Ъ) удовлетворяет спецификациям: (Бд-о) коалиция, переводящая q, в д, устанавливает

Г(а£)=Ь и ансамбль этой коалиции, устанавливающий Г(а£)=Ь, порожден синхронизированным правилом «=■

(Бдв-) на q' есть коалиция , не выводящая из q и устанавливающая Г(а£)=Ъ

Формула ф1£ строится с помощью следующих обозначений: о - множество номеров вхождений формулы вида Г(х£)=у в действия не^шхронизированных правил П;

сопй/^.х^у) асИ1(ё1,х£,у) ~ Г(х?)=у Л асг21(а1,х£,у) -правило, соответствующее 1-тому вхождению, 1<ео; ас1^ - аси^ асг2±. Формула ф1Г(ё',§,хг,у) строится в виде:

(2.6) ф1£(е',ё,хг,у):_

V Зг, (сопй.<§'>(з.,х<,,у) - асг1.<§>(а.дг,у))

1 1 X ± X

Формула ф2? строится с помощью следующих обозначений: П - множество номеров синхрогрупп программы П, действие хотя бы одного из правил которых содержит вхождение формулы вида £(хх)=у;

- множество номеров правил к-той синхрогруппы ;

с?к - множество номеров вхождений формулы вида Г(х£)=у в действия правил к-той синхрогруппы;

сопй^з^.Д^у) и ,у) - правило к-той синхро-

группы, соответствующее З-тому вхождению, Зезк;

- синхронизированные переменные к-той синхрогруппы;

^ (йк .)- несинхрониз1фованкые переменные кортежа

2,, ^(х^.у) (здесь точка обозначает конкатенацию);

v. . (ул •) - синхронизированные переменные кортежа „ «з о

Формула ф2г(§',у) из (2.5) строится в виде:

(2.7) ФрЛёчёД^у): V Л <К(ё'.ё>ь

а. х к£П

Формулы ф£ (кеП) удовлетворяют следующим спецификациям:

(310-=>) и коалиция, переводящая я' в q, устанавливает

I(аг)=Ъ и ансамбль коалиции, устанавливащий í(aí)=Ъ, порожден правилом к-той синхрогруппы -=»

(510=) на есть активный ансамбль, порожденный правилом """К-ой синхрогруппы, устанавливащий I)=Ь, и синхро-расширение которого на q' не выводит из ч =»

"-ЧоЬЧ'и (1,.в.5гЬ)1в,=Т(1,,в=Тч]. (Б^ ч'-М} и коалиция,переводящая q' в q,содержит ансамбль,

порожденный правилом К-той синхрогруппы -=■

(Б^с») на ч' есть коалиция, невыводящая из все ансамбли • которой порокдены правилами к-той синхрогруппы (такую коалицию обозначим через К£)

-I. и на q' есть активный

ансамбль, порожденный правилом к-той синхрогруппы..

Формула (§',£,хг,у) строится в виде:

(2.8) ф^г(ё',ё,х1.,у):

Пусть 1-тое правило к-той синхрогруппы имеет вид: сопйкД(Ёк11,У1сД) ь асгкД(гкД,7кД).

Формула Фк(ё',ё) (из 2.7) строится в виде:

(2.9) ф£(ё\ё>:

^ э2к11(ЗУкД(С0МкД<ё'Х2к11,\>1)) * - 16 -

Пусть 1 - предикат. Формула 4>pi(4>nf) (из 2.4) имеет такую же структуру, что и формула фг. Разница состоит в следующем. Формула фг строится по правилам, действия которых, содержат вхождения вида I(xf)=y, i - функция, а формула $pi(g',g,xf) (0ni(g',g,xf)) строится по правилам, действия которых содержат вхождения вида i(xf) (-ii(xf)). Формула <f>pf(g,xr) (<J>ni(g,xr)) получается из <!>f(g,xf,y) заменой в определении множеств о, ft и Oy. i(xf)=y на Г(хг) (ii(xf)) и удалением у.

Пусть Р - произвольная ЪЛ~ формула. Через Р обозначим область истинности L-формулы Р. Под Б(?) понимается формула P(g), в которой все свободные вхождения функциональных и предикатных переменных из g, заменены на соответствующие функции и предикаты

из Т. Для произвольной L-программы П, формула POST, выражающая postcni<Р) строится в виде:

POST: 3g (T(g,f) - P<g>).

Условие инвариантности из теоремы 2.1 с построением формулы для post приобретает вид Vg Ф1 (g), где ®,(g): (T(g,i) л P<g>) Р.

На самом деле условие инвариантности можно сфэрмулировать в более простом виде Vg ©2(g), где

®2(g): (Т,(ё,Г) - P<g» — P.

В условии инвариантности Vg можно опустить квантор

Vg, a g считать набором функциональных и предикатных констант, тем самым условие инвариантности фактически сводится к формуле логики первого порядка.

Пусть переменные g'€g', geg соответствуют Г из f. Формула

PIX, выражающая множество fix[П] строится в виде:

FIX: Vg( A_FXf(g)), где li t L

FXf(g): vxj.y (<Ef(I,g,xf,y) i(xf)=y), когда f функция, и

FX^g): vxr(®pf(i,g,xf) — i(xf)) -

- VXf (§ni(i,g,xf) ni(Xj)),

КОРД 8 i ПР6ДЖЗ?,

Среда неподвижных точек различаются конфликтные и неконфликтные.

Определение 2.1.

Конфликтной неподвижной точкой (к.н.т.) назовем неподвижную точку, такую что на ней существует множество активных ансамблей, которое удовлетворяет условиям синхронизации, но не является коалицией, т.к. не удовлетворяет условию непротиворечивости.

Пусть о - множество номеров правил программы П. Множество неконфликтных неподвижных точек программы П выражается формулой А Vz, (cond, (L) -*■ act. (s.)).

i€a 11 11

Таким образом благодаря тому, что эта формула, а также условие инвариантности является фомулами первого порядка, то все условия корректности из теоремы 2.1 для L-программ с неконфликтными неподвижными точками являются формулами логики первого порядка.

Стоит также отметить, что наличие к.н.т. в L-программе, моделирующей конкретную АПС, может означать либо некорректность этой АПС (достижимость дедлока), либо то, что такая L-программа на самом деле не является моделью АПС.

.В третьей главе подход, разработанный в главе 2 для анализа частичной корректности трансформационных АПС, развивается для верификации реагирующих АПС, а также для исследования завершаемости и недостижимости дедлоков в трансформационных АПС.

Сначала для систем переходов формулируются условия достижимости множества Рг из множества Р1 некоторых видов, наиболее интересных с точки зрения исследования дедлоков и лайвлоков. Проверка формулируемых условий может быть сведена к доказательству истинности логических формул второго порядка для конкретных достаточно широких классов аннотированных АПС с произвольным числом состояний. При этом исследование достижимости сводится к анализу определяемых здесь типов тесной достижимости, базирующемуся на применении ограничивающих функций. Затем с помощью таких понятий как инвариант и траектория предлагаются следующие условия: I) условия недостижимости дедлоков и лайвлоков из заданного предусловия; 2) условия достижимости заданного дедлока, лайЕлока из заданного предусловия; 3). условия максимальности достижимого из заданного предусловия дедлока, лайвлока.

- 18 -

Сведение проверки построенных условия достижимости к доказательству истинности логических формул для L-программ проводится с помощью формул из главы 2, а также посредством описания логическими формулами множества состояний pre, непосредственно предшествующих заданному, множеству состояний; множества заключительных состояний fin; множества состояний Ct, в которых переход t возможен; множества состояний Ст, в которых возможен один из переходов множества а (где т - множество переходов L-программы, переопределяющих произвольную фиксированную функцию или предикат в области, задаваемой L-формулой) и другие.

Эти условия позволяют обосновывать отсутствие дедлоков, лайв-локов в системе, а в случае неудачной попытки такого обоснования они позволяют выявлять дедлоки, лайвлоки с целью их устранения.

Основными используемыми в этой главе для системы переходов S понятиями являются следующие понятия:

Множеством финалъшс состояний ilnES) назовем множество состояний, из которых нет перехода в S:

linCS]={q|Vq*((q,q*)j£T)).

Через preCS] (Р) обозначим множество всех состояний системы переходов S, непосредственно предшествующих заданному множеству состояний Р, т.е.

pretSl(P)={q|3q'(q-*q'H q'cP)). Бесконечной траекторией W 'в системе переходов S, назовем множество состояний, проходимых бесконечными вычислениями S, т.е. W - бесконечная траектория » VqfqeW «=> 3q'(q-*q'H q'eW)), т.е.

WcpreCSl(W).

Пусть t обозначает произвольный переход в системе S, q-^-q* обозначает тот факт, что из q есть выход в q' по переходу t. Через обозначим множество состояний, из которых есть выход по переходу t, т.е.

Ct={q|3q'(q-^q')>.

Пусть D.LcQ. Множество состояний D образует дедлок для перехода t в S, если D - инвариант системы S и D=Ct. Множество состояний L образует лайвлок для перехода t в S, ест L - бесконечная траектория в системе S и L^C . Множество состояний L образует слабый лайвлок для перехода t в S, если L - бесконечная траектория в системе переходов S'= =(Q,T'), где

Понятия дедлока и лайвлока часто сообщают на случай множества

переходов, заменяя в определениях дедлока, лайвлока Ct на Сх,

где т обозначает произвольное подмножество множества переходов б

S; С - множество состояний, из которых существует переход,

принадлежащий т, т.е.Сг = {q | 3tet 3q" (q-^q* )>,или, что то же

самое, С = и С.. _tet *

Через q обозначается последовательность состояний

Qo. « •••» Чп» •••»

такая, что (ql,ql+1 )еТ для всех 150. Конечным вычислением называется конечная последовательность состояний q, которая завершается некоторым состоянием q efliUSK Бесконечным вычислением называется бесконечная последовательность состояний q. Система переходов S называется завершаемой относительно предусловия Icq, если все вычисления, начинающиеся в i, конечны.

Типы тесной достижимости определяются с помощью следующих понятий:

Определение ЭЛ.

a) префикс q' некоторого вычисления с началом в q приводит из q в F2 по Р.,,если 3q'^"(q^q.q^.q' и qeP., и q"€P'1 и q'ePg)

b) префикс q' некоторого вычисления приводит из Р1 б q по Р2, ест 3q',q"( q'=q*.q".q и q'eP, и q"*P2 и qcPg ).

Последовательность q" может быть пустой, а запись qeP означает, что каждый элемент последовательности q принадлежит Р.

В термине "тесная достижимость" слово "тесная" характеризует тот факт, что префиксы, посредством которых Р2 достигается из Р,, проходят только через состояния из P,UP£.

Определение 3,2.

a) 1-тесно достижимо из Р1? если для любого состояния qeP-jilPg существует префикс вычисления, приводящий из q в Р2 по Р.,.

b) ?2 2-тесно достхкихо из Р^, если для любого состояния

qePgHP^ существует префикс вычисления, приводящий из Р1 в q по Р2.

c) Р2 3-тесно достижимо из Р.,, если PinP2niln[S]=0 и для

любого состояния qeP^Pg произвольное вычисление, начинающееся в q, имеет префикс вычисления, приводящий из q в Р2

- 20 -

ПО Рг

Затем определяются типы достижимости более общего вида. Для этих типов, префиксы посредством которых Р2 достигается из Р.,, могут проходить через состояния, не принадлежащие - Р.,иР2. Эти типы достижимости определяются с помощью следующих понятий: Определение 3.3.

a) префикс 5' некоторого вычисления с началом в д приводит из q в Р, если и ч'еР).

b) префикс д' некоторого вычисления приводит из Р 6 д, если Зд'.срЧ и ).

Определение 3.4.

a) Р2 1-дошхжило из Р^, если для любого состояния qeP.¡ПP2 существует префикс вычисления, приводящий из ч в Р2>

b) Р2 1-сильно доаттию из Р1, если Р2 1-достижимо из роэ^ЗНР,).

c) Р2 2-достжимо из Р.,, если для любого состояния q€P2ПP1 существует префикс вычисления, приводящий из Р1 в о.

й) Р2 3-достжимй из Р1, если Р1ПР2П11п[31=0 и для любого

состояния qeP1ПP2 произвольное вычисление, начхшащееся в q, имеет префикс, приводящий из q в Р2. Анализ тесной достижимости множества состояний Р2 из множества состояний Р1 может проводиться с помощью метода ограничивающей функции, традиционно использующегося для исследования за-вершаемости. Так, справедливы следующие ниже утверждения.

Пусть У - множество, фундированное по отношению <; £:0-*У -частичная функция, которой будем обозначать ограничивающую функцию. (Под фундированным множеством здесь понимается частично упорядоченное множество, в котором отсутствуют бесконечно убывающие последовательности.)

Утверждение 3.1. Р2 1-тесно достижимо из Р1 » для некоторого фундированного по отновению < множества У и некоторой тотальной

на Р1и?2 функции ?:0-»У справедливо Уд^€Р.,ЛР2 Зq'(q-*<Г и

q^6P1UPг и S(q)>5(q,))).

Утверждение 3.2. Р2 2-тесно достижимо из Р1 » для некоторого фундированного по отношению < множества У и некоторой тотальной

на Р-,иРг функции £:С!-»-У справедливо \К}(д€Р0ПР., —• За'(а'-к} и

- 21 -

ЧЧ1'1иР2 и ич'Х ССч>>>-

Утвервдение 3.3. ?2 3-тесно достижимо из Р1 <=*> для некоторого фундированного по отношению < множества У и некоторой тотальной

на Р11)Р2 функции |:справедливо Vq(q€P1f!P2 цШШЗ]) и

( и ч-^ч' Ч'еР^Рз и 5>>-

Полученные средства анализа тесной достижимости также могут быть использованы для исследования завершаемое®.

Система переходов Б завершаема относительно предусловия I с 5 »ЗЧ»сСН1с«и iln.CS! 3-тесно достижимо из И).

Далее для произвольной Ь-программы П в логике второго порядка формулируются условия видов достижимости из определения 3.4, а также условия недостижимости, достижимости и максимальности дедлока, лайзлока и слабого лайвлока относительно заданного предусловия. Основу проверки этих условий составляет проверка следующих условий:

1)Условия тесной достижимости. Пусть множества Р.,, Р2, из утверждений 3.1 - 3.3 выражаются Ь-формулами Р.,, Р2, а функция £ - Ь-термом

а)Р2 \ -тесно достижимо из Р, в П <=> истинна формула

(Р,*тРг — Зё(Т1(Г,§)-(РГРг)ф-(5>5<й»)).

б)Р£ 2-тесно достижимо из Р, в П <=> истинна формула

в)Р2 3-тесно достижимо из Р, в П » истинна формула

(Р,лтРг тИН) - УЭ§,1'({Рд"1Рг)<ё>-Т(8,ё')

(р1-рг)<ё'>-(?<§»?<§'>)), где Р1Н - формула, выражающая множество ИпШЗ.

2)Условие инвариантности для Ь-формулы 1Ш,(из главы 2):

Т1 (|Д)'1Ш<§> 11Ш.

3)Условие дедлоковости для Ъ-фэрмулы ВЕЙ:

(Т1 (§Д)~БЕБ<{£> БЕБ)~ ~(БЕ0 пСОН.),

где в=4, либо 8=1, ССЖ^ и СОН^. - формулы, выражающие соответственно С«, и С .

ь т:

4)Условие лайвлоковости для Ь-фэрмулы ЫУ:

(ш вё(Т(1 - 22 -

где s=t, либо з=1.

5)Условие слабой лайвлоковости для ЫУ:

Ш — Э1(Т(1,8)'-.С011з<е>'И7ф) где 8=1, либо з=т.

В четвертой главе для произвольной системы из класса потоковых АПС указан способ построения Ь-программы, моделирующей работу этой системы. Показано, что анализ корректности потоковой АПС (корректность определяется через частичную корректность и нетупиковость) сводится к доказательству частичной корректности моделирующей Ь-программы. На основе_ результатов второй главы предлагается алгоритм построения условий корректности произвольной аннотированной потоковой системы из рассматриваемого класса в виде логических формул первого порядка. Таким образом, в этой главе математическое моделирование на основе Ь-программ применяется для научного исследования корректности класса потоковых АПС.

В заключении сформулированы основные результаты диссертации.

В приложении I с помощью методов, разработанных во второй главе, доказывается частичная корректность Ь-программы, отыскивавдей наибольший общий делитель п чисел.

В приложении 2 с помощью разработанных в третьей главе методов для задачи Дейкстры о пяти обедающих философах, обобщенной на п философов, в логике предикатов первого порядка выражаются: множество всех достижимых состояний, множество всех достижимых дедлоковых состояний, а также максимальные достижимые дедлоки и лййвлоки для конкретных множеств переходов.

В приложении 3 на основе результатов, полученных в четвертой главе, показывается корректность потоковой системы, осуществляющей суммирование элементов матрица размером т«п, где п=2к,. для некоторого целого .

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

В настоящей диссертационной работе было предложено использовать Ь-программы в качестве формальной модели для верификации, как трансформационных, так. и реагирующих АПС. Проведено обоснова-

- 23 -

ние такого использования L-программ и разработаны метода их верификации.

Для произвольной L-программы, рассматриваемой как система переходов, предложены алгоритмы построения логических формул, выражающих отношение перехода Т,множества состояний post, непосредственно достижимых из заданного множества состояний; множества состояний pre, непосредственно предшествующих заданному множеству состояний; множества неподвижных точек fix; множества заключительных состояний Tin; множества состояний Ct,B которых возможен переход t; множество состояний Сх, в которых возможен один из переходов множества % (где т - множество переходов L-программы, переопределяющих произвольную фиксированную функцию или предикат в области, задаваемой L-формулой) и другие.

С помощью этих формул, а также таких понятий, как инвариант и траектория для L-программ сформулированы следующие логические условия: I) частичной корректности относительно заданных пред- и постусловий; 2) завершаемости относительно заданного предусловия; 3) недостижимости дедлоков и лайвлоков из заданного предусловия; 4) достижимости заданного дедлока, лайвлока из заданного предусловия; 5) максимальности достижимого из заданного предусловия дедлока, лайвлока.

Для класса потоковых аннотированных АПС на основе сведения верификации АПС к верификации моделирующей L-программы получены алгоритмы построения условий корректности в виде логических формул первого порядка. При этом корректность определяется как частичная корректность и нетупиковость

Работа выполнена в РГУ по теме плана Госкомитета по высшему образованию РФ "Разработка логико-грамматических моделей вычислительных языков и систем на основе формализма предикативных грамматик и L-программ" (.& гос.регистрации 01818005143 ).

Результаты диссертации опубликованы в следующих работах:

1.Крицкий С.П., Панков C.B. Формальная модель асинхронных параллельных вычислений и ее верификация: Депонир. ВИНИТИ, 1992. - J6 3050 В-92с.

2.Панков C.B. Подход к верификации потоковых асинхронных параллельных систем. Депонир. ВИНИТИ, 1992. - J6 3051 5-92.3.

3.Крицкий С.П., Панков C.B. О верификации асинхронных программ продукционного типа.// Программирование. - 1994. - .45. -

- 24 -

С.40-52.

4.Крицкий С.П., Панков C.B. Об одном подходе к иоследоваи® достижимости тупиков в асинхронных параллельных системах. //Редакция журнала "Известия вузов. Северо-Кавказский регион", серия "Естественные науки".-Ростов н/Д, 1994. - № 1-2. - С.139. /Реферат/.

б.Крицкий С.П., Панков C.B. Об одном подходе к исследованию достижимости тупиков в асинхронных параллельных системах: Депо-НИр. ВИНИТИ, 1994. - J6 1705 В-94.

6.Панков C.B. Верификация потоковых асинхронных параллельных систем на основе L-программ. Отчет ВЦ РГУ по теме Л гос.рег. 0I8I8005Ï48, ИНВ.Я 02950000292.

7. Krltski S.P., Pankov S.7. "The Verification oî distributed Systems on the base of L-programme." in Proceedings oî the First International Workshop on High Speed Networks and Open Distributed Platforms, St.Petersburg, 1995, P.14.

8. Панков C.B. Анализ корректности потоковых асинхронных па-раллльных систем на основе L-программ. //Редакция журнала "Известия вузов. Северо-Кавказский регион", серия "Естественные науки".-Ростов н/Д, 1995. - М. /В печати/.