Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин ИСП РАН / кафедра СП ВМК МГУ научный руководитель: - презентация

1 Построение тестовых программ для проверки подсистем управления памяти микропроцессоров Евгений Корныхин ИСП РАН / кафедра СП ВМК МГУ научный руководитель: д.ф.-м.н. А.К.Петренко

2 Содержание 1. тестирование микропроцессоров 2. задача построения тестов 3. предлагаемый способ построения тестов 4. эксперименты

3 3 Место задачи тестирование: системное функциональное имитационное «сравнение с эталонным эмулятором» на наборе тестовых программ

4 Ситуации в MMU классификация поведения в виде ситуаций («нацеленные тесты») пример ситуации: в 1-й инструкции происходит «деление на ноль», во 2-й – происходит кэш-промах «длинные» цепочки инструкций (~10 инстр-й) 4

5 Ситуации в MMU ситуации для отдельных инструкций: возникновение исключительных ситуаций промахи/попадания в кэшах разных уровней, в TLB кэшируемые/некэшируемые обращения в память отображаемые/неотображаемые вирт.адреса ситуации для цепочек инструкций: чтение регистра после записи в него обращения по одинаковым/разным физическим/виртуальным адресам чтение после записи ячейки памяти одинаковые/разные страницы вирт.памяти одинаковые/разные строки кэш-памяти запись/чтение совместно с исключит.ситуациями 5

6 Построение нацеленных тестов нацеленные на ситуации тесты 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 тестовая программа 6 систематический выбор шаблонов

7 Существующие методы построения нацеленных тестов 1. прямое конструирование программ (MicroTESK) только для ситуаций из 2-3 инструкций 2. сведение к системам уравнений (RAVEN, Genesys-Pro) нет информации в открытых публикациях (проприетарное ПО) 7

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

9 Подход построения тестовых программ по шаблонам ситуация (шаблон программы) модель варианта инструкции 1... модель устройства формализовать микропроцессор система уравнений (constraints) начальные значения регистров инициализ-я устройства 1... тестовая программа 2. построение уравнений 3. решение уравнений 4. составление текста тестовой программы ручная работа автоматизированная 9

10 Модель устройства MMU пример: какие устройства нужны для ситуации (кэш, таблица страниц, TLB) устройство моделируется ассоциативным массивом смоделировать - задать характеристики: структурные вытеснение L1 { policy=LRU; lines=4; regbits=7; line( tag:24:key, d:32:data); keyMatch(k:30) { k[29:6] = tag }; } 10

11 Подход построения тестовых программ по шаблонам ситуация (шаблон программы) модель варианта инструкции 1... модель устройства формализовать микропроцессор система уравнений начальные значения регистров инициализ-я устройства 1... тестовая программа 2. построение уравнений 3. решение уравнений 4. составление текста тестовой программы ручная работа автоматизированная 11

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

13 Подход построения тестовых программ по шаблонам ситуация (шаблон программы) модель варианта инструкции 1... модель устройства формализовать микропроцессор система уравнений начальные значения регистров инициализ-я устройства 1... тестовая программа 2. построение уравнений 3. решение уравнений 4. составление текста тестовой программы ручная работа автоматизированная 13

14 Построение уравнений: этап 1 ситуация hit(miss) p i hit(miss) p i+1... цепочка промахов/ попаданий в блок 1 load(store) q i,d i load(store) q i+1,d i+1... цепочка загрузки/ сохранения данных в блоке 1... phys = x + (64)c phys[1:0] = 0^2... условия на значения регистров, адресов, других промежуточных значений модели вариантов инструкций модели устройств 14

15 Построение уравнений: этап 2 hit(miss) p i load(store) q i,d i phys[1:0] = 0^2 (свойства битовых строк) система уравнений (битовая и целочисленная арифметика) Hit [p i ] = p i {p 1,…,p i -1 } ΛEv(p 1,…,p i -1 ; p i ) Miss [p i ] = p i {p 1,…,p i -1 } Λ Ev(p 1,…,p i -1 ; p i ) равенство данных при равных адресах phys[1:0] = 0^2 (без изменений) модели устройств 15

