Программные продукты и системы

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

Одной из самых частых причин сбоя являются ошибки в драйверах операционной системы. Драйвер – программа, обеспечивающая взаимодействие между устройством и операционной системой. В большинстве случаев драйвер входит в состав операционной системы и является ее самой объемной частью по количеству строк кода. Это связано с необходимостью поддержки множества типов устройств, которым зачастую требуется доступ к функциям ядра операционной системы.

Как показано в [1], одной из самых распространенных ошибок в драйверах Linux являются ошибки синхронизации. Они возникают при неправильном использовании объектов синхронизации (семафоров, мьютексов, спин-блокировок и др.), а также при наличии разделяемых ресурсов без ограничения доступа к ним с помощью данных объектов. Это приводит к появлению в драйверах взаимоблокировок, двойных блокировок и к погоне за ресурсами. Такие ошибки довольно сложно обнаружить и воспроизвести, так как они могут проявляться лишь при определенных взаимодействиях функций драйвера, а также нескольких драйверов, имеющих общие ресурсы.

В статье описывается инструмент для поиска проблем синхронизации в драйверах Linux, использующий разработанный авторами метод обнаружения ошибочных ситуаций на основе семантических моделей [2]. Данный инструмент позволяет обнаруживать такие ошибки синхронизации, как зацикливания, взаимоблокировки, двойные блокировки. Рассмотрены основные компоненты данного инструмента, принципы их работы, описана процессная семантика объектов синхронизации ядра Linux на языке асинхронных функциональных схем (АФС).

Основные компоненты инструмента верификации

Верификатор объектов синхронизации имеет модульную структуру. Отдельные компоненты связаны между собой последовательно: выход одного компонента передается на вход следующего. Этот подход позволяет модифицировать отдельные части верификатора для адаптации к иному типу программ. Верификатор состоит из препроцессора, транслятора кода драйвера в программу на языке АФС, модуля представления программы АФС в виде системы рекурсивных уравнений, анализатора системы рекурсивных уравнений.

Схема работы верификатора представлена на рисунке 1. Рассмотрим особенности реализации каждого компонента.

Препроцессор реализован в виде сценария на языке bash. Его назначение – подготовка кода драйвера к трансляции в язык АФС.

