Сборники трудов ИСП РАН


Статический поиск ошибок повторной блокировки семафора.

А.Е. Бородин.

Аннотация

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

Ключевые слова

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

Издание

Труды Института системного программирования РАН, том 26, вып. 3, 2014, стр. 103-112.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2014-26(3)-5

Полный текст статьи в формате pdf Вернуться к содержанию тома