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

од

..МОСКОВСКИЙ ЭНЕРГЕТИЧЕСКИЙ ИНСТИТУТ (ТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ)

На правах рукописи КОРАБЛИН ЮРШ ПРОКОФЬЕВА

СЕМАНТИЧЕСКИЕ МЕТОДЫ АНАЛИЗА РАСПРЕДЕЛЕННЫХ СИСТЕМ

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

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

Москва

1994 г.

Работа выполнена в Московском энергетическом институте (Техническом университете)

Официальные оппоненты: академик МАИ,

доктор технических наук, профессор Евреинов Э.В.

доктор физико-математических наук Борщев В.Б.

доктор физико-математических наук, профессор Кислов Н.В.

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

Российской академии наук

Защита состоится " 3 " OjZi£jzSj)J>i 1994 г. в ■/б ^часов в аудитории f~34Q на заседании специализированного совета Д-053.16.09 в Московском энергетическом институте (Техническом университете).

С диссертацией можно ознакомиться в библиотеке МЭМ.

Отзывы в двух экземплярах, заверенные печатью, просьба направлять по адресу: 105835, ГСП, Москва, Е-250, Красноказарменная ул., 14, Ученый совет МЭИ.

Автореферат разослан "_"_1994 г.

Ученый секретарь специализированного

совета Д-053.16.09 к.т.н., доцент , Г / И.И. Ладыгин

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

Актуальность проблемч. Использование фон-нейм8новской структуры вычислительной систехи (ВС) с единственным центральным процессором было характерно для начального периода развития вычислительной техники. Стремление к повышению быстродействия ВС привело к появлению в 60-е годы идеи параллельной обработки информации на многопроцессорных ВС.

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

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

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

Большой вклад в решение различных аспектов проблемы распределенной обработки информации внесли ученые России и других стран СНГ Евреинов Э.В., Поспелов Д.А., Косарев Ю.Г., Самойленко С.И., Хорошевский В.Г., йценко Е.Л., Цейтлин Г.Е., Летичевский A.A., Котов В.Е., Нариньяни A.C., Миренков H.H., Бандман О.Л., Трахтенгерц Э.А., Кутепов В.П., Борщев В.Б. и др.

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

конструкций языков программирования, но и в реализации этж языков.

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

Еще одной областью приложения формальной семантию является анализ свойств программ, в частности, проблем! эквивалентности, завершимости программ, возможности ш зацикливания и т.д.

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

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

Объектами исследования в диссертации являются: языки 1 системы параллельного и распределенного программирования взаимодействие в которых базируется на механизме передач! сообщений, и модели и метода анализа процессной семантию

эспределенных систем.

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

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

Для решения поставленной цели в диссертации исследуются и зарабатываются следующие вопросы:

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

разработка семантической теории анализа процессов выполнения аспределенных систем, взаимодействие в которых базируется на ередаче сообщений;

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

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

Научная новизна. В работе на основе анализа имеющихся зыков распределенного программирования сформулирована и «ализована новая концепция распределенного программирования, базирующаяся на синтезе функционального подхода к построению ;зыков программирования и механизма асинхронного взаимодействия юмпонентов распределенной программы посредством сообщений :ерез каналы связи специального вида. Разработана семантическая ■еория анализа распределенных программ. В диссертации:

. на основе предложенной концепции распределенного

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

- разработан блочный метод построения семантических моделЕ распределенных программ, обеспечивающий гибкость предложенно1 аппарата для анализа распределенных систем в зависимости с языка разработки;

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

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

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

Практическая ценность. В работе:

- разработаны семантические модели и методы, которые могут быт использованы для решения задач анализа и контро: функционирования распределенных систем, а также щ проектировании и модификации этих систем;

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

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

Реализация результатов работы. Предложенные в работе змантические модели и методы разрабатывались в рожах НИР, дюлняекых па кафедре Прикладной матзматики МЭИ, по разработке зыков распределенного программирования (язык граф-схем ПА, /нкциональный язык параллельного программирования, язык ;инхронных функциональных схем), созданию инструментальных редств отладки и анализа прогрет в этих языках, а также шолнительных средств выполнения распределенных программ на ¿числительных системах. Использование семантического метода, ^поставляющего распределенной программа множество всех ее ¿числительных последовательностей, позволила решить проблем <вивал0нтности для подкласса функциональных схем программ, эдержащих циклы. Кроме того, разработанная семантическая здель для анализа программ в языке граф-схем ПА позволила ззрешить проблему корректности граф-схем ПА, что является зпременным условием правильного функционирования программы в зыко граф-схем ПА на ВС.

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

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

