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


Конфигурация CPA для Анализатора примитивов



Pdf просмотр
страница2/3
Дата18.11.2016
Размер0.92 Mb.
Просмотров731
Скачиваний0
1   2   3
5.2 Конфигурация CPA для Анализатора примитивов
синхронизации
Анализатор блокировок используется для определения множества захваченных блокировок для каждого использования разделяемых данных, которые были представлены на предыдущем этапе анализа.

Рисунок 6 — Конфигурация Анализатора примитивов синхронизации
BAMCPA, ARGCPA, LocationCPA и CallstackCPA являются теми же самыми.
UsageCPA собирает статистику использования данных. Оператор transfer определяет переменные, использованные в выражении в некотором доступе к
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 98 данным, сохраняет стек вызовов и множество захваченных блокировок для каждого использования.
В конце анализа мы получаем информацию обо всех использованиях для каждой разделяемой переменной. Каждое использование состоит из:
• множества захваченных блокировок;
• стека вызовов функций;
• номера строки;
• типа дуги ГПУ (вызов функции, присваивание и т.д.);
• тип доступа (чтение или запись).
LockCPA следит за множеством захваченных блокировок. Его состояние содержит множество блокировок, которые были захвачены на текущем пути анализа. Для каждой блокировки содержится информация о:
• имя блокировки;
• счетчик рекурсивного захвата;
• стек вызовов функций.
Оператор перехода меняет состояние, которое содержит множество захваченных блокировок. Когда вызывается функция захвата блокировки, соответствующая блокировка добавляется во множество или увеличивается счетчик, если она уже присутствует. При вызове функции освобождения функции счетчик уменьшается, а если он становится равным нулю, блокировка удаляется из множества.
Состояния всех CPA в этой конфигурации никогда не объединяются. Анализ останавливается, если это состояние уже было проанализировано.
5.3 Аннотации
Аннотации используются для более точной настройки метода на специфический код. Всего есть три класса аннотаций:

Аннотации влияния функции на примитивы синхронизации.

Аннотации влияния функции на разделяемость данных.

Аннотации целевых данных.
Рассмотрим следующий пример для объяснения первого типа аннотации.
U
V
W



X
U
Y

¡
¥
`
¨

§
¦
¨
a

¡


©

X
¨

b c


d e

f


¡


©

g g
d
U
Y

¡
¥
`
¨

§
¦
¨
a

¡


©

X
h

¨

b c


d

П.С. Андрианов, В.С. Мутилин, А.В. Хорошилов. Метод легковесного статического анализа для поиска состояний гонок.
Труды ИСП РАН, том 27, вып. 5, 2015 г., с. 87-116 99 i
i
В этом примере увеличение разделяемого счетчика всегда происходит под блокировкой. В случае же локального указателя захват блокировки не нужен.
Наш анализ рассматривает четыре пути, так как для каждого из двух условных операторов анализируются ветви then и else. Два из этих путей оканчиваются с захваченной блокировкой, а оставшиеся два оканчиваются в состоянии с пустым множеством блокировок. Пара состояний с захваченной блокировкой является недостижимой, так как условия в условных операторах одинаковы.
Такие ситуации не так часто происходят, но каждая из них порождает значительное число ложных сообщений об ошибке, так как финальное состояние в функции с захваченной блокировкой сильно влияет на дальнейший пути анализа. Аннотации функций используются для того, чтобы разобраться с такими случаями. Это лишь способ подсказать анализу, что функция всегда освобождает или захватывает блокировку.
В приведенным выше примере достаточно добавить аннотацию, что функция f всегда освобождает блокировку.
Аннотации описывают функции в терминах состояний LockCPA. После того, как функция была проанализирована, состояние уточняется в соответствии с аннотацией.
В данный момент используется 4 типа аннотаций используются:

Захват блокировки — функция всегда захватывает блокировку.

Освобождение блокировки
— функция всегда освобождает блокировку.

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

