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


О дедуктивной верификации Си программ, работающих с разделяемыми данными

М.У. Мандрыкин (ИСП РАН, Москва), А.В. Хорошилов (ИСП РАН, Москва; МГУ, Москва; МФТИ, Москва; ВШЭ, Москва)

Аннотация

В статье рассматривается задача дедуктивной верификации кода ядра ОС Linux, написанного на языке Си и выполняющегося в окружении с высокой степенью параллелизма. Существенной особенностью этого кода является наличие работы с разделяемыми данными, что не позволяет применять классические методы дедуктивной верификации. Для преодоления этих сложностей в работе представлены предложения по формированию подхода к спецификации и верификации кода, работающего с разделяемыми данными, основанные на доказательстве соответствия этого кода заданной спецификации некоторой дисциплины синхронизации. Подход иллюстрируется примерами упрощенной модели спецификации спин-блокировок и внешнего интерфейса механизма синхронизации RCU (Read-copy-update), широко используемого в ядре ОС Linux.

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

Верификация, параллелизм, владение, инварианты, семантика языка C

Издание

Труды Института системного программирования РАН, том 27, вып. 4, 2015, стр. 49-68.

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

DOI: 10.15514/ISPRAS-2015-27(4)-4

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