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

РГ6 и»

1 7 Ьмл ^^

Академия наук Украины Институт кибернетики имени В. М. Глушкова

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

ПАНФИЛЕНКО Валерий Павлович

УДК 681.3.06

МНОГОУРОВНЕВОЕ ПРОЕКТИРОВАНИЕ И ПРОВЕРКА СВОЙСТВ СТРУКТУРИРОВАННЫХ ПАРАЛЛЕЛЬНЫХ СХЕМ ПРОГРАММ

05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов, систем и сетей

Автореферат диссертации на соискание ученой степени кандидата физико-математических наук

Киев 1993

Работа выполнена в Институте кибернетики имени В. М. Глушкова АН Украины.

Научный руководитель: доктор технических наук

ЦЕЙТЛИН Г. Е.

Официальные оппоненты: доктор физико-математических

наук, профессор АНИСИМОВ А. В.,

кандидат физико-математических наук ГОРОХОВСКИЙ С. С.

Ведущее предприятие: Институт программных систем

АН Украины.

Защита состоится «-» - 19 г. в-

часов на заседании специализированного совета Д 016.45.01 при Институте кибернетики имени В. М. Глушкова АН Украины по адресу:

252207 Киев 207, проспект Академика Глушкова, 40.

С диссертацией можно ознакомиться в научно-техническом архиве института.

Автореферат разослан « »---19 г.

Ученый секретарь .специализированного совета СИНЯВСКИЙ В. Ф.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность теиы. В настоящее время интенсивно развиваются методы формализованных спецификация лрогра:.^. в теории программирования разработан рад формальные моделей н конструкций, удобных для построения строго обоснованных программных систем Еместе с доказательство» наличия в них тех или иных свойств. К числу известных методов относятся система алгебраического, логического, композиционного,

трансформационного программирования, формализованные

технические задания, VDU, й-технояогия и т.д. Развиваются средства инструментальной поддержи формализованных спецификаций, в той числе алгебраических. Отметим, что к числу первых отечественных языков алгебраического программирования относится АНАЛИТИК (Мир-2, CMI4I0 и др.), созданный в Институте кибернетики им. В.М.Глупкова АН Украины. Получила известность современная система алгебраического програиыиронакия APS, такта, созданная в Институте кибернетики.

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

'поддерякой МСПП -является структурный синтезатор программ ' МУЛЬТИПРОЦЕССИСТ, который по многоуровневым спецификациям генерирует программный продукт.

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

Цель и задачи работы. Целью диссертации является:

- фооиализация ' концепции ■ согласованности спецификаций алгоритмов и программ, заданных на разных уровнях абстракции, при проектировании по методу МСПП;

