П. С. Андрианов, В. С. Мутилин, А. В. Хорошилов. Метод легковесного статического анализа для поиска состояний гонок



Pdf просмотр
страница1/3
Дата18.11.2016
Размер0.92 Mb.
Просмотров728
Скачиваний0
  1   2   3

П.С. Андрианов, В.С. Мутилин, А.В. Хорошилов. Метод легковесного статического анализа для поиска состояний гонок.
Труды ИСП РАН, том 27, вып. 5, 2015 г., с. 87-116 87
Метод легковесного статического анализа
для поиска состояний гонок
1

1
П.С. Андрианов
1
В.С. Мутилин
1,2,3,4
А.В. Хорошилов
1
Институт системного программирования РАН,
109004, Россия, г. Москва, ул. А. Солженицына, дом 25
2
Московский государственный университет имени М.В. Ломоносова,
119991, Россия, Москва, Ленинские горы, д. 1.
3
Московский физико-технический институт (государственный университет),
141700, Россия, Московская облаcть, г. Долгопрудный, Институтский пер., 9
4
Национальный исследовательский университет «Высшая школа экономики»
101000, Россия, Москва, ул. Мясницкая, д.20
Аннотация. В этой статье представлен подход легковесного статического анализа для поиска состояний гонок, названный CPALockator. Он учитывает такую специфику ядер операционных систем, как сложный параллелизм и особые примитивы синхронизации.
Метод основан на алгоритме Lockset, но использует две эвристики, которые призваны уменьшить количество ложных предупреждений: модель памяти и модель параллелизма. В качестве примитивов синхронизации рассматриваются блокировки.
Основным предметом нашего исследования являются ядра операционных систем, но предложенный подход может быть применен также и для других программ. Метод основан на идее адаптивного статического анализа (Configurable Program Analysis,
CPA) и реализован в инструменте CPAchecker. Реализация метода состоит из двух стадий: сначала определяется множество разделяемых переменных для каждой точки программы, затем производится анализ примитивов синхронизации. На второй стадии собирается информация о всех возможных доступах к разделяемым переменным и захваченных примитивах синхронизации. После этого создается отчет, содержащий предупреждения для тех переменных, для которых было найдено хотя бы два доступа, образующие потенциальное состояние гонки. Для каждого доступа приводится один из возможных путей выполнения программы, который ведет к нему. Инструмент был апробирован на ядре операционной системы реального времени объемом приблизительно 200 000 строк кода. Он позволил найти 20 новых состояний гонки, признанных разработчиками. Кроме того, был произведен пилотный запуск инструмента на драйверах операционной системы Linux с помощью инфраструктуры
1
Исследование проводилось при финансовой поддержке РФФИ в рамках проекта №13-01-00694
P.S. Andrianov, V.S. Mutilin, A.V. Khoroshilov
. Lightweight Static Analysis for Data Race Detection in Operating
System Kernels. Trudy ISP RAN/ Proc. ISP RAS, vol. 27, issue 5, 2015, pp. 87-116 88 инструмента LDV, который использовался для подготовки заданий для инструмента
CPALockator. Дальнейшим направлением исследований является разработка более точной модели потоков, интеграция с более точными тяжеловесными техниками анализа.
Ключевые слова: статический анализ, состояние гонки, ядро операционной системы, разделяемые данные.
DOI: 10.15514/ISPRAS-2015-27(5)-6
Для цитирования:
Андрианов П.С., Мутилин В.С., Хорошилов А.В. Метод легковесного статического анализа для поиска состояний гонок.
Труды ИСП РАН, том
27, вып. 5, 2015 г., стр. 87-116. DOI: 10.15514/ISPRAS-2015-27(5)-6.
1. Введение

