авторефераты диссертаций БЕСПЛАТНАЯ  БИБЛИОТЕКА

АВТОРЕФЕРАТЫ КАНДИДАТСКИХ, ДОКТОРСКИХ ДИССЕРТАЦИЙ

<< ГЛАВНАЯ
АГРОИНЖЕНЕРИЯ
АСТРОНОМИЯ
БЕЗОПАСНОСТЬ
БИОЛОГИЯ
ЗЕМЛЯ
ИНФОРМАТИКА
ИСКУССТВОВЕДЕНИЕ
ИСТОРИЯ
КУЛЬТУРОЛОГИЯ
МАШИНОСТРОЕНИЕ
МЕДИЦИНА
МЕТАЛЛУРГИЯ
МЕХАНИКА
ПЕДАГОГИКА
ПОЛИТИКА
ПРИБОРОСТРОЕНИЕ
ПРОДОВОЛЬСТВИЕ
ПСИХОЛОГИЯ
РАДИОТЕХНИКА
СЕЛЬСКОЕ ХОЗЯЙСТВО
СОЦИОЛОГИЯ
СТРОИТЕЛЬСТВО
ТЕХНИЧЕСКИЕ НАУКИ
ТРАНСПОРТ
ФАРМАЦЕВТИКА
ФИЗИКА
ФИЗИОЛОГИЯ
ФИЛОЛОГИЯ
ФИЛОСОФИЯ
ХИМИЯ
ЭКОНОМИКА
ЭЛЕКТРОТЕХНИКА
ЭНЕРГЕТИКА
ЮРИСПРУДЕНЦИЯ
ЯЗЫКОЗНАНИЕ
РАЗНОЕ
КОНТАКТЫ

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

Московский государственный университет имени М. В. Ломоносова

На правах рукописи

Корныхин Евгений Валерьевич Построение тестовых программ для проверки подсистем управления памяти микропроцессоров 05.13.11 – математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата физико-математических наук

Москва – 2010

Работа выполнена на кафедре системного программирования факультета вы числительной математики и кибернетики Московского государственного уни верситета имени М. В. Ломоносова.

Научный консультант: доктор физико-математических наук, старший научный сотрудник Петренко Александр Константино вич.

Официальные оппоненты: доктор физико-математических наук, профессор Смелянский Руслан Леонидович;

доктор физико-математических наук Лацис Алексей Оттович.

Ведущая организация: Научно-исследовательский институт системных исследований РАН

Защита состоится 26 ноября 2010 года в 11 часов на заседании диссертацион ного совета Д 501.001.44 Московского государственного университета име ни М.В. Ломоносова по адресу: 119991, ГСП-1, Москва, Ленинские горы, МГУ имени М.В.Ломоносова, 2-й учебный корпус, факультет ВМК, ауд.

685.

С диссертацией можно ознакомиться в библиотеке факультета ВМК МГУ. С текстом автореферата можно ознакомиться на официальном сайте ВМК МГУ http://cs.msu.ru в разделе «Наука» — «Работа диссертационных советов» — «Д 501.001.44»

Автореферат разослан «14» сентября 2010 г.

Ученый секретарь диссертационного совета профессор Н.П. Трифонов

Общая характеристика работы

Актуальность темы Современные микропроцессоры — сложные многокомпонентные системы.

Размеры современных микропроцессоров оцениваются как 107 108 вентилей.

Естественно при разработке таких сложных систем в проекты микропроцессо ров вносятся ошибки, порой довольно критичные. Поэтому для обнаружения этих ошибок в цикл разработки микропроцессора в обязательном порядке входят этапы функциональной верификации.

Чем позднее будут обнаружены ошибки в микропроцессорах, тем дороже обойдётся исправление ошибок: сделать это в готовой микросхеме, тем более выпущенной на рынок, практически невозможно. Тем актуальнее становят ся методы обнаружения ошибок на ранних этапах разработки микропроцес соров. Цикл разработки предполагает подготовку микропроцессоров в виде исполнимых программных моделей на языках Verilog или VHDL. Это делает возможным проведение функциональной верификации на таких моделях (т.е.

до производства самих микропроцессоров) и актуальным исследование мето дов такой верификации. Целью функциональной верификации программных моделей микропроцессоров является обнаружение ошибок реализации функ циональности в программных моделях микропроцессоров.

Выделяют следующие виды функциональной верификации: экспертизу, имитационное тестирование и формальную верификацию. Экспертиза пред полагает анализ текстов моделей экспертами с целью оценки их корректности и обнаружения ошибок. Этот вид функциональной верификации эффективно применяется на ранних стадиях разработки. Однако, ввиду наличия человече ского фактора, после экспертизы ошибки в микропроцессоре всё же остаются.

