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

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