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

ЛЕНИНГРАДСКИЙ ОРДЕНА ЛЕНИНА ПОЛИТЕХНИЧЕСКИЙ ИНСТИТУТ имени М. И. КАЛИНИНА

На правах рукописи КАРПОВ Юрий Глебович

УДК 681.324:519.681

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

Специальность 05.13.13 — вычислительные машины, комплексы, системы и сети

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

ЛЕНИНГРАД 1990

Работа выполнена в Ленинградском ордена Ленина .политехническом институте имени М. И. 'Калинина на «эфедре информационных и управляющих систем.

Официальные оппоненты — доктор технических наук, ¡профессор Д. А. Поспелов, доктор технических ¡наук, трофее сор В. Е. Котов, доктор технических иаук, 'Профессор Ю. М. Смирнов.

Ведущая организация — Институт Проблем ¡Утравлени* АН ООСР (Москва).

Защита состоится «. . .»....... 1990 г. в . . . часоЕ

на заседании специализированного совета Д 063.38.04 в Ле-■нинррадскам ордена Ленина политехническом 'институте имени М. И. (Калинина (191251, Ленинград, Политехническая ул., 29, корпус . . . , ауд.....).

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

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

Ученый секретарь опециал'изирешамното совет; кандидат технических наук, доцент Дурандин К. П.

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

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

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

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

Решение проблемы связано с разработкой теорий параллелизма, исследованием моделей параллельных процессов, позволяющих на твердой формальной основе проверять отсутствие нежелательных свойств разрабатываемой программной системы и гарантировать наличие у нее требуемых свойств. К настоящему времени в этом направлении уже проведена значительная работа. Исследования Э.Дейкстры, Ч.Хоара, К.Петри, Р.Милнера,

I

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

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

Тема работы согласуется с направлениями исследований, проводимых в области информатики как за рубежом, так и в нашей стране. Так, одним из направлений, поддерживаемых Европейской стратегической npo-'J грэммой в области информационной технологии ESPRIT , является разработка технологии параллельного программирования. Национальная программа США ÔTARS "Стратегическая компьютерная инициатива" одной из главных целей ставит повышение производительности труда программистов и надежности программного продукта при разработке встроенных систем управления на параллельных и децентрализованных распределенных вычислительных архитектурах. В нашей стране аналогичные направления исследований поддерживаются общесоюзными программами НИР All СССР (в частности, комплексной целевой программой I.1.6 "Развитие технологии разработки и промышленного производства программных средств вычислительной техники") и ГКНТ СССР ^в частности, общесоюзной программой 0.16.10 "Создание автоматизированных производств", куда входит проблема "Разработка методов синтеза локальных вычислительных сетей низкого уровня с применением микроЭВМ"). 2 ° о

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

Для достижения этой цели в работе решались следующие задачи:

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

- построение методов анализа свойства когерентности заданной совокупности взаимодействующих активностей и конструктивной методики синтеза таких активностей, согласованно реализующих требуемое поведете;

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

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

Научная новизна работ;; заключается в следующем:

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

2. Проведено теоретическое обобщение в области параллельных процессов, в результате которого построены:

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

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

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

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

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

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

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

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

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

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

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

газированном в работе, позволило гарантировать отсутствие структурных ошибок в сложном комплексе программ АСИ;

2. В ОКБ "ИМПУЛЬС" при разработке систем управления специального назначения были использованы метод спецификации процессов л анализ их структурной согласованности, что позволило сократить сроки проектирования и повысить качество - разработки;

3. В Физико-техническом институте им.А.Ф.Иоффе при построении транспортной станции в стандарте ЕСМА-72 для локальной сети управления физическим экспериментом была использована предлагаемая в работе методика проектирования протоколов и программный комплекс СПРУТ для проверки когерентности системы процессов, специфицированных на этапе логического проектирования. Это позволило существенно сократить сроки проектирования и избавиться от логических ошибок на ранней стадии разработки;

4. В ОКБ "Радуга" на основе предлагаемого в диссертации подхода решен ряд задач создания технологии параллельного программирования для автоматизации разработки протоколов.

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

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

Апробация работы. Основные результаты докладывались более, чем на 40 конференциях и семинарах в НИИ, Вузах и КБ, э той числе на:

а) Международных семинарах и конференциях: конференции ученых ' соц.стран "Локальные вычислительные сети", Рига, 1985; Совместном советско-итальянском семинар© "Сети пакетной коммутации ЭВМ: архитекту-

5

pa сетей и теория протоколов", Ленинград, 1389; международном семинаре "Формальные модели параллельных вычислений", Телави, 1989;