Несмотря на большой прогресс в области верификации программного обеспечения, ошибки, связанные с параллельным выполнением кода остаются одними из наиболее труднообнаруживаемых. Более того, такие ошибки довольно многочисленны, например, в среднем они составляют около 20% от всех ошибок в файловых системах ядра операционной системы Linux [1].
Наиболее частыми причинами ошибок, связанных с параллельным выполнением ядра операционной системы, являются состояния гонки, при которых происходит одновременный доступ к разделяемым данным из нескольких потоков. В частности анализ исправлений за год разработки ядра
Linux показал, что ошибки, связанные с состояниями гонки, образуют наиболее многочисленный класс и составляют 17% от всех типичных ошибок
[2].
Существуют два пути для поиска состояний гонки автоматически: динамический анализ и статический анализ. Техники динамического анализа позволяют получить относительно небольшой процент ложных срабатываний.
Примерами инструментов, реализующих методы динамического анализа, являются Eraser [3], RaceHound [4] и DataCollider [5]. Они способны находить потенциальные состояния гонки только на тех путях выполнения программы, которые происходят в течение реального исполнения. Состояние гонки определяется двумя практически одновременными доступами к одним и тем же данным, что усложняет ее обнаружение. Инструменты, которые используют методы на основе векторных часов, могут работать с двумя разнесенными во времени доступами к памяти, но они чувствительны к порядку операций. Кроме того, известно, что значительную часть путей исполнения программы достаточно сложно воспроизвести в тестовом окружении.
Методы статического анализа имеют свои проблемы. Тяжеловесные техники достаточно точны, но требуют большого количества времени для анализа. В случае задачи поиска гонок общее число мест, где может возникнуть состояние гонки, слишком велико. Проводились некоторые эксперименты по

П.С. Андрианов, В.С. Мутилин, А.В. Хорошилов. Метод легковесного статического анализа для поиска состояний гонок.
Труды ИСП РАН, том 27, вып. 5, 2015 г., с. 87-116 89 верификации модулей ядра, и результаты показали, что тяжеловесный подход не масштабируется[6]. Происходит комбинаторный взрыв состояний, поэтому даже для небольших модулей количество затраченного времени и памяти было гигантским.
Методы легковесного статического анализа, например, метод, реализованный в инструмента Locksmith [7], работают очень быстро, но число ложных срабатываний обычно бывает очень велико. Для инструмента Locksmith средний процент ложных сообщений об ошибках составляет 73% на некоторых POSIX приложениях и около 96% на нескольких драйверах [8].
Существующие методы не принимают во внимание некоторую специфику ядра операционной системы, описанную ниже, поэтому большинство драйверов и особенно ядро само по себе анализировать существующими инструментами, предназначенными для пользовательских приложений, очень сложно.
Параллелизм в ядрах операционных систем устроен сложным образом, так как они являются асинхронными. Многие функции ядра могут быть выполнены параллельно друг с другом, и определить, когда начинается параллельное исполнение, очень сложно. Кроме того в ядрах операционных систем используются дополнительные примитивы синхронизации, такие как отключение прерываний или планирования. Еще одна важная особенность — это активное использование адресной арифметики. Как результат, поиск состояний гонок в ядрах операционных систем является более сложной задачей, чем в пользовательских приложениях.
В этой статье мы предлагаем новый метод легковесного статического анализа для обнаружения состояний гонок, названный CPALockator. Он может легко масштабироваться на большие объемы исходного кода, оставляя процент ложных срабатываний на приемлемом уровне и принимая во внимание специфику ядра операционной системы.
Оставшаяся часть статьи организована следующим образом. В разделе 2 даются необходимые определения. В разделе 3 описывается основная идея предложенного метода. После этого рассказывается о подходе адаптивного статического анализа. Реализация метода обсуждается в разделе 5.
Следующий раздел посвящен интеграции в систему LDV [12]. В разделе 7 мы рассказываем о полученных результатах, потом в разделе 8 — о близких работах. В заключении кратко описываются планы на будущее.
2. Определения
В этой статье термин поток используется, чтобы обозначить независимый поток выполнения инструкций в ядре операционной системы, например, прерывание от аппаратуры или выполнение системных вызовов от имени пользовательского потока. Если некоторый системный вызов может быть
P.S. Andrianov, V.S. Mutilin, A.V. Khoroshilov
. Lightweight Static Analysis for Data Race Detection in Operating
System Kernels. Trudy ISP RAN/ Proc. ISP RAS, vol. 27, issue 5, 2015, pp. 87-116 90 прерван прерыванием от аппаратуры, мы считаем, что этот системный вызов и прерывание могут выполняться параллельно друг с другом.
Блокировка
— это объект, использующийся для предотвращения одновременного доступа к памяти. Если некоторая блокировка захвачена из одного потока, то другой поток, пытающийся захватить ту же самую блокировку, не может продолжить свое выполнение до тех пор, пока блокировка не будет освобождена. Типичными примерами блокировок могут быть мьютексы и спинлоки. Мы считаем такие примитивы синхронизации ядра, как отключение прерываний или планирования, специальными блокировками. Например, функция
¡
¢
£
¤
¡
¥
¦
§
¨
©