Методы формальной верификации позволяют дать исчерпывающий ответ на вопрос о корректности отдельных модулей и всего микропроцессора. Однако трудоемкость формальной верификации чрезвычайно велика. Например, при разработке Intel Pentium 4 были формально верифицированы модуль работы с плавающей точкой (FPU), модуль декодирования инструкции и логика вне очередного выполнения (out-of-order), было найдено порядка 20 новых оши бок, однако трудоемкость этого проекта составила порядка 60 человеко-лет.

Имитационное тестирование позволяет ценой меньших усилий обнаружить значительную часть ошибок, в том числе критичных ошибок. Имитационное тестирование проводят для отдельных модулей (тогда оно называется мо дульным тестированием) и для всего микропроцессора в целом (тогда оно называется системным тестированием). Модули тестируются подачей на их входы специальных сигналов (модульных тестов) со снятием выходных сигналов и последующим анализом выходных сигналов. Входом при систем ном тестировании являются программы на машинном языке (тестовые про граммы). Проведение модульного тестирования требует кроме подготовки са мих входных данных еще и подготовку тестирующей установки (testbench), выделение тестируемого модуля из всего проекта микропроцессора и т.п. Си стемное тестирование избавлено от этой необходимости. Поскольку размер и сложность отдельного модуля всегда меньше размера и сложности микро процессора в целом, потенциально качество модульного тестирования может быть выше, чем системного. Однако для достижения высокого качества те стирования как число модульных тестов, так и совокупная трудоемкость их изготовления, получаются очень большими. Это вынуждает часть проверок проводить на модульном уровне, а другую часть на системном. Невысокая стоимость подготовки и проведения системного тестирования определила его наибольшую востребованность среди других методов функциональной вери фикации. Практически все разработчики микропроцессоров проводят систем ное тестирование.



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

Поэтому для тщательного системного тестирования нужно подобное же и количество тестовых программ. Это определяет актуальность задачи автома тического построения тестовых программ для системного тестирования.

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

К числу наиболее сложных механизмов современных процессоров (поэто му наиболее подверженных ошибкам), использующих конвейеры и многоуров невые буферы типа кэш-памяти, относится механизм доступа к памяти. По этому актуальной является задача построения тестовых программ для про верки подсистем управления (механизмами) памяти микропроцессоров.

Цель диссертационной работы Целью диссертационной работы является исследование и разработка ме тодов и программных средств построения тестовых программ для проверки подсистем управления памяти микропроцессоров.

Для достижения этой цели были поставлены следующие задачи:

1) исследовать описанные в научной литературе методы построения тесто вых программ на предмет их применимости для системного тестирова ния подсистем управления памяти микропроцессоров;

2) разработать методы построения тестовых программ для системного функ ционального тестирования подсистем управления памяти.

Научная новизна Научной новизной обладают следующие результаты работы:

1) предложен подход к построению тестовых программ для проверки под систем управления памяти микропроцессоров, сочетающий формализа цию документации и технику ограничений;

2) предложен метод моделирования устройств подсистемы управления па мяти, использующий конечные автоматы специального вида;

3) предложена формальная модель инструкций, описывающая отдельные пути их выполнения в виде утверждений о свойствах параметров ин струкций и модельном состоянии устройств;

4) в рамках предложенного подхода разработан метод формализации ме ханизма вытеснения данных при помощи построения ограничений, эф фективно разрешаемых современным инструментарием.

Практическая значимость Разработанные модели и методы могут быть использованы коллектива ми, занимающимися разработкой микропроцессоров, для автоматизации по строения тестовых программ. Разработанный прототип системы построения тестовых программ использовался для генерации тестов подсистем управле ния памяти ряда микропроцессоров архитектуры MIPS64. Результаты рабо ты могут быть использованы в исследованиях, которые ведутся в Институте системного программирования РАН, Московском государственном институ те электроники и математики, НИИ системных исследований РАН, Инсти туте точной механики и вычислительной техники им. С.А. Лебедева РАН, Институте проблем информатики РАН и других научных и промышленных организациях.

Апробация работы и публикации По материалам диссертации опубликовано одиннадцать работ [1–11], в том числе одна [4] в издании, входящем в перечень ведущих рецензируемых научных журналов и изданий ВАК. Основные положения докладывались на следующих конференциях и семинарах:

1) на втором и третьем весеннем коллоквиуме молодых исследователей в области программной инженерии (SYRCoSE) (2008 и 2009 гг.);

2) на шестнадцатой и семнадцатой международной конференции студен тов, аспирантов и молодых ученых «Ломоносов» (2009 и 2010 гг.);





3) на шестнадцатой всероссийской межвузовской научно-технической кон ференции студентов и аспирантов «Микроэлектроника и информатика - 2009» (2009 г.);

4) на седьмом международном симпозиуме по проектированию и тестиро ванию под эгидой IEEE (EWDTS) (2009 г.);

5) на российско-ирландской летней школе по научным вычислениям ( г.);

6) на научной конференции «Тихоновские чтения» (2009 г.);

7) на научной конференции «Ломоносовские чтения» (2010 г.);

8) на объединенном научно-исследовательском семинаре имени М.Р. Шура Бура (2010 г.);

9) на семинаре Лаборатории вычислительных комплексов факультета вы числительной математики и кибернетики МГУ имени М.В.Ломоносова (2010 г.);

10) на семинаре отдела Технологий программирования института системно го программирования РАН (2009, 2010 гг.).

Структура и объем диссертации Работа состоит из введения, трех глав, заключения, списка литературы и приложений. Общий объем основной части диссертации составляет 125 стра ниц. Список литературы содержит 71 наименование.

Содержание работы Во Введении обоснована актуальность диссертационной работы, сформу лирована цель и задачи исследований, сформулированы полученные резуль таты и показана их практическая значимость.

Первая глава содержит обзор существующих методов построения тесто вых программ, обзор подсистем управления памяти и уточнение задач иссле дования по результатам этих обзоров.

В разделе 1.1 дается схема системного тестирования микропроцессора, описываются его отдельные этапы, в том числе и этап построения тестовых программ. Рассматриваются методы псевдослучайного и целенаправленного автоматического построения тестовых программ. В разделе 1.2 кратко опи сываются функции и типичный состав подсистем управления памяти, спо собы повышения их эффективности и классы ошибок. В разделе 1.3 сделан обзор методов целенаправленного построения тестовых программ. Выделены методы на основе массовой генерации тестовых программ и методы непосред ственного построения тестовых программ. В разделе 1.4 сделан анализ мето дов целенаправленного построения тестовых программ по применимости этих методов для тестирования подсистем управления памяти, масштабируемости, возможности «нацеливания» на функциональность. Наиболее перспективны ми являются методы непосредственного построения тестовых программ по тестовым ситуациям, формализованным в виде тестовых шаблонов — цепо чек инструкций с указанием вариантов исполнения инструкций — и методы, включающие разрешение ограничений (constraint satisfaction). В разделе 1. уточнены задачи в соответствии с проведенным исследованием методов по строения тестовых программ.

Во второй главе предложен подход целенаправленного построения наце ленных тестовых программ, сочетающий особенности перспективных методов построения тестовых программ. В разделе 2.1 описаны этапы построения те стовых программ согласно предлагаемому подходу: чтение документации по архитектуре, формализация архитектуры, выделение и формализация тесто вых ситуаций (в виде шаблонов тестовых программ, далее тестовых шаб лонов), построение и решение системы ограничений для каждого тестового шаблона, конструирование текста тестовой программы на основе решения каждой совместной системы ограничений.

Тестовый шаблон содержит последовательность инструкций, для каждой из которых указан вариант исполнения (т.е. некоторый путь выполнения ин струкции). Для алгоритмического построения ограничений и затем тестовых программ варианта инструкций должны быть формализованы в рамках эта па формализации микропроцессора. Раздел 2.2 более детально освещает этот этап. В этом разделе предложены модель функционирования устройств под системы управления памяти и модель вариантов инструкций. В рамках этого этапа следует выделить и формализовать те варианты инструкций, которые входят в тестовый шаблон, и задействованные в них устройства подсистемы управления памяти. Моделью состояния устройства подсистемы управления памяти (кэш-памяти, таблицы страниц и т.п.) предлагается последователь ность ассоциативных массивов (далее эта последовательность будет назы ваться таблицей, а отдельный ассоциативный массив — регионом). Каждый регион состоит из строк, каждая строка состоит из набора полей, поля де лятся на поля ключа и поля данных. Поля ключа задают ключи в ассоциа тивном массиве, поля данных — значения. В модели устройства определены следующие операции: успешного обращения, успешного обращения с измене нием, неуспешного обращения с замещением. На входе операции успешного обращения — выражение, задающие ключ, и выражение, задающее номер ассоциативного массива из состояния устройства. Операция определена на тех входных данных и состоянии модели, при которых в соответствующем ассоциативном массиве есть строка, поля ключей которой соответствуют аргументу-ключу этой операции. Операция возвращает поля данных соответ ствующей аргументу-ключу строки. Операция успешного обращения с изме нением отличается от операции успешного обращения дополнительным аргу ментом — полями данных, которые нужно заменить в строке, соответствую щей аргументу-ключу. На входе операции неуспешного обращения с замеще нием 3 аргумента: выражение, задающие ключ, выражение, задающее номер ассоциативного массива, и выражения для полей данных строки. Операция определена на тех входных данных и состоянии модели, при которых в соот ветствующем ассоциативном массиве нет строки, поля ключей которой соот ветствуют аргументу-ключу этой операции. Эффект операции заключается в замене полей данных одной из строк в ассоциативном массиве, номер кото рого был передан в качестве одного из аргументов операции, на переданные операции поля данных. Выбор строки для замены определяется на основе стратегии вытеснения так же, как это делается в устройствах подсистемы управления памяти (например, в кэш-памяти). В рамках этапа формализации следует указать набор атрибутов, задающих модели устройств тестируемой подсистемы управления памяти: стратегия вытеснения, количество строк в массиве («ассоциативность»), двоичный логарифм количества массивов, име на и битовые длины полей ключа и полей данных, предикат соответствия строки некоторой битовой строке (эта строка является аргументом-ключом в операциях над моделью). Алгоритмы построения систем ограничений пара метризованы этими атрибутами. Таким образом моделируются кэш-память различных уровней, таблицы страниц, буферы трансляции адресов (TLB) и даже оперативная память.

В том же разделе предложены модели вариантов инструкций. Варианты инструкций соответствуют отдельным путям выполнения инструкций. Мо дель варианта инструкции формализует следующие виды требований: до пустимые значения операндов инструкции, вычисление значений операндов результатов инструкции, условия возникновения исключительных ситуаций (если вариант инструкции состоит в возникновении такой ситуации), вычис ление адресов (физических, виртуальных, эффективных) в инструкции, об ращения в устройства подсистемы управления памяти и успешность этих об ращений, какие данные загружаются или сохраняются. При формализации для варианта инструкции объявляются операнды инструкции и последова тельность операторов 4-х видов: оператор утверждения истинности свойства над битовыми строками (assume), оператор введения новой переменной (let), оператор попадания (hit), оператор промаха (miss). С помощью этой по следовательности операторов задается набор условий на значения операндов инструкции и для моделей устройств, задействованных в этом варианте ин струкции, условия на их состояние и изменение этого состояния в рамках данного варианта. Операторы let и assume имеют ту же семантику, которая используется при формализации императивных языков программирования.

Операторы hit и miss специфичны инструкциям, оперирующим с памятью.

Оператор попадания hitB(k;

R){loaded(d);

[storing(d’);

] }, где k, R, d, d’ — выражения над определенными ранее переменными-битовыми стро ками, означает, что в данном варианте инструкции должно осуществляться успешное обращение в устройство B по ключу k в массив с номером R, при чем ключу соответствуют данные d (если полей данных несколько, то соот ветствующие выражения для них перечисляются в скобках у loaded). Если указана секция storing, то в варианте инструкции должно осуществляться успешное обращение с изменением на поля данных d’. Оператор промаха missB(k;

R){[replacing(d);

]}, где k, R, d — выражения над определен ными ранее переменными-битовыми строками, означает, что в данном вариан те инструкции должно быть неуспешное обращение в устройство B по ключу k в массив с номером R. Секция replacing задает поля данных d’ вытес няющей строки. Если секция replacing отсутствует, изменение состояния устройства B не должно происходить.

Формализовав устройства подсистемы управления памяти и инструкции и составив тестовый шаблон, нужно определить те значения регистров и хра нящиеся данные устройств, при которых исполнение инструкций, указанных в тестовом шаблоне, будет проходить согласно указанным там вариантам.

Для этого составляется система ограничений, выражающая все необходимые условия на такие значения. В результате разрешения этой системы определя ются искомые значения. В разделе 2.3 описывается предлагаемый алгоритм построения ограничений для тестового шаблона. Исполнение инструкций кон вейеризовано, поэтому расположенные рядом инструкции в действительности будут выполняться с существенной долей параллелизма. Однако в алгоритме генерации ограничений считается, что инструкции выполняются последова тельно, а тестовые шаблоны составлены таким образом, чтобы при работе соответствующих им тестовых программ проявились все нужные параллель ные эффекты.

По каждому оператору алгоритм строит свою часть ограничений, кото рые выражают семантику этого оператора. Операторы обращений в устрой ства транслируются в ограничения без моделирования состояний устройств, несмотря на то, что определение этих операторов включало состояние устрой ства. Это позволяет существенно уменьшить количество переменных-бито вых строк и размер ограничений и, тем самым, ускорить разрешение ограни чений. Специальное представление выбрано и для начального содержимого устройств, а именно, последовательность обращений в это устройство. По этому в число переменных в ограничениях входят переменные, задающие аргументы этих, инициализирующих, обращений: ключи, номера ассоциатив ных массивов. Для операторов hit и miss строятся ограничения на аргу менты-ключи k и номера регионов R (эти ограничения должны гарантиро вать успешное обращение для hit и неуспешное — для miss) и ограничения на аргументы-данные d и d’ (обращения по одинаковым адресам должны давать одинаковые данные, если они не были изменены). Ограничения на ар гументы-ключи и аргументы-номера регионов строятся согласно следующим определениям операторов: hit(ki ;

Ri ) / miss(ki ;

Ri ) происходит, если () перед ним есть обращение по тому же ключу (ki ) в тот же регион (Ri ), () после которого и до этого обращения соответствующая строка не была вытеснена / была вытеснена из таблицы.

Трансляция свойства достаточно очевидна, трансляция свойства рас сматривается в разделе 2.5.

В этом же разделе диссертации сформулированы и доказаны теоремы кор ректности и полноты алгоритмов, гарантирующие, что ограничений, постро енные согласно алгоритму, не дают решений, не соответствующих тестовому шаблону, и задают все решения, соответствующие тестовому шаблону. Зна чение атрибута модели устройства, задающего стратегию вытеснения, рав ное none, означает, что при неуспешном обращении в это устройство заме щение не производится. Здесь и далее символами t1, t2,..., tm обозначаются аргументы-ключи инициализирующих обращений, r1, r2,..., rm — аргументы регионы инициализирующих обращений, k1, k2,..., kn — аргументы-ключи об ращений в инструкциях тестового шаблона, R1, R2,..., Rn — аргументы-реги оны обращений в инструкциях тестового шаблона, S1, S2,..., Sn — успешности обращений в инструкциях тестового шаблона (Si = hit или Si = miss).

Теорема 1 (Корректность алгоритма генерации ограничений на ключи обра щений для таблицы, стратегия вытеснения которой не none). Если система ограничений, построенная для последовательности обращений к таблице (S1, k1, R1 ), (S2, k2, R2 ),..., (Sn, kn, Rn ) c дополнительным предикатом P (k1, k2,..., kn, R1, R2,..., Rn ), является совместной, то ее решение t1, t2,..., tm, r1, r2,..., rm, k1, k2,..., kn, R1, R2,..., Rn, удовлетворяет последовательности S1,..., Sn и P при любом начальном состоянии таблицы.

Теорема 2 (Полнота алгоритма генерации ограничений на ключи обраще ний для таблицы, стратегия вытеснения которой есть none). Фиксируем неко торое начальное состояние L таблицы со стратегией вытеснения none.

Если при нем для последовательности обращений к таблице (S1, k1, R1 ), (S2, k2, R2 ),..., (Sn, kn, Rn ) c дополнительным предикатом P (k1, k2,..., kn, R1, R2,..., Rn ) существуют значения переменных k1, k2,..., kn и R1, R2,..., Rn, которые удовлетворяют последовательности S1, S2,..., Sn и P, то систе ма ограничений, построенная согласно алгоритму генерации ограничений на ключи обращений для таблицы со стратегией вытеснения none, будет совместной.

Стратегию вытеснения будем называть существенно вытесняющей, если w промахов в один регион полностью вытесняют его предыдущее содержимое (w — значение параметра lines таблицы).

Теорема 3 (Полнота алгоритма генерации ограничений на ключи обращений для таблицы, стратегия вытеснения которой не none и является существен но вытесняющей). Фиксируем некоторое начальное состояние L таблицы со стратегией вытеснения не none. Если при нем для последовательности обращений к таблице (S1, k1, R1 ), (S2, k2, R2 ),..., (Sn, kn, Rn ) c дополнитель ным предикатом P (k1, k2,..., kn, R1, R2,..., Rn ) существуют значения пере менных k1, k2,..., kn и R1, R2,..., Rn, которые удовлетворяют последова тельности S1, S2,..., Sn и P, то система ограничений, построенная соглас но алгоритму генерации ограничений на ключи обращений для таблицы со стратегией вытеснения не none, будет совместной, если стратегия вытес нения является «существенно вытесняющей».

В разделе 2.3.2 рассматриваются таблицы вытеснения, которые позволя ют формализовать стратегии вытеснения. Таблицы вытеснения были предло жены в 2008 году исследователями из Университета Саарланда. С использо ванием таблиц вытеснения в разделе 2.3.3 сформулированы и доказаны тео ремы о том, что стратегии вытеснения LRU, FIFO и Pseudo-LRU являются существенно вытесняющими:

Теорема 4. Стратегия вытеснения LRU является существенно вытесня ющей.

Теорема 5. Стратегия вытеснения FIFO является существенно вытесня ющей.

Теорема 6. Стратегия вытеснения Pseudo-LRU является существенно вы тесняющей.

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

Утверждение 1 (Верхняя оценка количества инициализирующих обраще ний).

n · (n + 2w) m где w — значение параметра lines таблицы, n — количество обращений в таблицу в шаблоне.

Для стратегии вытеснения LRU в этом же разделе сформулирована и доказана более сильная оценка количества инициализирующих обращений:

Теорема 7 (Верхняя оценка количества инициализирующих обращений для стратегии вытеснения LRU). Фиксируем некоторое начальное состояние L таблицы со стратегией вытеснения LRU. Если при нем для последователь ности обращений к таблице (S1, k1, R1 ), (S2, k2, R2 ),..., (Sn, kn, Rn ) c допол нительным предикатом P (k1, k2,..., kn, R1, R2,..., Rn ) существуют значе ния переменных k1, k2,..., kn и R1, R2,..., Rn, которые удовлетворяют по следовательности S1, S2,..., Sn и P, то система ограничений, построенная согласно алгоритму генерации ограничений на ключи обращений будет сов местной для любого m n · w + M, где M – количество элементов после довательности S1, S2,..., Sn, равных miss.

В разделе 2.4 предложено новое определение стратегии вытеснения Pseudo LRU. Обычно при определении Pseudo-LRU предлагают рассматривать для региона упорядоченное бинарное дерево с пометками в нелистовых вершинах, листовым вершинам дерева соответствуют строки региона. Как и прежде, об ращения осуществляются к одной из листовых вершин дерева, что приводит к изменению пометок вершин пути в неё из корневой вершины. Вытесняемая строка определяется также на основе пометок вершин дерева. Новое опреде ление задает стратегию вытеснения Pseudo-LRU как изменение битовых век торов (Pseudo-LRU-ветвей), сопоставленных строкам региона. Это определе ние позволит сократить количество ограничений и ускорить их разрешение.

Сформулирована и доказана теорема, задающее изменение Pseudo-LRU-вет вей и показывающая эквивалентность нового определения Pseudo-LRU ста рому (W = log2 w, для стратегии вытеснения Pseudo-LRU допустимы лишь те w, которые являются степенями двойки, абсолютная позиция(или просто, позиция) — это номер строки в регионе, относительная позиция позиции i относительно позиции j будем назыаать i j и обозначать как j ):

i Теорема 8 (Инвариантность преобразования Pseudo-LRU-ветвей относитель ными позициями). Пусть (1 2... W ) — Pseudo-LRU-ветвь некоторой позиции i. Тогда изменение этой ветви согласно стратегии вытеснения Pseudo-LRU определяется только относительной позицией (относительно i) и происходит следующим образом при обращении к ключу с (абсолютной) позицией j: если j [ 2k, w w i для некоторого k = 1, 2,..., W, то происхо ) 2k i дит изменение 1 := 0, 2 := 0,..., k1 := 0, k := 1;

если j = 0, то происходит изменение 1 := 0, 2 := 0,..., W := 0;

вытеснение ключа на позиции i происходит в том случае, когда 1 = 1 2 = 1... W = 1.

В разделе 2.5 предложен метод построения ограничений для свойства «быть вытесненным к моменту заданного обращения в таблицу» — метод по лезных обращений. С помощью него это свойство выражается в виде ограни чений в операциях над битовыми строками и целочисленной линейной ариф метике. В разделе предложена формализация понятия полезной для вытес нения (или просто, полезной) инструкции. Формулой полезного обращения будем называть предикат, истинный для всех обращений, являющихся полез ными, и ложный на всех обращениях, не являющихся полезными. В рамках метода полезных обращений свойство «быть вытесненным» рассматривает ся как ограничение снизу количества предыдущих обращений, являющихся полезными.

В разделе 2.5.1 предложено и формально обосновано представление свой ства «быть вытесненным» для стратегии вытеснения LRU в виде ограниче ний, составленное по методу полезных обращений («||» — операция битовой конкатенации, выражение [] равно 1, если истинно, и равно 0 в противном случае):

Теорема 9 (Выражение свойства «быть вытесненным» для LRU). Пусть (t1, r1 ), (t2, r2 ),..., (tm, rm ) – ключи и регионы инициализирующих обраще ний, (ki, Ri ) – ключ и регион обращения, для которого описывается вытес нение (будем его называть «вытесняемым»), причем (ki ||Ri ) {(t1 ||r1 ),..., (tm ||rm ), (k1 ||R1 ),..., (ki1 ||Ri1 )} и {(t1 ||r1 ),..., (tm ||rm )} — все разные. Тогда ki не вытеснен из региона Ri согласно определению LRU на перестановках тогда и только тогда, когда m+n [uki,Ri (sj )] w j= где последовательность s (t1 ||r1 ),..., (tm ||rm ), (k1 ||R1 ),..., (kn ||Rn ), R(si ) — вторая компонента si (регион), а формула полезного обращения такая:

uki,Ri (sj ) ((ki ||Ri ) {sj,..., sm+n } Ri = R(sj ) sj {sj+1,..., sm+n }) / / В разделе 2.5.2 предложено и формально обосновано представление свой ства «быть вытесненным» для стратегии вытеснения FIFO в виде ограниче ний, составленное по методу полезных обращений.

В разделе 2.5.3 предложено и формально обосновано представление свой ства «быть вытесненным» для стратегии вытеснения Pseudo-LRU в виде огра ничений, составленное по методу полезных обращений:

Теорема 10 (Выражение свойства «быть вытесненным» для Pseudo-LRU).

Пусть (t1, r1 ), (t2, r2 ),..., (tm, rm ) – ключи и регионы инициализирующих обращений, а (ki, Ri ) – ключ и регион обращения, для которого описыва ется вытеснение (будем его называть «вытесняемым»), причем (ki ||Ri ) {(t1 ||r1 ),..., (tm ||rm ), (k1 ||R1 ),..., (ki1 ||Ri1 )} и {(t1 ||r1 ),..., (tm ||rm )} — все разные. Тогда k не вытеснен из региона R согласно трактовке Pseudo-LRU в терминах ветвей бинарного дерева тогда и только тогда, когда m+n [uki,Ri,i (sj )] W j= где последовательность s (t1 ||r1 ),..., (tm ||rm ), (k1 ||R1 ),..., (kn ||Rn ), R(si ) — вторая компонента si (регион), а формула полезного обращения такая:

(ki ||Ri ) {sj, sj+1,..., sm+n } / Ri = R(sj ) (i ||Ri ) {(j ||Rj ), (j+1 ||Rj+1 ),..., (m+n ||Rm+n )} uki,Ri,i (sj ) m+n (Rj = Rk (i ||Ri ) {(j ||Rj ), (j+1 ||Rj+1 ),..., (k ||Rk )} / k=j+ P (j i, k i )) P (x, y) (y x x y x) i определено следующим образом: если Si = hit, то (ite ((ki ||Ri ) = (ki1 ||Ri1 )) (i = i1 ) (ite ((ki ||Ri ) = (ki2 ||Ri2 )) (i = i2 )... (i = 0))))...) если Si = miss, то ( {i,..., j }m обозначает подмножество множества позиций от i’го до j’го обращения из неуспешных обращений):

(ite ((ki ||Ri ) = (ki1 ||Ri1 )) (i = i1 ) (ite ((ki ||Ri ) = (ki2 ||Ri2 )) (i = i2 i {i1 }m ) (ite ((ki ||Ri ) = (ki3 ||Ri3 )) (i = i3 i {i1, i2 }m )... (i = 0))))...) i — позиции — дополнительные переменные, для которых надо постро ить ограничения: конъюнкцию для каждой пары (si, i ) и (sj, j ) при j i ограничений:

• если j’е обращение успешное, то (i ||R(si ) = j ||R(sj ) i ||R(si ) {m1 ||R(sm1 ), m2 ||R(sm2 ),..., mn ||R(smn )}) si = sj / • в противном случае (i ||R(si ) = j ||R(sj ) i ||R(si ) {m1 ||R(sm1 ), m2 ||R(sm2 ),..., mn ||R(smn )}) si = sj / где (m1, R(sm1 )), (m2, R(sm2 )),..., (mn, R(smn )) — позиции и регионы неуспешных обращений, расположенных между i’м и j’м.

В разделе 2.5.4 освещаются некоторые вопросы сложности разрешения ограничений, которые строятся согласно методу полезных обращений.

В разделе 2.6 рассматривается последний этап построения тестовой про граммы — этап конструирования текста программы. Текст тестовой програм мы состоит из инициализирующей части и инструкций тестового шаблона.

Инициализирующая часть состоит из инструкций для помещения вычислен ных на предыдущем этапе начальных значений в соответствующие регистры и последовательности инструкций, обращающихся в соответствующее устрой ство подсистемы управления памяти по вычисленным ключам в вычисленные регистры с вычисленными данными. Зачастую конструирование таких ин струкций не представляет сложности. Пример противоположного случая — инициализация многоуровневой кэш-памяти в случае, если инициализацию отдельных уровней кэш-памяти нельзя осуществить отдельно от остальных уровней. Поэтому в разделе 2.6 предложен и метод конструирования после довательности инициализирующих инструкций, учитывающий особенности многоуровневой кэш-памяти.

В третьей главе дается оценка предлагаемым методам. В разделах 3.1, 3. и 3.3 показывается, что подсистемы управления памяти микропроцессоров ар хитектур MIPS, PowerPC и IA-32 можно представить в виде набора таблиц и формализовать варианты инструкций, оперирующих с памятью. Причем име ется документация по каждой архитектуре, где эти варианты уже описаны на соответствующем псевдокоде. В разделе 3.4 описана автоматизация некото рых этапов предлагаемого во второй главе подхода: генератор ограничений, решатель ограничений и конструктор текстов тестовых программ. Решатель ограничений — это внешний инструмент (Z3) и разрабатывать его для авто матизации подхода не надо, что сильно сокращает трудоемкость автоматиза ции подхода. Затронут вопрос переиспользования перечисленных компонен тов при смене микропроцессора. Был реализован прототип генератора тесто вых программ для архитектуры MIPS64. В разделе 3.5 описаны эксперимен ты над этим прототипом по оценке времени построения тестовых программ и вероятности завершения построения за 60 секунд. Эксперименты показа ли увеличение допустимого размера тестовых шаблонов до 9-12 инструкций (по сравнению с 2-3 инструкциями в доступных инструментах). В разделе 3. проведено сравнение с инструментом Genesys-Pro (IBM): выделены сходства и отличия, преимущества и недостатки предложенных методов по сравнению с Genesys-Pro. В разделе 3.7 проведено сравнение с работами, проводящимися в Intel.

В Заключении диссертационной работы перечисляются ее основные ре зультаты.

Основные результаты работы 1) Предложен подход к построению тестовых программ для проверки под систем управления памяти микропроцессоров, позволяющий понизить сложность построения некоторого класса тестовых программ. Этот класс состоит из тестовых программ, в которых имеется цепочка длиной от 6 до 12 инструкций обращения к памяти. Понижение сложности обос новано при помощи ряда экспериментов на прототипе программного средства построения тестовых программ. Теоретически обоснована кор ректность алгоритмов в рамках предложенного подхода к построению тестовых программ. В рамках предложенного подхода разработаны мо дели устройств подсистемы управления памяти и модели вариантов ис полнения инструкций.

2) В рамках предложенного подхода разработан метод формализации ме ханизма вытеснения данных, позволяющий в отличие от других методов моделирования выразить ряд свойств вытесняемых данных в виде огра ничений, причем эти ограничения эффективно разрешаются современ ным инструментарием. Теоретически обоснована корректность метода формализации для ряда стратегий вытеснения. Показано применение метода формализации к нескольким важным на практике стратегиям вытеснения.

Публикации по теме диссертации [1] Корныхин, Е. В. Система генерации тестовых программ с использовани ем ограничений ТЕСЛА / Е. В. Корныхин // Сборник тезисов конфе ренции Ломоносов. — 2009. — С. 39.

[2] Корныхин, Е. В. Генерация тестовых данных для тестирования ариф метических операций центральных процессоров / Е. В. Корныхин // Труды Института Системного Программирования. — 2008. — Т. 15. — С. 107–117.

[3] Корныхин, Е. В. Система генерации тестовых данных для системного функционального тестирования микропроцессоров ТЕСЛА / Е. В. Кор ныхин // Сборник тезисов конференции «Микроэлектроника и инфор матика». — 2009. — С. 87.

[4] Корныхин, Е. В. Генерация тестовых данных для тестирования механиз мов кэширования и трансляции адресов микропроцессоров / Е. В. Кор ныхин // Программирование. — 2010. — Т. 36, № 1. — С. 40–49.

[5] Корныхин, Е. В. Метод зеркальной генерации ограничений для постро ения тестовых программ по тестовым шаблонам / Е. В. Корныхин // Труды Института Системного Программирования. — 2010. — Т. 18. — С. 67–80.

[6] Корныхин, Е. В. Генерация тестовых данных для системного функцио нального тестирования микропроцессоров с учетом кэширования и транс ляции адресов / Е. В. Корныхин // Труды Института Системного Программирования. — 2009. — Т. 17. — С. 145–160.

[7] Корныхин, Е. В. Генерация тестовых данных для системного функцио нального тестирования fo-кэш-памяти микропроцессоров / Е. В. Корны хин // Вычислительные методы и программирование. — 2009. — Т. 10. — С. 107–116.

[8] Корныхин, Е. В. Определение стратегии вытеснения pseudolru на ветвях бинарного дерева / Е. В. Корныхин // Сборник тезисов конференции Ломоносов. — 2010. — С. 20–21.

[9] Kornikhin, E. Smt-based test program generation for cache-memory testing / E. Kornikhin // Proceedings of 7th East-West Design & Test Symposium. — 2009. — Pp. 124–127.

[10] Kornikhin, E. Test data generation for lru cache-memory testing / E. Ko rnikhin // Proceedings of Spring Young Researchers’ Colloquium on Software Engineering. — 2009. — Pp. 88–92.

[11] Kornikhin, E. Test data generation for arithmetic subsystem of cpus mips64 / E. Kornikhin // Proceedings of Spring Young Researchers’ Colloquium on Software Engineering. — 2008. — Vol. 2. — Pp. 43–46.



 

Похожие работы:





 
2013 www.netess.ru - «Бесплатная библиотека авторефератов кандидатских и докторских диссертаций»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.