Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин кафедра СП научный руководитель: д.ф.-м.н. А. К. Петренко

Содержание 1. основные определения 2. постановка задачи построения тестовых программ 3. ее решение, возникавшие важные подзадачи 4. теоремы (обоснование решения)

Схема кэш-памяти

Схема таблицы страниц

Шаблон и программа DIV x, y, z « деление на 0 » LOAD y, x, c «промах в L1» потенциально ошибочная ситуация в виде тестового шаблона MOV x,0 MOV y,0 STORE y,x,3 STORE y,x,9 STORE y,x,7 STORE y,x,5 MOV z,0 DIV x,y,z LOAD y,x,1 тестовая программа задача – автоматически осуществить отображение :

Модель устройства MMU k – ключ, d – данные «hit» hit T (k) hitl T (k) : d hits T (k, d) «miss» miss T (k) missr T (k, d) «таблица»

Нотация модели устройства пример: L1 { policy = LRU; lines = 4; regbits = 7; key(tag:24); data(d:32); keyMatch(k:30) { k[29:6] = tag }; } 7

Модель варианта инструкции нотация: отдельный «путь выполнения» инструкции утверждения и hit/miss битовые строки и таблицы источники условий: какие входные значения допустимы как вычислить адреса какие попадания /промахи происходят в блоках что загружается / сохраняется в блоках при каких условиях возникают исключительные ситуации LOAD (y,x,c) «промах в L1» [var y:64; var x:64; const c:16;] phys

LRU на «перестановках» ABCDEF CABDEF XABCDE hit C miss X

Формулы полезных обращений для LRU: u x (x i ) = ( x{x i,…,x n } Λ x i{x i+1,…,x n } ) для LRU: u x (x i ) = ( x{x k,…,x i } Λ Λ j=1..i-1 (x{x j,…,x i-1 } V x j x i ) )

Схема генерации тестов ситуация (шаблон программы) модель варианта инструкции 1... модель устройства формализовать микропроцессор система уравнений (constraints) начальные значения регистров инициализ-я устройства 1... тестовая программа 2. построение уравнений 3. решение уравнений 4. составление текста тестовой программы ручная работа автоматизированная 11 DIV x, y, z « деление на 0 » LOAD y, x, c «промах в L1»

«Теорема корректности» если построенная система предикатов, для шаблона, будет совместной, то тестовая программа на основе ее «решения» будет удовлетворять шаблону

«Теорема полноты» если для шаблона существует тестовая программа, то будет построена система предикатов, среди «решений» которой есть соответствующее этой программе если построенная система предикатов несовместна, то (действительно) данному шаблону не соответствует ни одна тестовая программа

Эксперименты увеличение допустимого размера шаблонов (было 2-3, стало 9-12) среднее время построения одного теста – 1-30с.