Компиляция модели памяти OCaml в Power
https://doi.org/10.15514/ISPRAS-2019-31(5)-xx
Аннотация
В настоящее время для языков программирования и процессоров активно разрабатываются модели памяти, направленные на решение различных проблем многопоточного программирования. Так, модель памяти языка OCaml (OCamlMM) позволяет избежать неопределённого поведения, вызванного гонками по данным. Для применения этой модели на практике необходимо доказать корректность её компиляции в распространённые архитектуры процессоров. На данный момент это выполнено для моделей x86 и ARM, но не для Power. Для того, чтобы упростить доказательство корректности компиляции OCamlMM в модель Power, предлагается построить схему компиляции OCamlMM в промежуточную модель памяти (IMM). Для этой модели уже доказана корректность компиляции в модель Power и другие архитектуры, поэтому доказательство корректности компиляции OCamlMM в модель Power сводится к доказательству корректности компиляции OCamlMM в IMM. В данной работе предложена схема компиляции OCamlMM в IMM и доказана её корректность. В этой схеме используются барьеры памяти и инструкции compare-and-swap, которые позволяют исключить поведение, допустимое IMM и запрещённое моделью OCaml. Полученная схема компиляции даёт корректную схему компиляции OCamlMM в модель Power. Кроме того, при таком подходе доказать корректность компиляции OCamlMM в другую архитектуру можно, доказав корректность компиляции IMM в эту архитектуру.
Ключевые слова
При поддержке: Авторы благодарят коллег по научной группе за участие в обсуждении ранних версий статьи.
Об авторах
Егор Сергеевич Намаконов
JetBrains Research
Санкт-Петербургский государственный университет
Россия
Россия
Студент магистратуры Санкт-Петербургского государственного университета, член группы исследования слабых моделей памяти в JetBrains Research.
Антон Викторович Подкопаев
Национальный исследовательский университет «Высшая школа экономики»
JetBrains Research
Институт им. Макса Планка: Программные Системы
Россия
Россия
Доцент НИУ ВШЭ (СПб), руководитель группы исследования слабых моделей памяти в JetBrains Research, постдок Институт им. Макса Планка: Программные Системы.
Список литературы
1. Lamport L. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers, vol. C-28, isssue 9, 1979, pp. 690–691.
2. Owens S., Sarkar S., and Sewell P. A better x86 memory model: x86-TSO. Lecture Notes in Computer Science, vol. 5674, 2009, pp. 391–407.
3. Alglave J., Maranget L., Sarkar S., and Sewell P. Litmus: Running Tests Against Hardware. Lecture Notes in Computer Science, vol. 6605, 2011, pp. 41–44.
4. Batty M., Owens S., Sarkar S., Sewell P., and Weber T. Mathematizing C++ concurrency. In Proc. of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 2011, pp. 55–66.
5. Manson J., Pugh W., and Adve S.V. The Java memory model. In Proc. of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 2005, pp. 378–391.
6. ECMA International. 2018b. ECMAScript 2018 Language Specification – Memory Model. Available at: https://www.ecma-international.
7. Watt C., Rossberg A., Pichon-Pharabod J. Weakening WebAssembly. Proceedings of the ACM on Programming Languages, vol. 3, issue OOPSLA, 2019, 28 p.
8. Sewell P., Sarkar S., Owens S., Nardelli F.Z., and Myreen M. O. x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. Communications of the. ACM, vol. 53, issue 7, 2010, pp. 89-97.
9. Alglave J., Maranget L., and Tautschnig M. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Transactions on Programming Languages and Systems, vol, 36, issue 2, 2014, pp. 7:1–7:74.
10. Sarkar S., Sewell P., Alglave J., Maranget L., and Williams D. Understanding POWER Multiprocessors. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011, pp. 175-186.
11. Pulte C., Flur S., Deacon W., French J., Sarkar S., and Sewell P. Simplifying ARM concurrency: Multicopy-atomic axiomatic and operational models for armv8. Proceedings of the ACM on Programming Languages, vol. 2, issue POPL, 2017, pp. 19:1–19:29.
12. ARM Limited. ARM architecture reference manual: ARMv7-A and ARMv7-R edition, 2014. Available at: https://static.docs.arm.com/ddi0406/c/DDI0406C_C_arm_architecture_reference_manual.pdf.
13. Flur S., Gray K., Pulte C., Sarkar S., Sezgin A., Maranget L, Deacon W., and Sewell P. Modelling the ARMv8 architecture, operationally: Concurrency and ISA. In Proc. of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016, pp. 608–621.
14. Dolan S., Sivaramakrishnan K., and Madhavapeddy A. Bounding data races in space and time. Extended version. Available at: http://kcsrk.info/papers/pldi18-memory.pdf.
15. Dolan S., Sivaramakrishnan K., and Madhavapeddy A. Bounding data races in space and time. In Proc. of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018, pp. 242-255.
16. IBM Power Systems. IBM power systems facts and features: enterprise and scale-out systems with POWER8 processor technology. Available at: https://www.ibm.com/downloads/cas/JDRZDG0A.
17. Podkopaev A., Lahav O., and Vafeiadis V. Bridging the gap between programming languages and hardware weak memory models. Proceedings of the ACM on Programming Languages, vol. 3, issue POPL, 2019, pp. 69:1–69:31.
18. Lahav O., Vafeiadis V., Kang J., Hur C.-K., and Dreyer D. Repairing sequential consistency in C/C++11. Programming Language Design and Implementation, vol. 52, issue 6, 2017, pp. 618–632.
19. Podkopaev A., Lahav O., Melkonian O., and Vafeiadis V. Extending Intermediate Memory Model with SC accesses. Technical report. Available at: http://plv.mpi-sws.org/imm/immsctr.pdf. 2019.
20. Подкопаев А.В. Операционные методы в приложениях к слабым моделям памяти. Диссертация на соискание учёной степени кандидата физико-математических наук. Санкт-Петербург, 2018, 190 стр. / Podkopaev A.V. Operational methods in applications to weak memory models. The dissertation for the degree of candidate of physical and mathematical sciences. St. Petersburg, 2018,190 p. (in Russian).
21. Подкопаев А.В., Лахав О., Вафеядис В. О корректности компиляции подмножествa обещающей модели памяти в аксиоматическую модель ARMv8.3. Научно-технические ведомости СПбГПУ, том 10, № 4, 2017, стр. 51–69 / Podkopaev A.V., Lahav O., Vafeyadis V. On the correct compilation of a subset of a promising memory model into an axiomatic model ARMv8.3. St. Petersburg Polytechnic University Journal of Engineering Science and Technology, vol. 10, № 4, pp. 51-69 (in Russian).
22. Подкопаев А.В., Лахав О., Вафеядис В. Обещающая компиляция в ARMv8.3. Труды ИСП РАН, том 29, вып. 5, 2017, стр. 149-164 / Podkopaev A.V., Lahav O., Vafeiadis V. Promising Compilation to ARMv8.3. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 5, 2017. pp. 149-164 (in Russian). DOI: 10.15514/ISPRAS-2017-29(5)-9.
23. Kang J., Hur C.-K., Lahav O., Vafeiadis V., and Dreyer D. A promising semantics for relaxed-memory concurrency. In Proc. of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017, pp. 175–189.
24. Doherty S. Local data-race freedom and the C11 memory model. Surrey Concurrency Workshop Absracts, 2019. Available at: https://cw-srepls-19.github.io/abstracts.html#doherty/
25. Coq formalization of the Intermediate Memory Model. Available at: https://github.com/weakmemory/imm. 2019.
Рецензия
Для цитирования:
Намаконов Е.С., Подкопаев А.В. Компиляция модели памяти OCaml в Power. Труды Института системного программирования РАН. 2019;31(5):63-78. https://doi.org/10.15514/ISPRAS-2019-31(5)-xx
For citation:
Namakonov E.S., Podkopaev A.V. Compilation of OCaml memory model into Power. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2019;31(5):63-78. (In Russ.) https://doi.org/10.15514/ISPRAS-2019-31(5)-xx
Послать статью по эл. почте 