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

РГБ ОД

1 3 МА'1 19С'Й ГОСУДАРСТВЕННЫЙ КОМИТЕТ

' РОССИЙСКОЙ ФЕДЕРАЦИИ

ПО ВЫСШЕМУ ОБРАЗОВАНИЮ РОСТОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

Диссертационный совет К.063.52.12.

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

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

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

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

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

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

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

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

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

Официальные оппоненты - зав.кафедрой прикладной математ

ки и програмирования РТУ, профе сор, доктор физико- математичес наук Горстко А.Б.

старший научный сотрудник I Программных Средств (г.Рост н/Д), кандидат физико-матемаигс ких наук Чуев Н.В.

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

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

Защита состоится 1996 г. в _

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

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

Автореферат разослан " 4 " 19% г.

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

к.ф-м.н. —г Муратова Г.В.

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

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

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

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

- 3 -

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

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

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

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

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

- 4 -

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

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

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

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

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

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

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

- 5 -

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

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

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

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

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

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

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

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

- 6 -

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

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

cond (х) "-act (х),

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

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

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

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

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

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

- 7 -

правило L-программы condL(x)i-act(í). Ансамйлеж на q, порождаемым правилом г(х), назовем произвольную конкретизацию этого правила на q, т.е. запись вида г(с), где с=<сг...,сп>, CjeC . Ансамбль г(с) называется актвнил на q, если qf-cond(c). (Обычное отношение истинности f- формул расширяется для частичных структур следующим образом: для атомарной формулы рСЦ,.. • .tn) отношение qhp(t1 ,...,tn)t7] считается ложным, если при оценке 7 на q не определено значение хоть одного терма ti.)

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

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

Атожгршлки действиями, назовем формулы acti(a1,...,an), где a^Cq. Активность ансамбля conü(c)bact(c) может привести к одновременному выполнению всех его атомарных действий. При выполнении. на q атомарное действие р(а) устанавливает истинным р на а, np(ä) устанавливает ложным р на a, a I(ä)=b устанавливает значение Í на 5 равным Ь.

Коалицией на 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'. Ансамбль на q1 cond(c)i-act(c) не выводит из q, если на q истинна формула act (с). О множестве ансамблей, не выводящих из q, говорят, что оно также не выводит из q.

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

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

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

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

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

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

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

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

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

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

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

- 10 -

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

Верификация АПС на основе L-программ сводит анализ таких свойств АПС, как частичная корректность, завершаемость и т.д. к исследованию одноименных свойств моделирующей L-программы. Это достигается за счет того, что каждому вычислению АПС 30,sv..., s ,... в моделирующей L-программе взаимнооднозначно соответствует вычисление q0,q1....,qn..... где q^ - L-структура, представляющая состояние Sj, leiO.1,... ,п,___}. При этом данные представляются в q^, 1е(0,1,... ,п,...), с помощью функций и предикатов языка L, а их преобразования - посредством правил.

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

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

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

Любая АПС определяет систему переходов S=(Q,T), где Q- множество состояний, а Т - отношение перехода на множестве Q, т.е. TcQkQ. Запись q-*q' означает, что (q.q'KT. Пусть P=Q и q.q'eQ. Обозначим через posttS](?) множество всех состояний, достижимых

- II -

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

postCS](P)=iqiBq'(q'eP и q'-И})}.

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

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

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

где post°[S](P)=P, posti+1IS3(P)=post[S](posti[S](P)). Р называется инвариантом системы S, если postCSl (Р)=Р. Множеством неподвижных точек системы S называется множество состояний llxtSl, из которых нет переходов в другие состояния: lixtS]={qi Vq' (q-*-q' -=> q=q')>. Пусть I,E с Q. Отношением £I}SiE) выражается корретностъ (частичная, в смысле Хоора) систеш S относительно предусловия I и постусловия Е, т.е. {I)S£E5 « post*[S](I)nfixCSl с Е.

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

£I)S{E) с=» 3P=Q (post[S3 (?)=Р & IcP & PflflxtSteE) (первый член конъюнкции означает, что Р - инвариант).

Пусть система S аннотирована в смысле Хоора предусловием I, постусловием Е и инвариантом Р. Если множества I, Е, Р, IlxtS] и posttS] (Р) выражаются логическими формулами I, Е, Р, FIX и POST соответственно, то корректность системы следует из истинности логических формул POST Р, I Р, Р л FIX Е, первая из которых есть условие инвариантности Р.