Система распределенного программирования на базе языка АФС ыа разработана вначале для ко?.шлексов СМ4, а затем и для змплексов 1ВМ рс. Эти системы внедрены но предприятиях НИИА, 10 Космического приборостроения, ВНИИ "Альтаир", АО {риогокмаш" и др..

Выполненные НИР:

- исследование эффективности применения функциональных языков : качестве языков параллельного программирования высокого уровн (НИР МЭИ, 1979 - 1980, гос.per. N У63007, отв. исполнитель);

- исследование и создание математического обеспечения для параллельных вычислений на комплексах ЭВМ (НИР МЭИ, 1983 1985, гос.per. N 01830053441, отв. исполнитель);

- разработка системы параллельной и распределенной обработк информации в локальной микропроцессорной сети (НИР МЭИ, 1985 1988, гос.per. N У36793, научное руководство);

- разработка системы распределенного программирования для создания специализированных вычислительных комплексов (НИР МЭИ 1986 - 1989, N 335/86, научное соруководство);

- разработка инструментальных средств, предназначенных дл спецификации, отладки распределенной вычислительной программно системы реального времени по теме КОЛЧАН (НИР МЭИ, 1990 - 1991 N У69559, научное руководство).

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

Апробация работы. Результаты исследований, составляют основное содержание работы, докладывались: на всесоюзн* школах-семинарах "Параллельное программирование высокопроизводительные структуры" (Мукачево, 1980 г., Киев, 1984 г., Алушта, 1988 г., Уфа, 1990 г. ), на семинаре i Математическом центре (г.Амстердам) во время прохождения 1981 г. стажировки у проф. де Баккера, на двухсторонне( семинаре СССР-ГДР "Схемные и программные решения для локалын сетей" (Дрезден, 1987 г.), на семинарах ВЦ СО АН СССР (1979 г и Научного совета по комплексной проблеме "Кибернетика" АН СС( (Москва, 1988 г.), на республиканской научно-технической конференции по вопросам разработки и внедрения средств ВТ и У] в народное хозяйство (Тбилиси, 1977 г.), на IX Всесоюзна симпозиуме "Логическое управление в промышленности" (Ташкен 1986 г.), на YI Всесоюзном симпозиуме по модульным И

(Вильнюс, 1987 г.), на семинарах Московского ДНТП, кафедр ПМ, системотехники МЭИ и других научных форумах.

Публикации. По теме диссертации опубликовано 27 работ, выпущено 12 отчетов по темам НИР.

Структура и объем диссертации. Диссертация состоит из введения,* пяти глав, выводов, списка литературы и приложений. Общий объем основного текста включает 299 стр., в том числе 15 рис.. Список литературы состоит из iii наименований. содержание работы Во введении обоснована актуальность проблемы, отмечен вклад ученых в развитие теории и практики параллельного и распределенного программирования. Рассмотрены основные сферы применения формальной семантики языков программирования и определена область исследуемых систем. Сформулированы цели и задачи исследования, показана научная новизна и практическая ценность полученных результатов, излагается содержанке работы. глава i. языки РАСПРЕДЕЛЕННОГО ш>0гра1йшрсСШМ

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

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

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

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

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

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

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

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

5. Модели "пассивного" наблюдения, характеризующие систем извне. Два объекта считаются эквивалентными, если характе; их поведения, наблюдаемый извне системы, не отличается дру: от друга.

6. Модели "активного" наблюдения, характеризующие поведен» системы извне при возможности воздействия на нее извне. Дв объекта считаются семантически одинаковыми, если при любо: последовательности воздействий извне, невозможно выявлени различий в поведении систем, т.е. системы ведут себ одинаково.

глава 2. функциональные языки параллельного и распределенного программирования

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

рогр8ммиров8ние.

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

Одним из наиболее вакннх аспектов при разработке прак-■ических языков функционального программирования является выбор 'Пераций композиции компонентов программы. Так, использование ¡бстрэктных математических способов композиции приводит к кор-1вктным теоретическим моделям с ясной и простой семантикой, :орошо подходящим для исследований программ [1,3,8]. В главе [редложены две модели построения функциональных языков парал-[ельного программирования: а) посредством композиции функций; ¡) на основе формализации информационной подчиненности кс.чпонен-'ов программы. На базе этих моделей разработаны и реализованы [зыки функционального программирования (ФЯПП и грвф-схем ПА).

Одним из основных результатов этой главы является [оказательство разрешимости проблемы эквивалентности для мрокого подкласса циклических функциональных схем [3]. Этот )езультат является продолжением исследований, начатых в работе 1], где былэ доказана полнота для подмножества ациклических функциональных схем. Класс функциональных схем FS, для которых ¡ешается проблема эквивалентности, ограничен подмножеством функциональных схем, определенных ниже.

Множество выражений ЕХР с типичными элементами а,в,с.....

шределяется как:

i ::= a i а i 0 i (а1• кг) | (а1* а2) | (a,+ аг) f {а} ,

\цэ: а - функциональная переменная; е - тождественная функция; ' - нигде не определенная функция; (а1 • а2) и (а^ а2) -юследовательная и параллельная композиции выражений а1 и а2, соответственно; а + а? - объединение двух выражений, {а} -

оо

иерация а, обозначащая объединение Е а1, где а = в,

Для данного языка сформулирована система доказательства ¡формул вида а=в, состоящэя из множества аксиом и правил вывода. Зднако, наличие в системе рб единственной неделимой операции параллельной композиции "*" является, по-видимому, ^достаточным для доказательства полноты этой системы. Для

решения проблемы эквивалентности функциональных схем програм> указанного вида построена более мощная формальная систем! (РБ1 ), являющаяся расширением системы FS. Введение дополнительных операций, позволяющих представлять операцию "*", позволило доказать разрешимость проблемы эквивалентност! функциональных схем, принадлежащих множеству ехр. Алфавит FS1 содержит:

( 1 ) множество переленных vaй с типичными элементами обозначаемыми через а, Ъ, о,

(2) функциональные константы: е и 0;

(3) символы композиции:

• (последовательная композиция), v (разветвление),

+ (объединение), i (раздельное объединение)

* (конкатенация), д (соединение), {} ( итерация );

(4) скобки.

Отметим, что в отличие от PS, в системе FS1 введены тр:

новых символа композиции ( v, i, л ).

Каждое выражение F51 характеризуется типом. инохеств>

входных ( выходных ) типов TYPE с типичными элементами t, ...

определяется как

t ::= х | (tt, t£) , где х - атомарный тип.

Обозначим через t 4 t£ множество всех выражений FS1

которые имеют тип входа t1 е type и тип выхода t2 « type

Множество выражений ЕХР1 с типичными элементами А, В, с, ...

определяется как U (t 4 t ) следущим образом: t^t^TYPE 1 3

(1) а е х 4 1 ДЛЯ всех а € VAR;

(2) е € х 4 т;

(3) 0 е t1 4 tg для всех t^ , t2 е TYPE;

(4) если А 6 t, 4 t2 и В е t2 4 t3, то (А-В) е t1 4 t3;

(5) если А «= t1 4 tg и В с t1 4 t2, то (А + В) « t1 4 t2;

(6) если A s tt 4 t2 и В € t, 4 t3, то (A v в) € t, 4 (t2, t3)

(7) если А « t 4 t2 и В И3 4 t4, то (А I В) « (t1# t3) 4 (t2, t4);

(8) если A e t 4 1 И В e t2 4 11 ТО (A Л В) e (t1, tg) 4 H

(9) если A 6 t, 4 1 Й В € t, 4 t, И (A » в) e t, 4 t;

:ю) если A e t 4 t1 , то {A} « t1 4 .

Множество тождественных выражений, IDEN, с типичными

цементами е.....определяется следующим образом:

s ::= в | (е1 i е2) | е^ . Здесь и далее мы опускаем символ и скобки там, где это ie вызывает недоразумений.

Множество форлул FORM1 с типичными элементами f.....

шределяется следующим образом:

î ::= А = В, где А, В « ЕХР1 . Аксиомные схемы Asi :

1. А+В = В+А

2. (А+В)+С = А+(В+С)

3. А+0 = А

4. А0 = 0А = а

5. АЕ = SA = А

6. (АВ)С = А(ВС)

7. 01А = Aie = 0

8. (А+В)С = (АС)+ (ВС)

9. А(В+С) = (АС)+(АС) 10. (А+В)1С = (А IС)+(В IС)

Правила вывода ?г1:

1. ( Правило залет ). Пусть А входит в в и А = с. Тогда, если d - выражение, получанное из в заменой А на с, то з - D.

2. ( Решение равенства ). Если А = ВА + с и выражение е не входит в в, то а = {В}С.

Для определения семантики FS1 введем следующие семантические области:

- Непустое конечное множество м с типичными элементами m, ... ;

- Множество м* с типичными элементами Q, ..., где:

Q ::= m | Qm I <Q1, Q2> ;

- Множество M00 с типичными элементами a, ß, 7.....где:

а ::= Q | (сц ; с^) . Семантические значения элементов х « X, где х = vár и {в} и {0} задаются функцией Ф:Х (ы00-» if) :

(1) Ф (а) есть частично определенная функция вида Ф(а):М'-* М',

(2) Ф (е) - тождественная функция вида Ф(е):М'-» м\

(3) Ф (о) - нигде не определенная функция.

11. Al(В+С) = (АIС)+(АIС)

12. (AiB)(CID) = (АС)i(BD)

13. (AvBHCiD) = (AC)v(BD)

14. (AIB)(CAD) = (AC)A(BD)

15. A(BVC) = (AB)v(AC), если А не содержит символов "+" и "{}"

16. АС*BD = (AVB)(CAD)

17. (А) = 8 + А{А}

18. {А + £} = {А} 19- {8} = е

Семантические значения выражений FS1 задаются функцией ©1 :ехр1 - (^(ы00) - ^(м00)) , где ? (м00) есть множество всех подмножеств ы°° с типичными элементами Q и а, ¡3, 7.....

1. ©1 1x2 (Q) = { Ф (х) (Q) | Q е Q } , где X е х

2. ©1 ÎAB1 (а) = ©1 ЕВ! (Ф1 |а1 (а))

3. ©1 IavbI (а) = {(Р1 ;р2 )| Р1 « ©1|а1(т), Р2 € ®11вКт). 7 е а >

4. ©11А » BI (СЦ ,а2 ) = {(р1,р2)||31 «ЕЕ ©11А1 (сц ), Р2 е ©цв1(аг) }

5. ©1 [АлвПа1 ,а2) = { <р1,рг>|р1 еФЦАНа,), рг ^ <01 |в! (а2 ) }

6. ©1ÏA*B1(а) = { <р1.р2>|р1 е ®1(Al(7), р2 е ©1|В1(7). 7 е

7. ©1 ÎA + в! (а) = ©1 IAl (а) и ©1 в В В (а)

8. ©1 Ка}1 (а) = u ©1 1а1! (а), где а0 = е, al+1 = аЧ.

1 = 0

Семантика формул тsi задается с помощью функции

¡F1 :F0RM1 - (M00) - Т) где множество т = { true, false }, следующим образом:

!true, если ©1 1А1 (а) = ©1 IB1 (а)

для всех а е а false, в противном случае Теорема. Формальная система FS1 непротиворечива, т.е.

W* * f •

Лемма, is является подсистемой FS1.

Лемма. Для любых м, Ф и а « м® имеет место:

(в) © fА{ (а) = ©1 SaI (а), где а « ЕХР;

(б) г îa = BS (а) = ¡F1 1а = в| (а), где а, в е ехр.

Таким образом, проблема эквивалентности FS-выражений сводится к проблеме эквивалентности соответствующих PS1-выражений.

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

Показано, что, если выражения айв эквивалентны, то

существуют характеризующие их системы рекурсивных равенств, совпадающие с точностью до переименования переменных.

Далее в работе показано, что, если а и в - эквацконально характеризуемы множествами равенств, совпадающими с точностью цо переименования переменных, то нр31 А = в.

Прямым следствием этих двух фактов, а также непротиворечивости формальной системы FS1 является: Георема. Пусть А « ЕХР, в е ехр. Тогда: (1 ) р А = В ЬР31 А = В. (2) Утверждение t А = В разрешило.

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

Язык грсф-схел параллельных алгоритлов (ПА), предложенный s [2,4,9] и реализованный в [9], может рассматриваться как одна из моделей языков ПА, в которых понятие "параллелизма вычислений" формализуется на основе функциональной подчиненности операторов алгоритма.

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

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

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

Простота правил построения параллельных алгоритмов делает этот язык привлекательным для использования в качестве языка программирования ПА.

В то же время следует отметить, что использование простых правил построения параллельных алгоритмов в языке граф-схем ПА ( и аналогичных ему языках ) может привести к построению некорректных программ, результаты вычисления которых могут

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

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

а) ни для одного из входов любого оператора граф-схемы Ш не может быть одновременно вычислено более одной порции данных;

б) ни один из операторов граф-схемы ПА не может быт* повторно занесен в список готовых для выполнения операторов дс окончания его очередного выполнения.

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

Каждое состояние s^ l е я, процесса выполнения граф-схемь

ПА G идентифицируется парой (m^o/m^g)), где и ы± задают, соответственно, набор одновременно выполняемых операторов у набор операторов, для которых частично вычислены параметры. Определение. Последовательность состояний s , s , ...

