Обещающая компиляция в ARMv8.3
https://doi.org/10.15514/ISPRAS-2017-29(5)-9
Аннотация
Поведение многопоточных программ не может быть промоделировано попеременным последовательным исполнением различных потоков на одном вычислительном узле. На данный момент полное и корректное описание поведения многопоточных программ является открытой теоретической проблемой. Одним из перспективных решений этой проблемы является „обещающая“ модель памяти. Для того, чтобы некоторая модель могла быть использована в стандарте некоторого промышленного языка программирования, должна быть доказана корректность компиляции из этой модели в модель памяти целевой процессорной архитектуры. Данная статья представляет доказательство корректности компиляции из подмножества обещающей модели в модели памяти процессора ARMv8.3. Главной идеей доказательства является введение промежуточного операционного варианта модели ARMv8.3, поведение которого может быть симулировано обещающей моделью.
Об авторах
А. В. Подкопаев
Санкт-Петербургский Государственный Университет; JetBrains Research
Россия
Россия
О. Лахав
Тель-Авивский Университет
Израиль
Израиль
В. Вафеядис
Институт им. Макса Планка: Программные Системы
Германия
Германия
Список литературы
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. Трифанов В.Ю. Динамическое обнаружение состояний гонки в многопоточных Java-программах. Диссертация на соискание ученой степени кандидата технических наук. СПбГУ ИТМО, 2013, 112 стр.
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. Обещающая компиляция в ARMv8.3. Формальное доказательство. Октябрь 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.
Рецензия
Для цитирования:
Подкопаев А.В., Лахав О., Вафеядис В. Обещающая компиляция в ARMv8.3. Труды Института системного программирования РАН. 2017;29(5):149-164. https://doi.org/10.15514/ISPRAS-2017-29(5)-9
For citation:
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
Послать статью по эл. почте 