- исследование свойств тупиковости (клинчей, дедлоков, зацикливаний) и фиктивности (невыполняемых итерируемых 'компонент) спецификаций параллельных программ;

- разработка для метода МСПП и его инструментария средств обнаружения тупиков и фиктивностей в спецификациях параллелыг'х программ. .

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

Исследованы свойства монотонности операторов в соответствующих классах САА-М. Исследована и алгоритмизирована проблема тупиков и фиктивностей в асинхронных параллельных схемах програ!5М.

Практическая ценность. Концепция согласованности спецификаций ка разных уровнях абстракции представляет практический интерес при проектировании и синтезе программ по методу 'МСПП в связи с повышением надежности программного продукта и ускорением его отладки.

Расширены средства описания логических условий для синхронизации параллельных процессов, что обогащает 'изобразительные возможности входного языка системы МУЛЬТИПРОЦЕССКСТ.

В рамках метода МСПП в системе МУЛЬТИПРОЦЕССИСТ реализован . анализатор свойств тупиковости и фиктивности в спецификациях

параллельных алгоритмов и программ. Сш анализатор спроектирован и синтезирован средствами система мультипроцесскст.

Настоящая работа выполнялась в рамках исследований по темам:

- I.13.4.5, N ГР01860045697 "Разработать теоркз и иетоди автоматизированного производства п^облегыо-ориентировагжшс систем";

- СИНТЕЗ "Исследование математических основ доказательного программирования и трансформационной синтез хшессов алгоритмов, программ и программных систем".

Апробация. Результаты работы докладывались на 7-и (Киев, 1986) ,8-ы (Киев, 1988), 10-м (Алушта, 1РЭ2) ' ссдзшграх "Параллельное программирование и высокопроизводительные систеш", на семинарах научногб совета АН Украины по проблем» "Кибернетика".

Публикации. По reue диссертации опубликовано 6 работ..

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

содержание работы

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

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

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

Метод MC im основывается на аппарате конечнопорогдешшх CAA, операторы которых представляют алгоритмы и програздш на

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

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

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

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

Понижение уровня абстракции непосредственно связано с изменением структуры информационного множества CAA, поскольку ' более "подробная" структура информационного множества способна задавать более "детальные" отображения. Обозначим через А' и А CAA с более высоким и низким уровнем абстракции соответственно. Тем самым, построение А мояет быть достигнуто "разукрупнением"

элементов информационного множества А' на классы более подробно описанных элементов.

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

Теорема 1. Множество уточнений элементов из'А образует подалгебру А', обратное отношение í>-1 является гомоморфизмом из А' в А, а конкретизация является изоморфным влогением А в А'.

Обозначим через Т и Т' алгебры термов, соответствуйте' А и А', а через h и h' интерпретирующие отображения из Т в А и Т' в А' соответственно. Будем называть уточнением терма t?T терм t'eT', получаемый подстановкой любых допустимых термов вместо предметных переменных в t. Конкретизацией термов р будем называть взаимно однозначное соответствие термов из Т и подмножества их уточнений в Г,

Теорема 2. Конкретизация р изоморфное вложение Т в Т'.

Конкретизации термов р1 и р2 будем называть семантически эквивалентными, если VteT h'(р1(t))=h'(p2(t)). Отношение семантической эквивалентности действительно будет эквивалентностью на множестве конкретизации термов. Конкретизации термов р1 и р2 будут семантичеслси эквивалентны

тогда и только тогда, когда h'(р1(t))=h*(p2(t)), i=1,п для предметных переменных из Т.

Конкретизации тернов и элементов CAA соответствуют' синтаксическому и семантическому аспектам проектирования. Спецификацией 'класса алгоритмов на заданном уровне абстракции будем называть тройку <G,A,h>, где G - ГСП, Л - CAA, h -интерпретирующее отображение из алгебры термов Т в А. Пусть А имеет более высокий уровень абстракции, чем А', тогда <G,A,h> и <G',A',h'> спецификации алгоритмов на разных -уровнях абстракции. Спецификации <G,A,h> и <G',A',h'> убудем называть согласованными, если из того, что t'=p(t), зледует h(t)=4»(h' (t')), tíT.t'eT'. Это означает, что согласованные

спецификации в качестве возможных конкретизация термов из Т допускают не все уточнения из Т', а яшь те, интерпретации которых в САА А* уточняют соответствующие элементы САД А'.

Пару <р,р> будем называть конкретизацией спецификаций, если р - конкретизация элементов из А, ар- конкретизация термов' из L(G)cT. Конкретизацию <р,р>, будем называть корректной/если VteT h'(p(t))=p(h(t)). Пусть р - конкретизация термов. Тогда, если найдется такая конкретизация р элементов-С АЛ, что конкретизация <р,р> спецификаций корректна, то она единственна. И обратно, для известной конкретизации р элементов СМ существует такая конкретизация р термов, что конкретизация <р,р> спецификаций корректна.

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

Таким образом, согласованные спецификации и корректные конкретизации сводимы друг к другу.

Конкретизации <р,р1> и <р,р2> спецификаций будем называть семантически эквивалентными, если р^ и р^ семантически эквивалентны. Отметим, что любые корректные конкретизации вида <р,р1> и <р,р2> семантически эквивалентна. Тогда множество корректных Koraq -?изаций распадается на классы по отношению семантической эквивалентности. Для любого р существует единственная (с точностью до семантической эквивалентности) р такая, что конкретизация <р,р> корректна.' Таким образом, корректная конкретизация <р,р> восстанавливается однозначно из р с точность» до семантической эквивалентности.

Терш tj ,t2€T будем называть семантически эквивалентными (при интерпретации h), если h(t1) = h(tg). Тогда корректная конкретизация преобразует семантически эквивалентные термы в семантически эквивалентные.

