Методы и инструментальные средства формальной верификации функционально-потоковых параллельных программ

Актуальность темы и степень её разработанности. Постоянный рост объёма разрабатываемых программных систем и их ориентация на параллельную обработку дан- ных ведут к увеличению сложности программного обеспечения (ПО), что, в свою очередь, повышает вероятность возникновения различных ошибок. Традиционный способ обеспече- ния надёжности программ путём тестирования не может полностью удовлетворить возрас- тающие требования практического использования. Альтернативой тестированию являются методы формальной верификации, которые обеспечивают анализ всех возможных вариан- тов поведения системы. Формальная верификация — это формальное доказательство того, что программа соответствует своей спецификации [1, 2]. Методы формальной верификации позволяют доказать отсутствие ошибок в программе, в то время как тестирование лишь выявляет ошибки, но не даёт гарантии их отсутствия.
Существуют разнообразные подходы к формальной верификации программ [3]. Основ- ными являются методы проверки моделей [4], дедуктивный анализ [1], различные варианты уточнения программ [5, 6].
В настоящее время достигнуты определённые успехи в практическом применении фор- мальной верификации к последовательным программам. Разработан ряд систем для под- держки этого процесса. В качестве примера можно привести верификаторы программ на языке Си: Boogie [7] и система СПЕКТР [8]; системы для верификации объектно-ориентиро- ванных программ на Java: LOOP [9] и KeY [10]; системы для верификации функциональных программ: DSOLVE [11], HSOLVE [12].
Параллельное программирование позволяет существенно увеличить производитель- ность на современных вычислительных системах. Однако параллелизм приводит к значи- тельному усложнению разработки, а особенно отладки и верификации программ. Непосред- ственная ориентация современного параллельного программирования на существующие ар- хитектуры затрудняет формальную верификацию, так как наряду с логической корректно- стью программ приходится исследовать и влияние ресурсных ограничений, порождающих дополнительные ошибки. Ситуация может быть улучшена, если при разработке параллель- ных программ на первоначальных этапах можно было бы избавиться от ресурсных конфлик- тов. Одним из таких подходом является архитектурно-независимое параллельное програм- мирование [13, 14, 15, 166]. Представитель данного направления — функционально-потоковая модель параллельных вычислений (ФПМПВ) и созданный на её основе язык программиро- вания Пифагор [16, 17]. Основными идеями подхода являются исключение ресурсных огра- ничений и неявное управление вычислениями. В функционально-потоковой параллельной (ФПП) программе описываются только информационные связи между выполняемыми функ-
6
циями. Взаимодействие между функциями при этом осуществляется по готовности данных, что позволяет создавать программы с неограниченным параллелизмом, «сжатие» которого к конкретным вычислительным ресурсам и условиям эксплуатации будет происходить после верификации и отладки написанных программ [166, 167].
Перспективным видится то, что в отсутствии ресурсных ограничений основной упор в разработке параллельных программ и их анализе можно сделать именно на формальную верификацию при отсутствии ресурсных конфликтов. Вместе с тем следует отметить, что вопросы, связанные с формальной верификацией, в рамках данного направления практиче- ски не проработаны. Имеются работы, связанные с организацией отладки ФПП программ и использованием методов верификации для анализа корректности данных, не связанных с формальным доказательством логической корректности кода [18, 19, 168, 169].
Поэтому актуальной является разработка формальных методов и средств верифика- ции для языка функционально-потокового параллельного программирования, обеспечиваю- щих проверку логики функционирования программ.
Цель и задачи исследования. Целью работы является повышение надёжности и корректности функционально-потоковых параллельных программ посредством разработки методов формальной верификации.
Для достижения указанной цели в работе решаются следующие задачи:
— проанализировать существующие подходы к формальной верификации и возмож- ности их использования при функционально-потоковом параллельном программировании;
— формально описать семантику языка ФПП программирования Пифагор для фор- мирования основы методов анализа ФПП программ;
— разработать методы, обеспечивающие формальную верификацию ФПП программ;
— разработать инструментальное средство, обеспечивающее поддержку методов фор- мальной верификации ФПП программ.
Объектом исследования является функционально-потоковая модель параллельных вычислений и язык функционально-потокового параллельного программирования.
Предметом исследования являются методы и средства формальной верификации функционально-потоковых параллельных программ.
Научная новизна.
1. Для доказательства корректности функционально-потоковых параллельных про- грамм, написанных на языке Пифагор, впервые разработан метод верификации на базе ис- числения Хоара, эквивалентный по сложности методам доказательства корректности для по- следовательных программ, но позволяющий доказывать корректность программы без огра-