Исходный код драйвера поступает на вход препроцессора, который считывает файл Makefile драйвера и анализирует зависимости между файлами исходного кода модуля. Затем для каждого файла на языке C препроцессор вызывает компилятор gcc с ключом –E: эта команда запускает препроцессор языка C, обрабатывающий все операторы препроцессора языка C (#include, #define и другие). При необходимости подключения какого-либо заголовочного файла препроцессор может искать недостающие файлы в директориях, указанных в его параметрах. На выходе препроцессора получается один файл исходного кода драйвера на языке C, который передается на вход транслятора в язык АФС.

После всех подготовительных процедур препроцессор передает управление транслятору в язык АФС. В данном случае АФС выбран как основной язык для промежуточного представления структуры драйвера. Выбор обусловлен удобством при преобразовании в систему рекурсивных уравнений и наличием уже заданных семантических областей для данного языка [3]. Транслятор из языка С в язык АФС будем называть Front-end-транслятором, этот термин часто используется для трансляторов из исходного языка (в данном случае язык C) в язык промежуточного представления (язык АФС).

Транслятор написан с использованием генераторов лексических анализаторов GNU Flex и синтаксических анализаторов GNU Bison.

На вход Flex подается файл на языке Lex и описывает генерируемый лексический анализатор. Компилятор Flex преобразует этот файл в программу на языке C. Эта программа представляет собой работающий лексический анализатор, который может получать на вход поток символов и выдавать поток токенов. Правила трансляции имеют вид Шаблон { Действие }.

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

Генератор синтаксических анализаторов Bison на вход получает файл со спецификацией разрабатываемого транслятора на языке Yacc, который он преобразует в синтаксический анализатор на языке C. Основой файла на языке Yacc являются правила трансляции грамматических выражений и семантических действий для каждого из этих правил. На выходе Bison получается программа-транслятор, которая на основе заданных семантических правил преобразует исходную программу.

В основе транслятора кода драйвера в язык АФС лежат реализация шаблона для анализатора языка ANSI C, а также ранние версии компилятора GCC, синтаксис которого был задан с использованием Bison. Шаблон синтаксического анализатора дополнен правилами для генерации абстрактного синтаксического дерева (АСД), помимо этого, добавлено распознавание GCC-расширений языка C (атрибуты, ассемблерные вставки, инициализация структур и др.). После лексического и синтаксического анализа кода драйвера на выходе получается абстрактное синтаксическое дерево программы. Далее это дерево используется для анализа структуры программы и для генерации программы на языке АФС.

Вначале транслятор ищет функцию modu­le_init() и считывает название функции инициализации. Затем анализатор просматривает тело функции инициализации и находит инициализацию устройства при помощи функции cdev_init, из этого вызова считывается идентификатор структуры file_operations. Данная структура содержит указатели на операции open, close, read, write и др. Именно они и представляют особый интерес, так как зачастую выполняются параллельно. Каждой операции драйвера соответствует функциональный процесс на языке АФС. Транслятор исследует все эти функции и собирает информацию об использовании в них объектов синхронизации. Линейные операторы не представляют интереса и поэтому заменяются на команды вида Ci. Далее анализируется использование данных объектов функциями драйвера. Эти взаимосвязи необходимы для генерации программы на языке АФС. На выходе после выполнения всех шагов Front-end записывает программу на языке АФС в файл с расширением .afs. Данный файл используется для дальнейшего анализа программы.

Рассмотрим основные семантические правила преобразования объектов синхронизации драйвера, описанных подробно в [1], в язык АФС.

Операционная семантика условных переменных

Условные переменные позволяют синхронизировать задания, при этом один или несколько процессов ожидают на условной переменной, пока другой процесс не отправит ожидающим процессам сигнал о завершении события.

Семантическая функция для wait_for_comple­tion(op), ожидающая сигнал о завершении от переменной op типа struct completion, задается следующим образом:

C[wait_for_completion(op)] = read(op, 1)

Здесь и далее в статье C[c] задает семантическую функцию, сопоставляющую элементам синхронизации ядра Linux команды на языке АФС.

Для операции complete(op), посылающей сигнал о завершении операции op всем ожидающим процессам, семантическая функция имеет вид

C[complete(op)] = write(op, 1)

Предположим, что есть N процессов w1, w2, …, wN, ожидающих завершения операции в процессе wr:

struct completion *op;

init_completion(op);

void func_w1() {… wait_for_completion(op); …}

void func_w2() {… wait_for_completion(op); …}

…

void func_wN() {… wait_for_completion(op); …}

void func_wr() {… complete(op); …}

Рассмотрим, как такая ситуация моделируется на языке АФС:

NET

      CHAN op::ALL(1):ALL(1)

BEGIN

      FUN w1 :: … read(1, 1) …

      FUN w2 :: … read(1, 1) …

…

      FUN wN :: … read(1, 1) …

      FUN wr :: … write(1, 1) …

END

В данной программе операция read(1, 1) процессов w1–wN соответствует функции wait_for_ completion() ядра Linux, а операция write(1, 1) – отправке сигнала всем ожидающим процессам при помощи функции ядра complete().

Операционная семантика спин-блокировок

Спин-блокировки в драйверах встречаются довольно часто. Семантически спин-блокировка представляет собой циклическую проверку возможности захвата объекта типа spinlock_t. На языке АФС в качестве объекта для захвата выступает канал вида ALL(1):ALL(1). Захват блокировки соответствует попытке записи в канал, данная попытка повторяется в цикле LOOP до успешной записи. Семантическая функция для функции захвата блокировки выглядит следующим образом:

C[spin_lock(s_lock)]= =LOOP(ALT(write(s_lock, 1))®break))

Значит, конструкция spin_lock() на языке АФС соответствует конструкции вида LOOP(ALT(wri­te(i, 1))®break)). Для освобождения спин-блоки­ровки необходимо считать данные из канала, то есть функции spin_unlock() соответствует операция read(i, 1)

C[spin_unlock(s_lock)]=read(s_lock, 1)

Представим фрагмент программы на языке C из двух процессов с использованием спин-блоки­ровки:

spinlock_t s_lock=SPIN_LOCK_UNLOCKED;

void func1() { ... spin_lock(s_lock);… spin_un­lock(s_lock); … }

void func2() { ... spin_lock(s_lock);… spin_un­lock(s_lock); … }

Данная программа соответствует следующей программе на языке АФС:

NET

      CHAN 1::ALL(1):ALL(1)

BEGIN

      FUN 1::…LOOP(ALT(write(1, 1)®break))… read(1, 1)…

      FUN 2::…LOOP(ALT(write(1, 1)®break))… read(1, 1)…

END

Отметим, что функции попытки захвата блокировки spin_trylock() соответствует семантическая функция

C[spin_trylock(lock)]=ALT(write(lock, 1)®skip; tt®skip).

Операционная семантика спин-блокировок чтения-записи

Спин-блокировка чтения-записи реализуется на языке АФС посредством двух каналов – для чтения и записи соответственно: если захватывается блокировка на чтение, то производится запись в канал для чтения, если на запись – в канал для записи. В целом семантика спин-блокировки чтения-записи очень схожа с обычными спин-блокировками, к которым добавляются лишь дополнительные проверки при захвате блокировки.

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

