Меню
Публикации
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002
2001
Главный редактор
НИКИФОРОВ
Владимир Олегович
д.т.н., профессор
Партнеры
doi: 10.17586/2226-1494-2022-22-3-517-527
УДК 004.421.2:519.17 004.657
Формализация языков частично упорядоченных мультимножеств в системе Coq для спецификации слабых моделей памяти
Читать статью полностью
Язык статьи - русский
Ссылка для цитирования:
Аннотация
Ссылка для цитирования:
Моисеенко Е.А., Гладштейн В.П., Подкопаев А.В., Кознов Д.В. Формализация языков частично упорядоченных мультимножеств в системе Coq для спецификации слабых моделей памяти // Научно-технический вестник информационных технологий, механики и оптики. 2022. Т. 22, № 3. С. 517–527. doi: 10.17586/2226-1494-2022-22-3-517-527
Аннотация
Предмет исследования. Модели памяти задают семантику многопоточных программ, работающих с разделяемой памятью. В настоящее время эта область активно развивается, создаются новые модели памяти, востребованы новые средства формализации таких моделей, а также способы и средства доказательства их свойств. В работе рассмотрена задача формальной спецификации моделей памяти в системах интерактивного доказательства теорем. Метод. Использован семантический домен языков частично упорядоченных мультимножеств или языков помсетов. Предложен метод кодировки семантического домена с помощью фактор-типов и обсуждены его достоинства и недостатки. Основные результаты. Представлена библиотека, разработанная в системе Coq, реализующая предложенный метод. В рамках библиотеки установлена взаимосвязь языков помсетов с традиционной операционной семантикой, заданной в терминах помеченных систем переходов. Это позволило специфицировать в Coq модели памяти, параметризованные операционной семантикой структуры данных, и, таким образом, разделить определения модели памяти и структуры данных. Практическая значимость. Предложенная библиотека может быть использована для формальной спецификации и доказательства свойств широкого класса моделей памяти. Чтобы продемонстрировать это, в работе приведена формализация нескольких базовых моделей, а именно, моделей последовательной, причинной и конвейерной согласованности.
Ключевые слова: модели памяти, языки помсетов, формальная семантика, системы интерактивного доказательства теорем
Благодарности. Исследование выполнено при финансовой поддержке РФФИ в рамках научного проекта № 20-31-90088.
Список литературы
Благодарности. Исследование выполнено при финансовой поддержке РФФИ в рамках научного проекта № 20-31-90088.
Список литературы
1. Moiseenko E., Podkopaev A., Koznov D. A survey of programming language memory models // Programming and Computer Software. 2021. V. 47. N 6. P. 439–456. https://doi.org/10.1134/S0361768821060050
2. Sewell P., Sarkar S., Owens S., Nardelli F.Z., Myreen M.O. x86-TSO: A rigorous and usable programmer’s model for x86 multiprocessors // Communications of the ACM. 2010. V. 53. N 7. P. 89–97. https://doi.org/10.1145/1785414.1785443
3. Sarkar S., Sewell P., Alglave J., Maranget L., Williams D. Understanding POWER multiprocessors // Proc. of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. 2011. P. 175–186. https://doi.org/10.1145/1993316.1993520
4. Pulte C., Flur S., Deacon W., French J., Sarkar S., Sewell P. Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8 // Proceedings of the ACM on Programming Languages. 2018. V. 2. P. 19. https://doi.org/10.1145/3158107
5. Batty M., Owens S., Sarkar S., Sewell P., Weber T. Mathematizing C++ concurrency // ACM SIGPLAN Notices. 2011. V. 46. N 1. P. 55–66. https://doi.org/10.1145/1925844.1926394
6. Manson J., Pugh W., Adve S.V. The Java memory model // ACM SIGPLAN Notices. 2005. V. 40. N 1. P. 378–391. https://doi.org/10.1145/1047659.1040336
7. Bender J., Palsberg J. A formalization of Java’s concurrent access modes // Proceedings of the ACM on Programming Languages. 2019. V. 3. N OOPSLA. P. A142. https://doi.org/10.1145/3360568
8. Chakraborty S., Vafeiadis V. Formalizing the concurrency semantics of an LLVM fragment // Proc.of the IEEE/ACM International Symposium on Code Generation and Optimization (CGO). 2017. P. 100–110. https://doi.org/10.1109/CGO.2017.7863732
9. Watt C., Pulte C., Podkopaev A., Barbier G., Dolan S., Flur S., Pichon-Pharabod J., Guo S.-Y. Repairing and mechanising the JavaScript relaxed memory model // Proc. of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 2020. P. 346–361. https://doi.org/10.1145/3385412.3385973
10. Perrin M., Mostéfaoui A., Jard C. Causal consistency: beyond memory // Proc. of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP). 2016. P. 26. https://doi.org/10.1145/2851141.2851170
11. Jagadeesan R., Riely J. Eventual consistency for CRDTs // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2018. V. 10801. P. 968–995. https://doi.org/10.1007/978-3-319-89884-1_34
12. Anceaume E., Del Pozzo A., Ludinard R., Potop-Butucaru M., Tucci-Piergiovanni S. Blockchain abstract data type // Proc. of the 31st ACM Symposium on Parallelism in Algorithms and Architectures. 2019. P. 349–358. https://doi.org/10.1145/3323165.3323183
13. Batty M., Memarian K., Nienhuis K., Pichon-Pharabod J., Sewell P. The problem of programming language concurrency semantics // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2015. V. 9032. P. 283–307. https://doi.org/10.1007/978-3-662-46669-8_12
14. Lahav O., Vafeiadis V., Kang J., Hur C.-K., Dreyer D. Repairing Sequential Consistency in C/C++11 // ACM SIGPLAN Notices. 2017. V. 52. N 6. P. 618–632. https://doi.org/10.1145/3062341.3062352
15. Gonthier G. Formal proof – the four-color theorem // Notices of the AMS. 2008. V. 55. N 11. P. 1382–1393.
16. Leroy X. A formally verified compiler back-end // Journal of Automated Reasoning. 2009. V. 43. N 4. P. 363–446. https://doi.org/10.1007/s10817-009-9155-4
17. Pratt V. The pomset model of parallel processes: Unifying the temporal and the spatial // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1985. V. 197. P. 180–196. https://doi.org/10.1007/3-540-15670-4_9
18. Gischer J.L. The equational theory of pomsets // Theoretical Computer Science. 1988. V. 61. N 2-3. P. 199–224. https://doi.org/10.1016/0304-3975(88)90124-7
19. Mazurkiewicz A. Trace theory // Advances in Petri nets 1986, part II on Petri nets: applications and relationships to other models of concurrency. Springer, 1986. P. 278–324.
20. Winskel G. Event structures // Advances in Petri nets 1986, part II on Petri nets: applications and relationships to other models of concurrency. Springer, 1986. P. 325–392.
21. Peterson J.L. Petri nets // ACM Computing Surveys. 1977. V. 9. N 3. P. 223–252. https://doi.org/10.1145/356698.356702
22. Chakraborty S., Vafeiadis V. Grounding thin-air reads with event structures // Proceedings of the ACM on Programming Languages. 2019. V. 3. N POPL. P. 70. https://doi.org/10.1145/3290383
23. Jagadeesan R., Jeffrey A., Riely J. Pomsets with preconditions: a simple model of relaxed memory // Proceedings of the ACM on Programming Languages. 2020. V. 4. N OOPSLA. P. 194. https://doi.org/10.1145/3428262
24. Abdulla P., Aronis S., Jonsson B., Sagonas K. Optimal dynamic partial order reduction // Proc. of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 2014. P. 373–384. https://doi.org/10.1145/2535838.2535845
25. Kokologiannakis M., Lahav O., Sagonas K., Vafeiadis V. Effective stateless model checking for C/C++ concurrency // Proceedings of the ACM on Programming Languages. 2017. V. 2. N POPL. P. 17. https://doi.org/10.1145/3158105
26. Nielsen M., Sassone V., Winskel G. Relationships between models of concurrency // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1994. V. 803. P. 425–476. https://doi.org/10.1007/3-540-58043-3_25
27. Vaandrager F.W. Determinism → (event structure isomorphism = step sequence equivalence) // Theoretical Computer Science. 1991. V. 79. N 2. P. 275–294. https://doi.org/10.1016/0304-3975(91)90333-W
28. Sassone V., Nielsen M., Winskel G. Deterministic behavioural models for concurrency // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1993. V. 711. P. 682–692. https://doi.org/10.1007/3-540-57182-5_59
29. Cohen C. Pragmatic quotient types in Coq // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2013. V. 7998. P. 213–228. https://doi.org/10.1007/978-3-642-39634-2_17
30. Gonthier G., Mahboubi A., Tassi E. A small scale reflection extension for the Coq system. Inria Saclay Ile de France, 2016.
31. Aceto L., Fokkink W., Verhoef C. Structural operational semantics // Handbook of Process Algebra. Elsevier, 2001. P. 197–292. https://doi.org/10.1016/B978-044482830-9/50021-7
32. Lamport L. How to make a multiprocessor computer that correctly executes multiprocess programs // IEEE Transactions on Computers. 1979. V. 28. N 9. P. 690–691. https://doi.org/10.1109/TC.1979.1675439
33. Singh A., Narayanasamy S., Marino D., Millstein T., Musuvathi M. End-to-end sequential consistency // Proc. of the 39th Annual International Symposium on Computer Architecture (ISCA). 2012. P. 524–535. https://doi.org/10.1109/ISCA.2012.6237045
34. Fidge C.J. Timestamps in message-passing systems that preserve the partial ordering // Australian Computer Science Communications. 1988. V. 10. N 1. P. 56–66.
35. Raad A., Doko M., Rožić L., Lahav O., Vafeiadis V. On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models // Proceedings of the ACM on Programming Languages. 2019. V. 3. N POPL. P. 68. https://doi.org/10.1145/3290381
36. Martin-Löf P., Sambin G. Intuitionistic Type Theory. V. 9. Bibliopolis, 1984.
37. Barthe G., Capretta V., Pons O. Setoids in type theory // Journal of Functional Programming. 2003. V. 13. N 2. P. 261–293. https://doi.org/10.1017/S0956796802004501
38. Chicli L., Pottier L., Simpson C. Mathematical quotients and quotient types in Coq // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2003. V. 2646. P. 95–107. https://doi.org/10.1007/3-540-39185-1_6
39. Gross J.S. Performance Engineering of Proof-Based Software Systems at Scale: Ph. D. thesis / Massachusetts Institute of Technology. 2021.
40. Lamport L. Proving the correctness of multiprocess programs // IEEE Transactions on Software Engineering. 1977. V. SE-3. N 2. P. 125–143. https://doi.org/10.1109/TSE.1977.229904
41. Lahav O., Namakonov E., Oberhauser J., Podkopaev A., Vafeiadis V. Making weak memory models fair // Proceedings of the ACM on Programming Languages. 2021. V. 5. N OOPSLA. P. 98. https://doi.org/10.1145/3485475
42. Affeldt R., Cohen C., Rouhling D. Formalization techniques for asymptotic reasoning in classical analysis // Journal of Formalized Reasoning. 2018. V. 11. N 1. P. 43–76. https://doi.org/10.6092/issn.1972-5787/8124
43. Diaconescu R. Axiom of choice and complementation // Proceedings of the American Mathematical Society. 1975. V. 51. N 1. P. 176–178. https://doi.org/10.1090/S0002-9939-1975-0373893-X
44. Doherty S., Dongol B., Wehrheim H., Derrick J. Making linearizability compositional for partially ordered executions // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2018. V. 11023. P. 110–129. https://doi.org/10.1007/978-3-319-98938-9_7