7
ничения параллелизма, что обеспечивается концепцией неограниченных вычислительных ре- сурсов.
2. Для доказательства завершения функционально-потоковых параллельных прог- рамм впервые предложен метод, использующий ограничивающую функцию, который до- пускает изменение спецификации программы таким образом, чтобы доказательство частич- ной корректности одновременно характеризовало и завершение программы. Это позволяет строить инструментальные средства поддержки доказательства на одной общей основе.
3. Для функционально-потоковых параллельных программ впервые предложен метод удаления взаимной рекурсии нескольких функций, позволяющий преобразовывать произ- вольную функцию в функцию с прямой рекурсией, это повышает эффективность верифика- ции за счёт преобразования программы только к одной функции.
4. Впервые разработана архитектура и реализован прототип инструментального сред- ства, обеспечивающего поддержку верификации функционально-потоковых параллельных программ с помощью предложенных методов. Это позволяет упростить процесс формаль- ной верификации за счёт наглядной визуализации дерева доказательства и автоматизации преобразований графа анализируемой функции.
Положения, выносимые на защиту.
1. Разработанный метод верификации на базе исчисления Хоара для ФПП программ на языке Пифагор позволяет доказывать частичную корректность ФПП программ.
2. Разработанный метод доказательства завершения ФПП программ совместно с ме- тодом верификации позволяет доказать тотальную корректность программы.
3. Предлагаемый метод удаления взаимной рекурсии нескольких функций позволяет преобразовать любую рекурсивную функцию ФПП программы в прямую рекурсию, чтобы применить к ней метод верификации.
4. Разработанный прототип инструментального средства для поддержки верифика- ции ФПП программ позволяет визуализировать процесс доказательства и автоматизирует построение дерева доказательства для упрощения процесса формальной верификации.
Теоретическая и практическая значимость работы. Результаты работы могут быть использованы для повышения эффективности разработки параллельных программ. На основе предложенных методов формальной верификации разработано инструментальное средство, обеспечивающее поддержку верификации функционально-потоковых параллель- ных программ.
Исследование выполнено при финансовой поддержке РФФИ в рамках научных про- ектов No 13-01-00360, No 17-07-00288 и ФЦП «Научные и научно-педагогические кадры инно- вационной России» No 14.А18.21.0396.