отключает планирование и тем самым запрещает любое параллельное исполнение, поэтому мы считаем, что воображаемая глобальная блокировка
¡
¢
£
¤
¡
¥
¦
§
¨
©
захвачена. Некоторые блокировки могут быть захвачены несколько раз, в этом случае имеет место рекурсивный захват блокировки.
Разделяемые данные — это область памяти, которая доступна из нескольких потоков. В языке Си разделяемые данные представлены глобальными переменными и указателями на память, доступную из нескольких потоков через корректные конструкции языка Си. Важно отметить, что разделяемость данных является характеристикой, зависящей от времени. Локальные данные могут стать разделяемыми в некоторой точке программы и вернуть статус локальности позже.
Использование данных — чтение или запись данных.
Состояние гонки — это ситуация, при которой происходят два неупорядоченных использования одних и тех же разделяемых данных и по крайней мере одно из них является записью. Состояние гонки не всегда приводит к ошибке (так называемое доброкачественное состояние гонки), но является симптомом ее.
3. Легковесный метод для поиска состояний гонки
Метод CPALockator основан на алгоритме Lockset [3], который строит множество C(v) потенциальных блокировок для каждой разделяемой ячейки памяти v. Это множество содержит в себе те блокировки, которые защищают v для дальнейших действий. Блокировка l находится в C(v) в текущий момент времени, если для каждого потока доступ к v всегда происходил при захваченной блокировке l. C(v) инициализируется всеми возможными блокировками. Когда происходит доступ к данным, C(v) обновляется, как пересечение C(v) и того множества блокировок, которые захвачены на данный момент в текущем потоке. Если C(v) становится пустым, имеет место потенциальное состояние гонки.
Чтобы задать алгоритм поиска состояний гонок мы должны ответить на следующие вопросы:

Когда начинается параллельное исполнение?

П.С. Андрианов, В.С. Мутилин, А.В. Хорошилов. Метод легковесного статического анализа для поиска состояний гонок.
Труды ИСП РАН, том 27, вып. 5, 2015 г., с. 87-116 91

Что такое данные?

Какие данные считаются одинаковыми?

Что такое блокировки и какие существуют правила для операций с ними?

