Автореферат (1149930), страница 2
Текст из файла (страница 2)
Альтернативная модель памяти для стандарта C/C++11, предложеннаяв работе, отличается от обещающей модели памяти тем, что является запускаемой, т.е. для нее возможно создание интерпретатора (что и быловыполнено в рамках данной диссертационной работы). Это отличие является следствием того, что для получения эффекта отложенного чтенияпредложенная модель использует синтаксический подход (буферизацияинструкций), тогда как обещающая модель — семантический (обещание потоком сделать запись в будущем).2. Доказательство корректности компиляции из обещающей модели памяти в аксиоматическую модель ARMv8.3 не опирается на специфическиесвойства целевой модели, такие как представимость модели в виде набора оптимизаций поверх более строгой модели. Это отличает его отаналогичных доказательств для моделей x86 и Power (работы O.
Lahav,V.Vafeiadis и других).53. Доказательства корректности компиляции из обещающей модели памяти в модели ARMv8 POP и ARMv8.3, представленные в работе, являются первыми результатами о компиляции для данных моделей.Теоретическая и практическая значимость работы. Диссертационноеисследование предлагает новый операционный способ представления реалистичной семантики многопоточности с помощью меток времени и фронтов,который может быть полезен при верификации многопоточных программ снеблокирующей синхронизацией, а также при анализе реализации примитивовблокирующей синхронизации.Предложенный в диссертационном исследовании метод доказательствакорректности компиляции из обещающей в аксиоматические модели памяти может быть использован для доказательств корректности компиляции из обещающей модели в архитектуры других процессоров.
Последнее актуально в свететого, что в комитетах по стандартизации языков C и C++ активно обсуждаетсявопрос о смене модели памяти, и обещающая модель является одной из возможных альтернатив.Степень достоверности и апробация результатов. Достоверность иобоснованность результатов исследования обеспечивается формальными доказательствами, а также инженерными экспериментами. Полученные результатысогласуются с результатами, установленными другими авторами.Основные результаты работы докладывались на следующих научных конференциях и семинарах: внутренний семинар ННГУ им.
Лобачевского (13 декабря 2017, Нижний Новгород, Россия), открытая конференция ИСП РАН им. В.П.Иванникова (30 ноября–1 декабря 2017, РАН, Москва, Россия), семинар “Технологии разработки и анализа программ” (16 ноября 2017, ИСП РАН, Москва,Россия), внутренние семинары School of Computing of the University of Kent(август 2017, Кентербери, Великобритания), внутренние семинары Departmentof Computer Science of UCL (август 2017, Лондон, Великобритания), внутренние семинары MPI-SWS (май 2017, Кайзерслаутерн, Германия), The EuropeanConference on Object-Oriented Programming (ECOOP, 18–23 июня 2017, Барселона, Испания), конференция “Языки программирования и компиляторы” (PLC,3–5 апреля 2017, Ростов-на-Дону, Россия), Verified Trustworthy Software Systemsworkshop (VTSS, 4-7 апреля 2016, Лондон, Великобритания), POPL 2016 StudentResearch Competition (21 января 2016, Санкт-Петербург, Флорида, США).Публикации по теме диссертации.
Основные результаты по теме диссертации изложены в пяти печатных работах, зарегистрированных в РИНЦ. Из нихдве статьи изданы в журналах из “Перечня рецензируемых научных изданий, вкоторых должны быть опубликованы основные научные результаты диссертаций на соискание ученой степени кандидата наук, на соискание ученой степенидоктора наук”, сформированного согласно требованиям, установленным Министерством образования и науки Российской Федерации. Одна статья опубликована в издании, входящем в базы цитирования SCOPUS и Web of Science.6Личный вклад автора в публикациях, выполненных с соавторами, распределён следующим образом. В статьях [1, 2] автор предложил схему доказательства корректности компиляции для аксиоматических семантик и выполнил само доказательство для модели ARMv8.3; соавторы участвовали в обсужденииосновных идей доказательства.
В работах [3, 4] автор выполнил формализациюсемантики ARMv8 POP и доказал корректность компиляции методом симуляции; соавторы участвовали в обсуждении идей доказательства и редактировалитексты статей. В работе [5] личный вклад автора заключается в предложенииидеи меток времени и фронтов как способа операционного задания модели памяти, а также в создании компонентного метода задания семантики и реализацииинтерпретатора; соавторы предложили синтаксический способ обработки отложенных операций.Объем и структура работы. Диссертация состоит из введения, четырехглав, заключения и приложения. Полный объем диссертации 190 страниц текстас 29 рисунками и 4 таблицами. Список литературы содержит 109 наименований.Содержание работыВо введении обосновывается актуальность исследований, выполненных врамках данной диссертационной работы, приводится краткий обзор научной литературы по изучаемой проблеме, формулируется цель, ставятся задачи работы,излагается научная новизна и практическая значимость представленного исследования.Первая глава посвящена обзору области исследования.
Рассматриваютсятребования к реалистичным моделями памяти языков программирования, предъявляемые через призму наблюдаемых сценариев поведения многопоточных программ, применяемых компиляторами оптимизаций, а также моделей памяти процессорных архитектур. Описывается модель памяти C/C++11. Рассматриваютсяпроблемы модели C/C++11, в том числе проблема “значений из воздуха”.
Приводится описание существующих слабых моделей памяти без “значений из воздуха”, в частности, обещающей модели. На основе выполненного обзора делаютсяследующие выводы.– Модель памяти промышленного языка программирования должна удовлетворять, как минимум, трём критериям. Во-первых, должна существовать корректная схема компиляции в модель целевой процессорнойархитектуры.
Во-вторых, основные компиляторные оптимизации должны быть корректны в рамках модели. В-третьих, у модели должна отсутствовать проблема “значений из воздуха”.– При разработке новой модели памяти языка программирования нужнодоказывать корректность эффективной компиляции в модели памяти целевых процессорных архитектур.– Существующие модели памяти промышленных языков программирования не удовлетворяют всем приведённым выше критериям.7– Требуется разработать операционную модель памяти с синтаксисом модели C/C++11, которая не имеет проблемы “значений из воздуха”.Вторая глава посвящена описанию предложенной в диссертации операционной модели памяти OpC11 для C/С++. Модель представлена в виде операционной семантики малого шага с помощью редукционных контекстов.
Основноеотличие слабых моделей памяти от модели последовательной консистентностизаключается в том, что первые не гарантируют для локации в памяти единственность значения, которое может быть прочитано в каждый конкретный моментвремени. Так, например, следующая программа может завершиться с результатом [a = 1, b = 0], хотя, казалось бы, a = 1 гарантирует, что в локацию d ужезаписано новое значение 239:[f ] := 0; [d] := 0;[d] := 239; a := [f ];[f ] := 1b := [d]Как следствие, оперативная память (далее просто “память”) в рамках слабых моделей памяти не может быть представлена как функция из локации в значения.Память в модели OpC11 представляется как множество сообщений.
Каждое сообщение содержит целевую локацию, записываемое значение и метку времени — натуральное число, которое определяет полный порядок на сообщениях, относящихся к одной локации. Последнее нужно для того, чтобы гарантировать последовательную консистентность для программ, оперирующих тольконад одной локацией — эту гарантию предоставляют большинство слабых моделей памяти, в том числе модель C/C++11.
При выполнении инструкции чтенияиз некоторой локации поток может недетерминировано выбрать сообщение, относящееся к этой локации, и выполнить из него чтение. чтение из него.Недетерминированность чтения из локации ограничена гарантией, которую также предоставляет модель C/C++11: после того, как поток прочитал илизаписал сообщение в локацию x с меткой времени t, он (поток) больше не может читать из сообщений с меткой времени, которая меньше t. Для реализацииданного ограничения в модели OpC11 у каждого потока есть т.н. базовый фронт(current view, current viewfront) — функция из локаций в метки времени, определяющая осведомленность потока о сообщениях в памяти.Некоторые программы имеют слабые сценарии поведения, разрешенныемоделью C/C++11, которые не могут быть смоделированы только недетерминированной памятью, а также требуют исполнения инструкций не по порядку. Например, следующая программа может завершиться с результатом [a = 1, b = 1] вмодели C/C++11:[x] := 0; [y] := 0;a := [x]; b := [y];[y] := 1[x] := 1Для представления таких сценариев поведения в модели OpC11 у каждого потока есть буфер отложенных операций.
Так, модель позволяет потоку в каждый8момент отложить текущую операцию вместо её выполнения. С помощью этого механизма модель OpC11 может исполнить приведенную выше программу иполучить результат a = 1, b = 1 следующим образом. Сначала левый поток откладывает чтение из локации x и выполняет запись в y. После этого правый потокчитает из вновь добавленного сообщения и записывает 1 в x. Далее левый потокисполняет отложенное чтение из сообщения, добавленного правым потоком, иполучает результат [a = 1, b = 1].Для поддержки высвобождающих (release) барьеров и записей, а такжеприобретающих (acquire) барьеров и чтений модель OpC11 использует дополнительные фронты — высвобождающий и приобретающий для каждого потока, а также фронт сообщений для каждого сообщения в памяти.
Для поддержкичтений с модификатором доступа consume модель использует динамическую пометку инструкций, зависимых от consume-чтения.Для предложенной модели был реализован интерпретатор на языке Racket с помощью библиотеки описания редукционных семантикPLT/Redex. Код проекта доступен по адресу github.com/anlun/OperationalSemanticsC11.Апробация предложенной семантики была выполнена на наборе, состоящем более чем из 40 тестов (litmus tests), взятых из тематической литературы, атакже на алгоритме RCU (Read-Copy-Update). Поведение модели OpC11 совпадает с поведением модели C/C++11 на большинстве этих тестов. Отличие наблюдается на двух следующих категориях тестов.
Первая категория — это программы, которые имеют исполнения со “значениями из воздуха” в рамках моделиC/C++11. Для таких тестов модель OpC11 не выдает исполнения со “значениями из воздуха”, что является её положительным свойством. Вторая категория —это программы, в которых существуют антизависимости по управлению, адресу или значению, ведущие к инструкциям записи. На таких программах OpC11не способна получить все возможные в рамках C/C++11 исполнения, поскольку выполнение инструкций не по порядку в OpC11 реализовано синтаксическимспособом. Этот недостаток модели не позволяет ей поддержать все необходимыекомпиляторные оптимизации.Одновременно с моделью памяти OpC11 исследователями J. Kang, C.-K.Hur, O. Lahav, V.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
