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

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

ЧИСТЯКОВ Геннадий Андреевич

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

Специальности: 05.13.11 - Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей; 05.13.15 - Вычислительные машины, комплексы и компьютерные сети

6 НОЯ 2014

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

тг кои 9

Санкт-Петербург - 2014

005554538

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

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

Мельцов Василий Юрьевич.

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

Сенилов Михаил Андреевич, «Камский институт гуманитарных и инженерных технологий», заведующий кафедрой информационно-вычислительных технологий и программной инженерии;

кандидат технических наук, доцент Ивановский Сергей Алексеевич, «Санкт-Петербургский государственный электротехнический университет «ЛЭТИ» им. В.И. Ульянова (Ленина)», заведующий кафедрой МО ЭВМ.

Ведущая организация — ОАО «Научно-исследовательский институт

средств вычислительной техники» (ОАО «НИИ СВТ»), г. Киров

Защита диссертации состоится «24» декабря 2014 г., в часов

"Ьо минут, на заседании диссертационного совета Д 212.238.01 Санкт-Петербургского государственного электротехнического университета «ЛЭТИ» им. В.И. Ульянова (Ленина) по адресу: 197376, Санкт-Петербург, ул. Профессора Попова, дом 5.

С диссертацией можно ознакомиться в библиотеке Федерального государственного автономного образовательного учреждения высшего образования «Санкт-Петербургский государственный электротехнический университета «ЛЭТИ» им. В.И. Ульянова (Ленина)» и на сайте www.eltech.ru.

Автореферат разослан «11 » октября 2014 г.

Ученый секретарь диссертационного совета Д 212.23 8.01, к.т.н. Н.Л. Щеголева

6 /

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

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

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

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

Наиболее перспективным разделом формального подхода принято считать технику проверки моделей, авторы которой (Э. Кларк, Э. Эмерсон и Дж. Сифакис) в 2007 году были удостоены премии Тьюринга. Однако, в работах Г. Холзманна, М. Варди и Ф. Шноебелена показано, что большинство подобных методов обладают экспоненциальной временной сложностью, а универсальный, основанный на автомате Бюхи, способ сопоставления модели объекта верификации и спецификации в виде

формулы темпоральной логики линейного времени (1ЛЪ) не обладает достаточной производительностью.

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

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

Объектом исследования являются специализированные методы и машины логического вывода.

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

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

Для достижения цели решаются следующие задачи.

1. Разработка алгоритма формирования базы знаний на основе модели алгоритма и ТЬ-формулы, описывающей предъявляемые к нему требования, позволяющего свести задачу сопоставления к задаче логического вывода.

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

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

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

Области исследования. Задачи, решенные в диссертации, соответствуют областям исследования специальностей 05.13.11 —

Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей (п.1 - Модели, методы и алгоритмы проектирования и анализа программ и программных систем, их эквивалентных преобразований, верификации и тестирования) и 05.13.15 -Вычислительные машины, комплексы и компьютерные сети (п.З -Разработка научных методов и алгоритмов организации арифметической, логической, символьной и специальной обработки данных, хранения и ввода-вывода информации и п.4 - Разработка научных методов и алгоритмов организации параллельной и распределенной обработки информации, многопроцессорных, многомашинных и специальных вычислительных систем).

Методы исследования. Для достижения цели исследования использовались методы теории алгоритмов, теории множеств, теории графов, теории логического вывода, теории вычислительных систем, теории объектно-ориентированного программирования.

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

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

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

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

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

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

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

Пра1сгическая ценность исследования состоит в следующем.

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

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

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

На защиту выносятся следующие результаты.

1. Метод логического вывода делением дизъюнктов на основе определяющего элемента в логике предикатов первого порядка.

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

3. Алгоритм формирования базы знаний на основе структуры Крипке и формулы темпоральной логики.

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