называется вычислительны», путел граф-схеяы ПА G, если = &Q v.

для граф-схемы G возможен переход из в. в s. для любого р.

р р+1

Определение. Состояние s± называется корректны*, если для

пары (Mi (G)/m (G)), идентифицирующей это состояние, имеют место следующие условия:

1) любой элемент AI множества ы (G) входит в набор (G) не более одного раза;

2) любой элемент Ai(k,r) множестве м (G) входит в набор м (G] не более одного раза.

Лемма. Граф-схема ПА G является корректной, если и только

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

Теорема. Проблема корректности граф-схем ПА разрешима.

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

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

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

глава 3. язьк ашкрош1ш суншшшьшх СХЕМ I! ЕГО СЗШГГЛКЛ

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

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

Ключевым аспектом разработки языка АФС является поиск

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

Таким образом, в данной главе, наряду с заданием синтаксиса языка АФС, разработан метод задания формальной семантики языка АФС.

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

Взаимодействие функциональных процессов распределенной программы осуществляется только посредством передачи данных через кэналы связи. АФС-каналы могут иметь лного входов и выходов; АФС-каналы допускают различную логику соединения их входов и выходов и позволяют реализовать задаваемые программистом функции передачи данных с входов на выходы каналов; в АФС-каналах используется ассиметричный механизм передачи информации через каналы, т.е. операции записи данных в канал и чтения данных из канала разнесены во времени, что позволяет во многих случаях повысить быстродействие программы. Все каналы, в зависимости от логики объединения входов и выходов, могут быть разбиты на четыре типа: аы-aLL, ail-any, any-ail и any-any.

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

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

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

