ENG
РУС
Search
Menu
About the Edition
Open Access Statement
Editorial Board
Editorial Policy
Editorial Ethics
Rules for peer-review
Rules for presentation of papers
Forms of Submitted Documents
Recommendations for the Design of References to Our Journal
Editorial Staff
Information for Subscribers
Summaries of the Issue
List of Authors
Issues
Publishers license agreement
Procedure of work with personal data
Publications
2025
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002
2001
Editor-in-Chief

Nikiforov
Vladimir O.
D.Sc., Prof.
Partners













































doi: 10.17586/2226-1494-2022-22-3-517-527

Mechanization of pomset languages in the Coq proof assistant for the specification of weak memory models

E. A. Moiseenko, V. P. Gladstein, A. V. Podkopaev, D. V. Koznov


Read the full article  ';
Article in Russian

For citation:
Moiseenko E.V., 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, vol. 22, no. 3, pp. 517–527 (in Russian). doi: 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.

Keywords: memory models, pomset languages, formal semantics, interactive theorem proving

Acknowledgements. The reported study was funded by RFBR, project number № 20-31-90088.

References
  1. Moiseenko E., Podkopaev A., Koznov D.A survey of programming language memorymodels. 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 POWERmultiprocessors. 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. Proceedingsof 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 Javamemory 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 ofJava’s concurrent access modes. Proceedingsof the ACM on Programming Languages, 2019, vol. 3, no. OOPSLA, pp. A142.https://doi.org/10.1145/3360568
  8. Chakraborty S.,Vafeiadis V. Formalizingthe 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 theJavaScript relaxed memory model. Proc. of the 41st ACM SIGPLAN Conferenceon 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. Causalconsistency: beyond memory. Proc.of the 21st ACM SIGPLAN Symposium onPrinciples 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-89884-1_34
  12. Anceaume E., Del Pozzo A., Ludinard R.,Potop-Butucaru M., Tucci-Piergiovanni S.Blockchain abstract data type. Proc. of the31stACM 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. 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-colortheorem. 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 ComputingSurveys, 1977, vol. 9, no. 3, pp. 223–252.https://doi.org/10.1145/356698.356702
  22. Chakraborty S.,Vafeiadis V. Groundingthin-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 onProgramming 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 SIGPLAN-SIGACT 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 modelchecking 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 Coqsystem.Inria Saclay Ile de France, 2016.
  31. Aceto L., Fokkink W., Verhoef C. Structural operational semantics. Handbook ofProcess Algebra. Elsevier, 2001, pp. 197–292.https://doi.org/10.1016/B978-044482830-9/50021-7
  32. Lamport L. How to make a multiprocessorcomputer 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-passingsystems 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 weakmemory consistency: specifying and verifyingconcurrent libraries under declarative consistency models. Proceedings of the ACM onProgramming 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 FunctionalProgramming, 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 onSoftware 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. Makingweak 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 forpartially 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-98938-9_7


Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License
Copyright 2001-2025 ©
Scientific and Technical Journal
of Information Technologies, Mechanics and Optics.
All rights reserved.

Яндекс.Метрика