Mechanization of pomset languages in the Coq proof assistant for the specification of weak memory models
https://doi.org/10.17586/2226-1494-2022-22-3-517-527
Abstract
Memory models define semantics of concurrent programs operating on shared memory. Theory of these models is an active research topic. As new models emerge, the problem of providing a rigorous formal specification of these models becomes relevant. In this paper we consider a problem of formalizing memory models in the interactive theorem proving systems. We use semantic domain of pomset languages to formalize memory models. We propose an encoding of pomset languages using quotient types and discuss advantages and shortcomings of this approach. We present a library developed in the Coq proof assistant that implements the proposed approach. As a part of this library, we establish a connection between pomset languages and operational semantics defined by labeled transition systems. With the help of this theory, it becomes possible to define in Coq memory models parameterized by the operational semantics of an abstract datatype, and thus to decouple the definition of a memory model from the definition of the datatype. The proposed library can be used to develop formal machine-checked specifications of a wide class of memory models. In order to demonstrate its applicability, we present specifications of several basic memory models: sequential, causal, and pipelined consistency.
Supporting agencies: The reported study was funded by RFBR, project number № 20-31-90088.
About the Authors
E. A. Moiseenko
Saint Petersburg State University; JetBrains Research
Russian Federation
Russian Federation
Evgenii A. Moiseenko — PhD Student; Researcher
Saint Petersburg, 199034
Saint Petersburg, 194100
sc 57219492685
V. P. Gladstein
Saint Petersburg State University; JetBrains Research
Russian Federation
Russian Federation
Vladimir P. Gladstein — Student; Researcher
Saint Petersburg, 199034
Saint Petersburg, 194100
A. V. Podkopaev
JetBrains Research; HSE University
Russian Federation
Russian Federation
Anton V. Podkopaev — PhD, Associate Professor
Saint Petersburg, 194100
sc 56875418900
D. V. Koznov
Saint Petersburg State University
Russian Federation
Russian Federation
Dmitry V. Koznov — D. Sc., Associate Professor, Professor
Saint Petersburg, 199034
sc 8885649400
References
1. Moiseenko E., Podkopaev A., Koznov D. A survey of programming language memory models. Programming and Computer Software, 2021, vol. 47, no. 6, pp. 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, vol. 53, no. 7, pp. 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, pp. 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, vol. 2, pp. 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, vol. 46, no. 1, pp. 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, vol. 40, no. 1, pp. 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, vol. 3, no. OOPSLA, pp. 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, pp. 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, pp. 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, pp. 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, vol. 10801, pp. 968–995. https://doi.org/10.1007/978-3-319-898841_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, pp. 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. Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2015, vol. 9032, pp. 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, vol. 52, no. 6, pp. 618–632. https://doi.org/10.1145/3062341.3062352
15. Gonthier G. Formal proof — the four-color theorem. Notices of the AMS, 2008, vol. 55, no. 11, pp. 1382–1393.
16. Leroy X. A formally verified compiler back-end. Journal of Automated Reasoning, 2009, vol. 43, no. 4, pp. 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, vol. 197, pp. 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, vol. 61, no. 2-3, pp. 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, pp. 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, pp. 325–392.
21. Peterson J.L. Petri nets. ACM Computing Surveys, 1977, vol. 9, no. 3, pp. 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, vol. 3, no. POPL, pp. 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, vol. 4, no. OOPSLA, pp. 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, pp. 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, vol. 2, no. POPL, pp. 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, vol. 803, pp. 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, vol. 79, no. 2, pp. 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, vol. 711, pp. 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, vol. 7998, pp. 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, pp. 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, vol. 28, no. 9, pp. 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, pp. 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, vol. 10, no. 1, pp. 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, vol. 3, no. POPL, pp. 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, vol. 13, no. 2, pp. 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, vol. 2646, pp. 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, vol. SE-3, no. 2, pp. 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, vol. 5, no. OOPSLA, pp. 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, vol. 11, no. 1, pp. 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, vol. 51, no. 1, pp. 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, vol. 11023, pp. 110–129. https://doi.org/10.1007/978-3-319-989389_7
Review
For citations:
Moiseenko E.A., Gladstein V.P., Podkopaev A.V., Koznov D.V. Mechanization of pomset languages in the Coq proof assistant for the specification of weak memory models. Scientific and Technical Journal of Information Technologies, Mechanics and Optics. 2022;22(3):517-527. (In Russ.) https://doi.org/10.17586/2226-1494-2022-22-3-517-527
Views:
4
Email this article 