Содержание к диссертации
Введение
ГЛАВА 1. Сравнительный анализ существующих методов и средств обнаружения ошибок в многопоточных программах 16
1.1. Критерии оценки методов и средств обнаружения ошибок 17
1.2. Общие подходы к анализу параллельных программ 20
1.2.1. Подходы на основе анализа частичных порядков 20
1.2.2. Подходы на основе анализа наборов конструкций синхронизации 24
1.2.3. Подходы на основе извлечения инвариантов 26
1.2.4. Подходы на основе преобразования к последовательной программе 28
1.3. Методы обнаружения ошибок в многопоточных программах 31
1.3.1. Комбинирование алгоритмов анализа 31
1.3.2. Использование аппроксимаций 34
1.4. Средства обнаружения ошибок в многопоточных программах на языке С 36
Выводы 38
ГЛАВА 2. Модель многопоточной программы и представление результатов статического анализа 40
2.1. Общая структура предлагаемого подхода 40
2.2. Модель многопоточной программы 42
2.2.1 Объекты и функции Pthreads 44
2.2.2 Представление объектов и функций Pthreads в модели программы 54
2.3. Представление динамических свойств многопоточной программы 61
2.3.1. Состояние программы 61
2.3.2. Представление информации о параллельном выполнении программы з
ГЛАВА 3. Методы анализа параллельного выполнения программы 71
3.1. Организация совместного выполнения алгоритмов анализа 71
3.2. Алгоритм определения действий над объектами синхронизации... 74
3.3. Алгоритм определения состояний объектов синхронизации 80
3.3.1 Способы построения допустимых комбинаций 81
3.3.2 Построение неполных комбинаций 85
3.3.3 Правила расчета состояний объектов синхронизации 88
3.3.4 Анализ конструкции state 88
3.4. Алгоритм построения отношений параллельности 89
3.5. Алгоритм построения отношений синхронизации 97
3.6. Алгоритм учета взаимного влияния потоков программы 99
3.7. Итеративный алгоритм анализа конструкций 108
3.7.1 Правила работы итеративного алгоритма 110
3.7.2 Завершимость итеративного алгоритма 113
3.7.3 Сохранение полноты результатов анализа 114
ГЛАВА 4. Алгоритмы обнаружения ошибок в многопоточных программах 119
4.1 Классификация программных ошибок 119
4.2 Правила обнаружения программных дефектов 121
4.2.1 Правила обнаружения ошибок управления ресурсами и динамической памятью 122
4.2.2 Правила обнаружения утечек ресурсов и памяти 123
4.2.3 Правила обнаружения ошибок работы с буферами 124
4.2.4 Правила обнаружения ошибок отсутствия инициализации 125
4.2.5 Правила обнаружения ошибок синхронизации 126
4.3 Обнаружение множественных дефектов 130
ГЛАВА 5. Практическая реализация и оценка эффективности разработанных методов 132
5.1 Реализация разработанных методов 132
5.2 Проведение экспериментальных исследований 135
5.3 Оценки полноты и точности 138
5.4 Оценка вычислительной сложности 142
5.4.1 Вычислительная сложность правил, использующих допустимые комбинации 142
5.4.2 Вычислительная сложность итеративного алгоритма 147
5.4.3 Сравнение с существующими подходами 148
Заключение 150
Список использованных источников 154
- Подходы на основе анализа частичных порядков
- Представление объектов и функций Pthreads в модели программы
- Алгоритм определения состояний объектов синхронизации
- Правила обнаружения ошибок работы с буферами
Введение к работе
Актуальность работы
В настоящее время как никогда остро стоит проблема повышения качества программного обеспечения. Это связано с тем, что все большее число технических систем используют программные компоненты. Программные системы могут решать сложные и ответственные задачи, при этом практически все они содержат ошибки. Одним из видов ошибок в ПО являются нефункциональные ошибки -ошибки, связанные с нарушениями правил языка программирования, некорректным использованием библиотечных функций и системных вызовов и т.п.
Большая часть системного ПО, а также ПО для мобильных и встраиваемых систем, систем управления и других критически важных приложений создается с использованием языка С. По данным компании Coverity, в программах на языке С, в среднем, содержится 0.25 нефункциональных ошибок на 1000 строк исходного кода. Нефункциональные ошибки, характерные для последовательных программ, принято называть программными дефектами. Наиболее распространенными типами программных дефектов в программах на языке С являются: разыменование некорректного указателя, переполнение буфера и выход за границы объекта, использование неинициализированной переменной, утечки и повторное освобождение ресурсов. Проявление программных дефектов может приводить к выдаче неверных результатов, зависанию или аварийному завершению программы, нарушению конфиденциальности хранимой информации.
Обнаружение программных дефектов является одной из самых сложных и трудоемких задач в процессе разработке ПО, что приводит к необходимости автоматизации решения этой задачи. Современные методы автоматизированного обнаружения программных дефектов, можно разделить на два класса:
динамические методы - используют результаты выполнения программы,
статические методы - используют исходный код программы, модели программы, спецификации и другие артефакты, создаваемые в процессе проектирования.
К динамическим методам относятся: мониторинг, анализ трасс выполнения, различные виды тестирования. Использование динамических методов обеспечивает получение точных результатов. Основными недостатками динамических методов являются: неполнота получаемых результатов и невозможность полной автоматизации процесса обнаружения дефектов. К статическим методам относятся: верификация на основе проверки моделей, дедуктивная верификация и статический анализ. Наиболее перспективным методом обнаружения программных дефектов представляется статический анализ. Применение статического анализа позволяет обнаруживать все основные типы программных дефектов, при этом обеспечивается получение полных результатов. Еще одним преимуществом статического анализа является возможность полной автоматизации процесса обнаружения дефектов. Основным недостатком данного метода является неточность получаемых результатов.
В настоящее время существуют эффективные алгоритмы статического анализа, обеспечивающие обнаружение дефектов в последовательных программах, однако многие программные системы используют те или иные механизмы распараллеливания. Одним из широко распространенных классов параллельных программ являются многопоточные программы. В многопоточных программах кроме программных дефектов, могут встречаться ошибки синхронизации -нефункциональные ошибки, связанные с неправильной организацией параллельного выполнения программы. К ошибкам синхронизации относятся: конкурентная модификация и использование разделяемых объектов из разных потоков программы (Race Condition), взаимные блокировки потоков (Deadlock), некорректное использование функций синхронизации (Blocking Call Misuse) и др. Применение алгоритмов статического анализа, не учитывающих специфику многопоточных программ, приводит к снижению полноты и точности получаемых результатов, а также не позволяет обнаруживать ошибки синхронизации.
Исследования, посвященные обнаружению программных дефектов в параллельных (многопоточных) программах на основе статического анализа, ведутся в ряде отечественных (ИСП РАН, СПбГУ, СПбГУИТМО, МФТИ и др.) и зарубежных университетов (MIT, Stanford University, University of California и др.), а также в научно-исследовательских центрах (Microsoft Research, Intel Research, HP Laboratories и др.). Существующие методы статического анализа многопоточных программ решают только часть задач, необходимых для обнаружения программных дефектов, и обладают рядом недостатков: анализируется ограниченное подмножество конструкций языка С, имеются ограничения на способы синхронизации потоков программы, используются аппроксимации, приводящие к недостаточной полноте и точности получаемых результатов.
Большое количество проводимых исследований, а также недостаточная степень проработки и ограничения существующих методов, свидетельствуют о том, что задача создания методов автоматизации обнаружения дефектов в многопоточных программах, в том числе в программах на языке С, является актуальной.
Цель работы
Целью данной работы является исследование и разработка методов автоматизации обнаружения программных дефектов в многопоточных программах на основе статического анализа.
Задачи исследования
-
Анализ существующих подходов к обнаружению дефектов в многопоточных программах на основе статического анализа.
-
Разработка модели многопоточной программы.
-
Выбор алгоритмов статического анализа, обеспечивающих извлечение необходимой информации для обнаружения программных дефектов.
-
Разработка алгоритмов анализа параллельного выполнения многопоточной программы.
-
Организация взаимодействия отдельных алгоритмов анализа.
-
Выбор и уточнение алгоритмов обнаружения программных дефектов на основе результатов статического анализа.
-
Реализация прототипа средства автоматического обнаружения дефектов в многопоточных программах на языке С.
Методы исследования
При проведении теоретических исследований применяются методы теории множеств, теории графов, теории отношений, теории решеток, абстрактной интерпретации, статического анализа. При разработке прототипа средства автоматического обнаружения дефектов используются методы объектно-ориентированного анализа и проектирования.
Научная новизна работы
1. Разработан метод получения информации о параллельном выполнении
многопоточной программы, определяющий параллельно выполняющиеся блоки программы, взаимодействующие конструкции синхронизации, а также состояния объектов синхронизации. Построение допустимых комбинаций блоков программы при анализе конструкций синхронизации обеспечивает повышение точности результатов.
-
Разработан метод совместного анализа потоков программы, обеспечивающий корректный анализ многопоточных программ, использующих разделяемые объекты, а также программ с несколькими возможными порядками выполнения конструкций. Данный метод управляет последовательностью анализа конструкций и распространяет изменения значений разделяемых объектов между потоками программы. Определение актуальных значений разделяемых объектов обеспечивает повышение точности результатов.
-
Предложен способ организации совместного выполнения алгоритмов анализа, позволяющий расширить алгоритмы анализа последовательных программ на класс многопоточных программ. Данный способ обеспечивает учет всех взаимодействий между используемыми алгоритмами, что позволяет сохранить полноту получаемых результатов. Обмен промежуточными данными между алгоритмами в процессе анализа обеспечивает повышение точности получаемых результатов.
Достоверность результатов
Достоверность теоретических результатов подтверждается
доказательствами утверждений, лежащих в основе разработанных методов, а также результатами экспериментальных исследований разработанного прототипа средства обнаружения программных дефектов.
Практическая значимость работы
Разработанные методы предназначены для автоматизации обнаружения программных дефектов в многопоточных программах на языке С. Применение этих методов позволит повысить качество как вновь разрабатываемых, так и уже существующих программных систем, а также снизить трудоемкость и сократить сроки отладки ПО.
Реализованный в рамках данной работы прототип средства обнаружения дефектов позволяет обнаруживать основные типы программных дефектов и некоторые виды ошибок синхронизации в многопоточных программах на языке С, использующих потоки и объекты синхронизации 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 приложения.
Подходы на основе анализа частичных порядков
Сравнительный анализ существующих методов и средств обнаружения ошибок в многопоточных программах проводится с целью определения возможности их применения для повышения качества промышленных программных систем. Для проведения сравнительного анализа необходимо определить критерии оценки методов и средств обнаружения ошибок. Рассмотрим основные свойства многопоточных программ на языке С, которые должны учитываться при проведении статического анализа для обнаружения программных ошибок.
Многопоточные программы используют для организации параллельного выполнения потоки и объекты синхронизации. В реальных многопоточных программах потоки создаются динамически как из главного потока, так и из других потоков. При этом количество выполняющихся потоков не ограничено и может меняться в зависимости от входных данных программы. Определить количество потоков (или максимально возможное количество потоков) перед выполнением анализа в общем случае невозможно. Все это приводит к необходимости отдельного анализа каждого создаваемого потока, а также к необходимости определения функции выполняемой в этом потоке. Созданный поток может завершаться асинхронно либо завершение потока может ожидаться в родительском потоке. Для определения корректной последовательности выполнения конструкций в потоках программы также необходимо анализировать различные варианты завершения потоков.
Для синхронизации выполнения разных потоков программы и обеспечения атомарности выполнения наборов операций используются объекты синхронизации: мьютексы, семафоры, барьеры и другие. Количество и типы используемых объектов синхронизации в общем случае ничем не ограничены. Для реальных многопоточных программ обычно одновременно используются объекты синхронизации нескольких типов. Это приводит к необходимости анализа различных типов объектов синхронизации. Конкретный перечень и свойства объектов синхронизации определяются используемой библиотекой организации многопоточного выполнения. При анализе функций для объектов синхронизации необходимо идентифицировать эти объекты в разных потоках программы.
В программе на языке С операции с объектами программы могут выполняться через указатели. Поэтому для идентификации объектов-потоков и объектов синхронизации необходимо выполнять анализ указателей. Для обеспечения достаточной точности результатов также необходимо выполнять анализ значений интервальных переменных (переменных типа int, float, char и т.п.). Интервальные переменные используются в условиях операторов ветвления, в качестве счетчиков циклов, индексов при обращении к элементам массивов и т.д. Для определения значений переменных-указателей и интервальных переменных необходимо использовать соответствующие алгоритмы анализа.
Использование различных алгоритмов анализа требует организации их совместного выполнения. При этом необходимо учитывать все возможные взаимодействия и обеспечить обмен промежуточными результатами между отдельными алгоритмами.
Целью проведения анализа является обнаружение программных ошибок. Используемые методы анализа должны обеспечивать извлечение необходимой информации для обнаружения поддерживаемых типов ошибок.
Основными показателями эффективности алгоритмов статического анализа являются полнота и точность обнаружения ошибок. Одним из важных преимуществ методов статического анализа является возможность получения полных результатов (обнаружение всех ошибок поддерживаемых типов, которые имеются в программе). Используемые методы анализа должны обеспечивать полноту результатов равную или близкую к 100%. В качестве итога сформулируем основные требования к методам анализа многопоточных программ на языке С: Поддержка всего множества конструкций языка С (возможность анализа произвольных программ без ограничений). Анализ состояний обычных объектов программы (определение значений переменных-указателей и интервальных переменных). Извлечение необходимой информации для обнаружения широкого класса программных дефектов. Анализ произвольного числа потоков программы, в том числе, динамически создаваемых потоков. Анализ произвольного числа объектов синхронизации поддерживаемых типов с идентификацией этих объектов в разных потоках. Совместное выполнение алгоритмов анализа с обменом результатами между этими алгоритмами. Получение р езультатов с полнотой равной или близкой к 100% (обнаружение всех или почти всех дефектов поддерживаемых типов, имеющихся в программе).
Критериями оценки рассматриваемых методов и средств обнаружения ошибок является удовлетворение перечисленным выше требованиям. Для средств обнаружения ошибок дополнительным критерием является наличие открытой информации о методах и алгоритмах, используемых в этих средствах, а также об эффективности работы этих средств на открытых тестовых наборах или программах с открытым исходным кодом.
При проведении анализа реальных многопоточных программ возникает задача снижения ресурсоемкости алгоритмов анализа. Для обеспечения приемлемой ресурсоемкости применяются те или иные подходы, которые обычно называют аппроксимациями. Применение аппроксимаций лежит в основе всех методов статического анализа многопоточных программ. При проведении сравнительного анализа выбранных методов особое внимание будет уделяться используемым аппроксимациям.
При оценке полноты методов анализа следует также учитывать точность получаемых результатов. Количественные требования по точности результатов анализа могут предъявляться только к средствам обнаружения ошибок и только с указанием набора тестовых программ. Для рассматриваемых методов будут даваться качественные оценки точности в сравнении с другими методами. При формировании этих оценок будут учитываться упрощения и неточности методов за счет применяемых аппроксимаций.
Представление объектов и функций Pthreads в модели программы
Подходы на основе извлечения инвариантов являются достаточно перспективными и широко используются в качестве дополнения к классическим алгоритмам статического анализа и как самостоятельные подходы. Извлекаемые инварианты содержат информацию о состояниях отдельных объектов программы, зависимостях между объектами программы, а также связях между состояниями объектов и входными данными или результатами работы программы. Конкретные инварианты выполняются (являются верными) для некоторых частей или всей программы. Обычно рассматривают инварианты, которые выполняются для конструкций программы или для конструкций программы с учетом их контекстов.
В работе [44] решается задача обнаружения ошибок типа Race Condition в многопоточных программах на языке С. Для этого, предлагается определять для каждого разделяемого объекта е, объект (объекты) синхронизации, под защитой которого выполняются все операции с е (инвариант Consistent Correlation). Если каждого разделяемого объекта имеется хотя бы один такой объект синхронизации, то программа не содержит ошибок типа Race Condition.
Извлечение данного инварианта выполняется на основе системы типов и эффектов. Формируется набор ограничений, которые преобразуются в форму позволяющую выводить Consistent Correlation. Эффекты используются для определения связи указателя на объект синхронизации и самого объекта - определяются указатели, которые могут указывать на несколько объектов синхронизации. Для каждой точки программы вычисляется консервативный набор захваченных объектов синхронизации (в местах слияния выполняется пересечение этих наборов). Утверждается, что анализ является полным для всего множества конструкций языка С. Развитие данного средства и результаты экспериментальных исследований приводятся в работе [45] В работе [52] предлагается подход, позволяющий обнаруживать ошибки типа Race Condition в программах на языке С, использующих синхронизацию на основе семафоров. Основной идеей предлагаемого подхода является вычисление прав доступа к объектам программы в каждом выражении и использование этой информации для обнаружения ошибок. Права доступа определяют возможность чтения или изменения значения объекта в данной конструкции программы. При операциях с объектами синхронизации, права доступа к различным объектам переходят от одного потока к другому. При этом должно выполняться ограничение на сумму прав доступа к некоторому объекту во всех параллельно выполняющихся конструкциях. Нарушение данного ограничения свидетельствует о наличии ошибки типа Race Condition.
Предложенный подход использует систему типов и эффектов, для определения состояния программы в каждой точке. Реализация алгоритма использует внешний анализ указателей на объекты и функции, а также внешний алгоритм определения разделяемых объектов (Escape-анализ). Основными недостатками являются: невозможность анализа динамически порождаемых потоков и нерешенные вопросы, связанные с анализом циклов, содержащих конструкции синхронизации.
Подходы, которые предлагаются в работах [44], [45] и [52], не являются достаточно универсальными — извлекаемые инварианты не могут использоваться для обнаружения программных дефектов.
В работе [30] предлагается алгоритм анализа указателей для многопоточных С программ. В основе предлагаемого алгоритма лежит извлечение ресурсных инвариантов, связанных с объектами синхронизации. Ресурсный инвариант представляет собой область динамической памяти, операции с которой выполняются в разных потоках под защитой объекта синхронизации, а также возможные значения, которые могут принимать ячейки в этой области памяти. Извлечение указанных инвариантов производится автоматически, путем итеративного анализа конструкций отдельных потоков программы. В работе доказано, что такой анализ сходится и позволяет определить все инварианты, имеющиеся в программе. Данный подход использовался для анализа драйверов ОС Windows. Рассмотренный подход имеет существенные ограничения на подмножество поддерживаемых конструкций языка С и не может применяться для анализа широкого класса многопоточных программ.
В данной работе используются инварианты, содержащие информацию о линейных зависимостях между объектами программы [65]. Извлекаемые инварианты используются для повышения точности алгоритма анализа указателей и алгоритма интервального анализа.
В настоящее время активно развиваются подходы, основанные на преобразовании многопоточной программы к последовательному виду и дальнейшем анализе полученной последовательной программы с помощью известных алгоритмов.
Одной из первых работ в данном направлении является [46]. В этой работе предлагается заменять анализ параллельных потоков на анализ путей в последовательной программе. Для этого в последовательную программу вносятся искусственные конструкции, эмулирующие недетерминизм выполнения потоков параллельной программы, с учетом выбора, приостановки и завершения потока. Недетерминизм параллельной программы представляется с помощью недетерминированных переходов в последовательной программе, что приводит к получению всех возможных последовательностей выполнения конструкций в различных потоках. В данной работе рассматривается обнаружение ошибок типа Race Condition. Для этого в полученную последовательную программу автоматически вносятся конструкции assert. В конструкциях assert проверяется возможность влияния других потоков на переменную, над которой выполняется операция в некотором потоке программы.
В работе [35] предлагается способ преобразования параллельной программы, использующей разделяемую память, к последовательной программе. Данное преобразование выполняется при ограничении на число переключений контекстов (см. раздел 1.3). Симуляция переключения контекстов в многопоточной программе выполняется за счет использования копий разделяемых объектов программы — по одной копии для каждого переключения контекста. При анализе некоторого оператора программы рассматриваются возможные варианты значений из разных копий разделяемых объектов. В качестве примера приводятся алгоритмы анализа для некоторых классов программ (Boolean programs, Pushdown systems). Одним из недостатков данного подхода является невозможность анализа динамически создаваемых потоков.
В работе [36] предлагается подход, обеспечивающий автоматическое обнаружение ошибок синхронизации в программах на языке С. Предлагаемый подход состоит из трех основных стадий: упрощение исходной параллельной С программы за счет декомпозиции сложных конструкций в наборы более простых; преобразование параллельной программы в последовательную программу с учетом всех возможных вариантов выполнения исходной программы; автоматическая генерация условий и проверка этих условий с помощью SMT-решателя (Satisfiability Modulo Theories solver).
Алгоритм определения состояний объектов синхронизации
При создании потока в конструкции create множество действий в новом потоке пусто. В приведенных правилах, вместо пустого множества, множество действий содержит значение, не влияющее на состояния объектов синхронизации (см. раздел 3.3).
После завершения ожидаемого потока в конструкции join действия над семафорами, выполненные в данном потоке, необходимо учесть при дальнейшем анализе. В правиле для конструкции join выполняется сложение множеств действий для семафоров с помощью введенной операции :
Операция выполняется над множествами действий, результатом этой операции являются все возможные суммы из действий каждого множества.
В правиле для конструкции join необходимо учитывать действия только для семафоров, так как на момент завершения потока все мьютексы, заблокированные в данном потоке, должны быть освобождены. Завершение потока программы с заблокированным мьютексом является ошибкой. Обнаружение подобных ошибок рассматривается в главе 4.
Для конструкций lock, unlock правила выглядят следующим образом (обозначения блоков приведены на рис. 3.6):
Конструкции lock и unlock устанавливают новое значение действия над мьютексом. Конструкции wait и post соответственно уменьшают или увеличивают текущие значения действий над семафором. S/1
Алгоритм определения множества действий является полным (обеспечивает получение полных результатов) при условии полноты основных алгоритмов анализа. Полнота алгоритма определения множества действий означает, что этот алгоритм позволяет определить все возможные действия для объектов синхронизации в каждой точке программы. Полнота алгоритма определения множества действий обеспечивается используемыми правилами. В правиле для оператора ветвления входное множество действий распространяется в обе ветки без изменений. В правиле для -функции выполняется объединение множеств действий со всех входов. В правиле для конструкции join выполняется формирование всех возможных сумм из множеств действий.
Результаты основных алгоритмов статического анализа используются для идентификации объектов синхронизации и объектов-потоков. При идентификации объектов синхронизации, используемых в конструкциях синхронизации, может быть получен не один а несколько объектов (причиной этого являются неточности основных алгоритмов статического анализа). В этом случае, анализ конструкции синхронизации выполняется для всех полученных объектов - такая конструкция может быть представленная с помощью нескольких конструкций. Пример представления конструкции wait(m), в которой т может указывать на два объекта синхронизации тх и т2, приведен на рис. 3.8 (в операторе if используется неопределенное условие, 3/ - состояние программы перед конструкцией wait(m) ).
Анализ конструкции синхронизации с несколькими объектами Анализ конструкций синхронизации для всех возможных объектов обеспечивает сохранение полноты результатов основных алгоритмов анализа. Правила 10 и 11 алгоритма определения действий над объектами синхронизации выполняются для всех объектов синхронизации, на которые может указывать т . То же касается и потоков программы. В случае если определено несколько потоков, связанных с t, то в конструкции join(t) может быть несколько входящих дуг синхронизации из конструкций eot разных потоков. Правило 8 данного алгоритма выполняется для всех объектов-потоков, на которые может указывать t. Ситуация с ожиданием разных потоков в конструкции join, обеспечивает сохранение полноты, но приводит к потере точности (ни один из ожидаемых потоков не может считаться завершенным после конструкции join). На практике операции с объектами синхронизации и объектами-потоками являются достаточно «консервативными», что в большинстве случаев позволяет определять единственный объект для каждой конструкции синхронизации. Правила других алгоритмов анализа параллельного выполнения программы также применяются для всех полученных объектов синхронизации и объектов-потоков. Отметим, что все приведенные правила являются монотонными. Свойство монотонности можно определить следующим образом: состояние программы и информация о параллельном выполнении программы на входе конструкции, для которой выполняется правило F(X). Результат выполнения правила F(X) — состояние программы и информация о параллельном выполнении программы на выходе соответствующей конструкции. Доказательство монотонности правил алгоритма определения действий над объектами синхронизации не приводится в силу его очевидности. Свойство монотонности используется для доказательства сохранения полноты основных алгоритмов статического анализа (см. раздел 3.7).
Задача построения допустимых комбинаций сводится к задаче определения одновременной достижимости конструкций в параллельных потоках программы. Поэтому получение полных и точных результатов при построении допустимых комбинаций в общем случае невозможно [18]. Рассмотрим несколько способов (аппроксимаций) построения множества допустимых комбинаций для блоков произвольной многопоточной программы, обладающих приемлемой вычислительной сложностью. Каждый из рассматриваемых способов обеспечивает получение полных результатов (построение всех допустимых комбинаций), но при этом не обеспечивает получение точных результатов (некоторые из построенных комбинаций могут оказаться ложными).
Правила обнаружения ошибок работы с буферами
Докажем это утверждение. Сначала докажем, что выполнение используемых алгоритмов анализа без итеративного алгоритма (без повторного анализа конструкций) завершается за конечное число операций.
Анализ конструкций произвольного потока выполняется последовательно, в соответствии с порядком следования этих конструкций в графе потока управления. Любая достижимая конструкция программы анализируется ровно один раз в каждом контексте выполнения (стеке вызовов функций) и при каждом наборе итераций циклов. Любое из используемых правил требует выполнения конечного числа операций, не зависимо от анализируемой конструкции и всей программы в целом, при условии конечного числа анализируемых межблоковых конструкций программы (см. разделы 3.2, 3.3, 3.4 и 3.5). Таким образом, если число анализируемых конструкций программы (в том числе межблоковых конструкций) является конечным, то анализ завершается за конечное число операций.
Конечность числа анализируемых конструкций обеспечивается для программ, в которых отсутствуют незавершимые циклы и рекурсии на любом наборе входных данных — такие программы относятся к классу завершимых программ. Конечность числа анализируемых конструкций для незавершимых программ обеспечивается за счет использования различных аппроксимаций. Примерами таких аппроксимаций являются: ограничение числа итераций при анализе циклов, ограничение глубины стека вызовов при анализе рекурсивных функций и др. Эти и другие аппроксимации применяются при статическом анализе многопоточных программ.
Теперь докажем, что при порождении для ограничения числа анализируемых конструкций, для ограничения количества анализируемых объектов, а также размеров и набора возможных значений этих объектов. Подробное рассмотрение подобных аппроксимаций выходит за рамки данной работыцепочек повторно анализируемых конструкций анализ также завершается за конечное число операций. Все правила основных алгоритмов анализа и алгоритмов анализа параллельного выполнения являются монотонными. Правила алгоритмов анализа параллельного выполнения, в том числе, правило для анализа у/-функции, также являются монотонными по отношению к используемым данным из других потоков. Поэтому, при каждом повторном анализе конструкции программы состояние программы и информация о параллельном выполнении на выходе этой конструкции по крайней мере не уменьшаются. Порождение цепочек повторно анализируемых конструкций происходит только при увеличении состояния программы и/или информации о параллельном выполнении программы. Распространение повторно анализируемых цепочек на другие потоки также выполняется при увеличении состояния программы и/или отношений параллельности и синхронизации. Так как число объектов программы, число возможных значений этих объектов, а также число возможных отношений параллельности и синхронизации является конечным, то число повторно анализируемых конструкций также является конечным. Утверждение доказано.
Разработанные методы анализа параллельного выполнения программы обеспечивают сохранение полноты результатов в следующем смысле. При использовании полных основных алгоритмов анализа совместно с разработанными методами для произвольной многопоточной программы, либо обеспечивается получение полных результатов, либо анализ не завершается. Основные алгоритмы анализа являются полными, если для произвольной последовательной программы эти алгоритмы, либо обеспечивают получение полных результатов, либо анализ не завершается.
При анализе завершимых программ свойство сохранения полноты результатов можно сформулировать следующим образом.
При использовании основных алгоритмов анализа, обладающих полнотой, совместно с методами анализа параллельного выполнения, для завершимой многопоточной программы обеспечивается получение полных результатов.
Докажем это утверждение. Сначала докажем утверждение для программ с единственным порядком выполнения, которые не содержат конструкций типа state. Для таких программ существует последовательность анализа конструкций, обеспечивающая получение полных результатов (повторный анализ конструкций не требуется) [34].
Анализ конструкций первого блока программы и межблоковой конструкции после него обеспечивает получение полных результатов (используются основные алгоритмы обладающие полнотой). Докажем, что анализ конструкций блока Sj и межблоковой конструкции после него обеспечивает получение полных результатов, при условии, что в результате анализа предшествующих блоков у-го потока и блоков, выполняющихся строго до блока Sj в других потоках, получены полные результаты, а также построены все отношения параллельности и синхронизации при анализе межблоковой конструкции sx перед Sj .
Состояние программы на входе блока Sj является полным. Это обеспечивается анализом межблоковой конструкции sx перед этим блоком (см. рис. 3.39).