Восстановление блокировки — функция может модифицировать множество блокировок, но все изменения будут забыты при выходе из функции.
К этому типу аннотаций можно добавить конфигурацию блокировок.
Поддерживается возможность определить функции захвата, освобождения и сброса, а также глубину рекурсивного захвата. Эти аннотации обрабатываются в LockCPA.
Следующий тип аннотаций описывает влияние на разделяемые данные.
Функция может вернуть разделяемые данные или инициализировать указатель, передаваемый, как аргумент, локальными данными. Также данные могут стать разделяемыми после вызова функции. Все эти случаи могут быть специфицированы аннотациями, чтобы повысить точность анализа. В данный момент поддерживаются только описание функций, возвращающих локальные данные. Эти аннотации обрабатываются в LocalCPA.
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 100
Третий тип аннотаций используется для установки равенства между переменными так, чтобы они рассматривались, как одинаковые данные. Это требуется, например, для списков, в которых элементы обычно имеют одинаковые имена next. Если не удается различить элементы различных списков, будет выдано большое количество ложных предупреждений, так как доступ к различным спискам может защищаться различными множествами блокировок. Поэтому мы связываем переменные, представляющие элементы списка, с самим списком. Для этой цели конфигурация содержит функции, которые используются для работы со списком. Например, выражение
©
7

©

p
¨
©

©



¨
¡
¥


связывает переменную e с переменной list, передаваемой как параметр. Эти аннотации обрабатываются в UsageCPA.
Для операционной системы реального времени, на которой метод был апробирован, было аннотировано около 2% функций, что в абсолютных величинах составило 90 функций.
6. Интеграция инструмента
Метод CPALockator был интегрирован в систему LDV (Linux Driver
Verification), разработанную в рамках проекта по верификации драйверов операционной системы Linux (см. Рис. 7) [12].

П.С. Андрианов, В.С. Мутилин, А.В. Хорошилов. Метод легковесного статического анализа для поиска состояний гонок.
Труды ИСП РАН, том 27, вып. 5, 2015 г., с. 87-116 101
Рисунок 7 — Интеграция с архитектурой LDV
Сначала подготавливается ядро операционной системы. В течение этой стадии вызовы компилятора заменяются на вызовы нашего инструмента для извлечения команд сборки. Затем поток команд сборки извлекается с помощью специальных скриптов. Этот поток передается в компонент DSCV
(Domain-Specific C Verifier). Он инструментирует исходный код, используя описания блокировок. Например, он заменяет макросы, используемые для захвата и освобождения блокировок на вызовы модельных функций, аннотированных в конфигурации. Это делается из-за того, что макросы могут быть развернуты в очень сложную последовательность команд, тогда как модельные функции анализировать значительно проще.
После этого включается модель окружения. Она представлена функцией main, содержащей системные вызовы и обработчики прерываний. Считается, что все они могут выполняться параллельно.
После всей подготовки исходный код анализируется нашим инструментом поиска гонок. Он генерирует отчет, содержащий список предупреждений с детальной информацией о каждом из них.
Для визуализации трасс ошибок используется другой компонент LDV. Когда инструмент генерирует предупреждение о состоянии гонки, оно должно быть показано пользователю. Более того, пользователь должен иметь возможность проверить, является ли это предупреждение истинной ошибкой или ложным предупреждением. Таким образом, необходимо представлять трассу ошибки и ее связь с исходным кодом. Состояние гонки характеризуется по крайней мере двумя использованиями с непересекающимися наборами блокировок.
Визуализированная трасса ошибки содержит стек вызовов функций для двух использований с точками захватов блокировок. Визуализатор преобразует данные, полученные от верификатора и связывает их с исходным кодом. Для представления результатов генерируется HTML отчет. Главная страница отчета содержит общую статистику (Таблица 1).
Табл. 1 — пример отчета для драйвера Linux floppy.ko
Статистика
Общая
Предупреждения
Глобальные:
195 29
Переменные 122 23
Указатели 73 6
Локальные:
3 0
Переменные 0 0
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 102
Указатели 3 0
Поля структур:
118 24
Переменные 105 24
Указатели 13 0
Всего:
316 53
На ней отображены общее число переменных для каждой из трех категорий: глобальные, локальные и поля структур. Во втором столбце указано число переменных, для которых были получены предупреждения. Обозначение
«Указатели» означает доступ по указателю, а «Переменные» — доступ к самой переменной. После этого идет список всех найденных блокировок.
После этого расположен список всех предупреждений, для каждого из которых содержится пара использований с непересекающимся множеством блокировок.
Пример выдаваемого предупреждения об ошибке представлен на рисунках 8-9.