Внедрение результатов исследования. Полученные теоретические и практические результаты использованы в НИР «Разработка эффективной методики верификации параллельных алгоритмов и программ с использованием методов логического вывода» (стипендия Совета по грантам Президента Российской Федерации, проект СП-1891.2013.5), в НИОКР «Разработка программного комплекса для верификации параллельных алгоритмов» (грант Фонда содействия развитию малых форм предприятий в научно-технической сфере, проект №/17248), в НИР «Разработка интеллектуальной системы обработки знаний на базе специализированного СБИС-процессора с data-flow архитектурой» (МОН

РФ, ВятГУ, №01201270376), в НИР «Разработка способа оптимизации выражений модальных логик на основе методов динамического программирования» (МОН РФ, ВятГУ, №01201452001). Полученные в диссертационной работе теоретические и практические результаты используются в рамках курсов «Технология разработки программного обеспечения» и «Интеллектуальные системы». Значимость практических результатов также подтверждается наличием актов о внедрении.

Апробация работы. Основные результаты исследования докладывались и обсуждались на Четырнадцатой национальной конференции по искусственному интеллекту с международным участием (Казань, КИИ-2014), Международной научной конференции МНСК (Новосибирск, МНСК-2011, 2012, 2013, 2014), третьей международной научной конференции «Информационные технологии и системы» (Челябинск, ИТиС-2014), Всероссийской ежегодной научно-практической конференции «Общество, наука, инновации» (Киров, НТК-2011, 2012, НПК-2013, 2014). Проект «Программный комплекс для верификации параллельных алгоритмов» был отмечен дипломом лауреата на Всероссийском конкурсе прикладных разработок и исследований в области компьютерных технологий «Компьютерный континуум: от идеи до воплощения», проводимом компанией Intel и Суперкомпьютерным консорциумом университетов России.

Публикации. Результаты исследования представлены в 19 работах (из них 10 статей, 6 тезисов докладов). Четыре работы опубликованы в научных изданиях, рекомендованных ВАК. Получен патент на полезную модель и 4 свидетельства о государственной регистрации программ для ЭВМ.

Личный вклад. Все научные результаты, приведенные в диссертационной работе и сформулированные в положениях, выносимых на защиту, получены автором лично. Работы [2-7, 10-12, 17-19] опубликованы в соавторстве с научным руководителем, которому принадлежит формулировка концепции решаемой проблемы и постановка цели исследования. Основной объем работ по написанию программ, их отладке, тестированию и интерпретации результатов экспериментов выполнен автором. В работе [20] автору принадлежит разработанная структура блока управления процессором команд, форматы сообщений и команд.

Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения и библиографического списка (включающего 103 наименования). Основная часть работы изложена на 164 страницах, содержит 34 рисунка и 11 таблиц.

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

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

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

В первой главе рассматриваются современные подходы к верификации алгоритмов и программ. Особое внимание уделяется методам формальной верификации. Суть данных методов заключается в применении строгих математических техник для доказательства эквивалентности моделей объекта верификации и предъявляемых к нему требований. Формы представления моделей определяют способ их сопоставления.

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

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

Далее в первой главе обосновывается целесообразность применения математического аппарата теории логического вывода для верификации алгоритмов с помощью техники проверки моделей. Преимуществами предлагаемого подхода являются высокий параллелизм выбранного аппарата и возможность применения широкого спектра эвристик. Данные факторы могут быть использованы для сокращения временных затрат на верификацию. Для представления модели алгоритма выбирается структура Крипке М =< 8,Ба,Я,АР,Ь>, где 5 = у,,...} - конечное непустое множество состояний, с5 - непустое множество начальных состояний, Я с 5x5 - тотальное отношение на 5, т.е. множество переходов, АР -

конечное множество атомарных предикатов (событий), Ь:8—>2ЛР -функция пометок (каждому состоянию отображения Ь сопоставляет множество истинных в нем атомарных предикатов). Для спецификации требований предлагается использовать формулы темпоральной логики линейного времени (ЬТЬ).

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

Данный метод основан на операции деления дизъюнктов. Результат от деления дизъюнкта О на дизъюнкт с/ определяется как дизъюнкт-остаток Ь, состоящий из такого множества литералов, что БЛ: Ь а Л • £) и Л- 0\Ь = Л-с1' ,с1' ее! , где Л-X - операция применения унифицирующей подстановки Л к литералам дизъюнкта X. Операция деления дизъюнктов позволяет свести задачу проверки выводимости утверждения с! из секвенций Д.(/= 1.л) к задаче проверки выводимости набора утверждений с!^ (] = 1. ж), полученных в результате применения к конъюнкции остатков

