Отзыв официального оппонента 2 (1149942)

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

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

ОТЗЫВ Официального оппонента на диссертацию Антона Викторовича Подкопаева «Операционные методы в приложении к слабым моделям памяти», представленную на соискание ученой степени кандидата физико-математических наук по специальности 05.13,11— математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей Использование многопоточности при разработке ПО позволяет существенно повысить производительность вычислений и обработки данных, но значительно усложняет архитектуру программных продуктов и поэтому становится источником специфических и трудно обнаружимых ошибок. В связи с этим актуальной задачей является создание новых моделей и подходов для повышения эффективности практического использования многопоточности.

Одним из таких средств являются модели памяти формальные спецификации семантики параллельных конструкций в языках программирования и процессорах. Модель памяти предоставляет средства для рассуждения о поведении параллельных программ и может эффективно использоваться при проектировании таких программ, а также при их верификации. Такой подход находит применение при разработке критического ПΠ— ядер операционных систем, серверного ПО крупных клиент-серверных систем, суперкомпьютерного ПО, и т.д.

В последнее время в научном сообществе стали популярны слабые модели памяти, которые гюзволяют специфицировать программы, поведение которых не может быть получено по переменным последовательным исполнением. Такие модели созданы для известных языков программирования 1ача, С~С++, а также для различных процессоров, например, АКМ. Однако, существующие слабые модели обладают проблемами, затрудняющими их практическое использование, например, не поддерживают ряд известных оптимизаций (модель памяти 3ача), допускают значения из воздуха (модель памяти С/С++).

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

Он также выполнил доказательства корректности компиляции из другой операционной модели— обещающей модели — в модели архитектур ряда современных процессоров. Интересна интрига диссертационного исследования: первый результат (собственная модель) был опубликован одновременно с аналогичной моделью, созданной одними из лидеров в этой области — исследовательской группой из института Макса Планка, Кайзерслаутерн, Германия. После этого автор принял решение (и, что важно, смог его осуществить) продолжить исследования в составе этой группы. При этом, все результаты диссертации выполнены в тесной кооперации с международным сообществом, что крайне ценно. Кратко охарактеризую полученные автором основные научные результаты. Первым резулипатом является операционная модель для языков С!С++11.

Эта модель, в отличие от стандартной, лишена проблемы «значений из воздуха». Память в модели представляется в виде множества сообщений, в котором для одного адреса может присутствовать несколько значений, что позволяет эмулировать эффект недетерминированного чтения. Предложенный автором механизм откладывания операций позволяет потоку программы исполнять инструкции не по порядку, что, в свою очередь, дает возможность модели выразить эффект буферизации чтения, К ограничениям данного результата необходимо отнести то, что некоторые сценарии поведения, которые разрешаются в оригинальной модели С/С++11 и не имеют проблемы «значений из воздуха», предложенная модель не поддерживает, Второй результат диссертации — это доказательство теоремы о корректности компиляции из обещающей модели в модель памяти АКМч8 РОР (точнее, входом компиляции служило значимое подмножество обещающей модели). В этом доказательстве была использована техника прямой симуляции, стандартная для такого рода доказательств.

Однако, в данном случае для ее применения диссертанту пришлось ввести промежуточную модель — инструментированную версию модели АКМ~8 РОР и показать ее эквивалентность изначальной модели. Необходимость промежуточной модели связана с тем, что между обещающей и АКМч8 РОР моделями имеется существенная разница, связанная с особенностями упорядочивания сообщений на запись.

Относительно научной новизны данного результата отмечу, что это первое доказательство корректности трансляции обещающей модели в модель архитектуры данного процессора. Третий резулыиат диссертационного исследования заключается в доказательстве корректности компиляции из обещающей модели (также, как и в предыдущем доказательстве, речь идет о том же существенном подмножестве с той лишь разницей, что опущен механизм сертификации) в модель памяти АВМЖЗ. Последняя является самой новой на данный момент моделью архитектуры процессора АКМ~8. В отличие от модели АКМч8 РОР, она является аксиоматической, что требует создания нового доказательства. Соответствующее доказательство, предложенное диссертантом, основано на оригинальном методе обхода графа аксиоматического исполнения.

Этот обход последовательно добавляет события ~т. е. вершины графа) в два множества покрытых и выпущенных событий. Этот обход может быть непосредственно симулирован обещающей машиной. Так, добавление элемента в первое множество соответствует простому исполнению инструкции, а во второе— т. н. обещанию обещающей модели. Предложенный результат является новым, поскольку оказывается первым формальным результатом корректности компиляции из модели языка программирования в модель АКМ~8.3 (последняя была выпущена в 2017 году), Итак, можно сделать вывод о том, что результаты данной диссертации имеют значительную научную новизну, обоснованы и прошли апробацию на внушительном количестве международных семинаров и конференций, Все основные результаты работы опубликованы в 5 печатных работах, зарегистрированных в РИНЦ, из них 2 статьи — в журналах из "Перечня российских рецензируемых научных журналов, в которых должны быть опубликованы основные научные результаты диссертаций на соискание ученых степеней доктора и кандидата наук", 1 статья проиндексирована в базах данных цитирования Бсориз и %еЬ оГ Яс1епсе.

В тексте диссертации подробно описан личный вклад автора в статьях, написанных им в соавторстве, Следует отметить существенную теоретическую значимость данной диссертации, Так, в первом доказательстве диссертанту удалось связать достаточно разные операционные модели. При этом предложенный инструментированный вариант модели АКМ~8 РОР может быть использован в других доказательствах корректности компиляции в модель АКМч8 РОР из моделей, которые требуют наличия тотального порядка на сообщениях записи в каждую локацию.

К таким моделям относится и оригинальная модель С/С++11, и предложенная автором операционная модель С/С++11. Во втором доказательстве применяется новый метод, основанный на обходе графа аксиоматического исполнения. Данный подход, в отличие от использованных ранее для доказательства корректности компиляции из обещающей модели в модели х8б и Ров ег, не опирается на специфичные свойства моделей (которые, в частности, не выполняются для модели АКМч8.3), что позволяет применять его к более широкому классу моделей. Также этот подход неявно задает ограничения на то, для каких аксиоматических моделей в принципе может быть доказана корректность компиляции из обещающей модели. Диссертация также обладает практической ценностью. В настоящее время идет активная переработка модели памяти для языков С/С++, а также .1ача.

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

Тем не менее, работа не свободна от некоторых недостатков. 1, Доказательство корректности компиляции из обещающей модели в модель АКМ~8 РОР очень объемно (в диссертации оно занимает более 50 страниц), поэтому его крайне тяжело проверить, Если бы данное доказательство было проведено в некоторой системе доказательства теорем (например, Адйа или 1.еап), то его проверка человеком не требовалась бы.

2. Обещающая модель и доказательство корректности ее компиляции в модель АКМ~8.3 относится к конкретной архитектуре процессора. Результат можно было бы усилить, обобщив доказательство корректности компиляции для других вычислительных архитектур, Эти замечания не умаляют достоинств диссертационной работы. Диссертационное исследование является завершенной научноисследовательской работой, полностью удовлетворяет паспорту специальности 05.13.11 и отвечает всем требованиям пункта 9 «Положения о порядке присуждения ученых степеней», утвержденного Постановлением Правительства Российской Федерации № 842 от 24 сентября 2013 года. Считаю, что ее автор Антон Викторович Подкопаев заслуживает присуждения ученой степени кандидата физико-математических наук по специальности 05.13.11 — «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей».

Официальный оппонент: , Лукашин кандидат технических наук, д кафедры «Телематика (при Ц РТК)», Института прикладно математики и механики федерального государственн автономного образовательно учреждения высшего образов «Санкт-Петербургский политехнический университет Петра Великого» г. Санкт-Петербург, ул. Политехническая, 29 тел. (921) 3186929, (812) е-та11: а1ехе .1ц1савЬ|п,з Ьзш.гп 2018 г. .

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

Тип файла PDF

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

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

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