Дальне описывается метод построения формул POST и FIX для L-программ. Пусть П - произвольная L-программа, з g', g - наборы функциональных и предикатных переменных, взаимнооднозначно соответствующих набору Г изменяемых в П функциональных и предикатных символов, причем тип gi и g^^ совпадает с типом f^ Через L1 обозначим язык логики предикатов второго порядка, полученный из L добавлением переменных g' и g, а через L0 - язык логики предикатов полученный из L удалением изменяемых функций и

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

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

тогда г„ - это интерпретации I на а.

- 12 -

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

(S,) Vq', qeQ ( q'—q ~ qQb T(g* ,g) [g'=fq. ,g=T \ >.

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

Построение формулы 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) удовлетворяют следующим спецификациям:

q'^q — 40b Т, (S',g)Cg'=fq.,g=iq],

q'-^q q0t" T118'.g>tg,slq..fi=i,l и qVq,

q'-*q - ^(g'.Dtg^,,^],

на q' есть коалиция, не выводящая из q <=

q0^ ^(g'.Dlg^Iq-.g^qK _ Здесь выпишем только формулу T.jig' ,g), несущую основную семантическую нагрузку в формуле T(g',g). Формула Т., (g'.g) строится в виде:

(2.2) T-ig'.g): Л_ VxfTr(g',g,xf),

i f€I I х I

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