В языке АФС имеется возможность строить недешерлинированные программы. Недетерминированость

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

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

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

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

( !

--£

области и семантического метода осуществляется следующим образом. Вначале определяется некоторый простой язык, представляющий собой базис для построения языков распределенного программирования, взаимодействие в которых основано на концепции передачи сообщений ( к таким языкам, в частности, помимо АФС, относятся языки csp, OCCAM, DP Б.Хансена и др. ), и задается семантика этого языка. Затем, учитывая особенности языка АФС, строятся семантические определения для АФС-программ.

Исходные синтаксические области базисного языка:

1. Множество элементарных коланд Com с типичным элементом а.

2. Множество булевских выражений Ехр с типичным элементом ъ.

3. Множество коланд ввода ICom с типичным элементом in.

4. Множество коланд вывода осош с типичным элементом out.

5. Множество меток процессов PLab с типичными элементами i, J, где i, j = 1, 2.....

Выделим также следующие константы: skip - пустая команда; tt - тождественно истинное булевское значение.

Множество котнд Cmd с типичным элементом с задается следующим образом:

с ::= skip | а | in | out | o1;с2 | [gc] | *[go] , где gc - типичный элемент множества защищенных коланд GCom со следующим синтаксисом:

gc :: = g с | gc {□ gc} g ::= tt | b | in | out Множество програжи Prog с типичным элэментом рг есть:

pr ::= I::с | рг {« рг} . Семантика программы в базисном языке определяется в два этапа. Вначале определяется семантика каждого последовательного процесса, входящего в состав параллельной программы. Полученные таким образом значения называются априорной семантикой, которая задает для каждого процесса все возможные пути его выполнения без учета связей с другими процессами программы.

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

Для определения семантики базисного языка введем предварительно следующие исходные семантические области:

А е ACom (множество значений элементарных коланд) в е ВЕхр (ужжество значений булевских выражений) IN е picom (множество значений команд ввода) OUT е росот (множество значений команд вывода)

Множество вычислительных последовательностей SPath с типичным элементом зр определил следующим образом: зр ::= X | А | рО | IN | OUT | sp^spg | t~sp t ::= T | В | IN | OUT , где t - типичный элемент множества тестов TEST; т - тождественно-истинное значение; рО - символ завершения ВП; sp^spg - конкатенация ВП зр1 и sp2; t^sp - конкатенация теста t и ВП зр.

Введем множество Ргоо = у (SPath) с типичным элементом р, т.е. Proс - множество всех подмножеств шожества SPath. Определим на множестве Ргоо следующие операции: теоретико-множественного объединения (p^pg); последовательной композиции (Р.,*Р2); теоретико-множественного вычитания (р,\р2); минимальной фиксированной точки (р+). Прежде чем определить значение р+, введем два вспомогательных определения. Определение. ВП зр называется пустой и обозначается через е, если зр = 1, либо зр = ТЛе.

Бесконечную последовательность вида е-е-...-е-... обозначим через loop ( зацикливание ). Определение. е е р, если

1) р з е;

2) Р = Р1 + Р2 и хотя бы для одного (1 = 1, 2) ее р±;

3) р = р1 • р2 и е е р1, е « р2 одновременно.

Определим теперь р+ как линшшъную фиксированную точку оператора Р (р), т.е. р+ = рг(р), где р(р) имеет вид:

Р (р) = A,q . p-q + v ,

р, если е е р где р = -j V =

р\е, если е « р

' loop, если е с р

f р, есл]

1 р\е, если е « р д, если е « р

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

Функции с : cmd -» Ргоо определим следующим образом:

(1) cjsklpü = х (7) c|*[go]l = (£jgcl)+

(2) clal = А (8) C|g0logc2! = Cjgc, l+clgo2l

(3) «¡inj = IN (9) <cîin cl = cjinrcicl

(4) cloutj = OUT (10) Clout ч ol = cjoutrclcl

(5) Clo^.Cgl = Clo1|.Clo2l (11)C[tt-c| = Elttrcld

(6) C|[g0]l = с Ige I (12) Clb О] = Е1ЫлС1с1 где функция E : Exp -» TEST определяет семантические

значения выражений следующим образом:

Е ittj = т, е 5Ы = в.

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

Введем множество вычислительных последовательностей программ epath с типичным элементом ор:

ср ::= рО I А I В I (IN, OUT) | cp^opg | LOOP | a , где po - символ успешного завершения процесса (программы); (IN,OUT) - элемент множества PICom х POCom; в - останов, означающий невозможность выполнения никаких действий (блокировка). На множестве PICom х POCom зададим предикат

1С : PICom х POCom (true, false} , который принимает истинное значение (true) на тех парах семантических значений команд ввода/вывода, для которых взаимодействие возможно, и ложное значение (false) на остальных парах.

На множестве y(CPath) определены операции теоретико-множественного объединения и последовательной композиции.

Семантическая функция программ, в базисном языке задается функцией F : Prog -» ? (CPath).

Функция р для программы рг = i1 : :с1 н i2::c2 » ... « in: :cn определяется с помощью связывающего оператора s (р1, р , ..., рп), где р3 = IP ll^iCj! = с ïcj! • рО, l<j<n.

В общем случае значение р , 1 < i < п, в соответствии с определением семантической функции с, может быть представлено в виде :

pi = е а -р + s 7la-pis + е 'п1глр1г + (*)

1 i е N 13 13 s <= N 13 г « N 1Г

+ „ I /ikXk I Ah

к е N h е N

где а13 б { г, а }, 7ls е t in, out }, т)1г е { т, в },

р1к « { IN, out }, ôlh е { po, loop }.

■2 (р1 . р2. •••• Pn) =

(1) { LOOP I 31 (1 < i < n): LOOP « }

( Этот случай возникает, если хотя бы в одном из

последовательных процессов имеется возможность зацикливания )

(2) + { рО | vi (1 < i < П): р± н ро >

(Этот случай соответствует завершению программы)

(3) + ( (еа з (р1( р2.....p±q.....pn)| qeN}| ie{1 ,2.....n} }

+ { {е^ з (p1 , р2,..., р1г.....pn)|r«N}| ie{1 .2.....n} },

где имеет вид (*), причем.

еа (е ) = ''ir

А- (в-), если а1;) = А ( т)1г = в ) пусто, если з i ( rjlr н т )

