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

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

48440I£

Моисеев Михаил Юрьевич

АВТОМАТИЧЕСКОЕ ОБНАРУЖЕНИЕ ДЕФЕКТОВ В МНОГОПОТОЧНЫХ ПРОГРАММАХ МЕТОДАМИ СТАТИЧЕСКОГО АНАЛИЗА

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

АВТОРЕФЕРАТ

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

2 8 АПР 2011

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

4844612

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

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

кандидат технических наук, доцент

Ицыксон Владимир Михайлович

Официальные оппоненты

доктор технических наук, профессор

Лисс Александр Рудольфович

кандидат физико-математических наук, доцент

Иванов Александр Николаевич

Ведущая организация ГОУ ВПО «Санкт-Петербургский

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

Защита состоится 12 мая 2011 г. в 14 часов на заседании Диссертационного Совета Д 212.229.18 при ГОУ ВПО «Санкт-Петербургский государственный политехнический университет» по адресу: 195251, Санкт-Петербург, ул. Политехническая, д. 29, 9-й учебный корпус, ауд. 325.

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

Автореферат разослан « №у> апреля 2011 г.

Ученый секретарь диссертационного совета кандидат технических наук, доцент

/6

Васильев А.Е.

1. ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ Актуальность работы

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

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

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

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

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

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

В настоящее время существуют эффективные алгоритмы статического анализа, обеспечивающие обнаружение дефектов в последовательных программах, однако многие программные системы используют те или иные механизмы распараллеливания. Одним из широко распространенных классов параллельных программ являются многопоточные программы. В многопоточных программах кроме программных дефектов, могут встречаться ошибки синхронизации -нефункциональные ошибки, связанные с неправильной организацией параллельного выполнения программы. К ошибкам синхронизации относятся: конкурентная модификация и использование разделяемых объектов из разных потоков программы (Race Condition), взаимные блокировки потоков (Deadlock), некорректное использование функций синхронизации (Blocking Call Misuse) и др. Применение алгоритмов статического анализа, не учитывающих специфику многопоточных программ, приводит к снижению полноты и точности получаемых результатов, а также не позволяет обнаруживать ошибки синхронизации.

Исследования, посвященные обнаружению программных дефектов в параллельных (многопоточных) программах на основе статического анализа, ведутся в ряде отечественных (ИСП РАН, СПбГУ, СПбГУИТМО, МФТИ и др.) и зарубежных университетов (MIT, Stanford University, University of California и др.), а также в научно-исследовательских центрах (Microsoft Research, Intel Research, HP Laboratories и др.). Существующие методы статического анализа многопоточных программ решают только часть задач, необходимых для обнаружения программных дефектов, и обладают рядом недостатков: анализируется ограниченное подмножество конструкций языка С, имеются ограничения на способы синхронизации потоков программы, используются аппроксимации, приводящие к недостаточной полноте и точности получаемых результатов.

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

Цель работы

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

Задачи исследования

1. Анализ существующих подходов к обнаружению дефектов в многопоточных программах на основе статического анализа.

2. Разработка модели многопоточной программы.

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

4. Разработка алгоритмов анализа параллельного выполнения многопоточной программы.

5. Организация взаимодействия отдельных алгоритмов анализа.

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

7. Реализация прототипа средства автоматического обнаружения дефектов в многопоточных программах на языке С.

Методы исследования

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

Научная новизна работы

1. Разработан метод получения информации о параллельном выполнении

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

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

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

Достоверность результатов

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

Практическая значимость работы

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

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

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

Реализация результатов работы

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

Результаты диссертационной работы используются в системе обнаружения ошибок синхронизации в программах на языке SystemC, разработанной в рамках НИР по заказу ЗАО «Интел А/О» в 2010 году, имеется акт о внедрении.

Апробация работы

Основные идеи и результаты работы докладывались на конференциях «Software Engineering Conference in Russia 2010», «Approaches and tools for efficient design of reconfigurable/programmable SOC. Intel Workshop in Saint-Petersburg 2010», «Технологии Microsoft в теории и практике программирования», «Software Engineering Conference in Russia 2009», а также обсуждались на семинарах кафедры КСПТ, СПбГПУ и кафедры системного программирования, СПбГУ.

Публикации

По результатам диссертационной работы опубликовано 9 печатных работ, в том числе в журналах «Научно-технические ведомости СПбГПУ» и «Информационно-управляющие системы» (входят в «Перечень ведущих рецензируемых научных журналов и изданий, выпускаемых в Российской Федерации»). Всего по теме работы опубликовано 5 журнальных статей и 4 тезиса конференций.

Структура и объем работы

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

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

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

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