Какие блокировки считаются одинаковыми?
Инструмент динамической верификации Eraser, который первым реализовал
Lockset, использует точки создания потоков, чтобы определить, когда начинается параллельное выполнение. Для ядра операционной системы определить, когда начинается параллельное выполнение, достаточно сложно.
Мы считаем, что каждый системный вызов или обработчик прерывания может выполняться параллельно с любым другим, включая себя. В реальности взаимосвязь между ними более сложная. Модель потоков в методе
CPALockator представлена функцией main, которая содержит вызовы всех системных вызовов и обработчиков прерываний.
Eraser оперирует ячейками памяти при реальном выполнении. Метод
CPALockator считает все переменные и поля структур единицей данных по умолчанию. Существуют ситуации, в которых доступ к различным полям структур должен быть защищен блокировкой. Предположим, что у нас есть тип структуры, представляющий разделяемый связный список с полями next и prev. Пусть у нас есть два доступа: к полю next одной переменной этого типа и к полю prev другой переменной этого же типа. Все статические методы, оперирующие с ячейками памяти столкнутся с проблемой в этом случае, так как всегда очень сложно понять, что два различных указателя могут указывать на одну и ту же область памяти. В нашем методе мы имеем возможность считать этот случай двумя доступами к одним данным и выдать предупреждение об ошибке. Этот способ требует ручной аннотации, тем не менее достаточно прост в использовании. Подробнее он будет описан в
Разделе 5.3.
Так как Eraser оперирует ячейками памяти при реальном исполнении программы, то в нем данные считаются разделяемыми, если два доступа происходят по одному адресу. Статический инструменты, такие как Locksmith, строят граф потоков данных, чтобы определить, какие указатели указывают на одну и ту же память. Однако для ядра операционной системы сложно построить граф потоков данных из-за активного использования адресной арифметики и массивного параллелизма. Поэтому такой метод работает не так хорошо, как для пользовательских программ. В методе CPALockator равенство ячеек памяти следует только из синтаксических правил.
Глобальный указатель всегда считается указывающим на одну и ту же область памяти. Аналогичное предположение действует и для локального указателя в заданной функции. Считается, что два поля структуры указывают на одну область памяти, если совпадает тип структуры и имена полей. Важно отметить, что имена самих переменных в этом случае не учитываются. Так, если указатели на структуры A и B имеют одинаковый тип, доступы A->x и B-
P.S. Andrianov, V.S. Mutilin, A.V. Khoroshilov
. Lightweight Static Analysis for Data Race Detection in Operating
System Kernels. Trudy ISP RAN/ Proc. ISP RAS, vol. 27, issue 5, 2015, pp. 87-116 92
>x будут рассматриваться, как доступы к одной и той же памяти. Если структуры A и B не связаны друг с другом, это предположение приведет к ложному сообщению об ошибке. На практике из-за этой эвристики происходит 18% всех ложных предупреждений.
Eraser рассматривает блокировки, как объект, который может быть захвачен.
Он поддерживает только две операции с ним: захват и освобождение. Метод
CPALockator позволяет описать блокировку: задать функции захвата и освобождения
(возможны несколько вариантов), их аргументы, рекурсивность. Равенство блокировок следует из равенства имен объектов
(переменных) в обоих методах.
4. Адаптивный статический анализ
Для реализации метода CPALockator был выбран инструмент адаптивного статического анализа CPAchecker (Configurable Program Analysis, CPA) [10].
Он позволяет комбинировать различные техники анализа, встраивать дополнительные подходы, такие как CEGAR, BMC. В этом заключается одно из важных отличий описываемого метода от существующих техник легковесного анализа. Рассмотрим кратко теорию адаптивного статического анализа.
Адаптивный статический анализ может быть составлен из нескольких алгоритмов, предлагающих различные типы анализа. Кроме того, возможна дополнительная настройка алгоритмов путем выбора оператора слияния и способа проверки необходимости завершения анализа.
Адаптивный статический анализ (

,

¦

¥

©
,

©

©
,
¥



) состоит из абстрактного домена

, отношения переходов

¦

¥

©
, оператора слияния

©

©
и оператора останова
¥



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

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

¦

¥