б) Всесоюзных семинарах и конференциях: "Вычислительные сети коммутации пакетов" КСШАК'83, '85, '87, Рига; "Локальные вычислительные сети", ЛОКСЕТЬ'88, Рига; "Координация и декомпозиция в сложных системах", Челябинск, 1986; "Проблемы совершенствования синтеза, тестирования, верификации и отладки программ", Рига, 1986; "Технология программирования", Киев, 1986; "Формальные модели параллельных вычислений", Новосибирск, 1987; "Однородные вычислительные системы и систолические структуры", ОССС'88, Звенигород; "Параллельное программирование и высокопроизводительные системы", Алушта, 1988 и др.;

в) Постоянно действующих семинарах: "Управление на сетях связи", ЙППИ АН СССР, рук.Лазарев В.Г.; "Теория автоматов", НТО РЭС им.А.С.Попова, Ленинград, рук.Варшавский В.И.; "Теоретическое программирование", ВЦ СО АН СССР, рук.Котов D.E.; "Проблемы искусственного интеллекта", ВЦ АН СССР, рук.Поспелов Д.А.; "Многопроцессорные ВС", ВЦ СО АН СССР, рук.Миренков H.H.; "Программология и ее применение", КГУ, рук.Родько В.Н.; "Информационные проблемы вычислительных сетей", НСК АН СССР, рук.Самойленко С.И. и др.;•

г) Семинарах НИИ, Вузов и КБ: ИЭВТ АН Латв.ССР, рук.Кикутс А.Я., Куцевалов Д.В.; ИПУ АН СССР, рук.Юдицкий С.А.; ИПМ АН СССР, рук.Илюшин А.И.; НПО "Красная заря", рук.Колпаков В.В.; ЛЭТИ, каф.АСОИУ, рук. Советов Б.Я.; ЦНИИ Робототехнических комплексов, рук.Половко A.A.;

ИК АН УССР, рук.Вельбицкий И.В., Цейтлин Г.Е., Ющенко Е.Л. и др.

Публикации. По материалам диссертации опубликовано 35 печатных работ.

Структура и объем работы. Диссертация состоит из введения, шести разделов, заключения и приложений. Основное содержание составляет 359 страниц, в том числе 63 рисунка.

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

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

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

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

В п.1.2 приводится ряд некорректных программ из различных областей параллельного программирования. Первая из них является Совокупностью процессов, управляющих участком гибкой производственной системы. Система состоит из параллельно работающих агрегата, выполняющего обработку и сборку деталей из заготовок, и двух транспортных роботов. Каждый из трех управлящих алгоритмов этой системы очень прост, определен корректно, и при подходящем функционировании остальных в его выполнении никаких неожиданностей не возникнет. Однако, совместная спецификация этих алгоритмов некорректна: возможна блокировка системы, в результате которой работа всех агрегатов прекращается: все они находятся в обоюдном ожидании. Существуют методы, с помощью которых можно обнаружить возможность блокировки по текстам алгоритмов: строится и анализируется дерево глобальных достижимых состояний системы алгоритмов/ Для данного примера необходимо анализировать граф, содержащий 195 вершш. Анализ этого примера предложенным в работе методом достаточно прост; он проводится вручную в разд.З.

Другой пример - классическая задача о пяти обедающих философах Э.Дейкстры. На сложность ее анализа указывали многие исследователи. Сложность эта проистекает из огромной размерности дерева достижимых состояний системы процессов: она растет экспоненциально с числом процессов. Ч.Хоар дал оценку этой размерности. Общее число траекторий поведения системы на дереве достижимых глобальных состояний, которые 'нужно проверить при анализе, превышает 21'8 ылн. "Весьма маловероятно, что компьютер когда-нибудь сумеет исследовать все возможные случаи" - заключает Хоар. Представленным в работе методом анализ этой системы проводится вручную в разд.З. Сложность ее анализа растет линейно с росто:,: числа процессов.

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

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

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

Дальнейший пример - протокол передачи данных THE канального уровня, предложенный на Международной конференции по вычислительным сетям ICCC'78 как пример корректного протокола, верифицированного с помощью автоматизированной систеш APPROVER. Однако, понятия "верификация" и "корректность" в области разработки протоколов нуждаются в уточнении. Список "свойств корректности", включающий упоминаемые в различных публикациях желательные свойства протоколов, содержит более полугора десятка таких свойств. В связи с этим, протокол, проверенный например, на отсутствие дедяоков, может иметь ливлоки или зацикливания. Более того, упомянутый список является открытым, поэтому верификация протоколов в соответствии с ним не дает гарантии реальной правильности. Использование разработанных методов показало, что протокол THE некорректен. При редких сочетаниях условий он попадает в ситуацию "пробуксовки", не обнаруженную системой APPROVER: оба параллельных объекта посылают друг другу повторяющиеся сообщения, отвергаемые на' приемном конце. Программы "не понимают", друг друга, и дальнейшая производительная работа протокола прекращается. Результаты анализа этого протокола представлены в разд.5.

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

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

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

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

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

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

П.1.4 объясняет логику построения работы по 'разделам.

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

9

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

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

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

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