(Это случай выполнения элементарной команды (е_ ), либо

аи

разрешения локального недетерминизма (е„ ))

Чг

(4) + { (Ш^, 0ОТ±) - ж (р1.....р±а.....р3а.....рп) |

1С (т1а, 73з) = tt, либо 1С (р1з, р3з) = tt, либо

10 (р1з* = П> ЛИ0° 1С = П } •

где р1з и р определяются аналогично п. 3.

(Это случай успешного взаимодействия двух последовательных процессов, либо разрешения глобального недетерминизма в одном или двух процессах)

(5) + ( ж (р1 > ..., р^.....рп) |

Р1 = ( Е Л1гАР1г + Е Р-^Рщ )+ • Р| . причем, v г е n т}1г = В ( * т ) и

У к е N Р^ = Ш, ( р1к = ООТ, ) для некоторого 3 (1 < 3 < п) и р^ = рО } (Это случай неразрешимого недетерминизма в команде цикла. Цикл завершается и осуществляется выход из цикла, что соответствует значению д = т в определении выражения

р+, т.е. имеет место равенство р+ = р-р+ + т )

(6) + { 0 }, если ни один из п.п. (1) г (5) не применим.

Для доказательства корректности задания семантики необходимо доказать, что оператор Ф : в -> й, где

В = Ргоо ^ X Ргоо2 X ... X ?госп ? (СРа«1) , аппроксимирующий пошаговое применение л, имеет наименьшую фиксированную точку цф, т.е. доказать, что уравнение ФФ = ф имеет решение.

Оператор Ф определяется следующим образом:

Ф = ХФЛр.( Е a -$(suffix.(р)) + Е Ф(suffix (р)) + Е д, (р)), ieN JeN 3 keil

где р е ргос1 х ••• X рг0сп, а± е { а, в, (IN, OUT) ) ,

лк е L00P» .eufiix1 (р) есть выражение, являющееся

аргументом оператора s в п.п. 3f5.

Первая суша в этом определении соответствует пунктам 3 и 4, вторая сумма - пунктам 3 и 5, третья сумма - пунктам 1,2,6.

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

р е ргос~ = Ргос1 х Ргос2 х ••• X Ргосп последовательность аппроксимаций <(Ф11)>1 сходится к пределу lim Ф1!. Затем мы покажем, что этот предел является фиксированной точкой Ф, т.е.

Vp ф ( lim (Ф1].) )р = ( lim (Ф1!) )р . Для ср е cpath будем обозначать через ор[п] префикс, состоящий из первых n-элементов ср, т.е. я -Xg» ... »x (xt « {po, loop, ß} ), если длина ср больше или равна п, или само ср в противном случае. В качестве ср[о] будем брать неопределенный элемент ±. На этом множестве cPath введем отношение частичного порядка следующим образом: op е ср2, если ср1 является префиксом ср2.

Определение. Метрика р на множестве CPath определяется следующим образом :

:~п, если cp1tn-1]=ср2[п-1] и ср1[п]*ср2[п]

о, в противном случае

Лемма. Метрическое пространство (CPath, р) является полным.

Учитывая доказанный де Баккером результат о том, что, если (М,р) - полное метрическое пространство, то (?(Ю,р), где р -Хаусдорфова мера, также является полным, получаем, что (^(CPath), р) - полное метрическое пространство.

Наконец, определим функцию меры на множестве D = Ргос~ -» ? (CPath), где Proc~ = Ргос, X Ргос2 X ••• X Ргосп:

р' ( Ф1 , Ф2 ) = sup { Р ( Ф^, Ф2р ) I р е Ргос~ } Лемма. р'(Ф1, Ф2) < е для о < е < 1 тогда и только тогда,

когда vp е Ргос~ р(Ф1р, Ф2р) < 2~п, где n = min {k|2_k < е).

Р (ср1. ср2) = |

Лемма. Пространство (D, р') является полным метрическим пространством, т.е. каждая последовательность Кош <фк>к в D сходится и ее предел рввен Хр . lim Ф^э . Лемма. Для отображения Ф метрического пространства D найдется п такое, что Ф11 является сжимающим отображением, т.е.

*v

V р «= Ргоо~ V >®2 е D существует такое число к (0<к<1), что

р ( (АРФ^р, (Ф"Ф2)р ) < к • р ( Ф^, Ф2р ) Принимая во внимание известный результат , что, если Ф есть непрерывное отображение полного метрического пространства м в себя и некоторая его степень Фп является сжатием, то уравнение ФФ = Ф имеет единственное решение, нам остается показать, что Ф является непрерывным оператором. Отсюда немедленно будет следовать, что определенная таким образом семантика программ является корректной.

Далее в работе доказана справедливость следующих утверждений:

Лемма. Ф - непрерывный оператор, т.е. для всех сходящихся последовательностей <Фк>к имеет место

lim ФФк = Ф (lim Фк) . Теорема. Оператор -» В, где D = Ргос~ -. т (CPath), имеет минимальную фиксированную точку.

Последняя теорема завершает доказательство корректности задания семантики.

Схемы АФС-программ и их семантика Пусть заданными являются следувдие синтаксические области:

1. Множество элелентарных коланд Com с типичным элементом а.

2. Множество булевских выражений Ехр с типичным элементом ъ.

3. Множество коланд ввода RCom с типичным элементом read.

4. Мжжество коланд вывода wcom с типичным элементом write.

5. Множество леток каналов и процессов CPLab с типичными элементами inj.

6. Множество колеров входов/выходов каналов CNom с типичными эле?лентами к и 1.

Обозначим через Cmd множество коланд с типичным элементом с, а через Prog - множество схел АФС-програлл с типичным элементом рг.

Синтаксис схем АФС-программ зададим следующим образом: рг ::= NET { can > BEGIN fproo END

can ::= CHAN j: : type (k): typed ) | ca^ ; can2 type : := ALL | ANY fproc ::= FUN i::c | fproc1; iproc2 с := a I skip | exit | break | wait | read (i, 1) | write (i, 1) I SEQ (c {; с}) | ALT (gc) | PAR (c {; о}) I LOOP (ALT (gc)) gc ::= g -> с | gc1; gc2

g ::= tt I b I read (i, 1) |write (i, 1) | wait

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

При задании семантических значений функциональных процессов для языка АФС необходимо учесть также следующие его отличия от базисного языка: 1) наличие команды exit, завершающей выполнение функционального процесса; 2) наличие команды wait, приводящей к задержке процесса на некоторый интервал времени; 3) выход из цикла может осуществляться либо по команде break, либо в случае ложности значений всех булевских выражений, являющихся защитами альтернативной команды цикла. Кроме того, в АФС имеется параллельная команд (РАН), отсутствующая в базисном языке, а взаимодействие в языке АФС осуществляется через каналы связи. Все это влечет необходимость расширения соответствующих семантических областей и модификации оператора з.

Множества spath, Proc и test, введенные ранее, расширим следующим образом:

:= ... I со I EXIT I BREAK | TIME = ... ¡ EXIT I BREAK I TIME | p1 11 p2 := ... I TIME

где многоточие означает в точности все конструкции, определенные ранее; со - успешное завершение ветви параллельной команды; exit, break и time - семантические значения команд exit, break и wait, соответственно; р1 я р2 - параллельная композиция процессов р1 и р2, определяемая как смешивание процессов р1 и р..

Определим р через цр(р), где р(р) имеет вид:

зр

Р t

- 27 -Р (р) = Xq . p-q + V . Выражения р и v в этом операторе отличаются от соответствующих выражений для базисного языка. Прежде чем определить р и v, введем два вспомогательных определения. Определение. ВП зр называется прерываемой и обозначается через BR, возможно с индексом, если:

1) зр S BREAK; 3) зр = sp^BR;