16 Подход построения тестовых программ по шаблонам ситуация (шаблон программы) модель варианта инструкции 1... модель устройства формализовать микропроцессор система уравнений начальные значения регистров инициализ-я устройства 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, 7 STORE y, x, 9 STORE y, x, 5 MOV z, 0 DIV x, y, z LOAD y, x, 1 16

17 17 Область применимости многоуровневая кэш-память обращение в память с / без виртуальной памяти сквозная запись / отложенная запись доп.условия на строки кэш-памяти virtually indexed кэш-память virtually tagged кэш-память

18 18 Направления развития временные ограничения (длительности, зависимости от скорости выполнения) циклические действия с переменным числом итераций кэш-память инструкций многоядерные микропроцессоры тестирование, нацеленное на эти особенности, надо проводить иначе

19 19 Реализация существующий генератор шаблонов модели вариантов инструкций (xml) конструктор текстов asm (Java) ~100стр. на вариант исполнения инструкции ~2000стр. ~1000стр. уравнения (smt) стр. генератор уравнений (ruby) модели устройств (xml) ~10стр. на устройство шаблон теста решение равнений тесты (asm)

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

21 Спасибо за внимание

22 Ошибки в MMU ошибки обработки управляющих битов ошибки сопоставления тэгов конфликты использования ресурсов ошибки обновления/вытеснения данных ошибки синхронизации данных ошибки планирования обработки запросов ошибки, вызванные исключениями 22

23 23 Задача дан шаблон программы – (I, a 1, …, a n, С)* I – инструкция (название) a 1, …, a n – параметры инструкции С – вариант инструкции I (название отдельного пути выполнения инструкции I) построить программу, соответствующую шаблону (I, a 1, …, a n )* отношение соответствия: программа оканчивается той же цепочкой инструкций с параметрами, их исполнение в программе соответствует вариантам в шаблоне

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

25 Новизна ситуация (шаблон программы) модель варианта инструкции 1... модель блока 1 MMU... система уравнений начальные значения регистров инициализ-я блока 1... тестовая программа I. модели вариантов инструкций и блоков MMU II. методы построения уравнений III. написана программа, строящая уравнения 25

26 Примеры описаний инструкций rs rt rt rs rs rt rt temp temp арифметическое переполнение ADD rd, rs, rt

27 Уравнения (constraints)

28

29 Теоремы о количестве адресов, инициализирующих блок общий случай: m n · (n + 2w) для LRU: m n · w + M n – количество промахов/попаданий (~ длина шаблона) M – количество промахов w – ассоциативность блока

30 Метод построения уравнений для стратегий вытеснения Ev(x 1,…,x i ;x) = ( u x (x 1 ) + … + u x (x i ) > C ) C – константа (значение зависит от стратегии вытеснения) u x (x k ) = 1, если x k «способствует вытеснению» x; 0, иначе для LRU: u x (x k ) = ( x{x k,…,x i } Λ x k{x k+1,…,x i } )

31 Схема предлагаемого подхода ситуация S (шаблон программы) модель инструкции 1 в ситуации S... модель блока 1 MMU формализовать микропроцессор система уравнений начальные значения регистров инициализ-я блока 1... тестовая программа 2. построение уравнений 3. решение уравнений 4. составление текста тестовой программы ручная работа автоматизированная 31

32 Шаблоны и их связь с моделями инструкций и моделями блоков MMU DIV x, y, z « деление на 0 » LOAD y, x, c «промах в L1» ситуация в виде шаблона программы DIV (x,y,z) «деление на 0» { … } LOAD (y,x,c) «промах в L1» { …... L1... } модели инструкций модели блоков MMU L1 { … } модели инструкций формализуют, как должны работать инструкции модели блоков MMU формализуют кэши, таблицы страниц, пути выполнения инструкций