В п.2.I последовательный процесс формально определен аналогично операционной семантике Г.Плоткина помеченной системой переходов М = = (S , St , A,R) с множествами состояний <S и действий А, начальным состоянием и отношением перехода RSS-* . Символ Т.

означает внутренний переход в процессе, а используется для терминальных состояний. Описание динамики процесса - его поведения -также дано в терминах помеченной системы переходов. Вычислительной историей процесса М названа шестерка Иц = (Р, Т, Р А),где

Р и Т - конечные множества реализаций состояний и действий,^ РхТО ТхР - отношение причинной зависимости, PuT-*-S UA ставит в соответствие катдой реализации состояния или действия его оригинал. История последовательного процесса является, фактически, согыо-процессом Петри, все элементы которой линейно упорядочены. Элемент <г б Pl)T истории К. будем представлять парой <ord (х)> , где Ord (х) есть число таких элементов, предшествующих 5С. в отношении F* .которые являются реализация!® элемента ^-(х).

Основной целью раздела является введение модели, позволяющей задать произвольный процесс (в тем числе а параллельный) множеством всех историй его поведения. Обозначим множество историй М. При естественна.! определении отношения частичной упорядоченности; на Бдо и понятия префикса истории, % является црефзгасно-зашснугш. Это множество задает процесс Рц, состояниями которого являются истории процесса М. Этот новый процесс является разверткой исходного процесса. Рц сильно эквивалентен исходному процессу И, его анализ на слезнее анализа процесса М. Гра^гческя Ри представляется' деревом, изоморфным дереву историй процесса Ц. Подобное дерево Р.Ившерои названо деревом поведений процесса М.

В п.2.2 рассматриваются партдгурн - модель для задания поведения параллельных процессов. Мк используем здесь примитив синхронного взаимодействия (рандеву). Параллельные вычисления совокупности процессов состоят в том, что каждый процесс функционирует независимо и асинхронно за исключением выполнения действий, общих, с действиями какого-либо о другого процесса: такие действия определят одковреигавый неделимый переход обоих процессов, если оба готовы выполнить это действие. Партитура строится в соответствии с предЕЮиюявштем» лежащий в основе семантики максимального параллелизма А.Салшщкаго и Т.Малдера: каждый процесс функционируаг на своей процессоре. Партитурой будда зазывать детерминированную сонаестиув истории процессов, пградетавЕеадуы в виде, аналогичном О-сетз Петря, мэста которой ссотеетствуэт реализациям coll

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

Для формализации понятия партитуры введем определение полуслова {ЗМ^РС,«*,^,^) как помоченного частичного порядка с дополнительным требованием /ух^еХ):]"-^)3^)^^^ . Как и развертки последовательных процессов, полуслова представляются в канонической форме, отождествляющей все изоморфные объекты. Пусть для двух полуслов •

