Отзыв на автореферат (1149940)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

отзыв на автореферат диссертации Подкопаева Антона Викторовича <<Операционные методы в приложении к слабым моделям памяти», представленной на соискание ученой степени кандидата физико-математических наук по специальности 05.13.11 кМатематическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей» Диссертационная работа Подкопаева А.В.

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

Следует отметить, что результаты исследований в данной области активно применяются при разработке операционных систем, компиляторов и процессоров. Таким образом, актуальность темы не вызывает сомнений. В работе А.В.Подкопаева решаются следующие проблемы. Во-первых, предлагается операционная модель памяти для языка С/С++, которая решает ряд актуальных проблем — в частности, исключает появление при исполнении программ "значений из воздуха" и обосновывает эффективные проекции при компиляции. Далее, автором доказывается корректность компиляции для "обещающей" семантики для двух моделей архитектуры АКМ.

К сильным сторонам работы следует отнести то, что она выполнена с использованием самых последних достижений данной области. Для части Старший научный сотрудник Федерального государственного бюджетного учреждения науки Санкт-Петербургское отделение Математического института им. В, А.

Стеклова Российской академии наук (ПОМИ РАН), доктор физико-математических наук Куликов А.С. Телефон: (812) 571 43 92 Е-та11: а1ехапс1ег.з.1а~Нсоч а11.сотп Куликов Александр Сергеевич результатов используется один из самых перспективных и "свежих" подходов— так называемая "обещающая семантика", опубликованная только в 2017 году. В качестве метода доказательства применяются варианты симуляции, иногда довольно прихотливые.

Следует также отметить, что ряд приемов построения доказательств, разработанных автором, может найти применение и за пределами тематики диссертации. Наконец, важным свойством данной работы является то, что она выполнена в контакте с ведущими мировыми научными группами, работающими в данной области — 1МОЕА Бочаге 1пз11Ш1е (Мадрид, Испания) и Мах Р1апс1с 1пзт1ппе аког Бочаге Бузгетз (Кайзерслаутерн„ Германия). На основании анализа материалов автореферата считаю, что диссертация «Операционные методы в приложении к слабым моделям памяти» является законченным научно-квалификационным трудом и удовлетворяет требованиям Положения «О порядке присуждении ученых степеней».

Автор диссертации, Подкопаев Антон Викторович, заслуживает присуждения ученой степени кандидата физико-математических наук по специальности 05.13.11 «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей». .

Характеристики

Тип файла PDF

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

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов диссертации