2) зр = BR-sp1; 4) зр = tABR.

Определение. Головная часть прерываемой вычислительной последовательности BR, обозначаемая через head (BR), определяется следующим образом: 1 ) если BR з BREAK, то head (BR) = i;

2) если BR = BR1•зр, то head (BR) = head (BR1)I

3) если BR = tABR1, то head (BR) = t Л head (BR.,);

4) если br = sp-br1 и зр не является прерываемой, вп то head (br) = зр • head (br1).

Выражение р определим теперь как:

Р = р \ { е + Е BR. } , i « n 1

где е BR - множество всех прерываемых ВП, входящих в р.

i е n 1

Выражение v определим следующим образом: v = v' + v",

LOOP, если e « p;

где v'~ E head (BR.), v" =

i«n

i, если p = E В.Л p,;

i « N X

пусто, в остальных случаях.

Значение V характеризует завершение цикла по командам break. Значение v" характеризует три возможные ситуации выполнения цикла: 1) зацикливание в случае наличия в цикле альтернатив, не приводящих к каким-либо действиям; 2) выход из цикла, если все защиты являются булевскими выражениями, ни одно из которых не является истинным; 3) продолжение выполнения цикла, либо ожидание ввода/вывода.

С учетом отличий языка АФС переопределены функция с : cmd -» Proо для команд функционального процесса и функция е : Ехр test для выражений, задающие их априорную семантику. Априорную семантику функциональных процессов г : РРгос -» Ргос, где РРгос - множество функциональных процессов с типичным элементом гproс, определим как:

