Отзыв ведущей организации (1149935)

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

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

УТВЕРЖДАЮ Директор ИСП РАН д..,,,4~щ~-корр. РАН "'' -;"; 439»;:..апре~я 2018г. '.-",,,'~Ф~ ''~«:-, -, „,'„д;Ф- ОТЗЫВ ВЕДУЩЕЙ ОРГАНИЗАЦИИ Федеральное государственное бюджетное учреждение науки Институт системного программирования им, В.П. Иванникова Российской Академии Наук (ИСП РАН) на диссертационную работу Подкопаева Антона Викторовича «Операционные методы в приложении к слабым моделям памяти», представленную к защите на соискание ученой степени кандидата физикоматематических наук по специальности 05,13.11 — «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей Актуальность Параллельное программирование является крайне востребованной практической областью и в связи с этим актуальной сферой исследований.

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

Такие модели создают для того, чтобы служить средствами построения точных рассуждений при разработке и верификации параллельных программ. На данный момент создано значительное количество моделей памяти — для языков 1ача, С!С++, для процессоров х86, Роиег, АКМ и т.д, Важным частным случаем являются так называемые слабые модели памяти, которые допускаю сценарии поведения программы, которые нельзя получить последовательным попеременным исполнением ее потоков. Слабыми сценариями поведения обладают некоторые многопоточные программы с неблокирующей синхронизацией потоков, что, в свою очередь, является следствием компиляторных оптимизаций и исполнения программ на суперскалярных процессорах.

В последнее время все чаще используются алгоритмы, созданные на основе неблокирующей синхронизации, например, в ядре 1.1пих, в системах управления базами данных. Поэтому слабые модели памяти оказываются востребованными на практике и, таким образом, являются объектом активного изучения в научном мировом сообществе. Общая характеристика диссертационной работы Диссертационная работа Подкопаева А.В.

имеет общий объем 190 страниц и состоит введения, четырех глав, заключения и пяти приложений. Список использованной литературы состоит из 109 источников. В диссертации исследуется операционный подход к слабым моделям памяти, преимуществом которого является то, что он позволяет определять модель в форме, которая ближе к реальному исполнению программы по сравнению с аксиоматическим подходом, широко используемым для описания моделей памяти процессорных архитектур, а также модели памяти С/С++11.

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

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

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

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

«запаздывающую» симуляцию. 3. Доказана корректность компиляции из существенного подмножества обещающей модели в аксиоматическую модель памяти АКМч8.3. На настоящий момент модель АКМч8.3 является последней моделью архитектуры АКЦИЗ, и, в отличие от АКМ~З РОР, она является аксиоматической. В предложенном доказательстве рассмотрено то же подмножество обещающей модели, что и в предыдущем (с незначительными изменениями). Также, как и в предыдущем доказательстве, использовалась техника симуляции, но, поскольку целевая модель является аксно мати чес кой (в предыдущем доказательстве она — операционная), пришлось использовать специальный обход графа аксиоматического исполнения, который может быть непосредственно повторен обещающей моделью в рамках симуляции.

Научнаи новизна Представленные в диссертационной работе Подкопаева А.В. результаты обладают следующей научной новизной. 1. Предложенная операционная модель памяти для С/С++11 отличается от стандартной и обещающей моделей тем, что позволяет реализовать для модели интерпретатор. Для стандартной модели С/С++11 это невозможно в силу ее аксиоматичности, а для обещающей — поскольку в ней присутствует т. н. сертификация шагов исполнения, которая алгоритмически не разрешима.

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

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

Для статей, опубликованных в соавторстве, в диссертации и в автореферате описан личный вклад автора. Практическая ценность и рекомендации по использованию результатов диссертационной работы Предложенные доказательства корректности компиляции из обещающей модели памяти в модели промышленных процессоров важны в свете перспектив замены существующих моделей памяти 1ача и С!С++11 обещающей моделью (этот вопрос в данный момент активно обсуждается в международном сообществе). Также, предложенный подход задания семантики многопоточности с помощью меток времени и фронтов может быть использован для формальной верификации многопоточных алгоритмов неблокирующей синхронизации с помощью проверок на модели и верификации по Хоару. Результаты работы рекомендуются к использованию в Институте прикладной математики им.

М.В. Келдыша РАН, Институте системного программирования РАН, Институте программных систем им, А.К.Айламазяна РАН, Московском государственном университете им. М.В.Ломоносова, Санкт-Петербургском государственном университете, Санкт-Петербургском политехническом университете Петра Великого и других организациях, занимающихся разработкой и исследованиями в области параллелизма, процессорных архитектур и языков программирования.

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

Тип файла PDF

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

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

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