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

Authors

А. Бородин

PDF
bibtex

Abstract

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