Выписка из протокола заседания диссертационного совета (1149931), страница 2
Текст из файла (страница 2)
Таким образом, диссертационная работа Г1одкопаева Антона Викторовича соответствует специальности 05.13.11— «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», по которой диссертационному совету Д 212.232.51 предоставлено право проведения защиты диссертаций. Данная диссертационная работа посвящена тематике, актуальной и активно развивающейся, находящейся сегодня на переднем крае мировых исследований — слабым моделям памяти.
Данная тематика находится в контексте исследований по созданию эффективных средств параллельного программирования. Оказалось, что существующие стандарты языков программирования (в том числе таких лидеров промышленных разработок, как 1юа и С/С++), а также процессорные архитектуры, не обладают средствами, способными непротиворечиво и в тоже время формально и точно определять семантику параллельных программ в той ее части, где используются так называемые слабые эффекты — сценарии параллельного поведения, которые нельзя специфицировать попеременным последовательным исполнением потоков. А между тем такие сценарии активно используются при оптимизации параллельных программ, в разработке высокопроизводительных систем, таких как ядро Елпих и системы управления базами данных и т.д.
Отсутствие точных формальных моделей затрудняет проектирование подобных систем, а также формальную верификацию их свойств. В настоящее время лидирующими в этой теме являются две исследовательские группы — в университете города Кент (Кентерберри, Великобритания) и в институте Макса Планка (Кайзерслаутерн, Германия). Следует особенно подчеркнуть, что проблематика диссертации и полученные результаты исследования соответствуют международному уровню— автор лично обсуждал их с представителями данных школ, выступая с докладами на внутренних семинарах в университете Кента и институте Макса Планка. Более того, диссертационная работы была выполнена в тесном сотрудничестве с группой из Кайзерслаутерна, что отражено в совместных публикациях Подкопаева Антона Викторовича и членов этой группы. Обоснованность и достоверность полученных результатов диссертации подтверждается публикациями по материалам выполненных исследовательских работ (5 публикаций), включая 2 статьи из журналов, входящих в Перечень рецензируемых научных изданий, 1 статью — в издании, индексируемом международными реферативными базами Ясорпз и %еЬ о1 Яс(епсе.
Все выносимые на защиту результаты в достаточной мере отражены в опубликованных работах. Отметим также большое количество выступления Антона Викторовича на различных международных и Российских конференциях и семинарах. Диссертация прошла проверку в системе В!асКЬоап1 на предмет выявления объема текстовых совпадений между текстом диссертации и источниками, авторство которых установлено, для рассмотрения диссертации как оригинальной научно-квалификационной работы. Текст диссертации содержит 21% совпадений.
Содержательная экспертиза этих совпадений с учетом ссылок на источники совпадающих фрагментов и детальным анализом совпавшей информации показала, что выявленные совпадения представляют собой цитаты собственных материалов автора (статей и отчетов) — главным образом, формальных математических выкладок (формул и листингов алгоритмов, а также листингов примеров). Обьем таких выкладок весьма значителен в диссертационной работе Антона Викторовича. Таким образом, экспертиза показала, что диссертация Подкопаева Антона Викторовича может считаться полностью оригинальной авторской научной работой.
В диссертации отсутствуют недостоверные сведения о работах, опубликованных соискателем. В диссертационной работе Подкопаева Антона Викторовича представлены следующие результаты. 1. Предложена операционная модель памяти С/С++11, для этой модели реализован интерпретатор. 2. Доказана корректность компиляции из существенного подмножества обещающей модели в операционную модель памяти АКМч8 РОР. 3. Доказана корректность компиляции из существенного подмножества обещающей модели в аксиоматическую модель памяти АКМ~8.3. Все полученные результаты являются новыми и подтверждены формальными доказательствами, а также экспериментами, в силу этого данные результаты являются достоверными.
Практическая значимость результатов диссертационного исследования заключается в том, что в комитетах по стандартизации языков С и С++ в настоящее время активно обсуждается вопрос об изменении модели памяти, и обещающая модель, над которой активно работал Антон Викторович, является одной из вероятных кандидатов. Кроме того, имеются запросы на подобные модели из индустрии — со стороны разработчиков ядра Елпцх, систем управления базами данных и других высокопроизводительных систем; использование подобных моделей существенно повышает надежность проектирования различных критических алгоритмов. Комиссия считает, что диссертация Подкопаева Антона Викторовича соответствует критериям, которым должна отвечать диссертация на соискание ученой степени кандидата наук (пп.9-11, 13,14 «Положения о присуждении ученых степеней»).
Комиссия рекомендует принять к защите на диссертационном совете Д 212.232.51 кандидатскую диссертацию Подкопаева Антона Викторовича на тему «Операционные методы в приложении к слабым моделям памяти» по специальности 05.13.11 — «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей».
Комиссия рекомендует утвердить официальными оппонентами следующих компетентных в соответствующей отрасли науки ученых, имеющих публикации в областях программной инженерии, языков программирования, параллельного и распределенного программирования: 1. Доктора технических наук, профессора, директора института информационных технологий, математики и механики, заведующего кафедрой программной инженерии Федерального государственного автономного образовательного учреждения высшего образования «Нижегородский государственный университет им. Н.И.
Лобачевского» Гергеля Виктора Павловича. 2. Кандидата технических наук, доцента, доцента кафедры «Телематика (при ЦНИИ РТК)» институт прикладной математики и механики Федерального государственного автономного образовательного учреждения высшего образования «Санкт-Петербургский политехнический университет Петра Великого» Лукашина Алексея Андреевича. Председатель комиссии: " Демьянович Юрий Казимирович Терехов Андрей Николаевич Члены комиссии: Ромвиовоиий Иооиф Влвйимировии « ~~» февраля 2018 г. Комиссия рекомендует утвердить в качестве ведущей организации лидирующее в Российской Федерации научноисследовательское учреждение в области программирования и программной инженерии — «Федеральное государственное бюджетное учреждение науки Институт системного программирования Российской академии наук 1ИСП РАН)».
.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
