Формализация языков частично упорядоченных мультимножеств в системе Coq для спецификации слабых моделей памяти

Предмет исследования. Модели памяти задают семантику многопоточных программ, работающих с разделяемой памятью. В настоящее время эта область активно развивается, создаются новые модели памяти, востребованы новые средства формализации таких моделей, а также способы и средства доказательства их свойств. В работе рассмотрена задача формальной спецификации моделей памяти в системах интерактивного доказательства теорем.

Метод. Использован семантический домен языков частично упорядоченных мультимножеств или языков помсетов. Предложен метод кодировки семантического домена с помощью фактор-типов и обсуждены его достоинства и недостатки.

Основные результаты. Представлена библиотека, разработанная в системе Coq, реализующая предложенный метод. В рамках библиотеки установлена взаимосвязь языков помсетов с традиционной операционной семантикой, заданной в терминах помеченных систем переходов. Это позволило специфицировать в Coq модели памяти, параметризованные операционной семантикой структуры данных, и, таким образом, разделить определения модели памяти и структуры данных.

Практическая значимость. Предложенная библиотека может быть использована для формальной спецификации и доказательства свойств широкого класса моделей памяти. Чтобы продемонстрировать это, в работе приведена формализация нескольких базовых моделей, а именно, моделей последовательной, причинной и конвейерной согласованности.

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., TucciPiergiovanni 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 SIGPLANSIGACT 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