Сведения о результатах публичной защиты (1149946)
Текст из файла
ЗАКЛЮЧЕНИЕ ДИССЕРТАЦИОННОГО СОВЕТА Д 212.232.51НА БАЗЕ ФЕДЕРАЛЬНОГО ГОСУДАРСТВЕННОГО БЮДЖЕТНОГООБРАЗОВАТЕЛЬНОГО УЧРЕЖДЕНИЯ ВЫСШЕГО ОБРАЗОВАНИЯ«САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ»,ПРАВИТЕЛЬСТВО РФ, ПО ДИССЕРТАЦИИ НА СОИСКАНИЕ УЧЕНОЙСТЕПЕНИ КАНДИДАТА НАУКаттестационное дело № _________________решение диссертационного совета от 17 мая 2018 г. № 34.06-51-1-8ОприсужденииПодкопаеву Антону Викторовичу,гражданинуРоссийской Федерации, учёной степени кандидата физико-математическихнаук.Диссертация «Операционные методы в приложении к слабым моделямпамяти» по специальности 05.13.11 ― математическое и программноеобеспечение вычислительных машин, комплексов и компьютерных сетейпринятакзащитедиссертационнымгосударственногообразования01мартасоветомДбюджетного2018года,212.232.51протоколнаобразовательного«Санкт-Петербургский№ 34.06-51-1-3базеФедеральногоучреждениягосударственныйвысшегоуниверситет»,Правительство РФ, 199034, г. Санкт-Петербург, Университетская наб., д.
7-9,приказ 248/нк от 15.05.2014 г.Соискатель Подкопаев Антон Викторович 1992 года рождения.В 2014 году соискатель окончил Федеральное государственноеобразовательное учреждение высшего профессионального образования«Санкт-Петербургский государственный университет» по специальности«Математическое обеспечение и администрирование информационныхсистем», является аспирантом Федерального государственного бюджетногообразовательного учреждения высшего образования «Санкт-Петербургскийгосударственный университет», в настоящее время не работает.Диссертация выполнена на кафедре системного программированияФедерального государственного бюджетного образовательного учреждениявысшего образования «Санкт-Петербургский государственный университет»,Правительство РФ.Научный руководитель ― доктор технических наук Кознов ДмитрийВладимирович, Федеральное государственное образовательное учреждениевысшегопрофессиональногообразования«Санкт-Петербургскийгосударственный университет», кафедра системного программирования,профессор.Официальные оппоненты:Гергель Виктор Павлович, доктор технических наук, профессор,Федеральное государственное автономное образовательное учреждениевысшего образования «Нижегородский государственный университет им.Н.И.
Лобачевского», директор института информационных технологий,математики и механики, заведующий кафедрой программной инженерии;ЛукашинАлексейАндреевич,кандидаттехническихнаук,Федеральное государственное автономное образовательное учреждениевысшего образования «Санкт-Петербургский политехнический университетПетра Великого», доцент кафедры «Телематика (при ЦНИИ РТК)»дали положительные отзывы на диссертацию.Ведущая организация Федеральное государственное бюджетноеучреждение науки Институт системного программирования Российскойакадемии наук (ИСП РАН), в своём положительном отзыве, подписанномведущим научным сотрудником, кандидатом физико-математических наук(специальность 01.01.10 – Математическое и программное обеспечениевычислительных машин, комплексов и компьютерных сетей) В.А.
Падаряноми утверждённом директором ИСП РАН членом-корреспондентом РАН А.И.Аветисяном, указала, что диссертационная работа Подкопаева А.В. отвечаетвсемтребованиямПоложенияоприсужденииучёныхстепеней,предъявляемым к кандидатским диссертациям, а её автор заслуживаетприсуждения учёной степени кандидата физико-математических наук по2специальности 05.13.11 – математическое и программное обеспечениевычислительных машин, комплексов и компьютерных сетей.Соискатель имеет 8 опубликованных работ, из них по теме диссертации– 5, в том числе 2 работы опубликованы в рецензируемых научных изданияхиз перечня российских рецензируемых научных журналов, в которыхдолжны быть опубликованы основные научные результаты диссертаций насоискание учёных степеней доктора наук и кандидата наук, и 1 работаопубликована в издании, индексируемом в международных базах Scopus иWeb of Science.
В диссертации отсутствуют недостоверные сведения обопубликованныхсоискателемработах.Вопубликованныхработахсоискателя общим объёмом 89 страниц, исследованы вопросы, связанные соспецификациейслабыхмоделейпамяти,допускающихкорректнуюкомпиляцию в модели процессоров и лишённых традиционных проблемсуществующих моделей, таких как значения из воздуха. Работы выполненыавтором лично или при его активном непосредственном участии.Наиболее значительные научные работы по теме диссертации (вних соискателю принадлежит идея меток времени и фронтов как способаоперационного задания модели памяти языков С/C++, а также разработкакомпонентного метода задания семантики и реализации интерпретатора;схемы доказательства корректности компиляции для аксиоматическихсемантик и выполнение самого доказательства для модели ARMv8.3;выполнение формализации семантики ARMv8 POP и доказательствокорректности компиляции методом симуляции):1.Подкопаев,А.В.Окорректностикомпиляцииподмножестваобещающей модели памяти в аксиоматическую модель ARMv8.3 / А.В.Подкопаев, О.
Лахав, В. Вафеядис // Научно-технические ведомостиСПбГПУ. Информатика, Телекоммуникации. Управление. — 2017. — Т. 10,№ 4. — C. 51–69.32.Podkopaev, A. Promising compilation to ARMv8 POP / A. Podkopaev, O.Lahav, V. Vafeiadis // 31st European Conference on Object-OrientedProgramming (ECOOP 17), Leibniz International Proceedings in Informatics(LIPIcs). — 2017.— P. 22:1–22:28.3.Podkopaev, A. Operational Aspects of C/C++ Concurrency / A.
Podkopaev,I.Sergey,A.Nanevski[Электронныйресурс].—URL:http://arxiv.org/abs/1606.01400 (дата обращения: 14.11.2017).На автореферат поступили отзывы, все отзывы положительные:1. От доктора физико-математических наук, профессора, заведующегокафедройвычислительныхтехнологийФГБОУВО«Кубанскийгосударственный университет» Александра Ивановича Микова. Отзывзамечаний не содержит.2. От доктора физико-математических наук, старшего научного сотрудникаФедерального государственного бюджетного учреждения науки СанктПетербургское отделение Математического института им. В.
А. СтекловаРоссийской академии наук (ПОМИ РАН) Куликова Александра Сергеевича.Отзыв замечаний не содержит.3. От доктора физико-математических наук, профессора, главного научногосотрудника Института систем информатики им. А.П.Ершова СО РАНАлександра Гурьевича Марчука. Отзыв замечаний не содержит.4. От кандидата технических наук, заведующего кафедрой математическогообеспечения и применения ЭВМ Санкт-Петербургского государственногоэлектротехнического университета «ЛЭТИ» им. В.И. Ульянова (Ленина)Кирилла Владимировича Кринкина. Отзыв замечаний не содержит.5.
От кандидата физико-математических наук, ведущего программиста ООО«Тэга» Владимира Михайловича Дуденкова. Отзыв замечаний не содержит.Выбор ведущей организации обосновывается тем, что она являетсяведущейвРФнаучно-исследовательской4организациейвобластипрограммирования и программной инженерии,имеет значительный опыт висследовании и разработке архитектур микропопроцессорных систем исредств программирования и способна определить научную и практическуюценность диссертации. Выбор в качестве официального оппонента ГергеляВ.П. обусловлен тем, что он является одним из ведущих учёных РФ вобластипараллельногопрограммирования,имеетнепосредственноеотношение к теме и предмету диссертационного исследования, являетсяавтором многочисленных публикаций.
Выбор в качестве официальногооппонента Лукашина А.А. обусловлен тем, что он является экспертом вскалярных и суперскалярных архитектурах, а также в области параллельногопрограммирования.Диссертационный совет отмечает, что на основании выполненныхсоискателем исследований:разработана новая операционная модель памяти C/С++11, лишённаязначений из воздуха;предложен оригинальный метод доказательства корректности компиляциииз обещающей в аксиоматические модели памяти, которыйможет бытьиспользован для доказательств корректности компиляции из обещающеймодели в архитектуры других процессоров;доказана корректность трансляции из обещающей модели в моделипроцессоровARMv8.3(аксиоматическаямодель)иARMv8POP(операционная модель);введеныспецифическиеформализмыдляпредставленияпамятимногопоточной программы, потока управления программы и выполненияэтого потока управления.Теоретическая значимость исследования обоснована тем, что:доказана корректность трансляции из обещающей модели в моделипроцессоров ARM;5использованопредставлениеоперационнойсемантикипрограммыспомощью помеченной системы переходов и метод вычислительныхконтекстов, предложенный M.
Felleisen, а также техника прямой симуляции;изложены основы теории слабых моделей памяти;изучены операционные подходы к представлению слабых моделей памяти;проведена модернизация некоторых понятий обещающей модели памяти.Значение полученных соискателем результатов исследованиядля практики подтверждается тем, что:разработана программная реализация интерпретатора операционной моделипамятиC/C++11наязыкеRacketсиспользованиемпредметно-ориентированного расширения PLT/Redex;создана основа для доказательства корректности компиляции из обещающеймодели в модели различных процессоров;представлены корректные формальные доказательства для случая моделейпроцессоров ARMv8.3 и ARMv8 POP.Результаты работы рекомендуются к использованию в Институтепрограммныхсистемим.А.К.АйламазянаРАН,Московскомгосударственном университете им.
М.В.Ломоносова, Санкт-Петербургскомгосударственном университете, Институте прикладной математики им. М.В.Келдыша РАН, Институте системного программирования РАН, и могутнайти применение при реализации языков программирования, а такжепрограммного инструментария для оптимизации и верификации программ.Оценка достоверности результатов исследования выявила, что:теория построена на адекватном математическом аппарате и согласуется сболее ранними результатами;идеи базируются на использовании меток времени и фронтов как способаоперационного задания модели памяти, а также симулятивного подхода;6использованыпомощьюпредставление операционной семантики программы спомеченнойсистемыпереходов,методвычислительныхконтекстов, предложенный M.
Felleisen, а также техника прямой симуляции;установлено, что корректность трансляции из обещающей модели в моделипроцессорных архитектур может быть доказана общим подходом, сразу длянескольких моделей одновременно;использованы подходы симуляции и базовые методы доказательствакорректности трансляций различных формальных вычислительных моделей.Личный вклад соискателя состоит в предложении идеи меток времении фронтов как способа операционного задания модели памяти языков С/C++,а также в создании компонентного метода задания семантики и реализацииинтерпретатора;компиляциипредложениидлясхемыаксиоматическихдоказательствасемантикикорректностивыполнениисамогодоказательства для модели ARMv8.3; выполнении формализации семантикиARMv8POPсимуляции;идоказательствеапробациимеждународныхкорректностиработыконференцияхнаикомпиляцииразличныхсеминарах;методомвсероссийскихподготовкеиосновныхпубликаций по выполненной работе.Диссертационная работа Подкопаева А.В.
является завершённойнаучно-квалификационной работой, которая содержит новые научные ипрактическиерезультатыпоактуальнымвопросаммногопоточногопрограммирования, имеет существенное значение для развития средствтеоретического программирования и соответствует всем требованиямдействующего«Положенияоприсужденииучёныхстепеней»,предъявляемым к диссертациям на соискание учёной степени кандидатанаук, в том числе п.9 (абзац 2).На заседании 17 мая 2018 года диссертационный совет принял решениеприсудитьПодкопаевуА.В.учёнуюматематических наук.7степенькандидатафизико-.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