Пусть af - произвольный набор значений f.f. Формула ?f(g'.g,xf) удовлетворяет следующим спецификациям:

(S4—) q'-q = q0h Tf(g',g,af)[g'=fq,,g=Tq], (S4==) на q' есть коалиция, не выводящая из q и устанавливаю- 13 -

где Т (S2—

(S2=-

(S,-=> (s3—

щая значение Г(аг) .совпадающее с Г^ (а?) <=- значение 1ч(аг) не совпадает с ^.(а^ и Т£ (ёМ.^Нё'^д.,

1=7^).

Пусть Ш, переменные 8'€8', 8€8 соответствуют 1. В случае когда Г - функция, формула строится в

виде:

(2.3) Тг(1,,§,^):(8'(Х1)=8(Х£)-

^у-1(8'(хг)=у') - У,уп(е(хг)=у)--ЗуЫе' (хг)=у) - в(хг)=у - ,8,1Х,У)),

где формула фг (ё',ё,хг,у) для произвольного значения Ъ переменной у удовлетворяет следующим спецификациям:

и коалиция, переводящая я' в q, устанавливает

Г(аг)=Ь (в(аг)=Ъ - фг (§' ,8,а£,Ъ) )1§'=Т<1. ,8=^1 -

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

Ч0К8(аг)=Ь - ф1(вМ,а1,Ь))[в,=Тд,,|=Г3]. В случае когда Г - предикат, формула Т£(8',8» строится в виде:

(2.4) Тг(8\8,хг):(8'(хх) - - п8'(хг) Л

где формула фр£(§'удовлетворяет следующим спецификациям: (56-=>) q'-*q и коалиция, переводящая q, в q, устанавливает

Г(аг) ^ (8(аг) - ФрГ(1',8,аг))£8,=Г(1,,8=Г(1]), (36<=) на q' есть коалиция, не выводящая из ч и устанавливающая 1(аг) q0!= (8(аг)' Фр£ (еЧё.^Шё'^-.ё^], а формула Фп£(8'>8.хг) удовлетворяет спецификациям (Э7«=-;

совпадающими соответственно с (36-=»), ) с точностью до за-

мены <рр1 на фп1, ^(х^ на -\г(х£) и Г(хг) на II(1£).

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

(2.5) фг(§\8,хгу): фи(8',ё,хг,у) - ф2г(ё',ё,хг,у).

Формула ф1£(|',8,хг,у) удовлетворяет спецификациям: (Б8-=) Я'-♦Я и коалиция, переводящая q, в q, устанавливает 1(а£)=Ь и ансамбль этой коалиции, устанавливающий - 14 -

f(af)=b, порожден не синхронизированным правилом —=>

q0f= (8(áf)=b - фи(ЁМ,а£,Ь))Сё'=Г(1,,ё=Т(1], (Sg^-) на q' есть коалиция, не выводящая из q и устанавливающая í(áf)=b

— q0H (g(af)=b - 01f(g',g,af,b))[g'=fq,,s=íq3. а формула ф2Г(g'.g.a^b) удовлетворяет спецификациям: (Sg=>) q'-*q, коалиция, переводящая q' в q, устанавливает I(af)=b и ансамбль этой коалиции, устанавливающий í(af)=b, порожден синхронизированным правилом ==>

(eíaf)=b - $2f(g',g,af,b))tg'=Tq,,g=Tq]. (S9<=) на q' есть коалиция , не выводящая из q и устанавливающая Г(а^)=Ь

q0H (g(af)=b - 02f(g',g,af,b))[g'=íql, g=fqJ.

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

con<ii(zi,xf,y) н actl^fz^x^.y) Л f(xf)=у - act21(ai,xf,у) -правило, соответствующее i-тому вхождению, leo; acti - actl^ act?^. Формула (g',g,xf,y) строится в виде:

(2.6) 01f(g',g,xf,y):

^v 3zi(coMi<g,>(a1,xf,y) - acti<g>(zi,xf,y))

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

- множество номеров правил k-той синхрогруппы ; о^ - множество номеров вхождений формулы вида í(xf)=y в действия .правил k-той синхрогруппы;

condk;.(sk;j,xf,y) »- ^^¿(з^.х^у) - правило k-той синхрогруппы, соответствующее З-тому вхождению, Jío^;

vk - синхронизированные переменные k-той синхрогруппы; z¿ . (Gjj. j)- несинхронизированные переменные кортежа s,, .(х^.у) (здесь точка обозначает конкатенацию);

V. . (v' .) - синхронизированные переменные кортежа

(S

10

(S

11

Формула <t>2f(g',g,xf,y) из (2.5) строится в виде:

(2.7) <}>?f(g\g,xf,y): v ($¿f(g',g,xf,y) - <KI(g\g)).

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

(S10-=>) q'-vq и коалиция, переводящая q' в q, устанавливает l(ar)=b и ансамбль коалиции, устанавливающий I(af)=Ь, порожден правилом k-той синхрогруппы

— %Ь Фи (g,.g,af,b)[g,=í(l,,i=Tql.

■ ) на q' есть активный ансамбль, порожденный правилом синхрогруппы, устанавливающий í(af)=b, и синхро-расширение которого на q' не выводит из q

— V 4.1 (I,.e.5f.b)te,=rq.,§=T<li.

>) q'-»-q и коалиция,переводящая q' в q,содержит ансамбль, порожденный правилом k-той синхрогруппы -=

— Q0b ^(g'.g)fg'=íq.,g=íq3-■) на q' есть коалиция, невыводящая из q, все ансамбли

- Которой порождены правилами k-той синхрогруппы (такую коалицию обозначим через К£) <=

q0f* 4£(g' .g. )íg'=íq- .S=íq] К на q' есть активный ансамбль, порожденный правилом k-той синхрогруппы..

Формула фкг(g',g,xf,y) строится в виде:

(2.8) ф£г(в\ё,хгу):

* Vvk>á(condk>3<g'Xi'ki-j.x^-.V,) --actk>.<g>(z'kiá,i5k)¿,vk>;¡))).

Пусть 1-тое правило k-той синхрогруппы имеет вид: ^соМкД(акД,Ук11) ь actk>1(sk)1,vkil).

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

(2.9) ф£(в\в):

(S

11

' 3\fl(3Ykil(COr1dk?1<g->(Skfl,Ykil)^ -Vyk)1(condkil<g'>(2ka,ykil) - actkii<g>(E¿_1,vk>í¡)).

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

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

из i. Для произвольной L-программы П, формула POST, выражающая postin](P) строится в виде:

POST: Э§ (T(g,r) - P<g>).

Условие инвариантности из теоремы 2.1 с построением формулы для post приобретает вид Vg Cg). где (в> = (T(g,T) - P<g>) -V Р.

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

®2(g): (T^g.I) - P<g>) — P.

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

Пусть переменные g'€g', g€g соответствуют Г из ±. Формула PIX, выражающая множество 11х1Ш строится в виде: PIX: Vg( л_ух,(g)>, где Ш L

FXf(|): vxf,y (®f(i,g,xr,y) — I(xf)=y), когда Г функция, и

FXf(g): Vxf(®pf(T,g,xf) — i(xf)) -

* V*f («nfti.g.Xf) — ->i(Xf)), КОГДЗ Г ПрбДИКЗТ.

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

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

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

Пусть о - множество номеров правил программы П. Множество неконфликтных неподвижных точек программы П выражается формулой Л Уг,(сопйЛа,) асг.(§,)).

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

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

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

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

- 18 -

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

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

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

Множеством финальных состояний ilntS] назовем множество состояний, из которых нет перехода в S:

fintS]={q|Vq' ((q.q* )j£T)>.

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

pretS](P)={q|3q* (q-*q'H q'gP)}. Бесконечной траекторией W в системе переходов S, назовем множество состояний, проходимых бесконечными вычислениями S, т.е. W - бесконечная траектория «=» Vq(qeW —* 3q'(q-*q'H q'€W)), т.е.

WcpretSHW).

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

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

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

Понятия дедлока и лайвлока часто обобщают на случай множества переходов, заменяя в определениях дедлока, лайвлока С^. на С^, где т обозначает произвольное подмножество множества переходов в Б; С^ - множество состояний, из которых существует переход, принадлежащий т, т.е.Сх = £q | Эгет; Зq^ )),или, что то же

самое, С_= и С..

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

V V •••• Чп.....

такая, что (Ч^Ч^КТ Для всех IX). Конечным вычислением называется конечная последовательность состояний 5, которая завершается некоторым состоянием qneItn[S]: Бесконечным вычислением называется бесконечная последовательность состояний <}. Система переходов 8 называется завершаемой относительно предусловия 1с0, если все вычисления, начинающиеся в I, конечны.

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

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

a) префикс некоторого вычисления с началом в q приводит из q б Р2 по Р.,,если Зq,,q"(q*=q.q".q, и q€P1 и 5"еР1 и Ч'€?2)

b) префикс некоторого вычисления приводит из Р1 6 q по Р2, если За' ,с[и( с}^'.?}"^ и q'eP1 и и qeP2 ).

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

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

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

a) Р2 1-тесно достхило из Р1, если для любого состояния qíP1nP2 существует префикс вычисления, приводящий из ч в Р2 по Рг

b) Р2 2-тесно Оостихшо из Р.,, если для любого состояния

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

c) Р2 3-теско 0остихило из Р1, если Р1ПР2ПГ1п[3]=0 и для

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

- 20 -

ПО P1 .

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

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

a) префикс q' некоторого вычисления с началом в q приводит, из q в Р, если 3q'.^"(q^q.^.q* и q'eP).

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

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

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

b) Р2 1-сильно достихимо из Р1, если Р2 1-достижимо из post*CSi(P1).

c) Р2 2-досшжило из Pv если для любого состояния qePj/lP, существует префикс вычисления, приводящий из Р1 в q.

d) ?2 З-доститмо из Р1, если PlnP2nrinlS]=0 и для любого

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

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

Пусть Y - множество, фундированное по отношению <; -

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

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

на Р,иР2 функции l:Q-*-Y справедливо Vq(qeP1f1P2 -=» 3q' (q-w}' и q,6P1UP2 и ?(q)>5(q'))).

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

на ?.,UP2 функции ?:Q—>-Y справедливо Vq(q€P0nP1 -=» 3q' (q'-*-q и

- 21 -

q'€P1UP2 и Ç(q')< î(q)>).

Утверждение 3.3. P2 3-тесно достижимо из P1 » для некоторого фундированного по отношению < множества Y и некоторой тотальной

на P.,tJP2 функции Ç:Q-»-Y справедливо VqiqeP.,^ qefinCS] ) и

Vq,q'( qePlnP2 и q—q' — q'eP.,UP2 и Ç(q)>Ç(q')).

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

Система переходов S завершаема относительно предусловия I с Q » 3W = Q (I с Я и flnCS ] 3-тесно достижимо из W).

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

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

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

(Р,*тРг 3g(T1(ï,g)'(PrP2)<g>-(Ç>Ç<g>))).

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

(Рг-пР1 agiT^gJ^P^Kg^ig^ç))).

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

(Р^тРг tFIN) - vag.g'UP^^Hg^Ttg.g') -> -н- (Р1-Рг)<ё,>'«<ё»£<ё,>)),

где FIN - формула, выражающая множество ИпШЗ.

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

T1 (g,ï)-INW<g> -*• INW.

3)Условие дедлоковости для L-формулы DED:

(Т, (g,ï)-DED<g> DED)-4 -(DED -> -iCQNs),

где s=t, либо s=t, CONt и CON^. - формулы, выражающие соответственно Ct и С .

t X

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

(LIV 3g(T(f,g)-LIV<g>))-- 22 -

*(ЫУ — пОТз),

где либо Б=г.

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

ЫУ Э§(Т(Г,8)-пС0Яз<ё>~ЫУф) где б=1;, либо з=1.

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

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

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

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

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

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

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

- 23 -

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

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

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

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

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

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

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

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

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

- 24 -

С.40-52.

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

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

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

7. Kritski S.Р., Рапкоу S.V. "The Verification of distributed Systems on the base of L-programme. " in Proceedings of the First International Workshop on High Speed Networks and Open Distributed Platforms, St.Petersburg, 1995, P.14.

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