Г ¡FUN i::cl = С |о] • pO , Априорная семантика кэналов связи определяется семантической функцией к : сап Proо. к ICHAN J:: type1(k) : type (1)1 = = ((type1 (IN'''1 , .... IN3 )) • (type2 (OUT'''1 , OUT3'1)))4

Параметр type может принимать одно из двух значений: Abb

или ANY. Конструкции вида type (Х1, Х2.....хп) определяются

как:

ALL ( X,, Х0, .... X ) = X • сО 11 X -сО 11 ... Я X .00 12 и 1 г п

ANY ( X,, Х„.....X ) = X •сО + X «сО + ... + X -сО .

12 il 1 2 11

Семантическая функция АСС-программы tP:Prog ^(CPath) определяется с помощью связывающего оператора ж. Пусть рг = NET can1; oarig; ...; oanm

BEGIN iproc1; fproc2; ...; fprocn END.

Тогда P IprJ = 3 ( к Ioan1 J, к Ioan2J.....к IcanJ,

f" lfproo.,1, IF |fprOC2l.....OF IiprOOnl )

Поскольку семантические значения к foanl и ¡г irproci

тхотгаоппл^оф amirm и тлй жя оппяпти. имяйм:

Р 1рг1 =3 ( р2.....ри, рп+1, рт+2.....рт+п ),

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

Далее в главе 3 определен связывающий оператор ж, осуществляющий построение семантического значения АФС-программы.

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

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

Предложен блочный принцип описания свойств семантических объектов, позволявдий посредством расширения или сокращения количества блоков аксиом и правил вывода адаптировать

В качестве базисного языка распределенного программирования задан язык ъ, представляющий собой расширение базисного языка, описвнного в главе 3, посредством введения в него операций параллельной композиции команд и процессов.

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

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

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

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

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

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

Доказана зквациональная характеризуемость семантических

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

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

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

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

Априорная семантика процессов задается функцией с:Ргос 9 -» SP0 , где Э - множество функций с типичным элементом р, задающих среду вычисления. Под средой вычисления для подмножества компонентов Р программы понимается множество меток процессов, являющихся внешними по отношению к компонентам программы, входящих в Р. Множество spct отличается от ранее введенного множества sp = ^(CPath) тем, что все элементы этого множества, обозначаемые по аналогии с элементами множества sp через ара, имеют дополнительный параметр о « ^(РЪаь), характеризующий ореду вычисления элемента sp, и определяемый функцией р.

Ключевыми пунктами семантического определения являются

определения значений циклических и параллельных конструкций. В

•сачестве значения цикла с I*[go]lp берется (С1вс!р)+,где

значение зр+ есть минимальная фиксированная точка оператора

•Чзр) вида: F(sp) = Xq.sp«q + v ,

Г зр, если е в зр, г loop, если е « sp,

где: sp = j v = \

(. sp\e, если е « зр, t д» если в « зр,

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

Значение параллельной конструкции определяется как: с lpr1 иргг1р = с Ipi^lp II с 1ргг1р, 'де операция параллельной композиции "»", стоящая в правой [асти, определена на семантической области SPa. Введенная шерацйя параллельной композиции позволяет строить априорные ;емантические значения программ на основе вприорных ¡емантических значений компонентов этой программы.

Далее, в главе 4, приведены блоки аксиом, характеризующие ¡войства операций "•", "+", операций параллельной

юмпозиции, операций абстракции и инкапсуляции.

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

В этой главе мы доказали также, что для любого элемента pa е бр0 существует представление его в виде конечной системы

равенств вида:

Р1 = Е а • Р + Е Р1кл Р1к + б (Р ) . (*)

1 3 е N 13 к е N 1К 1

где: N={1,2, ..., п }; зра г р1 ; для любого 1 (1 < 1 < п) Р,, Р2.....Рп е БРа ; VI УЗ 31 е N. что Р^ = Р2 и

У1 Ук Зг € N. что Р„. = Р ;

1к г

а±3 и р1к - специальным образом определенные префиксы; б (Р1) - сумма простейших (атомарных) действий.

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

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

Доказана корректность предложенного семантического метода, т.е. доказано, что система рекурсивных равенств (*) имеет решение. Для этой цели мы ввели оператор Ф = ^<Р1.Ра.....Р>-< Е а • Р + Е Р1к + б (Р ),

п е N к е N К

• • * I

Е + Е ^ Рпк + 6 <Рп»

;) е N пл к « N ™ ^

Оператор

Ф : ^(СРаШ) X ... X '(СРа«1) - ^(СРа^) X ••• X ^(СРа№) задает пошаговое применение одновременной подстановки аппроксимаций множеств ВП Р,, Р2, ..., Р , получаемых на

предыдущем шаге в оператор Ф вместо аргументов Р1, Р£.....р ,

Вводя метрику <1 на областях СРаШ, ^(СРаШ) и метрику а на области Б = з> ( CPath ) х • • • X ^ ( СРаШ ), мы доказали следующие результаты:

Лемма . Пространство (Б, 5) является полным метрическим пространством.

Лемма. Отображение ® метрического пространства и = (Б, й) в себя является сжимающим отображением. Лемма, Ф - непрерывный оператор, т.е. для всех сходящихся последовательностей <хк>к имеет место

lim ffl ( iL ) = Ф ( lim TL ) . к к

Теорема. Оператор ®:S s, где s = r(cPath)x.. .x^(cPath),

имеет минимальную фиксированную точку.

Эта теорема завершает доказательство корректности

предложенного семантического метода.

Еще одним важным как с теоретической, так и с практической

точки зрения, результатом главы 4 является разработка

конструктивного метода сравнения систем рекурсивных равенств,

позволяющего дать ответ на вопрос об эквивалентности схем

программ в языке L. Кроме того, предложенный метод позволяет

осуществлять сравнение программ с точки зрения их

асинхронности, что позволяет часто повысить быстродействие

выполнения программ за счет более эффективного использования

оборудования ВС.

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

Вначале мы расширили множество защит G определенного в предыдущей главе языка Ь, добавив в него защиты, содержащие одновременно булевские выражения и команды ввода/вывода: g ::= 1 | rw I 1 & rw 1 ::= tt I il I b rw ::= in I out В остальном синтаксис языка остается без изменения.

Очевидно, что для задания семантики расширенного языка L необходимо ввести дополнения в множество тестов test: t ::= Ь I rw I [I^ * [lg *]] rw l ::= t i p i в rw ::= in i out | j Единственным отличием при представлении семантических значений программ без циклов в виде системы равенств является появление в качестве элементов ВП конструкций вида l#rw и i1*l2*rw. Кроме того, при построении систем равенств дополни-

тельно применяются аксиомы, описывающие свойства операции "*"

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

Следующим шагом при построении модели языка csp из построенной нами модели языка распределенного npoiраммирования является удаление из синтаксиса языка защит, содержащих команды вывода ( out .). Очевидно, что в этом случае не требуется никаких изменений в разработанную выше семантическую теорию для анализа схем программ в языке CSP.

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

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

Семантическая функция для функциональных процессов FiFproc -» SP определяется как:

!F Ifproc.,; fprocgl = ff" liproc.,! « г Hiproof F-IFUN i::c! = с Jcl , где c:cmd - SP есть функция, сопоставляющая командам языка АФС множества ВП.

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

Семантическая функция для АФС-програлл имеет вид:

P: Prog SP. Для программ, не содержащих команды exit, разработанная в главе 4 алгебраическая система и метода построения семантического значения могут быть непосредственно применены для построения семантического значения АФС-программы с учетом особенностей завершения циклов в ней. Так, например, если АФС-программа имеет вид:

рг = NET сап1; сап2; ___; canm

begin fproc1; Хргос2; ...; iprocn end , то !P Ирг! = К Лсагц J и к Icar^l н ... и к |canmI и

if frproc^ и if [fprocgl и ... n if ||fprocnI Введение аксиом, характеризующих свойства элемента exit, сопоставляемого команде exit языка АФС, и применение операции абстракции позволяет задать значение АФС-программы рг в общем случае следующим образом:

р IprJ = к lean.,! п к Jcaiigl н ... и к JcanmJ и

II ABSexit(IF4FUN i1::cl 1) я ... И ABS^^ (IF • |FUN i : :c± 1 ) ,

1 n

где функция if ' определяет выражение, характеризующее семантическое значение функционального процесса fun i::с±, т.е. f J fun i::c1J, приведенное к виду Е X1;J- EXIT, где не

J е N

содержит элементов EXIT.

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

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

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

IF : Prog S -» T (CPath X S), где s - множество состояний каналов АФС-программ, и определяется следующим образом:

Р !prj0° = Comp ( г Jiprocl )о° ,

где о0 ~ начальное состояние каналов АФС-программы рг. Функция Comp вида spxs -» spxs осуществляет вычисление множества ВП, характеризующих АФС-программу, исходя из априорного множества ВП if IfprocI, полученного без учета состояний каналов, и начального состояния каналов этой программы. Функция Comp напоминает действие оператора связывания г в главе 3.

выводы по работе

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

а) посредством композиции функций;

б) на основе информационной подчиненности компонентов программы;

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

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

2. Построены две формальные системы ( PS и FS1 ), предназначенные для анализа функциональных схем. Доказана разрешимость проблемы эквивалентности для подкласса циклических функциональных схем, характеризуемого, с точки зрения схематологии, как класс регулярных схем, расширенный операцией параллельной композиции (*).

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

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

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

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

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

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

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

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

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

11. Разработанные системы распределенного программирования, семантические модели и методы анализа распределенных систем реализованы в НИР и внедрены на ряде предприятий

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

работах:

1. Кораблин Ю.П., Кутепов В.П., Фальк В.Н. Исчисление функциональных схем // Цифровая вычислительная техника и программирование: Сов. Радио.- 1974.- И 8. - С. 8-15.

2. Кутепов В.П., Кораблин Ю.П. Язык граф-схем параллельных алгоритмов // Программирование.- 1978.- Ji 1.- С .3-11.

3. Korablin Yu.P. Deciding equivalence of functional schemes for parallel programs // Mathematical Centre.- Reseach Report IW 200/82.- Amsterdam.- 1982.- 33 p.

4. Арефьев А.А., Кораблин Ю.П., Кутепов В.П. Язык граф-схем параллельных алгоритмов и его расширения // Программирование.- 1981.- J* 4.- С. 14-25.

5. Кораблин Ю.П. Проблема корректности граф-схем параллельных алгоритмов // Программирование.- 1978.- Я 5.- С. 45-52.

6. Кораблин Ю.П., Налитов С.Д. Язык асинхронных функциональных схем - концепция распределенного программирования // Программирование.- 1989.- № 6.- с. 35-45.

7. Кораблин Ю.П., Налитов С.Д. Событийная семантика схем программ языка взаимодействующих последовательных процессов // Программирование.- 1993.- $ 3.- С. 48-61.

8. Кораблин Ю.П., Кутепов В.П., Фальк В.Н. Об одном аксиоматическом подходе к проблеме эквивалентных преобразований рекурсивных функциональных схем алгоритмов // Тр. ин-та / Моск. энерг. ин-т.- 1975.- Вып. 247.- С. 90-96.

9. Кораблин Ю.П. Языки параллельных алгоритмов и принципы их реализации: Автореф. дис. на соиск. уч. ст. канд. техн. наук.- М., 1977.- 20 с.

10. Кораблин Ю.П. Семантика языков программирования. - М.: Моск. энерг. ин-т, 1992.- 100 с.

11. Кораблин Ю.П. Программирование на языке граф-схем параллельных алгоритмов: Лабораторные работы по курсу "Структуры вычислительных машин и систем".- М.:МЭИ, 1983.- С.15-29.

12. Кораблин Ю.П., Кутепов В.П., Волочков Н.Ф. Диспетчер параллельных алгоритмов для систем М-6000/М-7000. / Программное обеспечение М-6000 АСВТ, 3008.ООО.С, НИИУВМ,-

Северодонецк.- 1976.

13. Кораблин Ю.П. Функциональное программирование для параллельных вычислительных систем // Параллельная и распределенная обработка информации / Под ред. В.П. Кутепова.-М.: Моск. энерг. ин-т, 1989.- С. 3-13.

14. Кораблин Ю.П., Кутепов В.П., Тиц П.Г. Вопросы реализации параллельных алгоритмов на вычислительных системах // Программирование.- 1975.- $ 2.- С. 3-10.

15. Кораблин Ю.П., Кутепов В.П., Строева Т.М., Фальк В.Н. Языки параллельных алгоритмов и вопросы их реализации на многомашинных комплексах // Тезисы докладов Республиканской научно-техническая конференция по вопросам разработки и внедрения средств ВТ и УВК в народное хозяйство.- Тбилиси, 1977.- С. 42-44.

16. Кораблин Ю.П.., Кутепов В.П. Реализация языка граф-схем параллельных алгоритмов на системах вычислительных машин // Тр. ин-та / Моск. энерг. ин-т.- 1980.- Вып.469.- С.123-131.

17. Арефьев А.А., Кораблин Ю.П. Вопросы реализации языка граф-схем параллельных алгоритмов на системах машин: Межвузовский сборник научных трудов "Прикладная математика и математическое обеспечение ЭВМ" / под ред. Н.А. Криницкого.-М.- 1982.- С. 43-52.

18. Волочков Н.Ф., Кораблин Ю.П., Кутепов В.П. Организация параллельной обработки информации на многомашинных и многопроцессорных комплексах // Проектирование и создание многомашинных и многопроцессорных систем для АСУ народного хозяйства.- И.: МДНТП им. Дзержинского, 1984.

19. Кораблин Ю.П., Кроввиди Р., Налитов С.Д. Реализация параллельных вычислений на многомашинных вычислительных комплексах мини- и микро-ЭВМ //Тр. ин-та / Моск. энерг. ин-т.- 1986.- Вып. 86.- С. 21-29.

20. Кораблин Ю.П., Волочков Н.Ф. Асинхронные функциональные схемы: концепция языка распределенной обработки информации // Логическое управление в промышленности: Тез. докл. IX Всесоюзного симпозиума.- Ташкент, 1986.- С. 247-249.

21. Кораблин Ю.П., Налитов С.Д., Волочков Н.Ф. Язык асинхронных функциональных схем - концепция распределенного программирования // VI Всесоюзный симпозиум по модульным ИБС: Тез. докл.- Вильнюс, 1987.- С. 82-84.

22. Кораблин Ю.П., Налитов С.Д. Распределенное программирование для локальных сетей / Параллельное программирование и высокопроизводительные структуры: Тез. докл. VIII Всесоюз. семинара.- Киев, 1988.- С. 73-74.

23. Кораблин Ю.П., Налитов С.Д. Применение языка асинхронных функциональных схем для моделирования распределенных систем // Параллельное программирование и высокопроизводительные структуры: Тезисы докладов VIII Всесоюзного семинара.- Киев, 1988.- С. 75-76.

24. Кораблин Ю.П., Налитов С.Д. Эквивалентность схем программ в языках распределенного программирования //Параллельное программирование и высокопроизводительные системы: методы представления знаний в информационных технологиях: Тез. докл. X Всесоюзного семинара.- Уфа, 1990.- С. 23-24.

25. Кораблин Ю.П., Налитов С.Д. Денотационная семантика языков распределенного программирования, построенных на основе механизма передачи сообщений J/ Параллельное программирование и высокопроизводительные системы: методы представления знаний в информационных технологиях: Тез. докл. х Всесоюзного семинара.- Уфа, 1990.- С. 25-26.

26. Кораблин Ю.П., Налитов С.Д. Программирование на языке асинхронных функциональных схем // Параллельная и распределенная обработка информации / Под ред. В.П. Кутепова.-М.: Моск. энерг. ин-т, 1989.- С. 14-38.

27. Кораблин Ю.П. Распределенные вычисления - М.: Моск. энерг. ин-т, 1989.- 67 с.

Подписано к печати Л— 1лл Лл л

_Тираж 400 Лмя

Типография М.-)Ц. Крпспокцзърщитяп, М