8
Полученные научные и практические результаты использованы в учебном процессе на кафедре вычислительной техники и кафедре высокопроизводительных вычислений Ин- ститута космических и информационных технологий СФУ при изучении дисциплин «Техно- логии разработки программного обеспечения», «Параллельное программирование», «Высо- копроизводительные вычисления на графических процессах» и при выполнении выпускных квалификационных работ.
Результаты исследования использованы при разработке функционально-потоковых параллельных программ для процесса высокоуровневого проектирования цифровых схем на базе функционально-потоковой парадигмы. Для разработки ФПП программ использовалась формализованная семантика языка Пифагор, проводилась формальная верификация ФПП программ перед их преобразованием в программы для сверхбольших интегральных схем.
Результаты практического применения диссертационного исследования подтвержде- ны актами о внедрении (приложение А).
Методы исследования. В работе использовались элементы теории множеств, ме- тоды математической логики (различные логики и аксиоматические теории, -исчисление, метод доказательства теорем на основе исчисления Хоара, методы доказательства заверше- ния программ на базе трансфинитной индукции), методы теории рекурсивных функций (по- строение универсальной рекурсивной функции для удаления взаимной рекурсии нескольких функций), элементы теории графов, методы и понятия теории алгоритмов, теории языков программирования, теории языков и формальных грамматик, теория разработки транслято- ров. Для описания результатов использовались UML-диаграммы, диаграммы Вирта и формы Бэкуса-Наура.
При создании программных инструментов использовались структурное и объектно- ориентированное программирование, кросс-платформенная библиотека Qt.
Апробация работы. Основные положения диссертации докладывались и обсуж- дались на 15 конференциях и семинарах, основные из которых: Международная научная конференция «Параллельные вычислительные технологии» (Челябинск, 2013; Ростов-на- Дону, 2018), Parallel Computing Technologies International Conference (Санкт-Петербург, 2013), Международная конференция «IX Сибирский конгресс женщин-математиков» (Красноярск, 2016), Всероссийская научная конференция памяти А.Л. Фуксмана «Языки программирова- ния и компиляторы» (Ростов-на-Дону, 2017), Международная конференция «Суперкомпью- терные дни в России» (Москва, 2018).
Получено два свидетельства о регистрации программного обеспечения (2013, 2021).
По теме диссертации опубликовано двадцать три научные работы; из которых шесть статей в изданиях, рекомендуемых ВАК; три статьи входят в список Web of Science Core

9
Collection; пять статей индексируется в Scopus.
Личный вклад автора. Основные результаты являются новыми и получены лично
автором. Автором проведён значительный объём научных изысканий, подготовлены публи- кации; предложен метод верификации на базе исчисления Хоара и доказательства завер- шения ФПП программ на языке Пифагор; предложен метод удаления взаимных рекурсий нескольких функций в программах на языке Пифагор; разработано инструментальное сред- ство поддержки формальной верификации ФПП программ. Научные работы, опубликован- ные в соавторстве с научным руководителем, заключаются в разработке метода формальной верификации ФПП программ на основе дедуктивного анализа; разработке архитектуры ин- струментального средства поддержки формальной верификации ФПП программ. Совместно с научным руководителем автор осуществлял постановку целей и задач и анализ полученных результатов. В совместных публикациях автора с Удаловой Ю.В. включен разработанный автором метод доказательства завершения программ на языке Пифагор. В совместных пуб- ликациях автора с Непомнящим О.В., Матковским И.В., Васильевым В.М. и Романовой Д.С. научные результаты автора являются дополнением к концепции разрабатываемого ими транслятора функционально-потоковых параллельных программ.
Структура работы. Диссертационная работа состоит из введения, 4 глав, заклю- чения, списка литературы, включающего 188 наименований, списка сокращений и 14 при- ложений. Работа изложена на 157 листах машинописного текста, содержит 41 рисунок, 6 таблиц.
Во введении приводится общая характеристика работы и даётся краткий обзор содер- жания диссертации.
В первом разделе проводится анализ существующих подходов к формальной верифи- кации программ. На основе проведённого анализа выбираются наиболее подходящие методы для верификации ФПП программ. Проводится анализ инструментальных средств поддержки формальной верификации программ. На основе анализа предлагается общая схема архитек- туры инструментального средства, подходящая для верификации ФПП программ.
Во втором разделе анализируются и предлагаются методы формальной верификации ФПП программ. Разрабатывается аксиоматическая система для верификации ФПП про- грамм на языке Пифагор, являющегося практическим воплощением ФПМПВ. Для этого проводится формализация семантики ФПП программ, выбирается язык спецификации для формулировки свойств ФПП программ, разрабатываются аксиомы и правила вывода аксио- матической системы. Предлагается наглядный способ проведения доказательства на инфор- мационном графе программы.
В третьем разделе рассматривается доказательство корректности функций, содержа-

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