Проблемы обеспечения корректности программ и аппаратуры Институт системного программирования Российской академии наук Камкин Александр Сергеевич Московский физико-технический институт (государственный университет), 11 марта 2013 г.

Корректность и надежность Корректность – соответствие системы налагаемым на нее требованиям – Минимизация ошибок проектирования Надежность – способность системы сохранять работоспособное состояние – Минимизация сбоев при эксплуатации (Корректность) (Надежность) – Ошибки – частая причина непредвиденных сбоев

Содержание лекции Введение – Ошибки и их последствия – Этапы проектирования – Функциональная верификация Основные подходы – Имитационная верификация – Генерация тестовых программ – Формальная верификация Проекты ИСП РАН – Проекты C++TESK / MicroTESK – Статический анализ и формальная верификация – Актуальные проблемы Основная тема: обеспечение корректности микропроцессоров

Цена ошибки проектирования Ракета-носитель Ариан 5, 1996 несовместимость SW/HW Ракета-носитель Ариан 5, 1996 несовместимость SW/HW Боинг 757 (рейс 965), 1995 отображение информации Боинг 757 (рейс 965), 1995 отображение информации Вертолет Чинук CH-47, 1994 система управления двигателем Вертолет Чинук CH-47, 1994 система управления двигателем Комплекс ПВО Пэтриот, 1991 система наведения ракет Комплекс ПВО Пэтриот, 1991 система наведения ракет Человеческие жизни > 100 млн долларов Потеря репутации Человеческие жизни > 100 млн долларов Потеря репутации

Статистика ошибок Среднее число ошибок на 1000 строк кода

Сложность микропроцессоров Микропроцессор > 10 9 транзисторов > 10 7 строк на Verilog ~4-10 ядер Проектирование > 500 разработчиков ~3-4 года работы > 100 млн долларов Верификация – более 60% затрат на проектирование микропроцессора! > ошибок проектирования (в спецификациях, Verilog-коде и т.д.) > 100 инженеров-верификаторов (модели, тесты, формальные методы) > 1000 компьютеров (круглосуточное моделирование и прогон тестов) Число транзисторов удваивается каждые 2 года

Проектирование микропроцессора Архитектурное проектирование Детальное проектирование Логический синтез Физический синтез Верификация Программный прототип (С/C++) Модель уровня RTL (Verilog/VHDL) Логическая схема Фотошаблоны Требования

Функциональная верификация Верификация – это проверка корректности, соответствия реализации ее спецификации – Экспертиза – непосредственный анализ результатов проектирования: инспекция кода программы и т.п. – Статический анализ кода – автоматическая проверка заданных правил, поиск ошибок по шаблонам и т.п. – Тестирование – оценка корректности системы по результатам ее работы в некоторых ситуациях – Формальная верификация – строгое доказательство корректности формальной модели системы

Автоматизация верификации Формальные модели, спецификации, правила Генерация тестов Генерация тестов Проверка поведения Проверка поведения Проверка моделей Проверка моделей Дедуктивный анализ Дедуктивный анализ Статический анализ Статический анализ автоматы, цепи Маркова пред- и постусловия, временные логики автоматы, временные логики аксиомы, правила вывода семантика языка, шаблоны ошибок

Модульная и системная верификация lui s1, 0x2779 ori s1, s1, 0xc8b9 lui s3, 0x4ee ori s3, s3, 0xf798 add v0, a0, a2 sub t1, t3, t5 add t7, s1, s3 Системная верификацияМодульная верификация Проверяется модель всего микропроцессора с помощью тестовых программ Проверяется модель отдельного модуля через входные и выходные сигналы