C[read_lock(rwlock)]=LOOP(ALT(write(r, 1)® break));read(r, 1); LOOP(ALT(write(w, 1)®break))

C[read_unlock(rwlock)]=read(r, 1)

C[write_lock(rwlock)]=LOOP(ALT(write(w, 1)® break)); read(w, 1); ALT(write(r, 1)®skip) … read(r, 1) …

C[write_unlock(rwlock)]=read(w, 1)

Здесь w и r – каналы, соответствующие захвату-блокировке на запись и чтение соответственно.

Рассмотрим программу, состоящую из двух потоков, в одном из которых захватывается спин-блокировка на чтение, а в другом – на запись

rwlock_t rwlock = RW_LOCK_UNLOCKED;

void func1() {...write_lock(rwlock);… write_un­lock(rwlock); … }

void func2() {...read_lock(rwlock);… read_un­lock(rwlock); … }

На языке АФС программа выглядит следующим образом:

NET

      CHAN w::ALL(1):ALL(1)

      CHAN r::ALL(1):ALL(1)

BEGIN

FUN 1: … LOOP(ALT(write(w, 1) ® break)); read(w, 1); ALT(write(r, 1) ® skip) … read(r, 1) …

FUN 2: … LOOP(ALT(write(r, 1) ® break)); read(r, 1); LOOP(ALT(write(w, 1) ® break)) … read(w, 1);…

END

Как видно из примера, на языке АФС добавлены дополнительные проверки возможности записи в каналы w и r при захвате блокировки на чтение и запись соответственно.

Операционная семантика семафоров

Семафоры на языке АФС моделируются несколько сложнее. Семафор ограничивает количество потоков в критическом участке кода специальным счетчиком, который моделируется на языке АФС каналами (значение счетчика должно совпадать с количеством каналов). Таким образом, выполнение операции down(sem) на АФС соответствует последовательной проверке возможности записи в первый канал; если этот канал занят, осуществляется попытка записи во второй канал и т.д. Если свободный канал не найден, операция прерывается в ожидании освобождения канала. При выполнении операции up(sem) действия совершаются в обратном порядке: последовательно осуществляется попытка считывания из канала N, затем из N–1 и так далее до канала 1, где N – максимальное значение счетчика семафора. Таким образом, семантические функции для захвата и освобождения семафора имеют вид

C[down(sem)]=ALT(write(1, 1)®skip;…; write(N, 1)®skip)

C[up(sem)]=ALT(read(N, 1)®skip;…; read(1, 1) ® skip)

Рассмотрим пример программы из двух потоков, которые используют общий семафор с начальным значением счетчика N.

struct semaphore sem;

sema_init(&sem, N);

void func1() { ... down(sem);… up(sem); … }

void func2() { ... down(sem);… up(sem); … }

Данной программе соответствует программа на языке АФС с N каналами вида ALL(1):ALL(1)

NET

      CHAN 1::ALL(1):ALL(1)

      CHAN 2::ALL(1):ALL(1)

…

      CHAN N::ALL(1):ALL(1)

BEGIN

      FUN 1:: … ALT(write(1, 1)®skip;…; write(N, 1) ® skip) … ALT(read(N, 1) skip;…; read(1, 1)® skip)…

      FUN 2:: … ALT(write(1, 1)®skip;…; write(N, 1) ® skip) … ALT(read(N, 1)®skip;…; read(1, 1)® skip)…

END

Таким образом, семафорам операции down() соответствует оператор ALT(write(1, 1)® skip;…; write(N, 1)®skip), а вызову функции up() – оператор ALT(read(N, 1)®skip;…; read(1, 1)® skip)

Операционная семантика семафоров чтения-записи

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

C[down_write(rwsem)] = write(r, 1); write(w, 1); read(r, 1)

C[up_write(rwsem)] = read(w, 1)

C[down_read(rwsem)] = write(w, 1); write(r, 1) ; read(w, 1);

C[up_read(rwsem)] = read(r, 1)

Рассмотрим программу, состоящую из двух потоков, в одном из которых ресурс захватывается семафором на чтение, а в другом – на запись:

static DECLARE_RWSEM(rwsem);

void func1() {...down_write(rwsem);… up_wri­te(rwsem); … }

void func2() {...down_read(rwsem);… up_re­ad(rwsem); … }

На языке АФС программа выглядит следующим образом:

NET

      CHAN w::ALL(1):ALL(1)

      CHAN r::ALL(1):ALL(1)

BEGIN

FUN 1: … write(r, 1); write(w, 1); read(r, 1)… read(w, 1);…

FUN 2: … write(w, 1); write(r, 1); read(w, 1); … read(r, 1) …

