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

• Автор: Павлов, Евгений Геннадьевич
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2013
• Место защиты: Москва
• Количество страниц: 231 с. : ил.

Оглавление
Оглавление
Введение
Г лава 1 Обзор исследований в области разработки драйверов
1.1 Анализ методов повышения надежности операционных систем
1.1.1 Автоматизация разработки драйверов
1.1.2 Использование языка более высокого уровня
1.1.3 Тестирование и верификация драйверов
1.1.4 Запуск драйверов в специальной безопасной среде
1.1.5 Ограниченный доступ к привилегированному режиму
1.1.6 Построение операционных систем, устойчивых к сбоям
1.1.7 Анализ рассмотренных методов
1.2 Инструменты для верификации драйверов операционных систем
1.2.1 Static Driver Verifier
1.2.2 SLICx
1.2.3 DDVerify
1.2.4 Linux Driver Verification
1.3 Вывод по главе
Глава 2 Анализ драйверной модели операционной системы Linux
2.1 Типы драйверов Linux
2.1.1 Символьные драйверы устройств
2.1.2 Блочные драйверы устройств
2.2 Ошибки в драйверах Linux
2.2.1 Взаимное исключение
2.2.2 Очередь ожидания

2.2.3 Тасклеты и очереди отложенных действий
2.2.4 Прерывания
2.2.5 Порты и память ввода/вывода
2.2.6 Использование памяти
2.2.7 Типичные ошибки в драйверах Linux
2.3 Объекты синхронизации в ядре
2.3.1 Атомарные операции
2.3.2 Спин-блокировки
2.3.3 Семафоры
2.3.4 Условные переменные
2.3.5 Секвентные блокировки
2.4 Выводы по главе
Глава 3 Применение процессной семантики для верификации драйверов
3.1 Язык асинхронных функциональных схем
3.2 Формальная семантика АФС-программ
3.3 Аксиоматизация свойств семантической области
3.4 Эквациональная характеризация априорных семантических значений
3.5 Априорная семантика функциональных процессов
3.6 Процессная семантика каналов связи и семантика АФС-программ
3.7 Семантика основных элементов языка программирования Си
3.7.1. Операционная семантика линейных операторов и выражений
3.7.2 Операционная семантика условий и операторов выбора
3.7.3 Операционная семантика циклов
3.7.4 Операционная семантика break, continue и return
3.7.5 Операционная семантика goto

3.7.6 Операционная семантика функций
3.8 Семантика объектов синхронизации драйверов Ьіпих
3.8.1 Операционная семантика условных переменных
3.8.2 Операционная семантика спин-блокировок
3.8.3 Операционная семантика спин-блокировок чтения-записи
3.8.4 Операционная семантика семафоров
3.8.5 Операционная семантика семафоров чтения-записи
3.8.6 Операционная семантика мьютексов
3.8.7 Атомарные переменные
3.9 Пример верификации драйвера на основе семантических моделей
3.10 Разделяемые ресурсы
3.10.1 Разделяемые переменные
3.10.2 Методы устранения состояния гонок
3.11 Сравнительный анализ с методом проверки моделей
3.12 Выводы по главе
Глава 4 Разработка инструментальной системы верификации драйверов Ьіпих.
4.1 Препроцессор
4.2 Транслятор кода драйвера в язык АФС
4.3 Преобразование АФС-программы в систему рекурсивных уравнений
4.4 Анализатор системы рекурсивных уравнений
4.5 Особенности структуры верификатора
4.6 Экспериментальная оценка эффективности метода
4.7 Оценка эффективности метода процессной семантики
4.8 Выводы по главе
Заключение

диться в критическом участке. Крайне нежелательно удерживать спин-блокировку в течение длительного времени. По своей сути спин-блокировка - это быстрая блокировка, которая должна захватываться на короткое время одним потоком. Интерфейс пользователя для спин-блокировки описан в файле . Рассмотрим пример использования спин-блокировок: spinlockt mrjock = SPlNJLOCK_UNLOCKED spinJock(&mrJock)
spin_unlock(&mrjmlock);
В операционной системе Linux спин-блокировки не могут быть захвачены дважды одним потоком. Это означает, что если поток пытается захватить блокировку, которую он уже удерживает, то этот поток начнет периодическую проверку в ожидании, пока он сам не освободит блокировку. Но так как освободить должен ее сам ожидающий поток, то возникнет тупиковая ситуация. Спин-блокировки могут использоваться в обработчике прерывания, для этого перед захватом надо запретить прерывания на данном процессоре. Для этого можно использовать функции spin_lock_irqsave{&lock, flags) - данная функция сохраняет текущее состояние системы прерываний, запрещает прерывания и захватывает блокировку lock. Для освобождения такой блокировки используется функция spinjmlock irqrestore{&lock flags). Важно, чтобы каждая блокировка была четко связана с тем, что она блокирует. Блокировки служат для блокирования данных, а не кода.
Иногда в соответствии с целью использования блокировки можно разделить на блокировки чтения и блокировки записи. Для таких случаев в операционной системе Linux введены спин-блокировки чтения-записи, которые обеспечивают два варианта блокировки. Блокировку на чтение может удерживать один или несколько потоков, которые одновременно выполняют операцию чтения. Блокировка на запись может удерживаться в любой момент времени только одним потоком, осуществляющим запись, никаких параллельных считываний не разрешается.