Языки описания аппаратуры (HDL) input S; output R1, R2; void design() { while(true) { wait(S); delay(6); R1 = 1; delay(1); R1 = 0; R2 = 1; delay(1); R2 = 0; } // Код Verilog CLK) begin if(state == 2h0 && S) begin state

Поведение цифровой аппаратуры

Задачи имитационной верификации Генерация стимулов Проверка реакций Оценка покрытия Тестовое покрытие Тестовый оракул Генератор стимулов Генератор стимулов Целевая система Тестовый оракул Тестовое покрытие

Тестирование на основе моделей Модель системы Генератор стимулов Целевая система Тестовый оракул Тестовое покрытие

Преобразование интерфейсов HDL Входной интерфейс #1 Входной интерфейс #N Data Выходной интерфейс #1 Выходной интерфейс #M Оракул Адаптер входного интерфейса Адаптер выходного интерфейса Эталонная модель input in; output out;... assert(i < MAX_SIZE); fifo[i++] = recv(in);... send(out, i == MAX_SIZE);...

Генерация тестовых программ Целевая система (HDL) lui s1, 0xdead ori s1, s1, 0x0 lui s3, 0xbeef ori s3, s3, 0xf add v0, a0, a2 sub t1, t3, t5 add t7, s1, s3 Тестовые программы (ассемблер) Эталонный симулятор (C/C++) Трассы выполнения (форматированный текст) 0x2000: lui... 0x2004: ori... 0x2008: ori... 0x200c: lui... 0x2010: add... 0x2014: sub... 0x2018: add... Компаратор трасс (Perl, Python) 0x2000: lui... 0x2004: ori... 0x2008: ori... 0x200c: lui... 0x2010: add... 0x2014: sub... 0x2018: add...

Генерация тестов на основе моделей Генератор на основе моделей Модель микропроцессора Модель тестового покрытия Ядро генератора Библиотеки Модель Генератор Test templates Шаблоны тестов Инженер по моделированию Инженер по верификации Test programs Тестовые программы Тестовая программа Resource Initial Values: R6 = 8, R3 = – 25,..., R17 = – = 7, 110 = 25,..., 1F0 = 16 Instructions: 500: Load R : Sub R : Add R6 1F0 580: Add R9

Формальная верификация Требования Целевая система Соответствие Модель системыМодель требований Формальное соответствие ~

Инструмент C++TESK Разработка моделей аппаратуры и адаптеров моделей на языке C++ Описание тестового покрытия и сценариев тестирования Генерация тестовой последовательности на основе обхода графа состояний модели Распараллеливание прогона теста на основе распределенного обхода графа состояний Генерация отчетов о тестировании

Описание архитектуры микропроцессора на ADL языке (Sim-nML) Конфигурирование типовых подсистем Извлечение тестовых ситуаций Описание шаблонов тестовых программ (Ruby) Генерация шаблонов тестовых программ на основе моделей Инструмент MicroTESK

Анализ потоков данных и зависимостей Извлечение автоматных моделей Автоматическая абстракция моделей Формальный анализ моделей Поиск зависаний и конфликтов Генерация направленных тестов Статический анализ HDL-описаний CLK) begin if(state == 3h0 && S) begin state

Моделирование сетей на кристалле Вероятностный анализ работы сетей Доказательство отсутствия зависаний Генерация тестов по сетевым моделям Моделирование конвейеров Верификация многоядерных процессоров Анализ коммуникационных сетей A. Gotmanov, S. Chatterjee, M. Kishinevsky. Verifying Deadlock-Freedom of Communication Fabrics.

Актуальные проблемы Автоматическая генерация функциональных тестов на основе разного рода моделей Глубокий статический анализ Verilog-описаний цифровой аппаратуры (потенциальные ошибки, мертвый код и т.п.) Автоматический поиск зависаний (deadlocks) в микроархитектурных моделях процессоров Формальная верификация протоколов обеспечения когерентности памяти в многоядерных процессорах Распараллеливание верификации, обработка больших графов (генерация тестов и проверка моделей)

Основные работы отдела ТП Создание технологий и инструментов – Тестирование на основе моделей (UniTESK) – Проверка соответствия стандарту Linux Standard Base – Верификация драйверов Linux – Верификация микропроцессоров Разработка тестов и тестирование – Информационная система оператора связи – Операционные системы реального времени – Базовые библиотеки Linux (Linux Standard Base) – Сетевые протоколы IPv6, Mobile IPv6, IPsec – Отдельные модули компиляторов Intel – Микропроцессоры архитектуры MIPS / Elbrus

Контактная информация Институт системного программирования РАН (ИСП РАН) Верификация ИСП РАН А.С. Камкин, к.ф.-м.н., с.н.с. ИСП РАН

Спасибо!