END

Как видно из примера, на языке АФС добав- лены дополнительные проверки возможности записи в каналы w и r при захвате семафора на чтение и запись соответственно, что аналогично захвату соответствующей спин-блокировки чтения-записи.

Операционная семантика мьютексов

Мьютексы по сути являются семафорами со счетчиком, равным единице. Они используются там, где в критический участок кода должен зайти только один поток. Семантически мьютексы отличаются от спин-блокировок тем, что при неудачном захвате мьютекса процесс засыпает. На языке АФС операция захвата мьютекса соответствует попытке записи в канал. Канал устроен таким образом, что при невозможности записи в данный момент процесс засыпает в ожидании освобождения канала. Для освобождения мьютекса необходимо прочитать данные из канала. Таким образом, семантические функции для мьютексов задаются следующим образом:

C[down(mutex)] = write(mutex, 1)

C[up(mutex)] = read(mutex, 1)

Приведем пример использования мьютекса при работе двух процессов:

struct semaphore mutex;

init_MUTEX(mutex);

void func1() { ... down(mutex);… up(mutex); … }

void func2() { ... down(mutex);… up(mutex); … }

Данная программа семантически соответствует программе на языке АФС:

NET

      CHAN 1::ALL(1):ALL(1)

BEGIN

      FUN 1:: … write(1, 1) … read(1, 1)…

      FUN 2:: … write(1, 1) … read(1, 1)…

END

Из примера видно, что на языке АФС функции down() соответствует операция write(1, i), а функции up() – операция read(1, i).

Следующий после представления драйвера на языке АФС этап – преобразование программы на языке АФС в систему рекурсивных уравнений. На основе теории, описанной в [3], сначала определяется априорная семантика функциональных процессов и каналов связи. Полученные априорные семантики объединяются посредством опе- рации композиции в алгебре вычислительных последовательностей. Затем с использованием аксиомы базисных свойств операции параллельной композиции и с применением по возможности операции инкапсуляции семантическое значение представляется в виде системы рекурсивных уравнений. Все операции производятся при помощи символьных вычислений с использованием аксиом из [3]. Полученная система рекурсивных уравнений задает множество вычислительных последовательностей, сопоставляемое струк- туре драйвера. На выходе система рекурсивных уравнений записывается в файл с расширени- ем .sem.

Система рекурсивных уравнений сама по себе довольно сложна для анализа программы. Поэтому с целью упрощения обнаружения исключительных ситуаций реализован инструмент для анализа системы рекурсивных уравнений. Он позволяет анализировать систему рекурсивных уравнений в файле с расширением .sem и выводить в удобочитаемом виде информацию о возможных ошибках синхронизации в драйвере. Данные о верификации записываются в файл с расширением .res в виде списка, где каждая строка указывает на возможную ошибку.

Модульность структуры верификатора

Модульная система верификатора позволяет адаптировать инструмент к программам самого разного назначения, для применения в новой сфере необходимо лишь переписать front-end. Исходный код верификатора написан с использованием языка C и утилит Flex + Bison. Так как существуют реализации этих утилит для множества различных операционных систем, данный верификатор является полностью переносимым. Однако для анализа определенных типов программ необходимо адаптировать front-end. Это связано с различной семантикой элементов синхронизации, а также с особенностью реализации библиотеки для работы с потоками.

В перспективе данный подход можно обобщить на верификацию драйверов операционной системы Windows, а также использовать для анализа многопоточных и параллельных программ как для операционных систем Linux, так и для Windows. Помимо этого исследуются возможности применения метода из [2] для обнаружения состояния гонок.

В заключение отметим, что в данной статье описан инструмент для поиска проблем синхронизации в драйверах Linux, основанный на разработанном авторами методе обнаружения ошибочных ситуаций на основе семантических моделей [2]. Кроме того, в статье описана процессная семантика объектов синхронизации ядра Linux на языке асинхронных функциональных схем.

Литература

1.     Corbet J., Rubini A., Kroah-Hartman G. Linux Device Drivers, 3-rd edition. O’Relly, 2006. 616 pp.

2.     Кораблин Ю.П., Павлов Е.Г. Разработка инструментов верификации драйверов на основе семантических моделей // Программные продукты и системы. 2012. № 1.

3.     Кораблин Ю.П. Семантические методы анализа распределенных систем // Автореферат дис. … д-ра техн. наук. М., 1994. 272 с.

4.     Кораблин Ю.П., Кучугуров И.В. Процессная семантика языков распределенного программирования // Программные продукты и системы. 2011. № 4.

5.     Костарев А.Н. Разработка инструментального комплекса для создания и семантического анализа распределенных информационных систем // Автореферат дис. … канд. техн. наук. М., 2004. 186 с.