л Ьк, УА: 3/, Л: Л • /), \Л-(1 =Ьк правил разъединения-соединения и переноса.

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

Приводится следующая постановка логической задачи формальной верификации. Требуется установить выводимость утверждения 1—>Р(з0) (отрицание предиката, сопоставленного корневой вершине ДГР для начального состояния модели) из содержащихся в базе знаний КБ посылок. База знаний может быть представлена как объединение посылок из двух множеств КВ=КВ/\^КВГ, КБ{ слКВг = 0. Здесь КБг - множество

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

где A - некоторая предикатная константа, возможно, с

т

символом отрицания. Правила имеют форму 1 —> Ai(ajl,...,aji/ti). При

¡=1

этом все предикатные константы совпадают с одним из имен Parent, Event, Path, End, Itself, P ,PX, P2, ..., P . Область допустимых значений аргументов всех предикатов, за исключением Event, ограничена элементами множества состояний модели S. Первый из аргументов двуместного предиката Event принимает значения из множества состояний модели, второй - из множества атомарных предикатов АР.

Описывается разработанный для наиболее эффективного решения сформулированной задачи метод вывода - метод логического вывода делением дизъюнктов на основе определяющего элемента (МВОЭ). Метод базируется на классическом методе логического вывода делением дизъюнктов и отличается от него введением нового типа литералов («определяющие» элементы), появлением новой процедуры (процедура ограниченного образования остатков) и новой операции (операция разбиения дизъюнкта).

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

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

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

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

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

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

Рассматривается вопрос построения структур Крипке, эквивалентных последовательным и параллельным алгоритмам.

Также во второй главе описывается разработанный метод построения оптимизированного дерева грамматического разбора формулы ЬТЬ. Отличительной чертой метода является применение к вершинам дерева в процессе их последовательного восходящего анализа оптимизирующей процедуры. Суть данной процедуры заключается в использовании разрешенных (или допустимых в контексте решаемой задачи) ЬТЬ-преобразований, изменяющих структуру поддерева, корнем которого является анализируемая вершина. Целью преобразований является минимизация заранее определенной функции МР(Т,2), где Т — оптимизируемое дерево, ъ. 2 - вектор, определяющий штраф за каждое вхождение темпорального оператора. Функция представляет собой отображение структуры дерева на область вещественных чисел. Она позволяет оценить структуру дерева с точки зрения ее влияния на дальнейший процесс верификации. Предлагается четыре варианта функции МР(Т,Т). Ориентация на обработку исключительно формул ЬТЬ позволяет, с учетом специфических для данного исчисления особенностей, обеспечить полиномиальную временную сложность метода.

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

В третьей главе предлагается структура комплекса для формальной верификации алгоритмов (рисунок 1).

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

• Требования к \ алгоритму /

Модуль построения модели алгоритма,.

Блок выделения специфицируемых параметров

Редактор алгоритма

Промежуточное представление алгоритма

Правила

обработки

БНФ

Модуль спецификации требований

интерпретации модели

Блок формирования спецификации

Блок построения

дерева грамматического -раэбора спецификации

Блок оптимизации дерева разбора

Шаблоны описания типовых ошибок

Допустимые СТи преобраэования

| Мера для оценки | структуры дерева граммати ческого разбора

Комплекс для формальной верификации алгоритмов

Рисунок 1 - Структура комплекса для формальной верификации алгоритмов

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

Модуль спецификации позволяет выразить предъявляемые к объекту верификации требования в виде формулы 1ЛЪ. В качестве элементов формулы используются атомарные предикаты из множества АР структуры Крипке. Для упрощения описания типовых ошибок доступны шаблонные выражения. Кроме того, в модуле выполняется построение оптимизированного ДГР спецификации. Для оценки оптимальности используется один из предложенных вариантов функции МР(Т, 2) .

Модуль верификации устанавливает соответствие модели исследуемого алгоритма спецификации. Для этого на основе структуры Крипке и ДГР 1ЛЪ-формулы, полученных в результате работы предыдущих модулей,

формируется база знаний. Затем, с помощью машины логического вывода (МЛВ), реализующей МВОЭ, решается задача формальной верификации. Успешное завершение вывода означает существование трассы, приводящей к нарушению требований. Тогда, по информации, полученной в ходе работы МЛВ, выполняется построения схемы процесса логического вывода. Неуспешное завершение вывода означает соответствие объекта верификации предъявляемым требованиям.

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

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

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

Так как связь между акторами существует только на уровне родитель-наследник, все процессы, не связанные данным отношением, могут выполняться независимо. Таким образом, модель обладает параллелизмом на уровне задач (параллельное выполнение К-акторов), правил (параллельное выполнение М- и А/-акторов) и предикатов (параллельное выполнение {/-акторов).

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

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

концентрации ресурсов, поддержка стратегии частичного анализа результатов.

Факты из базы знаний

Правила из базы знаний

Входное множество текущих остатков

I

Целевое утверждение

Выбор базовых правил

1 d

+ + N

и и

1

|Анализ, формирование пар остатков-делимых и остатков-делителей |

t

1

Анализ полученных результатов

Разбиение дизъюнкта d, формирование выходного множества текущих (

Выборка необходимых фактов, дополнение остатков-делителей инверсиями фактов

и

и

м

| Анализ, формирование остатков или создание М процессов |

М

±

м м

Анализ результатов, формирование выходного множества текущих остатков С, построение конъюнкции остатков_

Формирование множества Мо и подготовка множества С

Анализ результатов, формирование заключения

Результат вывода (целевое утверждение доказано успешно или утверждение не доказано)

Рисунок 2 - Схема потока логических вычислений

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

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

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

Исполнительный процессор (ИП) предназначен для обработки процессов в соответствии с алгоритмами, предусмотренными для каждого типа акторов. ИП является основным вычислительным ресурсом МЛВ. Рабочая

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

Процессор команд (ПК)

Внутренняя память

Таблица фреймов процессов

Таблица идентификаторов

СТо

Диспетчер исполнительных процессоров

Очередь задач

Очередь сообщений

Диспетчер задач

Ж

Статическая область памяти Динамическая область памяти

КВ, КВ,

I Диспетчер памяти I

Исполнительный процессор (ИП)

Исполнительный процессор (ИП)

Исполнительный процессор (ИП)

Рисунок 3 - Структурная схема машины логического вывода

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

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

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

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

В четвертой главе приводятся аналитические оценки основных характеристик МЛВ: временной, обменной и информационной сложностей. В лучшем случае (проход по одной ветви дерева), время выполнения логического вывода ТЕ МЛВ с одним ИП оценивается формулой (1). В худшем случае для получения решения потребуется рассмотреть все вершины дерева логического вывода. Тогда время решения задачи Т"Е оценивается выражением (2). Среднее время решения задачи ТЕ расположено в интервале [7^.', ТЕ ] и, с учетом применения отсекающих эвристик, оценивается формулой (3).

<¡-1

Р

TN+ЪTм■Y[Xj

\ М ]-1

] м

(1)

(2)

ТЕ=а-Т;+{\-а)-ТЕ (3)

В формулах (1)-(3) (Л - средняя длина ветви дерева логического вывода, Ту - среднее время выполнения 7-актора (в том числе инверсного), Гд, - среднее время выполнения УУ-актора, Тм - среднее время выполнения М-актора, — среднее число литералов в дизъюнкте, со - среднее число базовых правил для литерала, /? - коэффициент для учета частоты повторения одноименных литералов в выводимых дизъюнктах ( /7 > 1), от -максимальный уровень формируемой матрицы частных производных, -среднее число остатков, получаемых при формировании матрицы (г - 7^-ого уровня, £ - среднее число порождаемых К-актором К-акторов-наследников, у - коэффициент, определяющий частоту неуспешного частичного анализа результатов ( у > 0), а - коэффициент, определяющий успешность применения отсекающих эвристик (0 < а < 1).

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

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

ходе процесса вывода и изменении состояния узлов машины. Для обеспечения этой возможности в состав реализации включены модуль сбора данных (МСД) и модули анализа данных (МАД). Информация обо всех совершаемых в ходе логического вывода действиях передается в МСД. МСД последовательно обращается к МАД, которые могут сохранять необходимые им данные. Каждый МАД представляет собой оформленную специальным образом с111-библиотеку. Разработан механизм подключения библиотек, позволяющий изменять набор доступных МАД без перекомпиляции приложения. Разработан базовый набор МАД. Накопленные статистические сведения могут быть использованы при проектировании конфигураций МЛВ, ориентированных на эффективную верификацию алгоритмов определенного класса. На рисунке 4 представлено главное окно программной реализации МЛВ после завершения логического вывода. _

>,1„,1„.,.„,|.■ -■■ • ■ шшт • шя

Файл Снимки Ьыполнекче Отладочная информация КОнтртюиедгр Статистике Настрэжи Поиошь

Рисунок 4 - Главное окно программной реализации МЛВ

Также в четвертой главе рассматриваются вопросы реализации группы ИП на GPU и аппаратной реализации МЛВ. Предлагается аналитическая формула (4) для оценки прогнозируемого ускорения при аппаратной реализации МЛВ на ПЛИС в сравнении с программной реализацией МЛВ.

г. _ Тцсрц ' CEpFpGA

FPGA T, W

UFPGA ' ^ С CPU

Согласно формуле (4), при аппаратной реализации MJIB на высокопроизводительной современной ПЛИС семейства Virtex-6 получаемое ускорение в сравнении с программной реализацией на многоядерной ПЭВМ общего назначения составит до 0,35- CEPFPGA, где CEPFPGA - число исполнительных процессоров на ПЛИС. Например, при размещении на Virtex-6 128 ИП (максимальное рекомендуемое число процессоров в UMA-системах с наличием КЭШ-памяти) и реальной производительности в 50% от пиковой ускорение составит 22,4 раза.

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

Время выполнения верификации с применением различных реализаций МЛВ в сравнении с временем верификации в ИС SPIN представлено в таблице 1. Для реализаций МЛВ в скобках приведено ускорение.

Таблица 1 - Время выполнения верификации в сравнении со SPIN

Пример SPIN, мс. Программная реализация МЛВ на CPU, мс. Реализация МЛВ на CPU+GPU, мс. Реализация МЛВ на ПЛИС Virtex-6, мс.

Взаимное исключение с помощью мьютекса 31 46 (0,67) 142 (0,22) 8,2 (3,78)

Взаимное исключение с помощью дополнительных переменных 1279 1083 (1,18) 1113 (1,15) 193,4(6,61)

Алгоритм работы сетевого генератора данных 562 84 (6,69) 279(2,01) 15,0(37,47)

Протокол АВР 97 121 (0,80) 183 (0,53) 21,6 (4,49)

Протокол PAR 1478 1225(1,21) 1357 (1,09) 218,8 (6,76)

Алгоритм двухфазной фиксации 27913 24813 (1,12) 25201 (1,11) 4430,9 (6,30)

Алгоритм планирования sleep-wakeup 128 124(1,03) 174 (0,74) 22,1 (5,79)

I-протокол Тэйлора 24364 21650(1,13) 23113 (1,05) 3866,1 (6,30)

Алгоритм функционирования устройства управления парогенератором 14637 13719(1,07) 14086(1,04) 2449,8 (5,97)

Протокол обмена данными сети Cambridge Ring 1384 1087(1,27) 1306(1,06) 194,1 (7,13)

Вычисления выполнялись на ЭВМ под управлением ОС Windows ХР SP3, оснащенной процессором Core i3 2100 3,1 GHz, оперативной памятью DDR3 4Gb, видеокартой GeForce GTX 550 Ti, SSD-накопителем Crucial M3 128Gb. При верификации в ИС SPIN применялась редукция частичных порядков, выполнялся подбор оптимальных размеров стека и хэш-таблицы. Прочие оптимизации не использовались. SPIN функционировал в многопоточном режиме. В состав CPU и CPU+GPU программных реализаций MJIB были включены четыре и шестнадцать ИП соответственно. В CPU+GPU реализации использовался модифицированный алгоритм функционирования диспетчера исполнительных процессоров. Сбор статистики и отладочной информации не выполнялся. Оценка времени решения тестовых задач для аппаратной реализации MJIB на ПЛИС Virtex-б была получена аналитически по формуле (4) при CEPFPGA =16.

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

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

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

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

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

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

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

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

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

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

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

СПИСОК ПУБЛИКАЦИЙ ПО ТЕМЕ ДИССЕРТАЦИИ

Публикации в изданиях, рекомендованных ВАК

1. Чистяков, Г. А. Формирование контрпримера при верификации алгоритмов с помощью методов логического вывода / Г. А. Чистяков // Вестник Астраханского государственного технического университете. Серия: управление, вычислительная техника и информатика. - № 3. - 2014. - Астрахань. - С. 50-57.

2. Чистяков, Г. А. Формирование базы знаний на основе структуры Крипке и формул темпоральной логики / Г.А. Чистяков, В.Ю. Мельцов // Фундаментальные исследования.

- № 8-4. - 2013. - Пенза. - С. 847-852.

3. Чистяков, Г. А. Эффективный метод построения оптимизированного дерева грамматического разбора формул темпоральной логики линейного времени / Г.А. Чистяков, В.Ю. Мельцов // Веспгак Тамбовского государственного технического университета. - Ks 4. - 2012. -Тамбов. - С. 813-820.

4. Чистяков, Г.А. Разработка модуля построения структуры Крипке для системы верификации параллельных алгоритмов / Г.А. Чистяков, В.Ю. Мельцов // Научно-технический вестник Поволжья. - № 6. - 2011. - Казань. - С. 217-220.

Публикации в прочих изданиях

5. Чистяков, Г.А. Метод ускоренного логического вывода для решения задачи формальной верификации / Г.А. Чистяков, В.Ю. Мельцов // Четырнадцатая национальная конференция по искусственному интеллекту с международным участием (КИИ-2014): сборник материалов конференции. - Казань: Изд-во «РИЦ», 2014. - Том 1.-С. 68-76.

6. Чистяков, Г.А. Формальная верификация алгоритмов с помощью техники проверки моделей и математического аппарата теории логического вывода / Г.А. Чистяков, В.Ю. Мельцов // Третья международная научная конференция «Информационные технологии и системы»: сборник материалов конференции. - Челябинск: Изд-во ЧелГУ, 2014. - С. 106— 108.

7. Chistyakov, G. Development Modules for Specification of Requirements for a System of Verifiaction of Parallel Alorithms / G. Chistyakov, V. Meltsov // European Researcher. - № 51,- 2012. - Sochi.-C. 511-514.

8. Chistyakov, G. Software system of formal verification using the methods of inference / G. Chistyakov // Applied Science in Europe: tendencies of contemporary development. -Stuttgart, Germany, 4 november 2013. - P. 37-39.

9. Чистяков, Г.А. Организация отложенного гашения запросов в потоковой машине логического вывода / Г.А. Чистяков И Всероссийская ежегодная научно-практическая конференция «Общество, наука, инновации» (НПК-2014): сборник материалов конференции.

- Киров: Вятский государственный университет, 2014.

10. Чистяков, Г.А. Ускоренный способ формирования композиции структур Крипке / Г.А. Чистяков, В.Ю. Мельцов // Технические науки - от теории к практике. - № 25. - 2013. -Новосибирск. - С. 72-79.

П.Чистяков, Г.А. Модификация структуры Крипке для сокращения временных затрат при верификации параллельных алгоритмов логическими методами / Г.А. Чистяков, В.Ю. Мельцов // Международная научно-практическая конференция «Наука, образование, общество: современные методы и перспективы»: сборник материалов конференции, Мин.-во. обр. и паута!. - Москва: «Буки Веди», ч.3(4), 2013. - С. 44-45.

12. Chistyakov, G. Application of parallel logical conclusion in linear temporal logic / G. Chistyakov, V. Meltsov // European Science and Technology: materials of 11 international research

and practice conference. - Wiesbaden, Germany, «Bildungszentnim Rodnik e.V.», Vol II, 2012. - P. 301-305.

13. Чистяков, Г.А. Оптимизация метода логического вывода делением дизъюнктов на основе определяющего элемента для обработки выражений темпоральной логики линейного времени / Г.А. Чистяков // Технические науки - от теории к практике. - № 33. - 2014. — Новосибирск. - С. 62-68.

14. Чистяков, Г.А. Архитектура потоковой машины логического вывода для верификации параллельных алгоритмов / Г.А. Чистяков // 52-ая Международная научная конференция МНСК: сборник материалов конференции, секция «Информационные технологии». - Новосибирск: Изд-во НГУ, 2014. - С. 179.

15. Чистяков, ГА. Применение ленивого подхода к определению эквивалентности модели алгоритма и спецификации / Г.А. Чистяков // Всероссийская ежегодная научно-практическая конференция «Общество, наука, инновации» (НПК-2013): сборник материалов конференции. — Киров: Вятский государственный университет, 2013.

16. Чистяков, Г.А. Применение методов ускоренного вывода в логике высказываний для решения задачи верификации / Г.А. Чистяков // 51-ая Международная научная конференция МНСК: сборник материалов конференции, секция «Математика». -Новосибирск: Изд-во НГУ, 2013. - С. 22.

17. Чистяков, Г.А. Структура системы верификации параллельных алгоритмов на основе методов логического вывода / Г.А. Чистяков, В.Ю. Мельцов // Рукопись депонирована в ВИНИТИ РАН. №412-В2012- 12.11.2012. - 55 с.

18. Чистяков, Г.А. Формальная верификация параллельных алгоритмов с помощью техники проверки моделей и методов логического вывода / Г.А. Чистяков, В.Ю. Мельцов // Рукопись депонирована в ВИНИТИ РАН. №358-В2013 - 29.11.2013. - 140 с.

19. Чистяков, Г.А. Архитектура специализированной абстрактной машины логического вывода / Г.А. Чистяков, В.Ю. Мельцов // Рукопись депонирована в ВИНИТИ РАН. №207-В2014 - 11.07.2014. - 90 с.

Патенты и свидетельства о регистрации программ для ЭВМ

20. Мельцов, В.Ю., Чистяков, Г.А., Тарасов, A.B., Караваев, М.А. Патент на полезную модель «Процессор команд машины логического вывода», патент №144233 от 09.06.2014.

21. Чистяков, Г.А., Мельцов, В.Ю., Власюк, Е.А. Свидетельство о государственной регистрации программы для ЭВМ «Программная реализация параллельного логического вывода на многоядерном процессоре», охранный документ №2014616849 от 04.07.2014.

22. Чистяков, Г.А., Мельцов, В.Ю., Сапожникова, A.A. Свидетельство о государственной регистрации программы для ЭВМ «Программная реализация параллельного логического вывода на графическом процессоре», охранный документ №2014616950 от 08.07.2014.

23. Чистяков, Г.А., Мельцов, В.Ю. Свидетельство о государственной регистрации программы для ЭВМ «Программный анализатор формул темпоральной логики», охранный документ №2012660235 от 04.10.2012.

24. Чистяков, Г.А., Мельцов, В.Ю. Свидетельство о государственной регистрации программы для ЭВМ «Программа автоматического построения структуры Крипке для параллельного алгоритма», охранный документ №2012613587 от 20.02.2012.

Чистяков Геннадий Андреевич

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

Специальности: 05.13.11 - Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей; 05.13.15 —Вычислительные машины, комплексы и компьютерные сети

Подписано в печать 23.10.2014 Формат 60x841'Лб Цифровая Печ. л. 1.0 Тираж 100 Заказ 18/10 печать

Типография «Фалкон Принт» (197101, г. Санкт-Петербург, ул. Большая Пушкарская, д. 54, офис 2)