'

Построение тестовых программ для проверки подсистем управления памяти микропроцессоров

Понравилась презентация – покажи это...





Слайд 0

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


Слайд 1

Содержание тестирование микропроцессоров постановка задачи предлагаемый метод оценка метода


Слайд 2

3 Место задачи в разработке аппаратного обеспечения ... output sm_out; reg [1:0] c, next_state; always @ (posedge sm_cl) begin    if (reset == 1'b1) c <= 2'b00;    else c <= next_state; end ... проектные документы design на Verilog микропроцессор тестирование design’а


Слайд 3

4 Системное тестирование генерация тестовых программ эмулятор микропроцессора (эталон) ( на Си ) cравнение трасс Возникла ошибка Успешный прогон cимуляция design’а (на Verilog) lui s1,0x27 ori s1,s1,0xc8 lui s3,0x4e ori s3,s3,0xf7 ... проводится «сравнением с эталоном»


Слайд 4

Подсистемы управления памяти (MMU) 5


Слайд 5

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


Слайд 6

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


Слайд 7

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


Слайд 8

Построение нацеленных тестов нацеленные на ситуации тесты 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 тестовая программа 9


Слайд 9

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


Слайд 10

Задача s1 = f1(so) P1(so) s2 = f2(s1) P2(s1) … (I, a1, …, an, С)* - шаблон программы si – состояние микропроцессора Pi – предикат, определяющий вариант инструкции fi – функция изменения состояния So – множество допустимых начальных состояний so ? So = ? I(1) a1(1) … an(1) C(1) I(2) a1(2) … an(2) C(2) I(-m) a… … I(-1) a… = ? специфика MMU: fi содержат функции поиска типа lookup(k,s)


Слайд 11

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


Слайд 12

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


Слайд 13

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


Слайд 14

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


Слайд 15

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


Слайд 16

Модель варианта инструкции пример: отдельный путь выполнения инструкции в виде утверждений о свойствах битовых строк источники условий: какие входные значения допустимы как вычислить адреса какие попадания /промахи происходят в блоках что загружается / сохраняется в блоках при каких условиях возникают исключительные ситуации LOAD (y,x,c) «промах в L1» [var y:64; var x:64; const c:16;] phys <- x + (64)c; assume: phys[1:0]=0^2 miss<L1>(phys) {replace(y)}; hit<Mem>(phys) {load(y)}; 17


Слайд 17

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


Слайд 18

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


Слайд 19

Построение уравнений: этап 2 hit(miss) pi load(store) qi,di phys[1:0] = 0^2 (свойства битовых строк) система уравнений (битовая и целочисленная арифметика) Hit [pi] = pi ?{p1,…,pi-1} ? ?Ev(p1,…,pi-1; pi) Miss [pi] = pi ?{p1,…,pi-1} ? Ev(p1,…,pi-1; pi) равенство данных при равных адресах phys[1:0] = 0^2 (без изменений) это новые методы модели блоков MMU 20


Слайд 20

Схема предлагаемого подхода ситуация (шаблон программы) модель варианта инструкции1 ... модель блока1 MMU ... 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 21


Слайд 21

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


Слайд 22

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


Слайд 23

Особенности предлагаемых методов блоки инициализируются цепочкой обращений в них по адресам – адреса вычисляет решатель уравнений единая система уравнений компактность уравнений (в них выражается не изменение состояния, а зависимости адресов) 24


Слайд 24

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


Слайд 25

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


Слайд 26

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


Слайд 27

Практическое использование микропроцессор архитектуры MIPS блоки MMU в микропроцессоре: кэш L1 16кБ кэш L2 256кБ TLB 48 строк (по 2 страницы в строке) microTLB 4 строки 28


Слайд 28

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


Слайд 29

30 Публикации 1. статья в «Программировании» [из списка ВАК] 2. статья в «Вычислительных методах и программировании» 3-4. статьи на SYRCoSE-2008 и 2009 5. статья на EWDTS-2009 6-7. статьи в сборниках трудов ИСП РАН (тт.15, 17)


Слайд 30

Апробация конференции: SYRCoSE-2008 SYRCoSE-2009 EWDTS-2009 Микроэлектроника и информатика-2009 The Ph.D. Summer School on Scientific Computing 2009 Ломоносов-2009, 2010 Тихоновские чтения-2009 Ломоносовские чтения-2010 семинары: семинар отдела Технологий программирования ИСП РАН научно-исследовательский семинар им. М.Р.Шура-Бура


Слайд 31

32 Результаты модель блока MMU, описывающая его характеристики модель инструкции в виде совокупности отдельных вариантов, задаваемых в виде соотношений битовых строк и свойств наличия или отсутствия данных в блоках метод построения разрешаемых уравнений для шаблонов в виде уравнений над битовыми строками без описания изменения состояния MMU методы описания стратегий вытеснения c помощью уравнений над битовыми строками и ограничениями сумм бит на основе моделей и методов реализована система построения нацеленных тестов


Слайд 32

Примеры описаний инструкций <situation>     <argument name="rd" length="64" status="readonly" />     <argument name="rs" length="64" status="readonly" />     <argument name="rt" length="64" status="readonly" />     <assume><eq>             <bits end="63" start="32"><var>rs</var></bits>             <power index="32"><bit index="31"> <var>rs</var></bit></power>     </eq></assume>       <assume><eq>             <bits end="63" start="32"><var>rt</var></bits>             <power index="32"><bit index="31"> <var>rt</var></bit></power>     </eq></assume>       <let name="temp"><sum>                 <concat> <bit index="31"><var>rs</var></bit>                     <bits end="31" start="0"> <var>rs</var></bits>                 </concat>                 <concat>                      <bit index="31"><var>rt</var></bit>                      <bits end="31" start="0"> <var>rt</var></bits>                  </concat></sum></let>     <assume><neq>             <bit index="32"><var>temp </var></bit>             <bit index="31"><var>temp </var></bit>     </neq></assume> </situation> арифметическое переполнение ADD rd, rs, rt


Слайд 33

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


Слайд 34

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


Слайд 35

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


Слайд 36

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


Слайд 37

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


Слайд 38

Шаблоны и их связь с моделями инструкций и моделями блоков 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 формализуют кэши, таблицы страниц, ... 39 пути выполнения инструкций


×

HTML:





Ссылка: