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


с. 1



МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

имени М.В. Ломоносова
ФАКУЛЬТЕТ ВЫЧИСЛИТЕЛЬНОЙ МАТЕМАТИКИ И КИБЕРНЕТИКИ
СТЕНОГРАММА

заседания диссертационного совета Д 501.001.44

в Московском государственном университете

имени М.В. Ломоносова


от 26 ноября 2010 г.
Защита диссертации на соискание ученой степени кандидата физико-математических наук КОРНЫХИНА ЕВГЕНИЯ ВАЛЕРЬЕВИЧА на тему: «Построение тестовых программ для проверки подсистем управления памяти микропроцессоров».
Специальность: 05.13.11 – математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей.



Научный руководитель:

Петренко Александр Константинович,

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

заведующий отделом Института системного программирования РАН


Официальные оппоненты:

Смелянский Руслан Леонидович,

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


академик РАЕН, заведующий лабораторией факультета ВМК МГУ имени М.В. Ломоносова





Лацис Алексей Оттович,

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

заведующий сектором Института прикладной математики РАН


Ведущая организация

Учреждение Российской академии наук Научно-исследовательский институт системных исследований РАН

СТЕНОГРАММА

заседания диссертационного совета Д 501.001.44

от 26 ноября 2010.


ПРЕДСЕДАТЕЛЬ СОВЕТА - профессор Королев Л.Н.

УЧЕНЫЙ СЕКРЕТАРЬ СОВЕТА - профессор Трифонов Н.П.


На заседании присутствуют члены совета:


1

Королев Л.Н.

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

05.13.11

2

Васильев Ф.П.

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

01.01.09

3

Круглов В.М.

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

01.01.05

4

Трифонов Н.П.

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

05.13.11

5

Алексеев В.Б.

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

01.01.09

6

Васин А.А.

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

01.01.09

7

Королев В.Ю.

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

01.01.05

8

Краснощеков П.С.

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

01.01.09

9

Ложкин С.А.

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

01.01.09

10

Мальковский М.Г.

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

05.13.11

11

Машечкин И.В.

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

05.13.11

12

Новикова Н.М.

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

01.01.09

13

Рябов Г.Г.

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

05.13.11

14

Сапоженко А.А.

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

01.01.09

15

Сенатов В.В.

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

01.01.05

16

Смелянский Р.Л.

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

05.13.11

17

Соловьев С.Ю.

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

05.13.11

18

Ушаков В.Г.

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

01.01.05

19

Чибисов Д.М.

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

01.01.05

КОРОЛЕВ Л.Н.

Мы можем приступить к нашей работе. На повестке дня защита: Корныхин Евгений Валерьевич собирается представить свою диссертацию на наше рассмотрение "Построение тестовых программ для проверки подсистем управления памяти микропроцессоров" по специальности 05.13.11. Научный руководитель — Петренко Александр Константинович, доктор физико-математических наук. Официальные оппоненты — доктор физико-математических наук Смелянский Руслан Леонидович и доктор физико-математических наук Лацис Алексей Оттович. Ведущая организация — Научно-исследовательский институт системных исследований РАН.

Слово для ознакомления с личными документами соискателя предоставляется ученому секретарю диссертационного совета проф. Трифонову Н.П.


ТРИФОНОВ Н.П.

Оглашает материалы личного дела соискателя. (Все представленные документы и материалы полностью соответствуют требованиям «Положения о порядке присуждения ученых степеней ВАК РФ»). Личное дело прилагается.


КОРОЛЕВ Л.Н.

Есть ли вопросы к ученому секретарю по материалам личного дела соискателя? Нет вопросов. Евгений Валерьевич, просьба коротко и чётко рассказать об основных результатах работы.


ЧИБИСОВ Д.М.

Можно сразу вопрос по заголовку? «Управления памяти» у меня как-то не согласуется грамматически. Управляют чем?


КОРНЫХИН Е.В.

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


КОРНЫХИН Е.В.

Докладывает основные положения диссертационной работы. Автореферат прилагается.


КОРОЛЕВ Л.Н.

Есть ли вопросы к заслушанному сообщению?


ТРИФОНОВ Н.П.

Поясните, пожалуйста, на счет «ограничений»: что это за «ограничения», откуда они берутся, как задаются?


КОРНЫХИН Е.В.

Речь идет о системах уравнений и неравенств — их я для краткости назвал «ограничениями».


ТРИФОНОВ Н.П.

Ограничений на что?


КОРНЫХИН Е.В.

Ограничения на данные, с которыми работает генерируемая тестовая программа.


КОРОЛЕВ Л.Н.

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


КОРНЫХИН Е.В.

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


КОРОЛЕВ Л.Н.

Протестировать на предмет того, чтобы выяснить, насколько предложенная идея огранизации кэш-памяти эффективна? Много ли происходит промахов?


КОРНЫХИН Е.В.

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


КОРОЛЕВ Л.Н.

Насколько полна система тестов, которые автоматически генерируются Вашим инструментом? Можно ли об этом что-нибудь сказать? Охватывает ли она все возможные ньюансы, которые могут появиться при выполнении пользовательских программ на микропроцессоре?


КОРНЫХИН Е.В.

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


КОРОЛЕВ Л.Н.

Тестовые шаблоны Вы сами не создаете?


КОРНЫХИН Е.В.

Не создаю, и поэтому задача о полноте тестирования относится к алгоритмам выбора тестовых шаблонов.


КОРОЛЕВ Л.Н.

Кто создает тестовые шаблоны? Разработчик микропроцессора?


КОРНЫХИН Е.В.

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


КОРОЛЕВ Л.Н.

Хотелось, чтобы Вы привели формулировку какой-нибудь теоремы.


КОРНЫХИН Е.В.

На слайде приведена формулировка первой теоремы диссертации — это теорема о корректности метода построения ограничений для всего тестового шаблона.


ТРИФОНОВ Н.П.

Там было ограничение 60 секунд. Что это за ограничение? Почему именно 60 секунд?


КОРНЫХИН Е.В.

Это ограничение на время построения тестовой программы. Поскольку основное время тратится на решение ограничений, то по сути это ограничение на время решения ограничений. У этого числа есть ограничение как снизу, так и сверху.

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

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


ТРИФОНОВ Н.П.

Для нас важно время, затраченное на построение тестовых программ, или их качество? Чтобы повысить качество, нужно увеличить время.


КОРНЫХИН Е.В.

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


ТРИФОНОВ Н.П.

Что значит «часто»? Каждый час?


КОРНЫХИН Е.В.

Например, каждый день.


ТРИФОНОВ Н.П.

Каждый день появляется новая проектная модель?


КОРНЫХИН Е.В.

Могут меняться некоторые алгоритмы работы модели, которые требуеют повторного тестирования.


КОРОЛЕВ Л.Н.

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


МАШЕЧКИН И.В.

60 секунд зависит еще и от платформы, на которой строятся тестовые программы. Это не абсолютная граница, просто как пример. 60 секунд на ноутбуке или на сервере — это разные вещи.


КОРОЛЕВ Л.Н.

Пожалуйста, еще вопросы, если есть. Вопросов нет. Тогда слово предоставляется научному руководителю.


ПЕТРЕНКО А.К.

Я сначала хочу рассказать о диссертанте, а потом о задаче. Диссертант на нашем спецсеминаре появился с 4 курса, активно работал. Потом очень активно учился в аспирантуре. Помимо работы над исследовательской темой, он всегда активно участвовал в учебном процессе и сейчас участвует, хотя формально является сотрудником Института, и в ближайшее время есть планы вернуться обратно в Университет. В плане творческого подхода я скажу, что Евгений здесь в пятерке моих аспирантов, с которыми я за последние лет двадцать работаю. Это реальное творчество, которое не нужно подбадривать, подталкивать. Может быть, иногда надо направлять, но опять же не очень.

В качестве иллюстрации, можно сказать, что идея построения тестов как решение системы уравнений появилась давно (красивая идея, хотелось это делать). Евгений первые три года активно занимался аналитическим построением тестов для программ на Java, были вскрыты серьезные проблемы. Одновременно с этим он получил серьезное основательное представление о том, какие имеются решатели, в конечном итоге выбрал в действительности самый лучший решатель, который есть сейчас в распоряжении, это продукт Microsoft Research. Вникнув во всю эту проблему, он, в действительности сам, без внешнего давления, без особых подсказок, сместил поле исследования: он ушел с Java и перешел на тестирование микропроцессоров. Здесь оказались два «плюса»: во-первых, серьезное тестирование микропроцессоров гораздо более востребовано, чем тестирование какого бы то ни было программного обеспечения, риски и возможные потери (например, финансовые) в сроках при ошибках в микропроцессоре существенно, на порядки, выше, чем риски, которые имеются при программном обеспечении. Известно, что одна ошибка Intel стоила полмиллиарда долларов. Я не знаю ошибки в программном обеспечении такой цены. Кроме того, архитектура микропроцессоров в некотором плане регулярнее, чем архитектура программного обеспечения. И, поэтому, достижения в решателях, которые сейчас имеются, позволяют для микропроцессоров многие задачи решать аналитически, что диссертант и продемонстрировал в своей работе.

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

У диссертанта был достаточно ограниченный обзор литературы по данной теме. На основе наших контактов с компанией Intel удалось узнать, что техники верификации — это самый главный технический секрет компании Intel. Для меня это было несколько странным, я пытался объяснить, почему так происходит. Одно из объяснений следующее. Как только микропроцессор выходит на рынок, его дизайн перестает быть секретом. Всё, что было задумано лет пять назад, выкладывается, и все могут посмотреть: какая система команд, какая архитектура, можно сделать реверс-инжиниринг. А каким образом компания сумела это вывести на рынок, добиться хорошего качества, технологии и инструменты тестирования — вот это настоящий секрет, это можно не раскрывать. И, поэтому, здесь очень многие вещи приходится изобретать заново. Хотя абсолютно точно можно сказать, что у IBM есть аналогичные инструменты, у Intel, у AMD. Но если про инструменты IBM есть хоть какие-то публикации, то про инструменты Intel и AMD вообще никаких публикаций. Это самая строго охраняемая вещь. Поэтому поскольку в России сейчас начинают делать серьезные микропроцессоры, это очень серьезная задача.
КОРОЛЕВ Л.Н.

Спасибо, есть ли вопросы к научному руководителю?


МАШЕЧКИН И.В.

Кому такая работа нужна, если вы ее уже открыли?


ПЕТРЕНКО А.К.

Большие компании, IBM, Boeing, Microsoft, уже сейчас начинают открывать очень технически сложные вещи, потому что если их не открыть, в мире не появятся специалисты, которые, во-первых, сумеют ими пользоваться, а, во-вторых, сумеют развивать эту тему. На инструмент Z3, решатель ограничений, Microsoft потратил 30 миллионов долларов, два года он был совершенно секретным, а потом Microsoft понял, что внутри него есть десять человек, которые умеют этим инструментом пользоваться, а этого недостаточно — нужна сотня специалистов. Это была одна из причин, почему Z3 открывается, чтобы все по крайней мере научились им пользоваться. Т.е. в особо сложных технологиях ситуация сейчас такая, что, с одной стороны, тенденция к засекречиванию, а с другой стороны – вынужденно приходится что-то открывать.


КОРОЛЕВ Л.Н.

Есть ли еще вопросы? Спасибо. Слово предоставляется проф. Трифонову Н.П. для информации о поступивших отзывах.


ТРИФОНОВ Н.П.

Ведущая организация – Научно-исследовательский институт системных исследований. Зачитывается отзыв (отзыв прилагается). Отзывов на автореферат не поступило.


КОРОЛЕВ Л.Н.

Спасибо. Желает ли соискатель ответить на замечания ведущей организации?


КОРНЫХИН Е.В.

Согласен со сделанными замечениями.


КОРОЛЕВ Л.Н.

Переходим к обсуждению работы. Слово предоставляется доктору физико-математических наук, профессору Руслану Леонидовичу Смелянскому.


СМЕЛЯНСКИЙ Р.Л.

Зачитывает отзыв (отзыв прилагается).


КОРОЛЕВ Л.Н.

Спасибо. Желает ли кто-нибудь задать вопросы официальному оппоненту?


МАШЕЧКИН И.В.

Руслан Леонидович, а удалось ли разобраться с содержимым диссертации в условиях данной путаницы в обозначениях?


СМЕЛЯНСКИЙ Р.Л.

Конечно, были беседы с автором.


КОРОЛЕВ Л.Н.

Евгений Валерьевич, желаете ли Вы ответить на серьезные замечания Руслана Леонидовича?


КОРНЫХИН Е.В.

Я согласен с замечаниями.


КОРОЛЕВ Л.Н.

Теперь слово представляется оппоненту Лацису Алексею Оттовичу.


ЛАЦИС А.О.

Зачитывает отзыв (отзыв прилагается).


КОРОЛЕВ Л.Н.

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


ЛАЦИС А.О.

Мне кажется, работу надо судить по тому, что в ней есть, а не по тому, чего в ней нет, ведь прежде, чем «воевать» за когерентность, надо, чтобы составные части правильно работали. А это уже нелегко. Раньше у электронщиков было такое выражение, когда начинали проектировать новый большой компьютер, можно было указать на модель и сказать: «У тебя здесь датчик случайных чисел». Это был приговор, зачеркни проект, не пытайся это сделать, ты это никогда не отладишь. Сейчас приходится пытаться это сделать, потому что всё остальное работает медленно. Умение правильно разбить на части и хорошо отработать каждую часть, это очень много. А то, что этим не ограничивается количество задач, это естественно: каждый что-то делает и что-то не делает.


КОРОЛЕВ Л.Н.

Спасибо, желает ли еще кто-нибудь задать вопросы? Нет, благодарю Вас. Желает ли диссертант ответить на замечания?


КОРНЫХИН Е.В.

Я согласен с замечаниями уважаемого оппонента.


КОРОЛЕВ Л.Н.

Мы можем приступить к общей дискуссии. Я хотел бы возразить Алексею Оттовичу. Мне уже возражали, что если нашли теоремы и никуда их не «приложили», говорят, что тем не менее такая абстрактная проблематика двигает науку вперед: глядишь — где-нибудь и пригодится. Правильно ли это заключение, что всё должно быть привязано к конкретной проблематике?


ЛАЦИС А.О.

Нет, конечно. Мне кажется, что существуют работы, про которые можно высказаться так, как я высказался. Это экспертная оценка. Я не говорю о любых работах, не имеющих практического приложения. Есть работы, на которых большими буквами написано: «Это бессмыслица» - при том, что из «AB следует А». Об этом трудно говорить, не имея в руках конкретного примера.


СМЕЛЯНСКИЙ Р.Л.

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

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

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


КОРОЛЕВ Л.Н.

Спасибо. Желает ли кто-нибудь еще выступить в порядке общей дискуссии? Таких желающих нет. Тогда, уважаемый соискатель, Вам предоставляется заключительное слово.


КОРНЫХИН Е.В.

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


КОРОЛЕВ Л.Н.

Спасибо. Предлагается следующий состав счетной комиссии:



  1. Васин А.А. д.ф.-м.н.

  2. Машечкин И.В. д.ф.-м.н.

  3. Чибисов Д.М. д.ф.-м.н.

Нет возражений против такого состава комиссии? (Возражений нет. Состав счетной комиссии утверждается единогласно. Объявляется перерыв для тайного голосования).
КОРОЛЕВ Л.Н.

Слово представляется председателю счетной комиссии для оглашения результатов тайного голосования.


ЧИБИСОВ Д.М.

(зачитывается протокол счетной комиссии).



В составе диссертационного совета

-23 чел.

Присутствовало на заседании

-19 чел.

Докторов наук по профилю рассматриваемой диссертации

-6 чел.

Роздано бюллетеней членам совета

- 19

Осталось нерозданных бюллетеней

- 0

Оказалось в урне

- 19

Результаты голосования за присуждение ученой степени кандидата физико-математических наук КОРНЫХИНУ ЕВГЕНИЮ ВАЛЕРЬЕВИЧУ:


Подано голосов:


За

- 19

Против

- нет

Недействительных бюллетеней

- нет

КОРОЛЕВ Л.Н.

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

Прошу всех ознакомиться с проектом заключения. Какие будут замечания?


СМЕЛЯНСКИЙ Р.Л.

Я бы предложил вернуться к нормам русского языка и указать в заключении «подсистемы управления памятью».


КОРОЛЕВ Л.Н.

Никто не против, чтобы так поправить? Есть предложение утвердить заключение с высказанными правками. Заключение диссертационного совета принимается единогласно.


Председатель диссертационного совета

д.ф-м.н., профессор Королев Л.Н.

Ученый секретарь диссертационного совета

профессор Трифонов Н.П.


26 ноября 2010 года.
с. 1

скачать файл