Среди работ в области статического анализа параллельных программ можно выделить несколько основных направлений: подходы на основе извлечения частичных порядков выполнения (работы Д. Падуа, Д. Каллагана, К. Кеннеди, Дж. Саблока, Е. Штольца, Дж. Ли и др.), подходы на основе анализа наборов конструкций синхронизации (работы Д. Энглера, К. Ашкрафта, Ш. Кводера, Р. Чанга, С. Лернера и др.), подходы на основе извлечения инвариантов (работы Дж. Фостсра, М. Хикса, Т. Тераучи, А. Готсмана и др.), подходы на основе преобразования программы к последовательному виду (работы Ш. Кводера, Д. By,

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

Вопросы обнаружения программных дефектов в многопоточных программах рассматриваются в работах М. Ринарда, М. Найка, С. Парка,

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

В настоящее время существуют средства автоматизации обнаружения дефектов в многопоточных программах на языке С, наиболее распространенными являются: Coverity SA, Klocwork Insight, Parasoft C/C++ test, IBM SA, Mathworks

PolySpace, Frama-C. Большинство из существующих средств обнаружения дефектов являются закрытыми. Средства, для которых удалось получить экспериментальные результаты, показали достаточно низкие полноту и точность обнаружения дефектов.

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

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

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

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

Для представления функций над потоками и выбранными объектами синхронизации разработан базис конструкций управления параллельным выполнением программы (см. табл. 1). В работе приводятся представления основных функций Pthreads в разработанном базисе.

Таблица 1. Базис конструкций управления параллельным выполнением

Конструкция Краткое описание

create(t, pf) Создание потока и запуск в нем функции * pf

join(t) Ожидание завершения потока программы

Mí (т, val) Инициализация объекта т значением val

destroy (m) Уничтожение объекта синхронизации

lock{m,act) Блокировка мьютекса

nnlock{m,act) Освобождение мьютекса

wait (m, act) Блокировка семафора

post(m,act) Освобождение семафора

state{m) Получение состояния объекта синхронизации

Параметр act определяет изменение состояния объекта в данной конструкции.

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

8

переменных, конструкций ветвления (if) и слияния путей выполнения программы (0-функции), конструкции управления параллельным выполнением программы (см. табл. 1) и другие конструкции.

Для привязки конструкций программы к потокам, в которых они выполняются, конструкции объединяются в блоки программы. Блок программы - множество последовательных конструкций, среди которых отсутствуют межблоковые конструкции. Межблоковыми конструкциями являются: if, ф-функции, in it, create , join , lock, unlock, wait, post и state ■ Будем обозначать блок программы - S/, где j - уникальный номер потока программы, / -

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

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

Конструкции синхронизации взаимодействуют друг с другом с помощью блокировки и освобождения объекта синхронизации - будем представлять взаимодействие между парами конструкций синхронизации с помощью отношений синхронизации между блоками программы. Для блока s'1 »

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

имеет место отношение синхронизации, если существует набор входных данных, на котором выполнение s, невозможно без выполнения s2 • Будем обозначать отношение синхронизации между такими блоками - s/1 —> S '1 ■

Два блока из разных потоков программы являются совместными, если существует набор входных данных программы, на котором могут выполняться оба этих блока. Между блоками 5'1 и sj- существует строгая последовательность

выполнения, если на всех наборах входных данных сначала выполняется блок sj',

затем блок s/1 или наоборот. Блоки, из разных потоков программы, могут

выполняться параллельно, если эти блоки являются совместными и между ними отсутствует строгая последовательность выполнения - между такими блоками имеется отношение параллельности. Будем обозначать отношение параллельности между блоками s.', - 5/' 1151/3 •

Будем обозначать множество возможных состояний объекта синхронизации m в блоке S;' - m[s/)• Множество состояний мьютекса может включать значения 0 и 1, при этом значение 0 соответствует заблокированному

9

состоянию мьютекса, 1 - незаблокированному. Множество состояний семафора может включать значения 0,1,...,+°°, при этом значение 0 соответствует заблокированному состоянию семафора, положительные значения -незаблокированному. Будем называть изменение состояния объекта синхронизации действием над этим объектом. Действие над мьютексом устанавливает его состояние в значение 0 или 1, действие над семафором увеличивает или уменьшает его состояние на 1. Множество действий над объектом синхронизации т в блоке $( - учитывает возможные

изменения состояния объекта т с момента создания потока до начала блока на

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

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

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

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

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

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

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

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

S;"

5/'

'if (...)>

Uraile] • ■ ■

V У

J

1 * i

■►{ /0 ) (/«*)<--

J s/1 I ^ I

Ф К-

I К I «i j.4' J,

^/'ош^Ч--( col J

1 ЯД.

/ л

I M'iHi

\

— (post j \ *,

Рис. 1. Обозначения блоков в правилах алгоритмов анализа Правила для определения множества действий A{m,S!) выглядят следующим образом (см. рис. 1):

[si'; if 0 Silelse s!l J: A(m> s!i )=Am> s!i l Am> ) = Am< 1 [s/i = , Si)]; Am<)= 4m> st )U л(т,Si l

[create{t, pf)]: л[т, ,) = л(т, )i л[т, S/!) = {l} (мьютекс),

[create(t, pf)]: л(т, , )=л(т, S(' } A(m, S(2 )= {о} {семафор),

\jom(t)\.A[m,Si^)=A{m,Sil )®A(m,Si2) (семафор),

[lock(m,act)]: A[m,S[\t)={0},[unlock(m,act)]: A{m,Si;^)= {l},

[wait(m, act)]: а(ш,5Д, )=л(т, S* )Ф {-1}, [posl(m, act)]: а(ш,) = л(т,S^)Ф {l},

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

Алгоритм определения состояния объектов синхронизации использует действия над объектами синхронизации в потоках программы. Для определения возможных значений т в блоке Si (m(si')) строятся комбинации блоков других

потоков, параллельно с которыми может выполняться блок 5/1 - множество допустимых комбинаций, c(si)- Множество c(s/') формируется с помощью следующего правила:

VC: Се ф/')=>

(УSi : Si € С => (5/ 11 Si, V/2 : ;2 Ф i => S,/ $ C, : S(' e С => 5/ 11 S^ ))

В множество c{s/') входят комбинации из блоков программы, которые

параллельны блоку sJ' > в каждую комбинацию входит не более одного блока из

каждого потока, все блоки комбинации попарно параллельны между собой. Правила определения m{sf') выглядят следующим образом:

т.,

(X) а(ш, 5/) (мыотекс),

VSjuC

тс (S(1) = л(т, Sfr ) Ф ф А{т, S/) {семафор),

\fSjsC

где ® - операция умножения множеств действий, результат которой - все возможные произведения из действий каждого множества, тс (sf1) - состояние

объекта синхронизации в комбинации блоков С.

Алгоритм построения отношений параллельности использует следующие правила (см. рис. 1):

vsy : Si; II Sf V51/ : S* || 5/ v S* || S/

[Sl;;ifQS£elseS£ J: S* || S{,Si; || S/ ' = )J: S(' || S/ '

ViS/ : Si; || 5/

[create^pf)]:S^ ||S/' ' [create{t,pf)}: S^ ||5/ '

VS1/ g С : С e c{s{' \ Si; e С V.S/ e С: Се c(s* ), За e mc ): a > 0 \join{t)]:Sh || Si ' [lock{m)\wait(mj\:Si^ ||S/ '

Блок после конструкции join параллелен блокам, входящим в комбинации для блока перед этой конструкцией, в которые также входит последний блок ожидаемого потока. Блок, следующий после конструкции lock или wait, параллелен всем блокам, входящим в комбинацию для блока перед этой конструкцией, при условии, что объект синхронизации в данной комбинации может быть не заблокирован. Множество отношений параллельности в конструкциях unlock и post не меняется.

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

si; 11 si;

Ljom(t)}: S^ 5Д,' [hck(m)}: s£ 5Д, ' 3C-.Ce c{si; ),Эвб mc{s{;): a = 0, Sj; e С [wait(m)\.Si;

Отношение синхронизации имеет место для пары конструкций lock / unlock, оперирующих одним и тем же объектом синхронизации, при условии что блоки

12

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

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

Взаимное влияние потоков в многопоточной программе заключается в изменении значений разделяемых объектов. Алгоритм учета взаимного влияния потоков выполняет объединение значений разделяемых объектов с помощью специальных конструкций - ^/-функций. Добавление ((/-функций осуществляется для конструкций join, lock и wait - каждая (¡/-функция имеет один вход из текущего потока и один или несколько входов из других потоков. Входы в i//-функцию из других потоков строятся на основе отношений синхронизации.

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

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

Vee Ej Vee Е h Vee £\

4S£, ) = e(s* )' фД, ) = )' ) = 45/= )'

где gis/) - значение разделяемого объекта с в блоке s ', Е (Е ) ~ множество

\ 1 ' 1 j 1 ./2

разделяемых объектов, значение которых менялось только в блоках параллельных SJl (S'1 ) и не параллельных S'1 (SJ} ), Е - разделяемые объекты, не входящие

'i '2 ./1 • /2

в множества е. и е (при определении Е ,Е■ и £ учитываются блоки,

./1 J2 /I /2 ./lv/2

которые параллельны хотя бы одному из входных блоков ((/-функции). Корректность разработанного алгоритма доказана в работе.

I К I S/;

V У V у

1 Sh I

Рис. 2. Обозначения блоков в правилах для ((/-функции

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

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

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

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

Обнаружение программных дефектов выполняется с помощью обычных правил, используемых для обнаружения подобных дефектов в последовательных программах. В работе приводятся правила для обнаружения следующих групп программных дефектов: ошибки управления ресурсами и динамической памятью (RES), утечки ресурсов и памяти (LEAK), ошибки работы с буферами/массивами (BUF), ошибки отсутствия инициализации (INI). Рассмотрим несколько примеров подобных правил.

Обнаружение дефекта множественного освобождения памяти выполняется с помощью следующего правила:

[free{pjj -.DEFECT^'

где 3, - состояние программы перед /-й конструкцией, о/таЫ — специальный

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

3(p,(oj ,к))е 3,: {к < 0) v [к > size{oj)) [*p]:DEFECTBUF_m '

где предусловие (p,(oj,k)) означает, что указатель р указывает на объект о. со

смещением к, оператор size(o/) определяет размер объекта 0/. Правило

разыменования неинициализированного (освобожденного) или нулевого указателя выглядит следующим образом:

3 (р,(о

i rival it/

[* p\ : DEFECT01 где о ,d ~ специальный объект, представляющий значение NULL.

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

3S* , , е : S* 11 S¿>, е е Use(s/' ), е е Def{s[= ) DEFECT,,СЕ '

35^', S£,е: SИ S£,ee Def(s\ee Def{s';; ) DEFECTысе '

где ее Def(s') и eeUse(si) факты изменения и использования разделяемого объекта е в блоке S/ соответственно.

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

В качестве основы для реализации использовалась система обнаружения программных дефектов Aegis, разработанная на кафедре КСПТ СПбГПУ, при участии автора. Система Aegis позволяет обнаруживать программные дефекты в последовательных программах на языках C/C++. В данной работы была создана новая версия системы - Aegis МТ, которая выполняет обнаружение дефектов в многопоточных программах на языке С, использующих Pthreads. Структурная схема системы Aegis МТ приведена на рис. 3 (блоки, добавленные или модифицированные в версии Aegis МТ, выделены серым цветом).

Программа

? *

make ! г.,'.h !

AEGIS МТ

система обнаружения программных дефектов

Парсер& Линковщик

Модель программы

C.FO

Алгоритмы статического анализа

rpt^

Основные алгоритмы анализа

Отчет о дефектах

* xml

Рис. 3. Структурная схема системы обнаружения дефектов Aegis МТ Разработанная система выполняет анализ и обнаружение дефектов полностью автоматически. В работе доказано, что разработанные методы

15

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

При проведении экспериментальных исследований использовался набор специальных тестовых программ (140 программ), а также реальный программный проект - многопоточная звуковая библиотека, обеспечивающая запись и воспроизведение звука одновременно для нескольких клиентов. Для анализа звуковой библиотеки было разработано четыре тестовых проекта, использующих все основные функции этой библиотеки в многоклиентском режиме. В рамках проведенных исследований сравнивались три средства обнаружения дефектов: Aegis, Aegis МТ и Parasoft С++ test.

Экспериментальные оценки полноты и точности результатов, полученные на наборе тестовых программ, представлены на рис. 4 (средство Parasoft С++ test обозначено PS). Результаты, полученные при анализе тестовых проектов звуковой библиотеки, представлены на рис. 5 — на левой части рисунка приведено число истинных дефектов, обнаруженных средствами, на правой части рисунка приведено распределение дефектов, обнаруженных Aegis МТ, по типам дефектов.

р 06

Aegis Aegis МТ PS

is Aegis МТ PS

Рис. 4. Оценки полноты и точности результатов на тестовых программах

Aegis Aegis МТ PS

Aegis МТ

Рис. 5. Результаты анализа звуковой библиотеки 16

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

В работе приводится аналитическая оценка вычислительной сложности разработанных методов. Вычислительная сложность определяется конструкциями синхронизации, для которых строятся множества допустимых комбинаций (конструкции типа join, lock, wait и state). Сложность анализа одной такой конструкции оценивается как о(пк ■ к2-\og(k ■ п)\ где к - число параллельно выполняющихся потоков, и - число блоков параллельных блоку перед этой конструкцией в каждом потоке программы. Оценка вычислительной сложности анализа всей программы (без учета основных алгоритмов анализа) выглядит следующим образом:

0{ns\nk к2 Л0%{к-п)) п,\

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

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

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

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

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

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

4. Разработан метод совместного анализа потоков программы.

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

6. Разработанные методы реализованы в прототипе средства автоматического обнаружения дефектов в многопоточных программах на языке С.

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

1. Моисеев М.Ю. Автоматическое обнаружение дефектов в многопоточных программах методами статического анализа // Научно-технические ведомости СПбГПУ. - СПб.: СПбГПУ, 2010. №3. - С. 77-86.

2. Моисеев М.Ю. Автоматическое обнаружение дефектов в многопоточных программах методами статического анализа // Материалы межвузовского конкурса-конференции «Технологии Microsoft в теории и практике программирования» - СПб.: СПбГПУ, 2010. - С. 157-158.

3. Моисеев М.Ю., Ицыксон В.М.и др. Автоматическое обнаружение дефектов в программных системах на языке С на основе статического анализа. // Материалы межвузовского конкурса-конференции «Технологии Microsoft в теории и практике программирования» - СПб.: СПбГПУ, 2010. - С. 70-71.

4. Моисеев М.Ю. Итеративный алгоритм статического анализа для обнаружения дефектов в исходном коде программ // Информационные и управляющие системы. - Политехника, 2009. №3. - С. 33-39.

5. Moiseev M.Ju., ItsyksonV.M. et al. Automatic Defects Detection in Industrial C/C++ Software // Proceedings of the 5th Central and Eastern European Software Engineering Conference in Russia - IEEE, 2009. - P. 50-55.

6. Моисеев М.Ю., Ицыксон B.M. и др. Алгоритмы анализа указателей для обнаружения дефектов в исходном коде программ // Системное программирование. - СПб.: СПбГУ, 2009. - С. 5-30.

7. Моисеев М.Ю., Ицыксон В.М. и др. Алгоритм интервального анализа для обнаружения дефектов в исходном коде программ // Информационные и управляющие системы. - СПб.: Политехника, 2009. №2. - С. 34-41.

8. Моисеев М.Ю., Ицыксон В.М. Исследование и разработка системы автоматического обнаружения дефектов в исходном коде ПО // Материалы конференции по результатам выполнения мероприятий ФЦП "Исследования и разработки по приоритетным направлениям развития научно-технического комплекса России на 2007-2012 годы" - ОАО «ИИЦ», 2009. - С. 14-15.

9. Моисеев М.Ю., Ицыксон В.М., и др. Исследование средств автоматизации обнаружения дефектов в исходном коде программ // Научно-технические ведомости СПбГПУ - СПб.: СПбГПУ, 2008. №5. - С. 119-127.

Лицензия ЛР № 020593 от 07.08.97

Подписано в печать 07.04.2011. Формат 60x84/16. Печать цифровая. Усл. печ. л. 1,0. Уч.-изд. л. 1,0. Тираж 100. Заказ 7440Ь.

Отпечатано с готового оригинал-макета, предоставленного автором, в Цифровом типографском центре Издательства Политехнического университета. 195251, Санкт-Петербург, Политехническая ул., 29. Тел.: (812)550-40-14 Тел./факс: (812) 297-57-76

ВВЕДЕНИЕ.

ГЛАВА 1. СРАВНИТЕЛЬНЫЙ АНАЛИЗ СУЩЕСТВУЮЩИХ МЕТОДОВ И СРЕДСТВ ОБНАРУЖЕНИЯ ОШИБОК В МНОГОПОТОЧНЫХ ПРОГРАММАХ.

1.1. Критерии оценки методов и средств обнаружения ошибок.

1.2. Общие подходы к анализу параллельных программ.

1.2.1. Подходы на основе анализа частичных порядков.

1.2.2. Подходы на основе анализа наборов конструкций синхронизации.

1.2.3. Подходы на основе извлечения инвариантов.

1.2.4. Подходы на основе преобразования к последовательной программе.

1.3. Методы обнаружения ошибок в многопоточных программах.

1.3.1. Комбинирование алгоритмов анализа.

1.3.2. Использование аппроксимаций.

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

Выводы.

ГЛАВА 2. МОДЕЛЬ МНОГОПОТОЧНОЙ ПРОГРАММЫ И ПРЕДСТАВЛЕНИЕ РЕЗУЛЬТАТОВ СТАТИЧЕСКОГО АНАЛИЗА.

2.1. Общая структура предлагаемого подхода.

2.2. Модель многопоточной программы.

2.2.1 Объекты и функции РЙггеаёз.

2.2.2 Представление объектов и функций РЙ1геасЬ в модели программы.

2.3. Представление динамических свойств многопоточной программы

2.3.1. Состояние программы.

2.3.2. Представление информации о параллельном выполнении программы.

ГЛАВА 3. МЕТОДЫ АНАЛИЗА ПАРАЛЛЕЛЬНОГО ВЫПОЛНЕНИЯ

ПРОГРАММЫ.

3.1. Организация совместного выполнения алгоритмов анализа.

3.2. Алгоритм определения действий над объектами синхронизации.

3.3. Алгоритм определения состояний объектов синхронизации.

3.3.1 Способы построения допустимых комбинаций.

3.3.2 Построение неполных комбинаций.

3.3.3 Правила расчета состояний объектов синхронизации.

3.3.4 Анализ конструкции state.

3.4. Алгоритм построения отношений параллельности.

3.5. Алгоритм построения отношений синхронизации.

3.6. Алгоритм учета взаимного влияния потоков программы.

3.7. Итеративный алгоритм анализа конструкций.

3.7.1 Правила работы итеративного алгоритма.

3.7.2 Завершимость итеративного алгоритма.

3.7.3 Сохранение полноты результатов анализа.

ГЛАВА 4. АЛГОРИТМЫ ОБНАРУЖЕНИЯ ОШИБОК В МНОГОПОТОЧНЫХ ПРОГРАММАХ.

4.1 Классификация программных ошибок.

4.2 Правила обнаружения программных дефектов.

4.2.1 Правила обнаружения ошибок управления ресурсами и динамической памятью.

4.2.2 Правила обнаружения утечек ресурсов и памяти.

4.2.3 Правила обнаружения ошибок работы с буферами.

4.2.4 Правила обнаружения ошибок отсутствия инициализации

4.2.5 Правила обнаружения ошибок синхронизации.

4.3 Обнаружение множественных дефектов.

ГЛАВА 5. ПРАКТИЧЕСКАЯ РЕАЛИЗАЦИЯ И ОЦЕНКА ЭФФЕКТИВНОСТИ РАЗРАБОТАННЫХ МЕТОДОВ.

5.1 Реализация разработанных методов.

5.2 Проведение экспериментальных исследований.

5.3 Оценки полноты и точности.

5.4 Оценка вычислительной сложности.

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

5.4.2 Вычислительная сложность итеративного алгоритма.

5.4.3 Сравнение с существующими подходами.

Актуальность работы

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

Большая часть системного ПО, а также ПО для мобильных и встраиваемых систем, систем управления и других критически важных приложений создается с использованием языка С. По данным компании Соуег^у в программах на языке С, в среднем, содержится 0.25 нефункциональных ошибок на 1000 строк исходного кода [5]. Нефункциональные ошибки, характерные для последовательных программ, принято называть программными дефектами. Наиболее распространенными типами программных дефектов в программах на языке С являются [3]:

• разыменование некорректного или нулевого указателя,

• переполнение буфера и выход за границы объекта,

• использование неинициализированной переменной,

• утечки и повторное освобождение ресурсов.

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

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

Исследования в области автоматизации обнаружения программных дефектов ведутся начиная с момента появления первых программ. Для оценки эффективности методов обнаружения дефектов используются следующие количественные показатели [31]:

• полнота - доля обнаруженных дефектов среди всех дефектов имеющихся в программе,

• точность - д оля истинных дефектов среди всех обнаруженных дефектов,

• степень автоматизации - трудоемкость и сложность применения метода,

• ресурсоемкость - количество выполняемых операций и необходимый объем памяти.

Современные методы автоматизированного обнаружения программных дефектов, можно разделить на следующие классы [15, 62]:

• динамические методы — используют результаты выполнения программы,

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

• синтетические (гибридные) методы — сочетают несколько разных методов.

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

К статическим методам относятся методы проверки моделей, методы дедуктивной верификация и методы статического анализа. Методы проверки моделей [60, 61] гарантируют обнаружение нарушений спецификации, обеспечивают получение полных и точных результатов, позволяют анализировать параллельные программы и обнаруживать ошибки синхронизации. Основными недостатками этих методов являются необходимость ручного построения модели программы и высокая ресурсоемкость алгоритмов. Методы дедуктивной верификация [43] позволяют строго доказывать определенные свойства программы и могут применяться для обнаружения программных дефектов. Однако, существующие методы дедуктивной верификации допускают лишь частичную автоматизацию и требуют высокой квалификации пользователя. Обнаружение программных дефектов на основе методов статического анализа [41, 21] представляется наиболее перспективным подходом. Применение статического анализа позволяет обнаруживать все основные типы программных дефектов, при этом обеспечивается получение полных результатов. Еще одним преимуществом статического анализа является возможность полной автоматизации процесса обнаружения дефектов.

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

• конкурентная модификация и использование данных (разделяемых объектов) из разных потоков программы (Race Condition),

• блокировки и взаимные блокировки потоков (Deadlock),

• некорректное использование функций синхронизации (Blocking Call Misuse).

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

Исследования, посвященные обнаружению программных дефектов в параллельных (многопоточных) программах на основе статического анализа, ведутся в ряде отечественных (ИСП РАН, СПбГУ, СПбГПУ, СПбГУИТМО, МФТИ, МГУ и др.) и зарубежных университетов (MIT, Stanford University, University of California, University of Cambridge, Cornell University и др.), a также в научно-исследовательских центрах (Microsoft Research, Intel Research, HP Laboratories, NEC Laboratories и др.). Существующие методы статического анализа многопоточных программ на языке С решают только часть задач, необходимых для обнаружения программных дефектов и обладают рядом недостатков: анализируется ограниченное подмножество конструкций языка, имеются ограничения на способы синхронизации потоков, используются аппроксимации программы, приводящие к недостаточной полноте и точности получаемых результатов.

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

Цель работы

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

Задачи исследования

Основными задачами исследования являются:

1. Анализ существующих подходов к обнаружению дефектов в многопоточных программах на основе статического анализа.

2. Разработка модели многопоточной программы.

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

4. Разработка алгоритмов анализа параллельного выполнения многопоточной программы.

5. Организация взаимодействия отдельных алгоритмов анализа.

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

7. Реализация прототипа системы автоматического обнаружения дефектов в многопоточных программах на языке С.

Методы исследования

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

Научная новизна работы

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

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

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

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

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

Достоверность результатов

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

Практическая значимость работы

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

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

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

Реализация результатов работы

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

Результаты работы используются в системе обнаружения ошибок синхронизации в программах на языке 8уз1етС, разработанной в рамках НИР по заказу ЗАО «Интел А/О» в 2010 году, имеется акт о внедрении.

Апробация работы

Основные идеи и результаты работы докладывались на конференциях «Software Engineering Conference in Russia 2010», «Approaches and tools for efficient design of reconfigurable/programmable SOC. Intel Workshop in Saint-Petersburg 2010», «Технологии Microsoft в теории и практике программирования», «Software Engineering Conference in Russia 2009», a также обсуждались на семинарах кафедры КСПТ, СПбГПУ и кафедры системного программирования, СПбГУ.

Публикации

По результатам диссертационной работы опубликовано 9 печатных работ, в том числе в журналах «Научно-технические ведомости СПбГПУ» и «Информационно-управляющие системы» (входят в «Перечень ведущих рецензируемых научных журналов и изданий, выпускаемых в Российской Федерации»). Основные результаты диссертационной работы изложены в статье «Автоматическое обнаружение дефектов в многопоточных программах методами статического анализа» опубликованной в журнале «Научно-технические ведомости СПбГПУ» в 2010 году. Всего по теме работы опубликовано 5 журнальных статей и 4 тезиса конференций.

Структура и объем работы

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

Основные результаты работы заключаются в следующем:

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

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

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

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

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

6. Разработанные методы реализованы в прототипе средства автоматического обнаружения программных дефектов в многопоточных программах на языке С.

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

Разработанная система обнаружения дефектов Aegis МТ обеспечивает полную поддержку языка С стандарт С99 [6] и позволяет выполнять анализ многопоточных программ на основе Pthreads. Получение полных результатов, при анализе многопоточных программ, обеспечивается в случае использования основных алгоритмов статического анализа, обладающих полнотой. Возможность получения полных результатов подтверждается экспериментальными исследованиями разработанной системы Aegis МТ. Оценка точности результатов, полученная экспериментально, является достаточно высокой (20%), что позволяет говорить о возможности применения разработанного средства для повышения качества промышленного ПО. v

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

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

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

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

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

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

Можно определить следующие направления развития разработанных методов и системы обнаружения дефектов Aegis МТ:

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

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

3. Поддержка всех основных типов объектов синхронизации Pthreads, в том числе, объектов RWLock и переменных состояния.

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

5. Расширение разработанных методов и средства на другие способы создания многопоточных программ и другие языки программирования.

ЗАКЛЮЧЕНИЕ

1. AEGIS Defect Detection System Electronic Resource. / Digitek Labs. — http://www.digitek-labs.ru/aegis/

2. Boost С++ libraries Electronic Resource. / Официальный сайт . — http://www.boost.org/.

3. CERT С Secure Coding Standard Electronic Resource. / Carnegie Mellon University : 2008. https://www.securecoding.cert.org/confluence/display/seccode/CERT+C+Se cure+Coding+Standard

4. Coverity Static Analysis Electronic Resource. / Компания Coverity. — http://www.coverity.com/products/static-analysis.html

5. OPEN SOURCE REPORTS 2008 and 2009 Electronic Resource. / Компания Coverity. — http://www.scan.coverity.com/report/.

6. С Language Standard ISO/IEC 9899:1990 Electronic Resource. / Официальный сайт международной организации стандартизации. — http://www.iso. org/iso/cataloguedetail.htm?csnumber= 17782.

7. GCC, the GNU Compiler Collection Electronic Resource. / GNU Project. — http:// gcc. gnu.org/.

8. IBM Software Analyzer Electronic Resource. / Официальный сайт компании IBM. — http://www-01 .ibm.com/software/awdtools/swanalyzer/

9. IEEE 1003. IEEE Standards Electronic Resource. / Официальный сайт ассоциации стандартов IEEE. — http://standards.ieee.org/.

10. ISO/IEC 9126. ISO Standards Electronic Resource. / Официальный сайт международной организации стандартизации. — http://www.iso.org/iso/isocatalogue/cataloguetc/cataloguedetail.htm7csn umber=50516.

11. ISO/IEC 9945. ISO Standards Electronic Resource. / Официальный сайт международной организации стандартизации. —http://www.iso.org/iso/iso catalogue/cataloguetc/catalogue detail.htm?csn umber=50516.

12. Klocwork Insight Electronic Resource. / Официальный сайт компании Klocwork. — http://www.klocwork.com

13. The OpenMP API specification for parallel programming Electronic Resource. / Официальный сайт OpenMP. — http://openmp.org/wp/openmp-specifications/.

14. Parasoft С++ test Electronic Resource. / Официальный сайт компании Parasoft. — http://www.parasoft.com

15. SWEBOK Guide to the Software Engineering Body of Knowledge — 2004 Version. — Washington: IEEE Computer Society, 2004.

16. Intel Th reading В uilding В locks Electronic R esource. / Официальный сайт. —■ http://threadingbuildingblocks.org/.

17. TIOBE Software: The Coding Standards Company / Официальный сайт компании TIOBE. — http://www.tiobe.com/index.php/content/company/Home.html

18. Bouajjani A., Esparza J., Touili T. A Generic Approach to the Static Analysis of Concurrent Programs with Procedures // Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. — New York: ACM, 2003. — p. 62-73.

19. From Single Thread to Multithreaded: An Efficient Static Analysis Algorithm Electronic Resource. / Carre J-L., Hymans C.: 2009. — http://arxiv.org/PS cache/arxiv/pdff0910/0910.5 833v 1 .pdf

20. Chess В., West J. Secure Programming with Static Analysis. — Addison-Wesley, 2007. —619 p.

21. Callahan D., Kennedy K., Subhlok J. Analysis of Event Synchronization in Parallel Programming Tool // Proceedings of the second ACM SIGPLAN symposium on Principles & practice of parallel programming. — New York: ACM, 1990. —p. 21-30.

22. Chugh R., Voung J., Jhala R., Lerner S. Dataflow Analysis for Concurrent Programs using Datarace Detection // Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation. —New York: ACM, 2008. — p. 316-326.

23. Cytron R., Ferrante J., Rosen B. et al. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph // In ACM Transactions on Programming Languages and Systems. — New York: ACM, 1991. —p. 451-490.

24. Emrath P., Ghosh S., Padua D. Event Synchronization Analysis for Debugging Parallel Programs // In Proceedings of Supercomputing '89. — New York: ACM, 1989. — p. 580-588.

25. Emrath P., Ghosh S., Padua D. Detecting Nondeterminacy in Parallel-Programs // In IEEE Software, v.9, n.l. — Washington: IEEE Computer Society, 1992—p. 69-77.

26. Emmi M., Qadeer S., Rakamaric Z. Delay-Bounded Scheduling // Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. — New York: ACM, 2011. — p. 174-186.

27. Engler D., Ashcraft K. RacerX: Effective, Static Detection of Race Conditions and Deadlocks // Proceedings of the nineteenth ACM symposium on Operating systems principles. — New York: ACM, 2003. — p. 237-252.

28. Godefroid P. Model checking for programming languages using VeriSoft // Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. — New York: ACM, 1997. — p. 174-186.

29. Gotsman A., Berdine J., Cook B., Sagiv M. Thread-Modular Shape Analysis // Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation. — New York: ACM, 2007. —p. 266-277.

30. Jackson D., Rinard M. Software Analysis: A Roadmap // Proceedings of the Conference on The Future of Software Engineering. — New York: ACM, 2000, —p. 133-145.

31. Ladkin P., Simons B. Static Analysis of Interprocess Communication. Lecture Notes in Computer Science. — Berlin: Springer, 1995. — 145 p.

32. Lai A., Reps T. Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis // Formal Methods in System Design. — New York: ACM, 2009. —p. 73-97.

33. Lahiri S., Qadeer S., Rakamaric Z. Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers // In Computer Aided Verification — Berlin: Springer, 2009. — p. 73-97.

34. Naik M., Park C., Sen K., Gay D. Effective Static Deadlock Detection // Proceedings of the 31st International Conference on Software Engineering. — Washington: IEEE Computer Society, 2009. — p. 386-396.

35. Naik M., Aiken A. Conditional Must Not Aliasing for Static Race Detection // Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. — New York: ACM, 2007. — p. 327-338.

36. Naik M. Effective Static Race Detection for Java. PhD thesis, Stanford University, 2008.

37. Nielson F., Nielson H.R., Hankin C. Principles of Program Analysis. — Berlin: Springer, 2005. — 452 p.

38. Netzer R., Ghosh S. Efficient race condition for shared-memory programs with post/wait synchronization // International Conference on Parallel Processing. — 1992. — p. 242-246.

39. Peled D. Software Reliability Methods — Berlin: Springer-Verlag, 2001. — 331 p.

40. Pratikakis P., Foster J., Hicks M. LOCKSMITH: Context-Sensitive Correlation Analysis for Race Detection // Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation. — New York: ACM, 2006. — p. 320-331.

41. Pratikakis P., Foster J., Hicks M. LOCKSMITH: Practical Static Race Detection for C // Journal ACM Transactions on Programming Languages and Systems, Volume 33, Issue 1. —New York: ACM, 2011.

42. Qadeer S., Wu D. KISS: Keep It Simple and Sequential // Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation. —New York: ACM, 2004. — p. 14-24.

43. Qadeer S., Rajamani S., Rehof J. Summarizing procedure in Concurrent Programs // Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. — New York: ACM, 2004. — p. 245-255.

44. Ramanujam J., Mathew A. Analysis of Event Synchronization in Parallel Programs // In Languages and Compilers for Parallel Computing. — Berlin: Springer, 1995. — p. 300-315.

45. Rinard M. Analysis of Multithreaded Programs // Lecture Notes in Computer Science, Vol. 2126/2001. — Berlin: Springer, 2001. — p. 1-19.

46. Lecture Notes on Static Analysis Electronic Resource. / Schwartzbach M.: 2000. — lara.epfl.ch/web2010/media/sav08:schwartzbach.pdf.

47. Terauchi T. Checking Race Freedom via Linear Programming // Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation. —New York: ACM, 2008. —p. 1-10.

48. Torre S., Madhusudan P., Parlato G. Reducing Context-Bounded Concurrent Reachability to Sequential Reachability // Proceedings of the 21st International Conference on Computer Aided. — Berlin: Springer, 2009.—p. 477-492.

49. Исследование и разработка системы автоматического обнаружения дефектов в исходном коде программного обеспечения. Выбор направлений исследований: отчет о НИР / СПбГПУ, Рудекой А.И.— СПб., 2008.— С. 136. № ГР 0120.0 808661. -Инв. № 02 2009 00405.

50. Гайсарян С.С., Чернов А.В., Белеванцев А.А. и др. О некоторых задачах анализа и трансформации программ // Труды Института системного программирования РАН, 2004.

51. Ицыксон В.М., Моисеев М.Ю., Захаров A.B. и др. Алгоритм интервального анализа для обнаружения дефектов в исходном коде программ // Информационные и управляющие системы. № 2 (39). — СПб.: Политехника, 2009. —с. 34-41.

52. Ицыксон В.М., Глухих М.И. ' Язык спецификаций поведения программных компонентов // Научно-технические ведомости СПбГПУ

53. СПб.: СПбГПУ, 2010. №3. — с. 63-70.

54. Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. — СПб.: БХВ-Петербург, 2010.552 с.

55. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. — М.: МЦНМО, 2002. — 416 с.

56. Кулямин В.В. Методы верификации программного обеспечения // Всероссийский конкурсный отбор обзорно-аналитических статей по приоритетному направлению "Информационно-телекоммуникационные системы", 2008. — 117 с.

57. Моисеев М.Ю. Итеративный алгоритм статического анализа для обнаружения дефектов в исходном коде программ // Информационные и управляющие системы. — Политехника, 2009. №3. — с. 33-39.

58. Моисеев М.Ю., Ицыксон В.М., и др. Исследование средств автоматизации обнаружения дефектов в исходном коде программ // Научно-технические ведомости СПбГПУ — СПб.: СПбГПУ, 2008. №5.с. 119-127.

59. Несов B.C., Маликов О.Р. Использование информации о линейных зависимостях для обнаружения уязвимо стей в исходном коде программ // Труды Института системного программирования РАН, 2006.