Диссертация (1149932), страница 2
Текст из файла (страница 2)
Alglave, S. Ishtiaq, L. Maranget, F. ZappaNardelli, S. Sarkar, P. Sewell и др. исследователями [6–8]. Новые версии моделейпродолжают появляться в связи с развитием процессорных архитектур. В частности, в 2016 и 2017 годах были представлены модели памяти для архитектурARMv8.0 и ARMv8.3 [9, 10]. В 1995 году была стандартизована слабая модельпамяти для языка Java [3]; в дальнейшем модель существенно менялась вплотьдо 2005 года. В 2011 году появилась аксиоматическая модель памяти для языковC/C++ [4].В 2017 году исследователи J. Kang, C.-K.
Hur, O. Lahav, V. Vafeiadis иD. Dreyer представили обещающую модель памяти (promising memory model,8Promise) [11], которая является перспективным решением проблемы задания семантики для языка с многопоточностью. Авторы доказали, что модель допускаетбольшинство необходимых оптимизаций, а также показали корректность эффективных схем компиляции в архитектуры x86 и Power.
Открытым остался вопросо корректности компиляции в архитектуру ARM.Целью данной работы является исследование применимости операционных подходов для описания реалистичных моделей памяти и анализа многопоточных программ на примере языков C/C++.Для достижения поставленной цели были сформулированы следующие задачи.1. Разработать операционную модель памяти С/С++11, свободную от проблемы “значений из воздуха”.2. Доказать корректность эффективной схемы компиляции из существенного подмножества обещающей модели в операционную модель памятиARMv8 POP.3. Доказать корректность эффективной схемы компиляции из существенного подмножества обещающей модели в аксиоматическую модель памятиARMv8.3.Постановка цели и задач исследования соответствует следующим пунктампаспорта специальности 05.13.11: модели, методы и алгоритмы проектированияи анализа программ и программных систем, их эквивалентных преобразований,верификации и тестирования (пункт 1); языки программирования и системы программирования, семантика программ (пункт 2); модели и методы создания программ и программных систем для параллельной и распределенной обработкиданных, языки и инструментальные средства параллельного программирования(пункт 8).Mетодология и методы исследования.
Методология исследования базируется на подходах информатики к описанию и анализу формальных семантикязыков программирования.В работе используется представление операционной семантики программыс помощью помеченной системы переходов [12], а также метода вычислительных контекстов, предложенного M. Felleisen [13]. Для доказательств корректности компиляции используется техника прямой симуляции [14, 15]. Программнаяреализация интерпретатора операционной модели памяти C/C++11 выполнена на9языке Racket [16,17] с использованием предметно-ориентированного расширенияPLT/Redex [18, 19].Основные положения, выносимые на защиту.1.
Предложена операционная модель памяти C/С++11, для этой модели реализован интерпретатор.2. Доказана корректность компиляции из существенного подмножестваобещающей модели в операционную модель памяти ARMv8 POP.3. Доказана корректность компиляции из существенного подмножестваобещающей модели в аксиоматическую модель памяти ARMv8.3.Научная новизна результатов, полученных в рамках исследования, заключается в следующем.1. Альтернативная модель памяти для стандарта C/C++11, предложенная вработе, отличается от обещающей модели памяти [11] тем, что являетсязапускаемой, т.е. для нее возможно создание интерпретатора (что и быловыполнено в рамках данной диссертационной работы).
Это отличие является следствием того, что для получения эффекта отложенного чтенияпредложенная модель использует синтаксический подход (буферизацияинструкций), тогда как обещающая модель — семантический (обещаниепотоком сделать запись в будущем).2. Доказательство корректности компиляции из обещающей модели памяти в аксиоматическую модель ARMv8.3 [10] не опирается на специфические свойства целевой модели, такие как представимость модели в виденабора оптимизаций поверх более строгой модели. Это отличает его отаналогичных доказательств для моделей x86 и Power (работы O.
Lahav,V.Vafeiadis и других [11, 20]).3. Доказательства корректности компиляции из обещающей модели памяти в модели ARMv8 POP [9] и ARMv8.3 [10], представленные в работе,являются первыми результатами о компиляции для данных моделей.Теоретическая и практическая значимость работы. Диссертационноеисследование предлагает новый операционный способ представления реалистичной семантики многопоточности с помощью меток времени и фронтов, которыйможет быть полезен при верификации многопоточных программ с неблокирующей синхронизацией, а также при анализе реализации примитивов блокирующейсинхронизации.10Предложенный в диссертационном исследовании метод доказательства корректности компиляции из обещающей в аксиоматические модели памяти можетбыть использован для доказательств корректности компиляции из обещающей модели в архитектуры других процессоров.
Последнее актуально в свете того, чтов комитетах по стандартизации языков 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.Личный вклад автора в публикациях, выполненных с соавторами, распределён следующим образом. В статьях [21,22] автор предложил схему доказательства11корректности компиляции для аксиоматических семантик и выполнил само доказательство для модели ARMv8.3; соавторы участвовали в обсуждении основныхидей доказательства.
В работах [23,24] автор выполнил формализацию семантикиARMv8 POP и доказал корректность компиляции методом симуляции; соавторыучаствовали в обсуждении идей доказательства и редактировали тексты статей. Вработе [25] личный вклад автора заключается в предложении идеи меток времении фронтов как способа операционного задания модели памяти, а также в созданиикомпонентного метода задания семантики и реализации интерпретатора; соавторы предложили синтаксический способ обработки отложенных операций.Благодарности.Я хочу выразить признательность своим коллегам, друзьям и семье, присутствиекоторых в моей жизни сделало эту работу возможной. Начать я хотел бы с выражения благодарности Д. Ю. Булычеву, А.
В. Иванову и компании JetBrains, которыепредоставили мне уникальную возможность заниматься наукой как основной деятельностью. Я признателен своему научному руководителю Д. В. Кознову, который помог мне пройти через тернистый путь создания диссертации. Я благодаренИ. Д. Сергею и А. Наневски (A. Nanevski) за бескорыстную поддержку и руководство моей работой на первых этапах. Я хотел бы выразить признательностьстаршим коллегам В. Вафеядису (V. Vafeiadis) и О. Лахаву (O. Lahav) за помощьв исследованиях и сотрудничество. Я очень благодарен коллективам MPI-SWS,IMDEA Software и кафедры системного программирования, а также лично А. Н.Терехову за создание душевной и плодотворной атмосферы для работы.Я признателен за удивительную отзывчивость и дружбу Д.
А. Березуну, запомощь в тяжелейших ситуациях и человеческую доброту А. М. Карачуну, занемыслимые поддержку и понимание А. В., Т. П. и В. Е. Турецким и моей семье. Я горячо признателен моей маме за её самоотверженное стремление помочьмне на каждом этапе моей жизни. Я безмерно благодарен моему папе за всё.12Глава 1. Обзор предметной областиВ данной главе вводятся основные понятия, использующиеся в этом диссертационном исследовании: модель памяти, слабая модель памяти и др.
— а также приводятся примеры. Рассматриваются существующие модели памяти языковпрограммирования и процессорных архитектур, а также требования, предъявляемые к ним. Приводится описание проблемы “значений из воздуха” (OOTA, out-ofthin-air values).
Подробно описывается модель памяти C/C++11 [4]. В конце главыприведены выводы о состоянии предметной области и о существующих открытыхпроблемах.1.1Модели памяти и слабые сценарии поведенияВ диссертационном исследовании под моделью памяти понимается семантика системы с многопоточностью, и рассматриваются два типа таких систем:языки программирования и процессорные архитектуры.Модели памяти разделяются по принципу того, какие ограничения на сценарии поведения программ они накладывают [26]. Так, строгая консистентностьгарантирует, что любая запись в память становится мгновенно видна всем потокам в системе.
Эта модель требует наличия некоторого абсолютного счётчика времени, разделяемого всеми потоками системы, что зачастую является недостижимым. Менее строгая модель последовательной консистентности [1] (SC,sequential consistency) предполагает, что любой сценарий поведения может бытьполучен исполнением потоков на одном вычислительном ядре с вытесняющеймногозадачностью. Это означает, что все операции над памятью, совершаемыепотоками в рамках одного сценария поведения, могут быть упорядочены, и полученный порядок согласуется с порядком инструкций в самих потоках. Сценарииповедения программ, которые не могут быть получены в рамках модели SC, называются слабыми, а модели, допускающие слабые сценарии поведения, — слабымимоделями памяти [2].Несмотря на то, что модель SC кажется наиболее естественной, а статья [1],в которой эта модель описывается, называется “How to make a multiprocessorcomputer that correctly executes multiprocess programs”, современные процессорные архитектуры и языки программирования активно используют слабые модели памяти.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