Б^ОО.,-;,/*;.,5^), и= 1,2 множества и ^г^А^д

совпадают. Для таких полуслов введем отношение с "менее упорядочено, чем": Ессли^, на этих множествах. Эти полуслова будем считать согласованными, если отношения и -г на этих множествах не противоречат друг другу, т.е.^усс^еХ^Х^сс.^^-Л^х

Разделим % на пару множеств: множество состояний $ и множество действий А. Множество X также разобьем на множество Р условий (реализаций состояний) и множество Г событий (реализаций действий). В отношение частичной упорядоченности внесем ограничение: отношением непосредственной упорядоченности могут быть связаны только элементы различных множеств (как и в сетях Петри, событие может выполниться после наступления соответствующих условий и вызвать наступление новых условий). Такая структура будет рассматриваться как партитура - 'одна из возможных историй параллельной системы.. Определение. Партитурой назовем такое полуслово (X ,ух что:

. частичный'

порядок 4 представлен бинарным отношением ~~~г , структура которого такова: а) Р^Р*ТиТхР 1 б)(нреР): л1'ри {;

Партитуру будем записывать как шестерку П = (Рп .Т,,,^ ._рп.$п>Ат)- Две партитуры П< и Па будем называть согласованными, если согласованы полуслова П, У Ат и П^А^« Аналогично, будем считать П^П*. если ГЦА^ЕП^Апг. (здесь'

ША означает ограничение партитуры П на . всех реализациях элементов из множества ■ А).

Из определения партитуры следует, что партитура является частным случаем 0-сети Петри. На множестве партитур в работе определены две алгебраические операции: параллельная композиция и конкатенация, а также отношение частичного порядка. Множество й£ партитур будем называть процессом, если оно префиксно замкнуто и возможные продолжения любой пар^туры из я£ однозначно зависят от ее максимального среза.

С помощью модели партитур удобно описать динамику совокупности 12 °

последовательных взаимодействующих процессов. Каждый элемент 3:6 У1Л партитуры является реализацией состояния или действия ул (х) одного из компонентных процессов, а отношение инцидентности Р является реализацией переходов процессов. Множество всех партитур ЗСм. совокупности Л = {И1)...,МП_\ последовательных процессов, очевидно, является процессом, задающим параллельное поведение процессов тЛ, и его можно принять за определение результата операции параллельной композиции процессов.

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

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

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

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

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

13

боте показано, что к этой задаче полиномиально сводится Я? -полная задача 3-выполнимости, откуда следует вывод о том, что задача построения дерева партитур не менее сложна, чем любая-А/Р -полная задача.

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

В третьем разделе свойство когерентности формализуется дня модели партитур. Свойства, аналогичные когерентности, рассматривались и ранее для других моделей параллельных систем. В.Е.Котов л Л.Л.Черкасова ввели свойство U-шготности дая сетей Петри, Е.Бест рассмотрел свойство адекватности для траекторных программ, П.Лауэр и М.Шилдис использовали свойство адекватности для программ на языке COSY-

На множестве Дл. всех партитур совокупности по-

следовательных процессов определим отношение J>-u . Две партитуры связаны этим отношением, если у них совпадают минимальные префиксы, содержаще реализации состояния процесса Mi. , входящие в заключительный срез партитур. Это отношение является эквивалентностью. Проекцию ММ;, параллельной композиции К=\М,1\-Мл представленной множеством., партитур , на компонентный процесс Л построит,! следующим образом. Множеством состояний процесса MVMi будем считать систему классов эквивалентности J\ на ¿Kit. Алфавит

действий этого процесса совпадает о алфавитом действий Н;, а отношение перехода определяется следующим образом. Переходы между состояшш® Ш3-и и [П'3'v. под воздействием элементов из A-L индуцируются соответствующими переходами между состояниями П и Л1 параллельной композиции процессов М. Переход [П]-—»-Ш1;. включается в 0L-U , если все партитуры, префиксом которых является П, находятся с П в одном классе эквивалентности j>L : так отражается возможность для процесса MVMv бесконечно долгого нахождения в состоянии Dili.. Определение. Совокупность последовательных процессов {М^...назовем Ht-когерентной, если процесс КM.L строго эквивалентен процессу Hi • Если совокупность процессов когерентна для всех Mto , то ее будем называть просто когерентной.

Проверка когерентности совокупности процессов относительно неко-14 0

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

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

Исследованы также свойства, связанные с возможностью управления когерентной системой процессов подачей сигнала из внешнего окружения. Этим свойствам близко введенное У.Монтанари свойство проявляемое«! ( vi.ta.Uty ): процесс когда-нибудь выполнит наблюдаемое извне событие.

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

Алгоритм проверки когерентности состоит в том, что строится дерево партитур системы процессов и каждая реализация каждого состояния процесса Ни , когерентность которого остальной части системы нужно' проверить, сравнивается по реализованным возможностям поведения с возможностями поведения М;. в этом состоянии. Дерево достижимых состояний можно рассматривать как дерево партитур с нарушением единственного требования: общие префиксы ветвей в нем не объединены. На проверку когерентности это не влияет, но увеличивает время анализа.

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

15

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

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

Теорема. Пусть М- - множество процессов с графом связности и

Я ~ точка сочленения Сгц. , т.е. граф распадается на к.

несвязанных между собой графов Сгд,, » пРеД°тгзлялЩ1Х

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

Л,и{м\ ,лки{м\.

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

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

Параллельной композицией полусловназовем полуслово(ии(1ГХ1;(ии1 Я;,)* ^^А;), построенное объединением

всех компонентов исходного полуслова и транзитивным замыканием объединения их отношений частичного пбрядка. Если каждое из полуслов опи-»»

сывает поведение некоторой компоненты, то их параллельная композиция описывае? параллельное поведение этих компонентов. Множество полуслол 16

назовем когерентным, если как количества реализаций каждого события из объединенного алфавита, так и отношение их упорядоченности в каждом полуслове и в их параллельной композиции совпадают. Теорема. Если (' (р^ )АОI } множество когерентных полуслов, то их параллельная композиция является полусловом

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

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

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

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

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

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

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

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

17

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

Четвертый раздел посвящен рассмотрению систолических структур. Систолические структуры - построенные па СБИС специализированные матричные процессоры - состоят из большого числа простых процессорных элементов, связанных регулярным образом. Все элементы работают параллельно, обмениваясь данными ритмически под управлением глобального синхронизатора, упорядочивающего вычисления. Значительный практический интерес представляет проблема построения структур с асинхронным параллелизмом, при котором выполнение операций в каждом процессорном элементо управляется потоком данных или, более общо, событиями, происходящими в системе и внешней среде. Такие структуры были названы волновыми ( \^ал/е-£гоп£ ) матрицами. Существует ряд преимуществ использования асинхронного принципа управления в схемотехнике, они неоднократно обсуждались в литературе. Прежде всего, это отказ от глобальной системы синхронизации. Платой за эти преимущества является необходимость аппаратной поддержки свойства самосинхронизации и связанные с этим аппаратные затраты. Кроме того, проблема правильного выбора временных интервалов синхронизации и расчет периода подачи на входы реальных и нейтральных элементов заменяется проблемой корректного построения асинхронных вычислений. Это именно та проблема, которой посвящены предыдущие разделы работы; их результаты применяются здесь к анализу и синтезу волновых структур. •

В определенном смысле волновые структуры очень просты для анализа: каждый процесс выполняет цикл вычислений вида < ввод; операция; вывод> . Ни функция каждого процесса, ни значения вводимых данных не г :шют "образца поведения" (т.е. частичного порядка наступления событий) в каждом процессе и во всей системе в целом. Общий подход к анализу асинхронных процессов применить здесь, однако, невозможно: в общем случае такой анализ необходимо проводить для произвольного числа процессов.

В п.4.1 для нескольких опубликованных в литературе асинхронных алгоритмов на систолических структурах проведен анализ их когерентности с использованием модели партитур. Вместо с доказательством частично!'! корректности подобных алгоритмов доказательство их когерентности является составной частью методики верификации асинхронных систоли-18

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

В п.4.2. для стандартного описания поведения в систолических структурах каждого процессорного элемента вида: < ввод; операция; вывод > доказывается "теорема существования" - показывается, что любая систолическая структура может быть преобразована в волновую матрицу с асинхронными процессами, взаимодействующими по рандеву, при подходящей начальной установке этих процессов. Поведение всей.совокупности процессов при этом будет.когерентным. Рассматривается два примера такого преобразования: линейная структура для умножения ленточной матрицы на вектор и классическая гексагональная структура для умножения двух ленточных матриц. Систему можно сразу проектировать как волновую матрицу без предварительного построения систолической структуры. Для алгоритмов, заданных решетчатым графом зависимости данных - стандартным исходным пунктом распределения методик проектирования систолических структур - в п.4.3 предложен метод получения из такого графа волновой матрицы. Ограничения при построении волновой матрицы оказываются другими, чем в классических методах построения систолических структур, и в ряде случаев это позволяет выбирать более оптимальные проектные решения.

Пусть - направление проецирования-решетчатого графа (х~ (V, Е)) заданного на целочисленной решетке . Вектор 5 задает преобразование ^ , отображающее & в . является матрицей размерности (п~1)хп. с рангом П.-1 . При таком проецировании вершина графа О- с координатами т? проецируется в вершину и графа Ста с координатами П-Ь^т?.

Теорема. Пусть Ст^У.Е) _ решетчатый граф алгоритма А 7 я Н -его высота. Если направление проецирования § графа & удовлетворяет ; т0 при выб0_ ре подходящих алгоритмов процессоров и схемы их коммутации алгоритм А. реализуется на волновой матрице (3- за время Н. Иод терликом "время" реализации алгоритма на самосинхронной структуре в этой теореме понимается число шагов, на каждом из которых выполняются все операции, для которых готовы операнды. г

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

19

них алгоритмов.' Для первого примера - алгоритма пузырьковой сортировки, записанного на языке фортран, стандартным методом построен решетчатый граф и на основании теоремы построено несколько волновых структур. Только одна из этих структур, и не самая .лучшая, может быть синтезирована классическим методом Д.Ыолдована: в этом' методе не допускается выбор направления проецирования, ортогонального векторам зависимости данных. Другой пример - умножение ленточной матрицы на вектор. Выбор одного из возможных в соответствии с теоремой направлений проецирования дает ту же структуру, которая была построена в п.4.2 по систолической матрице. Необходимость начальной установки процессорных элементов волновой структуры имеет ряд неудобств; с помощью предложенного в работе приема, названного "надстройкой алгоритма", этих неудобств удается избежать за счет увеличения времени решения.

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

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

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

Вариант аппаратной реализации рандеву разработан соавторами совместной работы /19/ и приведен лишь для полноты картины. Критерием корректной работы схемы является свойство когерентности функциош!ро-вания всех ее элементов и узлов. Именно в участии в формальной верификации схемных решений заключается вклад автора в этой части.

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

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

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

21

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

Факторизация действий ввода/вывода при передача произвольного множества значений производятся так. Нусть осеЗ^ , где - выходной порт, а Dt*. - множество воэгложних значений, передаваемых по Л . Обозначим оС? (х | Р(х)) шоаесиво действий {ы.?(х)1Р(з}} ; будем обозначать оС?(х) множество действий d? (х | х € ) „ Если состояние, в которое переходит процесс после выполнения действия et?CxiPfx)) зависит от введенного значения, эту зависимость удобно представить

параметрически. Множество переходов {ft JRfr) I xelU & P(x) } будем

n dl^XlPW) n / v „ „

записывать как один переходЦ. —"-в линеикои записи,

как в СС£ : 0-=oL? (х |P(x)).R(x) . Альтернативные перехода в линейной записи будем соединять символом "+", например:

Q^rCxlPCxW-iKaJ^jlV^.ß^-rr.ai .

Аналогично факторизуются действия вэдачя информации по выходное порту. В общем случае некоторые перехода кигут быть допустимы не для всех состояний, факторизованных в оддаш фавгщмвдожестве. Это можно отразить с помощью предиката, приписанного к&тсдому переходу гак: <переход> : -<Условие> <Взаимодействие> < Новое состояние> . Такая структура в разд.6 будет использоваться для спецификации модулей параллельных систем, анализ которых можно провести на твердом фундаменте формальной теории асинхронных взаимодействующих процессов. В простых случаях такая система может быть представлена графически. Описанную выше фор-■му можно считать нормальной формой записи спецификаций на языке CSP с некоторыми расширениями. Формализация взаимодействия в этой специ- , (фикации может быть задана с помощью операционной семантики GC^.

Рассмотрим применение этой модели для спецификации и верификации протоколов канального уровня: протокола альтернирующего бита, прото-

<ола t\U- Y и протокола Линча. Для этих простых протоколов- верифика-дая может быть выполнена в рамках модели обобщенных асинхронных провесов путем объединения процессов в систему на основе семантики оператора параллельной композиции. Верификация каждого из протоколов оказалось гораздо более простой, чем известные из литературы доказательства. Например, публикация, посвященная верификации протокола AUV названа: "Простой протокол, который доказывается непросто". В работе штора /5/ показывается, что с помощью подходящей формализации провер-<а корректности этого протокола может быть значительно упрощена. Протокол Линча был верифицирован при найденной подходящей инициализации '15/, хотя ранее в литературе он был объявлен некорректным по причине >тсутствия такой инициализации.

Верификация более сложных протоколов'проводится с помощью модели гартитур. В п.5.2 показано, что свойство когерентности является фун-хаментальиым свойством корректного протокола: все структурные некорректности протоколов, обсуждаемые в литературе (их список содержит бо-хее десятка их видов) отсутствуют в когерентном протоколе. Традицион-1ая техника верификации протоколов обычно включает средства проверки ^которого подмножества этого списка по дереву достижимых глобальных зостояний протокола. Проверка когерентности с помощью дерева партитур выявила тонкую некорректность протокола THE - пробуксовку - не найден-1ую с помощью традиционной техники. Для этого протокола построен сце-гарий его работы, показывающий то редкое сочетание условий (относи-сельных скоростей протокольных объектов, задержек в каналах связи и возникновения ошибок в них),которое в реальных условиях работы может 1ривести к этой некорректной ситуации.

Анализ протоколов, включающих таГмауты, рассматривается в п.5.3. Цироко распространенная модель параллелизма на основе перестановочной земантяки не может отразить временные ^характеристики параллельных синем. Используя дополнительную информацию о времени выполнения отдель-шх действий в процессах, мы остаемся в рамках модели частичных порядив, анализ которой может быть выполнен с помощью дерева партитур. В заботе комбинируются два подхода к построению модели Временных сетей 1етри: подход П.Мерлина и Д.Фарбера и подход У.Зуберека. Дерево партитур системы процессов для анализа временных свойств протокола строит-зя Ъ учетом заданных задержек процессов .J? состояниях и длительности выполнения действий. Построение временного дерева партитур сводится, бактически, к событийному моделированию процессов. С помощью временной лоделй партитур оказалось возможным обнаружить некорректное поведение

23

протоколов при неправильном выборе таймаутов. В работе проанализирован протокол связи ЧПУ с центральной ЭВМ, который утвержден как межотраслевой стандарт двух министерств: Минприбора и Минстаикопрома СССР. Реализация этого протокола осуществлялась в ЛПИ им.М.И.Калинина при разработке Гибкой производственной системы механообработки. Было найдено несколько вариантов некорректного выбора значений таймаутов. Если тайгаут передатчика мал ("нетерпеливый передатчик"), то возможно дублирование пакетов, не обнаруживаемое приемником. Такая ситуация давно известна в теории протоколов; она вотречается при передаче ненумерованных пакетов и нумерованных квитанций. Гораздо менее очевидны другие найденные в этом протоколе аномалии, возникающие при неподходящем выборе значений таймаутов: разделение приемником одного непрерывного сеанса на несколько с потерей части пакетов и слияние нескольких последовательных сеансов приемником в один. В обоих случаях передатчик и приемник имеют разные мнения о результатах связи.

В п.5.4 показано, что свойство когерентности может использоваться не только для проверки структурной корректности протоколов, но и для полной верификации протокола - проверке правильности его внешнего поведения. Дусть S - частичный порядок. Обозначим Lin.CS) множество линейных порядков над элементами S , включающих & . Если П -партитура некоторого процесса M с алфавитом внешних событий А, го Цп(ГНк) представляет множество всех линейных упорядоченностей внешних событий, которые может допустить М. Языком, допускаемым параллельным процессом M с алфавитом внешних событий А назовем множество Lm =

Теорема. Дусть Ми// два процесса с совпадающими алфавитами внешних действий. Если M - последовательный процесс и множество {M } когерентно, то любая цепочка внешних событий, допускаемая М, принадлежит языку, допускаемому Я •

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

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

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

Аксиома. Любое событие использования или выдачи некоторой информации в каждом процессе должно причинно зависеть от события образования или приема этой информации.

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

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

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

25

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

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

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

Композициональная система верификации построена для варианта языка СБР, в котором используются статически определенные каналы взаимодействия, каждый из которых связывает два процесса. Для определения семантики операторов ввода/вывода используются историчсские вспомогательные переменные; для каждого процесса существует одна локальная такая переменная, которая хранит историю взаимодействия процесса с окружением.

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

В п.6.2 демонстрируется использование свойства когерентности для анализа и синтеза распрсдолонных программ. Проведен статический анализ

одного из известных алгоритмов распределенного завершения, в котором обнаружен ряд нетривиальных логических ошибок, допущенных разработчиками. Статический анализ состоит в проверке когерентности синхронизационного скелета распределенной программы. Такой синхронизационный скелет, абстрагируясь от функций преобразования данных в программе, отражает свойства, существенные для анализа параллельных программ: параллелизм, синхронизацию, недетермшшзм, взаимодействие. Такой статический анализ, при котором игнорируются булевы защиты альтернативных операторов и операторов цикла, может привести к обнаружению некорректностей, относящихся к совместно не реализуемым траектория,! отдельных подсистем. Поэтому для каждой найденной некорректности должен проводиться анализ значений локальных переменных и булевых защит с целью выяснения вопроса о тон, совместимы.ли траектории процессов, приводящие в некорректное глобальное состояние. Совместимость их свидетельствует о логической ошибке в nporpai.ir.ie. Несмотря на то, что публикация выбранного алгоритма распределенного завершения сопровождалась неформальным доказательством его корректности, анализ позволил определить несколько вариантов функционирования базового алгоритма, соотношения скоростей процессов и передачи информации по каналам, которые приводят к блокировкам распределенного алгоритма.

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

В п.6.3 рассматривается синтаксис для спецификации последовательных модуле]' параллельных программ. Во многих Моделях (в частности, в исчислении CCS Р.Миллера) описание «одуля указывает для каждого его состояния возможные взаимодействия с окружением по вход/выходным портач с приемом или передачей значений и далее определяет новые поведения, которые судет выполнять модуль, если взаимодействия по этим портам произошли. При большом числе возможных состояний более удобной представляется дуальная форма описания: для каждой альтернативы взаимодействия модуля указать множество состояний, для которых это взаимодействие допустимо, и оператор преобразования состояния'после взаимодействия. Та--:им образом, естественным'расширением обычно используемой в теории недеторминировашпк последовательных вычислений модели СЛ (Cancliiion-Actio п . условио-дойотвио) для систем взаииодейству»-

27

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

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

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

ЗАКЛЮЧЕНИЕ

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

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

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

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

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

2. Разработана методика логического проектирования протоколов связи, допускающая языковое и графическое представление систем взаимодействующих процессов и спецификации поведения процессов. Методика позволяет проводить анализ структурной корректности протоколов, семантической их корректности, а также оценку и выбор временных параметров протокольных объектов, гарантирующих корректное функционирование протоколов. В качестве примеров приведены полные доказательства корректности классического однобитового протокола и протокола;А 1ГУ, Существующие в литературе доказательства корректности этих протоколов значительно более сложны, чем приведенные в. диссертационной работе. На основе этой методики разработана транспортная станция в соответствии со стандартом ЕСМА-72. Разработка показала эффективность используемой методики.

3. Разработана программная система СПРУТ для проверки структур-

29

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

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

Метод проверки семантической корректности протоколов с учетом их временных характеристик позволил определить границы таймаутов корректного поведения протокола PA R ; о возможности некорректного поведения этого протокола не указывается в тех работах, в которых проводилась формальная верификация этого протокола. В протоколе, утвержденном Минприбором и Минстанкопромом СССР (Межотраслевой стандарт МУ-25-741--85) для распределенных сетей ГПС было обнаружено несколько вариантов некорректного выбора таймаутов.

4. Разработан метод синтеза протоколов из спецификации сервиса. Метод дает систематический способ построения протоколов, корректных

, построению. В качестве примеров построено несколько протоколов канального уровня (в том числе ряд новых, не опубликованных ранее протоколов). В частности, построен протокол ОiV3V ( являющийся, по-видимому, самым сложным протоколом, для которого проведена формальная верификация: доказательство его полной корректности, приведенное в литературе, в рамках модели CPA требует более 40 страниц выкладок, форт мулировки и доказательства более 30 теорем, утверждений, лемм. Метод синтеза, предложенный в работе, гарантирует корректность.полученного протокола при условии корректности спецификации erg, внешнего поведения, выраженного в требуемо;/.1 формализме частичных порядков событий. 30

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

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

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

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

ОСНОВНЫЕ ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Карпов й.Г. Согласованность систем параллельных информации!-. 1шх процессов// Известия АН СССР. Техническая кибернетика.- 1987.-№ 5.- C.I7S-I86.

2. Карпов Ю.Г. О свойстве когерентности протоколов// Автоматик', и вычислит.техника.- 1987,- 4.- С.З#-40.

3. Карпов Ю.Г. Партитуры - модель поведения параллельных взанмг действуящих процессов// ¿¿ормалыше модели параллельных вычислений.-Новосибирск, ВЦ СО АЛ СССР, 1£?08.- С. 136-150.

4. Карпов В.Г. Спецификация взаимодействующих процессов// Труды ЛШ.- 1986. 407.- С.22-26.

5. Карпов Ю.Г. Простой протокол, который доказывается просто// Автоматика и гичислит.техника,- 1987.- .'г*'..- С.22-30.

6. iia;>no:: 7,Т. !.'отод проекций в анализе протоколов: доказательство нокопрок: нести протокола "ГШ// Вычислительные соти коммутации

3.1

пакетов.- Рига: 1985, Ч.1.- С.181-185.

7. Карпов Ю.Г. Структурная корректность систем, построенных из взаимодействующих компонентов// Декомпозиция и координация в сложных системах.- Челябинск: 1986, ч.2.- С.18-19.

8. Карпов Ю.Г. Спецификация и верификация протоколов на основе ССS // Автоматика м вычислит.техника.- 1986.- К 6.- C.I8-25.

9. Карпов Ю.Г. Синхронизация параллельных систем с помощью управляющего модуля// Известия АН СССР. Техническая кибернетика.-1989.- JE 5.- С. 192-199.

10. Карпов Ю.Г. Статический анализ одного распределенного алгоритма// Автоматика и вычислит.техника.- 1989.- Г' I.- С.30-35.

11. Карпов Ю.Г. Синтез спецификации протокола из спецификации сервиса// Автоматика и вычислит.техника.- 1989.- И 4,- С.3-12.

12. Карпов Ю.Г. Асинхронные процессы на систолических структурах// Однородные вычислит.системы и систолические структуры.- ГЛ.: 1988.- С.15-16.

13. Карпов Ю.Г. Примеры синтеза спецификации протоколов из спецификации сервиса// Автоматика и вычислит.техника,- 1989.- ß 6.-C.3-I4.

14. Карпов Ю.Г. Метод спецификации и анализа взаимодействующих процессов// Автоматика и вычислит.техника.- 1986.- J5 3,- С.3-10.

15. Карпов Ю.Г., Толстяков A.D. Аналитический метод верификации протоколов// Автоматика и вычислит.техника - 1985.- JE I,- С.35-41.

16. Карпов Ю.Г., Мещерский A.A., Борщев A.B. Интегрированный стенд СПРУТ-2 дая логического проектирования и верификации протоколов// Проектирование вычислительных средств.- Каунас:1989.-С.73-74.

17. Карпов Ю.Г., Борщев A.B., Мещерский A.A. Анализ семантической корректности протоколов с использованием свойства когерентности // Автоматика и вычислит.техника,- 1989.- 5.- С.Г4-18.

18. Карпов Ю.Г., Борщев A.B., Мещерский A.A., Григорьев В.Н. Опыт разработки программного обеспечения транспортной станции// Локальные вычислительные сети.- Рига: 1988, Ч.1.- С.16-20.

19. Захаров В.Н., Карпов Ю.Г., Розеиблюм Л.Я., Яковлев A.B. Реализация асинхронных процессов на систолических структурах// Известия АН СССР. Техническая кибернетика.- 1989.- Js I.- С. 199-207.

20. Карпов Ю.Г., Щтурц И.В., Романовский A.B., Васильев В.В. Анализ структурной корректности параллельных программ в Р-техноло-гии// Управляющие системы и машны.- 1989.- JS I,- С.54-58.

21. Карпов Ю.Г., Роглаловский A.B., Штурц И.В. Операционная сре-

да высоконадежных программных систем реального времени // Вычислительные, измерительные и управляющие системы.—Л.: 1987. — С. 7—12.

22. Карпов Ю. Г., Толстяков А. В. Программирование параллельных процессов в АСУТП //Труды ЛПИ. — № 372, 1980.— С. 52—<55.

23. ¡Карпов Ю. Г. О группе автоморфизмов конечного автомата //Автоматика и телемеханика.— 1973. — № 8. — С. 70—74.

24. Карпов Ю. Г. Спецификация и верификация программного обеспечения распределенной обработки данных //Экономика, организация и технология разработки программных средств. — Калинин: 1986, ч. 2. С. 51—53.

Подписано к печати 25.01.90. М-32508. Заказ 57. Тираж 100. Бесплатно.

Отпечатано на ротапринте ЛПИ им. М. И. Калинина. 195251, Ленинград, Политехническая ул., 29.