Компиляция модели памяти OCaml в Power
В настоящее время ведётся активная разработка моделей памяти, направленных на решение различных проблем многопоточного программирования. В частности, модель памяти языка OCaml [Dolan et al. PLDI 2018] позволяет точно описать поведение программ, содержащих гонки по данным. Чтобы использовать эту модель на практике, необходимо показать, что её можно корректно реализовать на распространённых архитектурах процессоров. На данный момент это выполнено для x86 и ARM, но не для Power – архитектуры, широко используемой в серверном оборудовании. В данной работе построена схема компиляции модели OCaml в Power (с использованием промежуточной модели памяти (IMM) [Podkopaev et al. POPL 2019]) и доказана её корректность. Кроме того, полученные результаты формализованы в Coq.
1. Введение
2. Постановка задачи
3. Обзор
3.1. Пример исполнения в слабой модели памяти
3.2. Проблема корректности компиляции на примерах . . . 8
3.3. Графыисполнения …………………. 12
3.4. Описание используемых моделей памяти . . . . . . . . 15
3.4.1. МодельпамятиOCaml(OCamlMM) . . . . . . . . . . 15
3.4.2. Промежуточная модель памяти . . . . . . . . . . 15
4. Обоснование схемы компиляции 18
4.1. Необходимость введения дополнительных инструкций 18
4.2. Схемакомпиляции …………………. 20
5. Доказательство корректности компиляции 21
5.1. Соответствиеграфовисполнения . . . . . . . . . . . . . 21
5.2. Построение графа, соответствующего данному . . . . . 22
5.3. Доказательство последовательной согласованности по от-
дельнымадресам ………………….. 24
5.4. Доказательство отсутствия буферизации при чтении . . 25
6. Формализация доказательства в Coq 30
7. Существующие исследования 33
8. Заключение
Список литературы
Результат исполнения многопоточной программы, как правило, яв- ляется недетерминированным. Конкретное множество допустимых ре- зультатов многопоточной программы определяется моделью памяти языка программирования. Наиболее известной является модель после- довательной согласованности (sequential consistency, SC [11]). Она пред- полагает, что любой результат исполнения программы может быть получен путём попеременного исполнения инструкций отдельных по- токов согласно программному порядку в них. Однако из-за оптимиза- ций, выполняемых современными компиляторами и процессорами, могут наблюдаться сценарии поведения, невозможные в такой моде- ли. Так, на архитектуре x86 чтение по адресу в памяти может вернуть не самое последнее записанное значение, так как операция записи может быть буферизована.
Отказ от подобных оптимизаций нежелателен, поэтому современ- ные модели памяти допускают некоторые сценарии поведения, невоз- можные в модели SC. Такие модели памяти называются слабыми. На- пример, слабыми являются модели памяти языков C++ [2], JavaScript [22] и Java [13], а также архитектур Power [1], x86 [16] и ARM [19].
Модель памяти OCaml [4] (далее — OCamlMM) отличается свойством т.н. локальной свободы от гонок по данным (local data race freedom). Имен- но, гарантируется, что выполнение конфликтующих обращений по выбранному адресу в памяти (т.е. ситуация гонки по данным) не вли- яет на обращения к другим адресам, а также на последующие обра- щения по тому же адресу. Благодаря этому даже при возникновении гонки по данным в некоторый момент исполнения следующие участ- ки программы будут исполнены согласно модели SC.
Чтобы гарантировать выполнение этого свойства, при компиляции нужно запретить некоторые оптимизации в зависимости от целевой архитектуры. Для этого может понадобиться, например, добавить в ассемблерный код инструкции-барьеры, которые запрещают нежела- тельные оптимизации на уровне процессора. Набор таких правил, по-
крывающий все возможные типы инструкций, называется схемой ком- пиляции. Схема компиляции должна быть корректной — при исполне- нии любой программы, полученной при компиляции согласно этой схеме, должно наблюдаться только сценарии поведения, разрешён- ные OCamlMM для исходной программы.
Авторы OCamlMM разработали схемы компиляции OCamlMM в модели x86-TSO и ARMv8 [4] и доказали их корректность. При этом отсутству- ет схема компиляции в модель архитектуры Power. А между тем дан- ная архитектура часто используется в современном серверном обору- довании [7]. Задача построения такой схемы осложнена тем, что мо- дель Power, в отличие от моделей x86-TSO, ARMv8 и OCamlMM, не обла- дает т.н. свойством multicopy atomicity. Такое свойство означает, что записанные в память значения становятся доступны всем потокам в одном и том же порядке [19]. Из-за отсутствия этого свойства коррект- ная схема компиляции OCamlMM в Power должна расставлять барьеры в результирующей программе так, чтобы запретить нежелательные сценарии поведения.
В рамках данной работы была поставлена задача разработать схе- му компиляции OCamlMM в модель Power и доказать её корректность. Для этого было решено использовать промежуточную модель памяти (Intermediate Memory Model, далее — IMM) [18], для которой уже доказа- на корректность компиляции в модель Power. Использование IMM как промежуточного этапа компиляции позволяет разбить доказательство корректности на два, которые впоследствии можно использовать в других доказательствах. Таким образом, построение схемы компиля- ции OCamlMM в IMM даёт схемы компиляции OCamlMM не только в Power, но и другие архитектуры, в которые компилируется IMM (на данный момент — x86 и ARM).
В данной работе представлена схема компиляции OCamlMM в проме- жуточную модель, позволяющая получить схему компиляции OCamlMM в Power. При этом были получены следующие результаты.
• ПредложенасхемакомпиляцииOCamlMMвIMM,использующаяба- рьеры памяти и инструкции read-modify-write для необходимой синхронизации доступов к памяти.
• Быладоказанакорректностьпредложеннойсхемы.Дляэтогобы- ло введено формальное понятие соответствия графов, которое позволило связать сценарии исполнения исходной и скомпили- рованной программ. Затем было доказано, что для каждого со- гласованного по IMM графа исполнения скомпилированной про- граммы существует соответствующий ему граф исполнения ис- ходной программы, согласованный по OCamlMM.
• ПолученноедоказательствобылоформализовановCoq.Безучё- та существующей формализации IMM формализация заняла по- рядка 8 тыс. строк кода.
Результаты работы были представлены на Открытой конференции ИСП РАН и опубликованы в ”Трудах Института системного програм- мирования РАН” [23].
Данное исследование может быть продолжено при реализации свой- ства локальной свободы от гонок в других моделях памяти. Например, изучается возможность реализовать это свойство в модели памяти C++ [3]. Результаты, полученные в данной работе, могут быть исполь- зованы для построения схем компиляции таких моделей. В частно- сти, сравнение схемы компиляции OCamlMM в ARMv8 [4] и полученной в данной работе позволяет предположить, что с большой вероятностью для компиляции инструкции атомарной записи в подобных моделях необходимо будет использовать инструкцию атомарной замены.
[1] Jade Alglave, Luc Maranget, and Michael Tautschnig. “Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory”. In: ACM Trans. Program. Lang. Syst. 36.2 (July 2014), 7:1–7:74. ISSN: 0164-0925. DOI: 10.1145/2627752. URL: http://doi.acm.org/10.1145/2627752.
[2] Mark Batty et al. “Mathematizing C++ Concurrency”. In: POPL 2011. ACM, 2011, pp. 55–66. DOI: 10.1145/1925844.1926394.
[3] Simon Doherty. Local Data-race Freedom and the C11 Memory Model. Surrey Concurrency Workshop. 2019.
[4] Stephen Dolan, KC Sivaramakrishnan, and Anil Madhavapeddy. “Bounding Data Races in Space and Time”. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2018.
[5] Brijesh Dongol, Radha Jagadeesan, and James Riely. “Modular Transactions: Bound-
ing Mixed Races in Space and Time”. In: Proceedings of the 24th Symposium on Principles and Practice of Parallel Programming. PPoPP ’19. Washington, District of Columbia: Association for Computing Machinery, 2019, pp. 82–93. ISBN: 9781450362252. DOI: 10.1145/3293883.3295708. URL: https://doi.org/10.1145/3293883. 3295708.
[6] Georges Gonthier. “The Four Colour Theorem: Engineering of a Formal Proof”. In: Computer Mathematics: 8th Asian Symposium, ASCM 2007, Singapore, December 15-17, 2007. Revised and Invited Papers. Berlin, Heidelberg: Springer-Verlag, 2008, p. 333. ISBN: 9783540878261. URL: https://doi.org/10.1007/978-3-540-87827- 8_28.
[7] IBM Power Systems. IBM Power Systems Facts and Features:Enterprise and Scale- out Systems with POWER8 Processor Technology. https://www.ibm.com/downloads/ cas/JDRZDG0A. 2018.
[8] Jeehoon Kang et al. “A Promising Semantics for Relaxed-memory Concurrency”. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. POPL 2017. Paris, France: ACM, 2017, pp. 175–189. ISBN: 978-1-4503- 4660-3. DOI: 10.1145/3009837.3009850. URL: http://doi.acm.org/10.1145/ 3009837.3009850.
[9] Ori Lahav and Viktor Vafeiadis. “Explaining Relaxed Memory Models with Pro- gram Transformations”. In: FM 2016: Formal Methods. Ed. by John Fitzgerald et al. Cham: Springer International Publishing, 2016, pp. 479–495. ISBN: 978-3-319- 48989-6.
36
[10] Ori Lahav et al. “Repairing Sequential Consistency in C/C++11”. In: SIGPLAN Not. 52.6 (June 2017), pp. 618–632. ISSN: 0362-1340. DOI: 10.1145/3140587.3062352. URL: http://doi.acm.org/10.1145/3140587.3062352.
[11] Leslie Lamport. “How to Make a Multiprocessor Computer That Correctly Exe- cutes Multiprocess Programs”. In: IEEE Transactions on Computers C-28 9 (1979), pp. 690–691. URL: https://www.microsoft.com/en-us/research/publication/ make-multiprocessor-computer-correctly-executes-multiprocess-programs/.
[12] Xavier Leroy. “Formal verification of a realistic compiler”. In: Communications of the ACM 52.7 (2009), pp. 107–115. URL: http://xavierleroy.org/publi/compcert- CACM.pdf.
[13] Jeremy Manson, William Pugh, and Sarita V. Adve. “The Java Memory Model”. In: POPL 2005. ACM, 2005, pp. 378–391. DOI: 10.1145/1040305.1040336.
[14] Batty Mark et al. C/C++11 mappings to processors. https://www.cl.cam.ac.uk/ ~pes20/cpp/cpp0xmappings.html. 2016.
[15] Evgenii Moiseenko et al. “Reconciling Event Structures with Modern Multiproces- sors”. In: (Nov. 2019), Accepted for European Conference on Object–Oriented Pro- gramming 2020.
[16] Scott Owens, Susmit Sarkar, and Peter Sewell. “A Better x86 Memory Model: x86- TSO”. In: Theorem Proving in Higher Order Logics. Ed. by Stefan Berghofer et al. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009, pp. 391–407. ISBN: 978-3- 642-03359-9.
[17] Anton Podkopaev, Ori Lahav, and Egor Namakonov. Intermediate Memory Model. https://github.com/weakmemory/imm. 2019.
[18] Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. “Bridging the Gap Between Programming Languages and Hardware Weak Memory Models”. In: Proc. ACM Pro- gram. Lang. 3.POPL (Jan. 2019), 69:1–69:31. ISSN: 2475-1421. DOI: 10.1145/ 3290382. URL: http://doi.acm.org/10.1145/3290382.
[19] Christopher Pulte et al. “Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8”. In: Proc. ACM Program. Lang. 2.POPL (Dec. 2017), 19:1–19:29. ISSN: 2475-1421. DOI: 10.1145/3158107. URL: http://doi. acm.org/10.1145/3158107.
[20] Coq development team. The Coq Proof Assistant. https://coq.inria.fr/.
[21] Viktor Vafeiadis, Ori Lahav, and Anton Podkopaev. Hahn library. https://github. com/vafeiadis/hahn/. 2020.
37
[22] Conrad Watt et al. “Repairing and mechanising the JavaScript relaxed memory model”. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Lan- guage Design and Implementation (2020). DOI: 10.1145/3385412.3385973. URL: http://dx.doi.org/10.1145/3385412.3385973.
[23] Егор Намаконов и Антон Подкопаев. «Компиляция модели памяти OCaml в Power». В: Труды ИСП РАН 31.5 (2019), с. 63—78. DOI: 10.15514/ISPRAS-2019- 31(5)-4.
Последние выполненные заказы
Хочешь уникальную работу?
Больше 3 000 экспертов уже готовы начать работу над твоим проектом!
4.8 (13 отзывов)
5 (174 отзыва)
4.8 (2878 отзывов)
5 (428 отзывов)
5 (44 отзыва)
5 (22 отзыва)
4.8 (211 отзывов)
5 (154 отзыва)
4.5 (9 отзывов)
