Compilation of OCaml memory model into Power
https://doi.org/10.15514/ISPRAS-2019-31(5)-xx
Abstract
The development of memory models aimed at solving various concurrency problems is an active research topic. One such model is the OCaml memory model (OCamlMM), which allows to mitigate undefined behavior caused by data races. To use this model in practice one has to prove the correctness of its compilation into mainstream CPU architectures. At the moment, it is done for x86 and ARM but not for Power.One way to prove the correctness of compilation of OCamlMM into the Power model is to develop a compilation scheme from OCamlMM into the Intermediate Memory Model (IMM). It would be sufficient since there already exists a compilation scheme from IMM to the Power model. In this paper, the compilation scheme from OCamlMM into IMM is presented and proved to be correct. Memory fences and compare-and-swap instructions are used to permit only behavior allowed by OCamlMM. The resulting compilation scheme gives a correct compilation scheme from OCamlMM to the Power model. Moreover, when a compilation scheme from IMM into another CPU architecture will be developed, such an approach would immediately give a correct scheme of compilation of OCamlMM into that architecture.
Supporting agencies: Authors are grateful to the research group colleagues for participating in early paper versions’ discussions.
About the Authors
Egor Sergeevich Namakonov
St Petersburg University,
JetBrains Research
Russian Federation
Master’s student in St Petersburg University, a member of weak memory model research group in JetBrains Research
Russian Federation
Master’s student in St Petersburg University, a member of weak memory model research group in JetBrains Research
Anton Viktorovich Podkopaev
St Petersburg University,
National Research University «Higher School of Economics»,
Max Planck Institute for Software Systems
Russian Federation
Associate professor in NRU HSE (SPb), the weak memory model group leader in JetBrains Research, a postdoc in MPI-SWS
Russian Federation
Associate professor in NRU HSE (SPb), the weak memory model group leader in JetBrains Research, a postdoc in MPI-SWS
References
1. Lamport L. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers, 1979, C-28, 9:690–691. doi: 10.1109/TC.1979.1675439.
2. Owens S., Sarkar S., and Sewell P. A better x86 memory model: x86-TSO. In Theorem Proving in Higher Order Logics, 2009, pages 391–407. doi: 10.1007/978-3-642-03359-9_27.
3. Alglave J., Maranget L., Sarkar S., and Sewell P. Litmus: Running Tests Against Hardware. In TACAS. Springer, 41–44. 2011. doi: 10.1007/978-3-642-19835-9_5.
4. 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.
5. 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.
6. 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.
7. 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.
8. 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.
9. ECMA International. 2018b. ECMAScript 2018 Language Specification – Memory Model. Available at: https://www.ecma-international.
10. Watt C., Rossberg A., Pichon-Pharabod J. Weakening WebAssembly. Proceedings of the ACM on Programming Languages, vol. 3, issue OOPSLA, 2019, 28 p.
11. 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.
12. 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.
13. 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.
14. 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.
15. 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.
16. 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.
17. 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.
18. 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.
19. 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.
20. 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.
21. 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.
22. 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.
23. Подкопаев А.В. Операционные методы в приложениях к слабым моделям памяти. Диссертация на соискание учёной степени кандидата физико-математических наук. Санкт-Петербург, 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).
24. Подкопаев А.В., Лахав О., Вафеядис В. О корректности компиляции подмножеств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).
25. Подкопаев А.В., Лахав О., Вафеядис В. Обещающая компиляция в 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.
26. 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.
27. 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/
28. Coq formalization of the Intermediate Memory Model. Available at: https://github.com/weakmemory/imm. 2019.
Review
For citations:
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
Email this article 