A model-based approach to design test oracles for memory subsystems of multicore microprocessors

В работе представлен метод построения тестовых оракулов для подсистем памяти многоядерных микропроцессоров. Метод основан на использовании недетерминированной эталонной модели тестируемой системы. Идея подхода состоит в динамическом уточнении поведения модели на основе реакций, полученных от системы. При возникновении недетерминированного выбора в эталонной модели создаются и запускаются дополнительные экземпляры модели, каждый из которых моделирует возможный вариант поведения подсистемы памяти. При получении реакции от тестируемой подсистемы завершаются экземпляры модели, для которых данная реакция является некорректной. Признаком ошибки является отсутствие активных экземпляров эталонной модели. Эталонная модель и построенный на ее основе тестовый оракул разделены на три уровня: (1) уровень операции, (2) уровень кэш-строки и (3) уровень подсистемы памяти. Оракул уровня операции проверяет корректность обработки отдельного запроса соответствующего типа. Оракул уровня кэш-строки состоит из оракулов операций и предназначен для проверки запросов к заданной кэш-строке. Оракул уровня подсистемы памяти объединяет оракулы кэш-строк и производит общую оценку поведения устройства. Для эффективной реализации метода необходимо, чтобы тестируемая подсистема памяти удовлетворяла следующим двум ограничениям: (1) запросы к разным кэш-строкам исполняются независимо друг от друга; (2) запросы в одну кэш-строку сериализуются (в каждый момент времени исполняется не более одного запроса к одной кэш-строке). Предложенный метод с небольшими изменениями использовался для верификации кэш-памяти третьего уровня микропроцессора «Эльбрус-8C»; в результате было найдено три ошибки.