Обещающая компиляция в ARMv8.3
Автор: Подкопаев А.В., Лахав О., Вафеядис В.
Журнал: Труды Института системного программирования РАН @trudy-isp-ran
Статья в выпуске: 5 т.29, 2017 года.
Бесплатный доступ
Поведение многопоточных программ не может быть промоделировано попеременным последовательным исполнением различных потоков на одном вычислительном узле. На данный момент полное и корректное описание поведения многопоточных программ является открытой теоретической проблемой. Одним из перспективных решений этой проблемы является „обещающая“ модель памяти. Для того, чтобы некоторая модель могла быть использована в стандарте некоторого промышленного языка программирования, должна быть доказана корректность компиляции из этой модели в модель памяти целевой процессорной архитектуры. Данная статья представляет доказательство корректности компиляции из подмножества обещающей модели в модели памяти процессора ARMv8.3. Главной идеей доказательства является введение промежуточного операционного варианта модели ARMv8.3, поведение которого может быть симулировано обещающей моделью.
Многопоточность, корректность компиляции, слабые модели памяти
Короткий адрес: https://sciup.org/14916470
IDR: 14916470 | DOI: 10.15514/ISPRAS-2017-29(5)-9
Список литературы Обещающая компиляция в ARMv8.3
- 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
- Aho A.V., Sethi R., Ullman J.D., Compilers: Principles, Techniques, and Tools, Addison-Wesley, 1986.
- 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
- 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
- Sarkar S., Sewell P., Alglave J., Maranget L., and Williams D. Understanding POWER multiprocessors. In PLDI 2011, pages 175-186. ACM, 2011. 1993520 DOI: 10.1145/1993498
- 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
- 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.
- 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
- 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
- Trifanov V.Yu. Dynamic detection of race conditions in multithreaded Java programs. Dissertation, ITMO University, 2013, p. 112.
- Š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
- 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
- Kang J., Hur C.-K., Lahav O., Vafeiadis V., and Dreyer D. A promising semantics for relaxed-memory concurrency. In POPL 2017. ACM, 2017. 3009850 DOI: 10.1145/3009837
- 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
- October 2017. URL: https://podkopaev.net/armpromise
- Leroy X. A formally verified compiler back-end. J. Autom. Reasoning, 43(4):363-446, 2009 DOI: 10.1007/s10817-009-9155-4
- 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
- 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
- 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.
- 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
- 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
