Promising Compilation to ARMv8.3
https://doi.org/10.15514/ISPRAS-2017-29(5)-9
Abstract
Concurrent programs have behaviors, which cannot be explained by interleaving execution of their threads on a single processing unit due to optimizations, which are performed by modern compilers and CPUs. How to correctly and completely define a semantics of a programming language, which accounts for the behaviors, is an open research problem. There is an auspicious attempt to solve the problem - promising memory model. To show that the model might be used as a part of an industrial language standard, it is necessary to prove correctness of compilation from the model to memory models of target processor architectures. In this paper, we present a proof of compilation correctness from a subset of promising memory model to an axiomatic ARMv8.3 memory model. The subset contains relaxed memory accesses and release and acquire fences. The proof is based on a novel approach of an execution graph traversal.
About the Authors
A. V. Podkopaev
St. Petersburg University; JetBrains Research
Russian Federation
Russian Federation
O. Lahav
Tel-Aviv University
Israel
Israel
V. Vafeiadis
Max Planck Institute for Software Systems
Germany
Germany
References
1. Lamport L. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers, 28(9):690-691, 1979. doi:10.1109/TC.1979.1675439.
2. Aho A.V., Sethi R., Ullman J.D., Compilers: Principles, Techniques, and Tools, Addison-Wesley, 1986.
3. Sewell P., Sarkar S., Owens S., Zappa Nardelli F., and Myreen M. O. x86-TSO: A rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM, 53(7):89-97, 2010. doi:10.1145/1785414.1785443.
4. Alglave J., Maranget L., and Tautschnig M. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst., 36(2):7:1-7:74, 2014. doi:10.1145/2627752.
5. Sarkar S., Sewell P., Alglave J., Maranget L., and Williams D. Understanding POWER multiprocessors. In PLDI 2011, pages 175-186. ACM, 2011. doi:10.1145/1993498. 1993520.
6. Flur S., Gray K. E., Pulte C., Sarkar S., Sezgin A., Maranget L., Deacon W., and Sewell P. Modelling the ARMv8 architecture, operationally: Concurrency and ISA. In POPL 2016, pages 608-621. ACM, 2016. doi:10.1145/2837614.2837615.
7. Pulte C., Flur S., Deacon W., French J., Sarkar S., and Sewell P. Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8. URL: http://www.cl.cam.ac.uk/~pes20/armv8-mca/armv8-mca-draft.pdf. July 2017.
8. Batty M., Owens S., Sarkar S., Sewell P., and Weber T. Mathematizing C++ concurrency. In POPL 2011, pages 55-66. ACM, 2011. doi:10.1145/1925844.1926394.
9. Manson J., Pugh W., and Adve S. V. The Java memory model. In POPL 2005, pages 378-391. ACM, 2005. doi:10.1145/1040305.1040336.
10. Trifanov V.Yu. Dynamic detection of race conditions in multithreaded Java programs. Dissertation, ITMO University, 2013, p. 112 (in Russian).
11. Ševčík J. and Aspinall D. On Validity of Program Transformations in the Java Memory Model. In Proceedings of the 22nd European conference on Object-Oriented Programming(ECOOP '08), Jan Vitek (Ed.). Springer-Verlag, Berlin, Heidelberg, 27-51. doi: 10.1007/978-3-540-70592-5_3.
12. Boehm H.-J. and Demsky B. Outlawing ghosts: Avoiding out-of-thin-air results. In MSPC 2014, pages 7:1-7:6. ACM, 2014. doi:10.1145/2618128.2618134.
13. Kang J., Hur C.-K., Lahav O., Vafeiadis V., and Dreyer D. A promising semantics for relaxed-memory concurrency. In POPL 2017. ACM, 2017. doi:10.1145/3009837. 3009850.
14. Lahav O. and Vafeiadis V. Explaining relaxed memory models with program transformations. FM 2016. Springer, 2016. doi:10.1007/978-3-319-48989-6_29.
15. [Promising compilation to ARMv8.3. A formal proof]. October 2017. URL: https://podkopaev.net/armpromise
16. Leroy X. A formally verified compiler back-end. J. Autom. Reasoning, 43(4):363-446, 2009. doi:10.1007/s10817-009-9155-4.
17. Kumar R., Myreen M. O., Norrish M., and Owens S. CakeML: A verified implementation of ML. In POPL ’14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 179-191. ACM Press, January 2014. doi:10.1145/2535838.2535841.
18. Sevcı́k J., Vafeiadis V., Zappa Nardelli F., Jagannathan S., and Sewell P. Relaxed-memory concurrency and verified compilation. In Proceedings of the 38th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 43-54, 2011. doi:10.1145/1926385.1926393.
19. Batty M., Owens S., Sarkar S., Sewell P., and Weber T. Mathematizing C++ concurrency: The post-Rapperswil model. technical report n3132, iso iec jtc1/sc22/wg21. URL: http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2010/n3132.pdf.
20. Batty M., Memarian K., Nienhuis K, Pichon-Pharabod J., and Sewell P. The problem of programming language concurrency semantics. In ESOP, volume 9032 of LNCS, pages 283-307. Springer, 2015. doi:10.1007/978-3-662-46669-8_12.
21. Podkopaev A., Lahav O., and Vafeiadis V. Promising compilation to ARMv8 POP. In ECOOP 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. doi: 10.4230/LIPIcs.ECOOP.2017.22.
Review
For citations:
Podkopaev A.V., Lahav O., Vafeiadis V. Promising Compilation to ARMv8.3. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(5):149-164. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(5)-9
Email this article 