Пусть ГСП G задает класс алгоритмов L(G) = Т и ГСП G* задает класс алгоритмов L(G') с Т' на более низком уровне абстракции. Тогда для L(G) с т p(L(G)) с т будут составлять ' конкретизации алгоритмов на более низком уровне абстракции.

Замену заданной ГСП G на ГСП G' при проектировании алгоритма будем называть поуровневкм переходом, если I). VteL(G) p(h(t)) = h'(p(t)).

2). pCL(G)) = L(G').

Условие 1 следует из корректности, конкретизации. Упорядоченное по включению инокество языков М", удовлетворяющих условию 1, составляеет полную решетку, в которой р (L(G)) будет едино т Ее ниш наименьшим элементом. Тогда условие 2 гарантирует единственность построения 1(G). .

Пусть G=<T,N,o,P> и G'=<T' ,N' ,о* ,Р'> -ГСП и с^ с'±, l=T7i - предметные переменные Т и Т' соответственно. По построению

p(c1)=t^(cj,...,c¿), 1=Т7ш.

Теорема 4. При поуровневсм переходе ГСП G можно получить из ГСП G1 по следующим правилам:

Т' = íc^, i=T7m), N' = N U Т, о' = о,

Р- = Р U {с ±-» 1=Пп>.

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

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

Главы 2,3 посвящены проверке сзойств тупиковости и фиктивности параллельных регулярных схем программ (ПРС).

Рассматриваются модифицированные СМ, дополненные средствами описания параллельных вычислений. Множество логически! значений в алгебре условий дополнено значением "неопределенность" для описания аварийных ситуаций. Сигнатура СМ-М включает операцию разделенной дизъюнкции, состоящую в асинхронном параллельном выполнении операторов. Тогда параллельные регулярные схемы (ПРС) это операторные термы. Синхронизация вычислений в параллельных регулярных схемах осуществляется путем расстановки контрольных точек и операторов задержки (сяидання) с ними связанных. Контрольной точкой назы! /ется место на стыке операторов, входящих в IIPC. С контрольной точкой связывается логическое условие, которое

становится истинным, когда процесс вычислений достигает данной контрольной точки. Предполагается, что логическое условие сохраняет истинность и далее в процессе вычислений. Такое свойство называется свойством замкнутости. Логическое условие, обладающее этим свойством, называется замкнутым. Синхронизатором (оператором задержки, ожидания) называется оператор, осуществляющий задержу вычислений в вплоть до момента достижимости процессом вычислений контрольной точки, е1зУ 'соответствующей. Путем применения тождественных соотношение ПРС можно представить в стандартизованном виде, когда, в частности, а-итерации не будут содержать внутренних контрольных точек.

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

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

Пусть пара <Б,Р> - система алгоритмических алгебр и М -информационное множество (множество состояний). Предполагается, что в М существует неопределенное состояние игЫ, такое что УабБ0П а(и)=*. Подмножество Ы'^М называется замкнутым (относительно операций САА), если \fqeM' а^КЫ'.

Подмножество Ы'сМ называется изолированным (относительно операций САА), если его «ополнение Ц\Н* зашснуто.

Утверждение 1. Если Ы^М, ^см и М1- замкнуты (изолированы), то И^им^ и ЬЦП!^ - замкнуто (изолировано).

Утверждение 2. Замкнутые (изолированные) подмножества информационного множества И образуют решетку. Пусть Ы°(а) = < деМ I а^)=0 > - множество ложности,

= ( чеЫ I } множество неопределенности,

М1(а) = { q€Ы I а(^)=1 > - множество истинности. Логическое условие аеБусл замкнуто, если М1 (а) и ыР(а) -замкнуты.

Утверждение 3. Если а.реБ и а,р - замкнуты, то алр -

замкнуто..

Дизъюнкция замкнутых условий, вообще говоря, не замкнута. Утверздение 4. Достаточные признаки замкнутости дизъюнкции:

1. Если а,р замкнуты и всюду определены (#(а)=0 и #(р)=0), то а^р - замкнуто.

2. Если а,р замкнуты и М1 (а)П#(Р)=0 и #(а)ПЫ1 (р)=0, то сц,р -замкнуто.

п ч _ .

Пусть М = ч/И1( Ы1ПМн=0, где Ы замкнуто У1=1,п.

1=1 1 1 3

Замкнутость означает, что УагБ^ и УдеИ^ а^)^ VI«1,п.

Введем следующие обозначения: М^(а) = { qeM1 I а(д) = 1 >,

М°(а) = { qeH1 I а^) = 0 >,

М^(а) = { I. a(q) = ц }.

Будем говорить, что лопгческое условие а замкнуто на М-^Ы, если

М^(а) и замкнуты.

Утверждение 5. Если а замкнуто на М, то а замкнуто на

1=1,п и обратно, если а^ замкнуты на М^, 1=1,п, то

' а.| (q), если q£M1 a(q) = • ... , замкнуто на множестве М.

, Од^), если qeMn

Доопределим условие а^ так, чтобы оно было замкнуто как на так и на Ы. Пусть а лопгческое условие, заданное ка Ы. Логические условия

если qeM1

, т] е (0,ц.1>

•Л , если

будем называть сужениями условия а на Ы,, 1=Т7п. Тогда услов

п и п 1

а предстаниыо следуй.^« образом а = V а; = л сц. И поэтому а -

1=1 1 1=1 1

замкнуто тогда и только тогда, когда Vl=T7n а1 (-0) - замкнуты. ' Верны следующие равенства:

аЛР '= = 1У1(а1Л^31)' = " «4^1 > 3 Д

Следует отметить справедливость следупцих соотношений:

(а) = а , (ayb) = |Ojb Ы ¿а, где а - замкнутое логическое

5 а

условие, ¡Oj = (E,N> - операция фильтрации, Е - тондественный, а

К - неопределенный операторы. В силу приведенных соотношений, а такке на основании утверздений 1-5 и разработанной в теории САА-М процедуры ставдартизации Г1РС справедлива следующая теорема: произвольная IIPC в САА-М с замкнутыми логическими условиями сводима к форме, в которой логические условия в «-дизъюнкциях и а-итерзцнях представимы монотонными ДНФ.

Сохранение свойства замкнутости при логических операциях и разложение условий и выражений на областях вычислений позволяют использовать логические выражения от замкнутых логических условий для синхронизации параллельных процессов, что обогащает изобразительные возможности входного языка системы МУЛЫЗШРОЦЕССЕСТ.

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

Рассматривается абстрактная модель вычислительной системы, являющаяся обобщением абстрактной кодели ЭВМ, которая представляет собой композицию операционной и управляющей структур. Операционная структура делится на непересекающиеся подструктуры P=(P1Ü6l>. Управляющая структура представляет собой совокупность управляй^« терминалов U={U*!iel), действующих в своих гктимых зонах: I'1 - активная зона U1 Viel.

Чтобы икеть возможность отразить факт одновременного независимого выполнения операторов а и b в и/. активных зонах, в

сигнатуру. CAA вводится операция разделенной дизъюнкции Разделенная дизъюнкция операторов а и b состоит в асинхронном параллельном выполнении операторов а и Ь. Пусть А - СМ с зонкнутыми логическими- условиями и Тд - соответствующая ей алгебра термов. Тогда параллельные регулярные схемы (ПРС) это операторные- термы из Тд.

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

Пусть t=0,1,... обозначает дискретное время. Контрольной точхой называется место на стыке операторов, входящих в схему, которое связывается с замкнутым логическим условием

1, если процесс вычислений к моменту t достиг контрольгэй точки,

o(t)H О, если процесс вычислений к моменту t не достиг контрольной точки,

ц, если процесс вычислений аварийно завершен до момента достижения контрольной точки. • Условие а называется условием синхронизации.

Синхронизатором (оператором задержи, окидания) называется

оператор S1(a)={E1), где К1 - тождественный оператор с активной а 1

зоной Р^. Синхронизатор осуществляет задержку вычислений . в активной зоне вплоть до момента достижимости процессом вычислений контрольной точки, с которой связано данное условие синхронизации.

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

В результате ПРС сводима к форме, составленной из параллельных ветвей, а порэллельпке вет л являются разделенной дизъюнкцией последовательных ветвей.

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

к соответствующим итерациям.

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

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

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

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

Теорема 7. Существуют тупиковые итерации только первого и второго рода и их множества не пересекаются.

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

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

исоответствувдей ей сети Петри.

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

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

Утверядение 6. Итерация 1(а) - тупиковая первого рода тогда и только тогда, когда 1(а)<Т(а).

Утверждение 7. Итерация 1(а) - фиктивная тогда к только тогда, когда í(a)<I(a).

Результаты теорем S-8 и утверидений 6, 7 используются при проектировании алгоритма обнаружения тупиков и фиктивностей в ПРС.

Глава четыре посвящена развитию инструментария структурного синтеза программ, спроектированных по методу МСРП. Осноеу инструментария составляет система МУЛЬТИПТОЦЕССИСТ -структурный синтезатор программ. Входным для синтезатора служит САА/1 - язык проектирования в структурированных схемах программ (САЛ-схемах), базирующихся на аппарате САЛ-М. Система МУЛЬТИПРОЦЕССИСТ дополнена анализатором тупиков к фиктивностей в спецификациях параллельных алгоритмов и программ. Анализатор моделирует прохождение процессом вычислений контрольных точек и итераций в ПРС. При этом тупики будут обнаружены, когда вычисления по всем ветвям будут задераакы (теорема 8, утзерхдекие 6).

Неформальное описание алгоритма обнаружения тупик в.

1. Удаление достижимых контрольных точек.

2. Удаление достижимых синхронизаторов.

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

Фиктивную итерацию процесс вычислений гсегда прейдет раньше контрольной точки с ней связанной (утверждение 7), что такие будет отмечено при работе алгоритма. Учет особенностей ПРС-графэ позволяет построить алгоритм обнаружения туляков и фиктивностей линейной сложности 0(п), где п - число узлов графа

(число контрольных точек и ожиданий). Сан анализатор разработан и реализован средствами системы МУЛЬТИПРОЦЕССйСТ. Приведены САА-схеш анализатора.

ОСНОВНЫЕ РЕЗУЛЬТАТЫ ДИССЕРТАЦИИ Выполненная диссертационная работа посвящена формализации согласованности спецификаций алгоритмов и программ при проектировании по методу МСПП, исследованию свойств тупиковости и фиктивности параллельных регулярных схем программ и реализации инструментальных средств для их проверки. Работа содержит следующие основные результаты:

1. Предложена концепция согла соракностк, базируюцаяся на разделении синтаксического и семантического аспектов проектирования. Установлены критерии согласованности спец:;ф:,г.каций алгоритмов и программ на разных уровнях абстрагщш. На основе полученных критериев Предложено расширеше грамматики структурного проектирования при переходе к спецификациям на более низком уровне абстракции.

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

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

4. Система МУЛЪ'ГИПРОЦЕССИСТ дополнена анализатором тупиков и фиктивностей в спецификациях параллельных алгоритмов и программ. Анализато" имеет линейку» сложность от числа контрольных точек и охидашй.

Основные положения диссертации опубликованы в следующих работах:

1. Пакфиленко В.П. О формальных основах многоуровневого

проектирования // Тез. докл. 7-й Всэсоюз. шк.-семинара "Параллельное программирование и высокопроизводительные системы". - Киев: Ин-т кибернетики им. В.М.Глушкова АН УССР, 1986. С. 80-82.

2. Нагорная Л.И., Панфиленко В.П. Поуровневоа проектирование транслятора с параллельного КОБОЛа // Средства реализации систем программирования. - Киев: Ин-т кибернетики им. В.М.Глушкова АН УССР, 1987. С. 8-14.

3. Панфиленко В.П. О грамматиках структурного проектирования и системах алгоритмических алгебр в гягогоуровневоы проектировании. // Тез. докл. 8-го Есесоюз. семинара "Параллельное программирование и высокопроизводительные системы". - Киев: Ин-т кибернетики им. В.М.Глушкова АН УССР, 1Г38. С. 32-34.

4. Панфиленко В.П. Алгоритм проверки невыровдршгости алгебры термов. // Средства представления знаний в информационных технологиях. - Киев: Ин-т кибернетики им. В.М.Глушкова АН УССР, 1992. С. 60-64.

5. Панфиле;£;:о В.П. Согласованные спецификации при многоуровневом проектировании программ // Разработка математического и программного обеспечения ППП и репэниа задач дискретной оптимизации. - Киев: Ин-т кибернетики им. В.М.Глушкова АН УССР, 1992. С. 89-95.

6. Панфиленко В.П. Тупики в параллельных регулярных схемах программ - Киев, 19ЭЗ. - 23 с. (Препр. АН Украины, Ин-т кибернетики им. В.М.Глушкова; 93-1).