П.С. Андрианов, В.С. Мутилин, А.В. Хорошилов. Метод легковесного статического анализа для поиска состояний гонок.
Труды ИСП РАН, том 27, вып. 5, 2015 г., с. 87-116 103
Рисунок 8 — Пример исходного кода. Параллельное выполнение print() и increase()
может привести к состоянию гонки
Рисунок 9 — Пример сообщения об ошибке. Трасса ошибки с точками захвата
блокировок и точками вызова функций, каждая из которых ссылается на
соответствующую строку исходного кода (см. рис. 8)
Еще раз подчеркнем, что мы используем модель параллелизма, и две функции, вызываемые из функции main, считаются выполняющимися параллельно.
Функция print печатает информацию о переменной
0
q
"
r
%
q
, а s
&
t
$
(
%
(
увеличивает ее значение под блокировкой. В таком примере возможно состояние гонки, потому что функция s
&
t
$
(
%
(
может записывать переменную одновременно с ее проверкой в функции
#
$
s
&
!
. Наш инструмент генерирует предупреждение для переменной
0
q
"
r
%
q с трассой ошибки, показанной на рисунке 9.
В первой строке указано общее число найденных использований. Только два из них визуализируются далее. Первое использование означает, что доступ к
0
q
"
r
%
q был в вызове функции. Второе происходит в присваивании при захваченной блокировке q
"
t u
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 104
Кроме того имеется опция для генерации покрытия исходного кода. Оно показывает код, который был проанализирован верификатором, и его связь с общим кодом ядра.
7. Результаты
Инструмент был применен для анализа операционной системы реального времени, которая уже была протестирована и находилась в использовании уже несколько лет. Общий объем кода был около 200 000 строк кода, но только 50 000 были проанализированы. Основной причиной является то, что не все возможные функции были включены в функцию main. Мы обнаружили 20 новых состояний гонки, которые были подтверждены разработчиками. Общее число предупреждений было 139. Без Анализатора разделяемых данных число предупреждений было 378. В данный момент большая часть ложных сообщений об ошибках происходит из-за неточности в анализе выражений.
Например, сейчас анализ не полностью поддерживает условные операторы.
Один запуск инструмента на машине с 6 Гб памяти и восьмиядерным процессором 2.80 ГГц занял 3 минуты на ядре описанной выше операционной системы. Кроме этого, был пробный запуск инструмента на ядре операционной системы Linux 3.8 на директории
¤
¡
v
©
¥
. Общее число проанализированных модулей было около 3500. Инструмент сообщил о 900 предупрежденях. Некоторые из них были проанализированы, и одна реальная ошибка была найдена, однако в текущей версии эта ошибка была уже исправлена.
8. Похожие работы
Мы не будем рассматривать методы динамического анализа, которые имеют свои преимущества. Также мы рассмотрим только методы анализа программ на языке Си.
8.1 Тяжеловесные техники анализа
Традиционно идеи тяжеловесных подходов применяются к небольшим программам. Зачастую в таких подходах предполагается, что взаимодействие между потоками производится только через глобальные переменные. Так как в реальных программных системах число предупреждений, которое приходится на поля структур, сопоставимо с предупреждениями, полученными для глобальных переменных, а иногда даже выше, то для нас было важно учитывать в анализе поля структур.
Еще одной важной особенностью тяжеловесных инструментов, нацеленных на анализ многопоточного программного обеспечения, в том, что они проверяют другое свойство, а именно свойство достижимости ошибочной метки в условиях параллельного окружения. Для того чтобы проверить наличие состояния гонки, необходимо дополнительно изощряться, чтобы записать это

П.С. Андрианов, В.С. Мутилин, А.В. Хорошилов. Метод легковесного статического анализа для поиска состояний гонок.
Труды ИСП РАН, том 27, вып. 5, 2015 г., с. 87-116 105 требование, как условие достижимости.
Например, после каждого присваивания в разделяемую переменную добавить проверку, что сейчас в данной переменной находится именно то, что мы только что туда записали.
Это значительно усложняет анализ. Более того, операции захвата и освобождения блокировки тоже могут быть представлены, как операции с переменными. Например, в инструменте ESBMC [13] моделирование примитивов синхронизации происходит с помощью конструкции assume(P), которая рассматривает пути выполнения программы, для которых в данный момент выполнен предикат P. Операция захвата блокировки m представляет собой атомарную последовательность assume(m==0); m=1. Моделирование захвата блокировки таким образом усложняет анализ, так как теперь приходится учитывать значение еще одной переменной.
Методы тяжеловесного анализа обыкновенно рассматривают все варианты параллельной работы программы, то есть анализируются возможные варианты переключений потоков (англ. interleavings). Одним из подходов является анализ параллельной композиции потоков, при котором так или иначе строится дерево достижимых состояний (ART), которые представляют собой произведение состояний каждого потока. Далее неизбежно возникает проблема комбинаторного взрыва, которую различные инструменты решают по-своему. Например, наблюдение, что состояние гонки проявляется уже при небольшом числе переключений контекста, позволило ограничить число переключений некоторым фиксированным K — подход, получивший название проверка моделей с ограниченным переключением контекста (англ. context- bounded model checking). Примерами инструментов, реализующих методы тяжеловесного анализа, могут быть ESBMC [13] и SATABS [14], которые используют различные подходы к анализу программ (BMC[15] и CEGAR [16,
17] соответственно)
В предыдущих инструментах число потоков было ограничено несколькими экземплярами и известно заранее. Однако большие программные системы, такие как ядро операционной системы, работают со значительно большим количеством потоков. Для анализа таких систем был предложен метод абстракции по счетчику состояний, который реализован, например, в инструменте Boom[18]. Идея метода заключается в том, чтобы рассматривать не состояния каждого потока, а количество потоков в том или ином состоянии.
Кроме того, были предложены такие оптимизации как символическое представление, то есть состояние локального потока описывается не конкретным значением, а некоторым символическим. Однако такой подход применим только в случае, если один и тот же код выполняется в несколько потоков. В сложных программных системах большая часть кода, выполняющегося параллельно, является уникальным.
Еще одним вариантом борьбы с большим пространством состояний является использование редукции частичных порядков.
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 106
Вторым большим классом тяжеловесных подходов является построение модульной абстракции, реализованное в инструменте Threader [19, 20, 21] или
BLAST[22]. Такие подходы не рассматривают все возможные чередования, а строят абстракцию взаимодействия между потоками. Сначала используется неточная модель, которая предполагает, что все потоки могут изменять любые разделяемые данные произвольным образом, затем эта модель уточняется в процессе анализа. Возможно уточнение как множества точек переключения контекста, так и влияния потоков друг на друга. Потенциально такой подход должен дать лучшие результаты нежели те, которые были получены для инструментов, типа ESBMC, однако разработчики приводят результаты только на тестах порядка нескольких сотен строк исходного кода, поэтому остаются вопросы о масштабируемости такого подхода.
Задача верификации многопоточных программ может решаться с помощью трансляции параллельной программы в последовательную с последующей ее верификацией с помощью существующих инструментов или какую-нибудь другую промежуточную форму, например, формулу, которая затем может быть проверена решателем. В основном, методы трансляции опираются на контекстно-ограниченную проверку моделей (англ. Context-Bounded Model
Checking [23, 24, 25, 26]) - подход к проверке многопоточных программ, при котором число активных потоков ограничивается некоторым числом в процессе верификации. Для преобразования параллельной программы фиксируется число возможных потоков n и число возможных переключений контекста K. Требуется построить такую последовательную программу, которая покрывала бы все возможные варианты выполнения n потоков, каждый из которых прерывался бы не более K раз.
Некоторые тяжеловесные инструменты предпочитают работать не с программой на языке Си, а на некотором более простом языке. В таком случае сначала применяется трансляция исходной программы в другой язык.
Например, для инструмента Storm [27] — это язык Boogie [28], в котором нет таких конструкций, как динамическое выделение памяти, арифметика указателей, преобразование типов. Параллельная программа преобразуется в последовательную, и для нее уже строятся формулы, которые проверяются с помощью SMT-решателя. Для моделирования переключения контекста используется понятие карты памяти, которое означает локальную копию всей памяти, занимаемой глобальными переменными. В данном подходе для каждого потока создается копия карты памяти. Переключение контекста моделируется переключением работы с одной картой памяти на другую. Все потоки выполняются один за другим. Для того чтобы повысить масштабируемость метода, применяется слайсинг по полям структур. Такая идея базируется на предположении, что для проверки конкретного свойства необходимо наблюдение за очень небольшим количеством полей. Построение множества отслеживаемых полей производится с помощью метода CEGAR.
Для верификации циклы разворачиваются на конечную глубину, что может

П.С. Андрианов, В.С. Мутилин, А.В. Хорошилов. Метод легковесного статического анализа для поиска состояний гонок.
Труды ИСП РАН, том 27, вып. 5, 2015 г., с. 87-116 107 привести к потере точности, а вызовы функций заменяются на их тела. Кроме того, принимается предположение о том, что в системных программах редко встречается рекурсия, чтобы можно было заменить вызов функции на ее тело.
В статье [24] авторы предлагают три варианта трансляции параллельной программы в логическую формулу.
Первый вариант - это метод Explicit Program Counter (EMC) [29], использование явного счетчика команд. В этом случае состояние программы включает в себя все локальные переменные и счетчик команд для каждого потока.
В возможных точках переключения контекста вставляется специальный оператор недетерминированного выбора, который выбирает поток для переключения и корректную строку кода, на которой закончилось его выполнение в прошлый раз. Это самый простой способ, но он требует много времени и памяти.
Второй вариант - Lal-reps(LR) [23]. В этом случае каждый поток символически выполняется независимо от других, с учетом того, что значения глобальных переменных могут измениться случайным образом. Задача упрощается тем, что заранее задается, когда происходит переключения контекста, а значит, задаются и точки, когда глобальным переменным присваиваются новые значения.
Третий вариант - LMP [30]. Его основное отличие от предыдущего подхода в том, что он присваивает глобальным переменным не случайные значения, а только те, которые возможны во время выполнения программы. После переключения контекста текущее локальное состояние потока сбрасывается, и чтобы его восстановить приходится заново исполнять поток из начального состояния с учетом того, что становятся известны значения глобальных переменных до переключения.
Попытки применения подхода с контекстно-ограничиваемыми проверками показали, что он плохо масштабируется и на реальных программах пока не может быть использован [27]. Авторы сравнивают свой способ верификации, основанный на генерации логических формул со способом логической проверки моделей, при котором все переменные программы преобразуются к бинарным, для которых уже генерируются формулы для проверки решателем
[31]. Такой подход, например, использован в статье [18]. Эксперименты показали, что эти две парагдимы сильно отличаются, и для них нужны различные способы трансляции. LR - лучший способ для проверки логических формул. Что интересно, самый простой способ EMC оказался лучше, чем LMP почти во всех тестах.
Еще два варианта трансляции рассматриваются в статье [32]. В ней представлен подход ленивой трансляции параллельной программы в последовательную с ограниченным числом переключений контекста. Важной особенностью описываемого метода является то, что множество достижимых состояний полученной программы является тем же, что и для исходной программы. Известные методы сохраняют локальное состояние потока перед
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 108 переключением контекста. Для того чтобы избежать этого, предлагается использовать копии глобальных переменных для каждого из переключений контекста. Таким образом, после каждого переключения ведется работа со своей картой памяти, а условия на равенство их между собой будут выписаны позднее. При ленивой трансляции выполнение происходит постепенно, с реальным переключением. Инициализируется только первая карта памяти.
Далее, при переключении контекста она копируется во вторую и происходит анализ второго потока. При переключении контекста обратно в первый поток происходит его выполнение заново, но уже до следующей точки переключения контекста.
Кроме того, была реализована вторая стратегия, противоположная, - нетерпеливая трансляция, которая предполагает, что поток выполняется сразу от начала и до конца. В начале карты памяти инициализируются произвольными значениями. В точках переключения контекста происходит смена карты памяти. Для сравнения этих стратегий использовались несколько тестов, которые показали, что нетерпеливая трансляция тратит больше времени и памяти на проверку.

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


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


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

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


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