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

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

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

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

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

Шаблон и программа

Модель устройства MMU k – ключ, d – данные «hit» hitT (k) hitlT (k) : d hitsT (k, d) «miss» missT (k) missrT (k, d)

Нотация модели устройства пример:

Модель варианта инструкции нотация:

LRU на «перестановках»

Формулы полезных обращений для LRU: ux(xi) = ( x{xi,…,xn} Λ xi{xi+1,…,xn} ) для LRU: ux(xi) = ( x{xk,…,xi} Λ Λj=1..i-1 (x{xj,…,xi-1} V xj≠xi) )

Схема генерации тестов

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

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

Эксперименты