ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Публикационная активность

(сведения по итогам 2016 г.)
2-летний импакт-фактор РИНЦ: 0,493
2-летний импакт-фактор РИНЦ без самоцитирования: 0,389
Двухлетний импакт-фактор РИНЦ с учетом цитирования из всех
источников: 0,732
5-летний импакт-фактор РИНЦ: 0,364
5-летний импакт-фактор РИНЦ без самоцитирования: 0,303
Суммарное число цитирований журнала в РИНЦ: 5022
Пятилетний индекс Херфиндаля по цитирующим журналам: 355
Индекс Херфиндаля по организациям авторов: 499
Десятилетний индекс Хирша: 11
Место в общем рейтинге SCIENCE INDEX за 2016 год: 304
Место в рейтинге SCIENCE INDEX за 2016 год по тематике "Автоматика. Вычислительная техника": 11

Больше данных по публикационной активности нашего журнале за 2008-2016 гг. на сайте РИНЦ

Вход


Забыли пароль? / Регистрация

Добавить в закладки

Следующий номер на сайте

3
Ожидается:
16 Сентября 2018

Разработка инструментальных средств анализа драйверов операционной системы Linux

Analysis tools of Linux operating system drivers development
Статья опубликована в выпуске журнала № 3 за 2012 год. [ на стр. 160-165 ][ 12.09.2012 ]
Аннотация:Описывается инструмент для поиска проблем синхронизации в драйверах операционной системы Linux, который использует метод обнаружения ошибочных ситуаций с помощью семантических моделей, основанный на теории, описанной в работе [2]. Метод позволяет обнаруживать такие ошибки синхронизации, как зацикливания, взаимобло-кировки, двойные блокировки и другие. Инструмент для поиска ошибок синхронизации состоит из четырех основных частей: препроцессора, транслятора кода драйвера в программу на языке асинхронных функциональных схем (далее АФС), модуля представления программы АФС в виде системы рекурсивных уравнений, анализатора системы рекурсивных уравнений. Препроцессор реализован в виде сценария на языке bash, его назначение – подготовка кода драйвера к трансляции в язык АФС. После всех подготовительных процедур препроцессор передает управление транслятору в язык АФС. Транслятор написан с использованием генераторов лексических анализаторов GNU Flex и синтаксических анализаторов GNU Bison. Драйвер преобразуется в программу на языке АФС на основе заданной в настоящей статье операционной семантики для объектов синхронизации. Следующим этапом является преобразование программы на языке АФС в систему рекурсивных уравнений. На основе теории из [3] программа на языке АФС представляется в виде системы рекурсивных уравнений, которая задает множество вычислительных последовательностей, сопоставляемое структуре драйвера. С целью поиска ошибок синхронизации реализован инструмент для анализа полученной системы рекурсивных уравнений. Он имеет модульную архитектуру, поэтому возможна его адаптация для различных типов ПО. Помимо этого, в данный момент ведутся исследования, изучающие возможность применения метода из [2] для обнаружения состояния гонок.
Abstract:The article describes the tool for search of synchronization problems in Linux operating system drivers that uses the detection of error situations by using semantic models. This method is based on theory, described in the work [2], it enables to detect such errors of synchronization as loops, deadlocks, double locking and others. Tool for search of synchronization errors consists of four main parts: the preprocessor, the compiler of driver code to program in the language of asynchronous functional schemes (AFS), the presentation of the AFS program as a system of re-cursive equations, analyzer of recursive equations system. The preprocessor is implemented as a script in the bash language, its purpose is to prepare the driver code to translate into the AFS language. After all the preparatory procedures the preprocessor passes control to the translator into the AFS language. The translator is written using the GNU Flex lexical analyzer generators and GNU Bison syntax analyzers. The driver is translated in the AFS language, based on the specified in this article operational semantics for synchronization objects. The next step is to convert the AFS language programs into the recursive equations system. On the basis of the theory of [3] the program in the AFS language is presented as a system of recursive equations, which sets a lot of computing sequences associated with the driver structure. In order to search synchronization errors there is implemented a tool for analyze of recursive equations system received. The tool has a modular architecture, so it can be adapted for different types of software. In addition, the possibility of applying the method of [2] for races state detection is being currently studied.
Авторы: Кораблин Ю.П. (y.p.k@mail.ru) - Российский государственный социальный университет, г. Москва, Москва, Россия, доктор технических наук, Павлов Е.Г. (lucenticus@gmail.com) - Российский государственный социальный университет, г. Москва, ,
Ключевые слова: алгебраическая семантика., эквациональная характеристика, взаимодействующие последовательные процессы, драйверы устройств, верификация
Keywords: algebraic semantics, equational characterization, communicating sequential processes, device drivers, verification
Количество просмотров: 4972
Версия для печати
Выпуск в формате PDF (7.64Мб)
Скачать обложку в формате PDF (1.33Мб)

Размер шрифта:       Шрифт:

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

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

Как показано в [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 с.


Постоянный адрес статьи:
http://swsys.ru/index.php?page=article&id=3235
Версия для печати
Выпуск в формате PDF (7.64Мб)
Скачать обложку в формате PDF (1.33Мб)
Статья опубликована в выпуске журнала № 3 за 2012 год. [ на стр. 160-165 ]

Возможно, Вас заинтересуют следующие статьи схожих тематик: