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

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

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

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

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

Так, за последние 20 лет были разработаны слабые модели для процессорных архитектур, таких как х86, Роччег, АКМ и др., а также для языков программирования 1ача, С/С++ и пр. Тем не менее, стандартные модели памяти 3ача и С/С++11 обладают рядом известных недостатков.

Так, модель 1ача не разрешает ряд компиляторных оптимизаций, а модель С/С++11 разрешает сценарии поведения со «значениями из воздуха», что не дает возможности эффективно рассуждать о корректности программ в теримнах этой модели. Для устранения отмеченных недостатков может быть использована операционная модель памяти для языка программирования, разработка и изучение которых является главной целью данного диссертационного исследования.

Общая характеристика работы. В рамках диссертационной работы рассмотрены две операционные модели памяти для языков С/С++11. Первая модель (ОрС11 ММ) разработана диссертантом. Второй моделью является т. н. обещающая модель, которая на данный момент рассматривается научным сообществом как перспективная замена существующих моделей памяти для языков 3ача и С/С++11.

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

Это позволяет эмулировать эффект недетерминированного чтения из памяти. Во-вторых, в рамках модели поток может исполнять свои инструкции не по порядку, что реализовано через механизм откладывания операций. Это позволяет выразить в модели эффект, который в литературе называются буферизацией чтения (!оас1 Ьпйег1п8). Для предложенной модели был разработан интерпретатор, и с его помощью была проверена адекватность модели на наборе из 40 тестов, взятых из релевантной литературы. То, что для модели возможно разработать интерпретатор, выгодно отличает ее от существующих аналогов, в частности, от обещающей модели.

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

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

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

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

Основные результаты работы опубликованы в 5 печатных работах, зарегистрированных в РИНЦ, из них 2 статьи — в журналах из "Перечня российских рецензируемых научных журналов, в которых должны быть опубликованы основные научные результаты диссертаций на соискание ученых степеней доктора и кандидата наук", 1 статья — в издании из баз цитирования Бсорцз и %еЬ оГ Яс1епсе, Для статей, опубликованных в соавторстве, в диссертации и в автореферате описан личный вклад автора.

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

выполнена на высоком научно-техническом уровне, однако имеются следующие замечания. 1. В целом, можно отметить хорошее грамотное изложение текста автореферата и диссертации — так, при тщательном изучении работы оказалось возможным выделить лишь незначительные недостатки по оформлению диссертационного материала (на стр. 17 и 18 слово «на ряду» пишется раздельно, заголовок на стр.

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

Доказательство корректности компиляции в модель АКМ~8 РОР содержит большое количество математических выкладок, что затрудняет ручную проверку корректности. Формализация доказательства в системе доказательства теорем, такой как Сос1 или 1заЬе11е/Н01, существенно усилила бы данный результат. .

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

Тип файла PDF

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

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

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