©
определяет для каждого состояния e потенциальные следующие абстрактные состояния {e'}, для которых каждый переход помечен соответствующей дугой графа потока управления (ГПУ).
Оператор

©

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

П.С. Андрианов, В.С. Мутилин, А.В. Хорошилов. Метод легковесного статического анализа для поиска состояний гонок.
Труды ИСП РАН, том 27, вып. 5, 2015 г., с. 87-116 93
Оператор
!
"
#
проверяет, является ли текущее состояние покрытым данным множеством уже проанализированных состояний. Он определяет, когда анализ пути завершается в текущей вершине. В классических легковесных подходах останов происходит когда полученное абстрактное состояние не содержит новых конкретных, то есть достигнута неподвижная точка. В тяжеловесных техниках останов происходит, в случае если множество конкретных состояний полученного абстрактного состояния является подмножеством множества конкретных состояний, соответствующих некоторому уже проанализированному абстрактному состоянию.
Рис. 1. Пример дерева конфигураций CPA
Рассмотрим пример дерева конфигурации CPA. В нем изображены три анализа. Основным является CompositeCPA. Он включает в себя LocationCPA и CallstackCPA.
Состнояние LocationCPA содержит в себе вершину ГПУ, то есть номер строки с исходным кодом. Таким образом, его абстрактный домен является множеством всех возможных вершин ГПУ. Оператор
!
$
%
&
'
(
$
меняет номер строки текущего состояния на номер строки вершины, в которую входит соответствующая дуга. Для этого анализа оператор
)
(
$
0
(
никогда не объединяет состояния. Останов происходит только если состояние уже было проанализировано ранее.
Состояние CallstackCPA состоит из стека вызовов функций. В случае если вызывается новая функция, ее имя помещается на вершину стека. Когда производится возврат, имя функции удаляется из стека. Это описание работы оператора перехода. Операторы stop и merge такие же, как и для предыдущего анализа.
Задача CompositeCPA — объединение анализов, описанных выше. Ее абстрактный домен является декартовым произведением доменов LocationCPA и CallstackCPA. Оператор перехода CompositeCPA вызывает операторы переходов вложенных анализов. Сначала он получает новое состояние от
LocationCPA, затем — от CallstackCPA и объединяет их вместе. Это объединение состояние является новым состоянием CompositeCPA.
P.S. Andrianov, V.S. Mutilin, A.V. Khoroshilov
. Lightweight Static Analysis for Data Race Detection in Operating
System Kernels. Trudy ISP RAN/ Proc. ISP RAS, vol. 27, issue 5, 2015, pp. 87-116 94 1
©

©
и
¥



операторы также объединяют соответствующие операторы вложенных анализов. Для того, чтобы объединить два состояния
CompositeCPA, нужно сначала объединить состояния LocationCPA, которые включены в данные состояния CompositeCPA, а потом — состояния
CallstackCPA. Оператор stop работает похожим образом: если все вложенные
CPA решают остановить анализ, CompositeCPA также останавливает его.
Рассмотрим, как такая композиция CPA анализирует простую программу (Рис.
2). На рисунке 3 изображен абстрактный граф достижимости для этой программы.
Рисунок 2 — Пример программы
Рисунок 3 — Пример анализа. Первое число в
скобках представляет собой состояние
LocationCPA (номер строки) и затем идет
стек вызовов функций
Инструмент начинает из функции

¦
¡

, затем он анализирует функцию

, после этого — переходит в функцию

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

П.С. Андрианов, В.С. Мутилин, А.В. Хорошилов. Метод легковесного статического анализа для поиска состояний гонок.
Труды ИСП РАН, том 27, вып. 5, 2015 г., с. 87-116 95
Классические анализы, реализующие подход
CPA решают задачу достижимости, то есть, доказывают достижимость некоторой метки в программе (вызова функции и т.п.). Состояние гонки характеризуется двумя точками и для того, чтобы пойти по пути классических анализов, нужно было бы определить состояние нашего анализа, как декартово произведение состояний в двух потоках, то есть получить семантику чередования (англ. interleaving). Мы же используем модульную абстракцию для описания взаимодействия нескольких потоков.
Этот подход предполагает использование упрощенной модели взаимодействия потоков.
При необходимости эта модель может быть уточнена, но так как в текущем варианте анализа не учитываются условия, то взаимодействие потоков не может быть учтено ни при какой его модели.
5. Реализация
Реализация метода CPALockator состоит из двух этапов. Сначала определяются разделяемые данные, затем для каждого использования разделяемых данных сохраняется множество захваченных блокировок. На рисунке 4 представлены эти этапы.
Рисунок 4 — Этапы CPALockator
Конфигурация CPA для Анализатора разделяемых данных состоит из функций, предоставляющих локальные данные, например,
2 3
4 4
5 2
,
6 3
4 4
5 2
и др. Мы предполагаем, что указатели, возвращаемые этими функциями,
P.S. Andrianov, V.S. Mutilin, A.V. Khoroshilov
. Lightweight Static Analysis for Data Race Detection in Operating
System Kernels. Trudy ISP RAN/ Proc. ISP RAS, vol. 27, issue 5, 2015, pp. 87-116 96 указывают на локальные данные, которые не могут быть разделяемыми в соответствующей точке программы. Конфигурация для Анализатора блокировок включает в себя описание блокировок и аннотации, которые описываются в секции 5.3.
5.1 Конфигурация СPA для Анализатора разделяемых
данных
Анализатор разделяемых данных используется для формирования списка разделяемых переменных для каждой точки программы (см. Рис 5).
Рисунок 5 — Конфигурация Анализатора разделяемых данных
BAMCPA (Block Abstraction Memorization) [11] отвечает за модульность анализа. Если функция была уже проанализирована с некоторым состоянием до текущего вызова и было сохранено множество конечных состояний, то она не анализируется еще раз, а используются сохраненные состояния. Мы добавили в оригинальный BAMCPA возможность обработки рекурсии и некоторые способы для взаимодействия BAMCPA и наших новых CPA.
ARGCPA
(Abstract
Reachability
Graph)
отвечает за возможность восстановления пути из любого состояния до начального. Он хранит для каждого состояния множество предыдущих и последующих, и предоставляет эти данные для обхода и восстановления пути.
CompositeCPA, LocationCPA и CallstackCPA были уже описаны.
LocalCPA отвечает за определение локальности всех переменных, доступных в данной точке программы. Отдельну следует отметить, что под переменными мы также понимаем указатели, то есть, анализ также учитывает информацию о том, куда они указывают. Оператор перехода

¦

¥

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

П.С. Андрианов, В.С. Мутилин, А.В. Хорошилов. Метод легковесного статического анализа для поиска состояний гонок.
Труды ИСП РАН, том 27, вып. 5, 2015 г., с. 87-116 97 8
9
переностится на область памяти
8 3
. После присваивания считается, что a также указывает на разделяемую память. На точках объединения оператор merge объединяет результаты. В случае неопределенности всегда выбирается наихудший результат, то есть, статус shared. Рассмотрим следующий пример:
@
A
B
2 5
C
D
E
F
E
5
C
G
H
3
I
9
P
Q
R
S
T
R
H
3
I
2
P
Q
Если
9
указывает на локальные данные, а
2
— на разделяемые, то после анализа этого блока кода считается, что а указывает на разделяемые данные.
Результатом этого этапа анализа является список разделяемых переменных для каждой точки программы.

Каталог: proceedings -> docs
docs -> Статья рассказывает о проблемах совместимости и переносимости приложений
docs -> Перспективы виртуализации высокопроизводительных систем архитектуры x64
proceedings -> Архитектурные предпосылки к созданию однокристального многопроцессорного
proceedings -> Задача контроля качества при создании и развитии систем оптического распознавания печатного текста
docs -> О синтаксическом определении класса языков, распознаваемых недетерминированными машинами Тьюринга на логарифмической памяти


Поделитесь с Вашими друзьями:
  1   2   3


База данных защищена авторским правом ©nethash.ru 2019
обратиться к администрации

войти | регистрация
    Главная страница


загрузить материал