Preview

Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS)

Advanced search

Mechanized Theory of Event Structures: A Case of Parallel Register Machine

https://doi.org/10.15514/ISPRAS-2021-33(3)-11

Abstract

The true concurrency models, and in particular event structures, have been introduced in the 1980s as an alternative to operational interleaving semantics of concurrency, and nowadays they are regaining popularity. Event structures represent the causal dependency and conflict between the individual atomic actions of the system directly. This property leads to a more compact and concise representation of semantics. In this work-in-progress report, we present a theory of event structures mechanized in the COQ proof assistant and demonstrate how it can be applied to define certified executable semantics of a simple parallel register machine with shared memory.

About the Authors

Vladimir GLADSTEIN
Saint Petersburg State University
Russian Federation

Bachelor student 



Dmitrii MIKHAILOVSKII
Saint Petersburg State University
Russian Federation

Bachelor student 



Evgenii MOISEENKO
Saint Petersburg State University
Russian Federation

PhD student 



Anton TRUNOV
Zilliqa Research
Singapore

Research engineer 



References

1. G. Winskel. Event structures. Lecture Notes in Computer Science, vol. 255, 1986, pp. 325-392.

2. A. Jeffrey and J. Riely. On thin air reads: Towards an event structures model of relaxed memory. In Proc. of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016, pp. 759-767.

3. J. Pichon-Pharabod and P. Sewell. A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. ACM SIGPLAN Notices, vol. 51, issue 1, 2016, pp. 622-633.

4. S. Chakraborty and V. Vafeiadis. Grounding thin-air reads with event structures. Proceedings of the ACM on Programming Languages, vol. 3, issue POPL, 2019, pp. 1-28.

5. A. Fellner, T. Tarrach, and G. Weissenbacher. Language inclusion for finite prime event structures. Lecture Notes in Computer Science, vol. 11990, 2020, pp. 314-336.

6. The Coq Development Team. The Coq Proof Assistant, 2021. Available at https://coq.inria.fr/, accessed 7-May-2021.

7. Agda language reference. Available at https://agda.readthedocs.io/, accessed 7-May-2021.

8. T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: a proof assistant for higher-order logic. Lecture Notes in Computer Science, vol. 2283, 2002, 240 p.

9. Arend theorem prover. Available at https://arend-lang.github.io/, accessed 7-May-2021.

10. X. Leroy. Formal verification of a realistic compiler. Communications of the ACM, vol. 52, no. 7, 2009, pp. 107–115.

11. A.W. Appel. Verified software toolchain. Lecture Notes in Computer Science, vol. 6602, 2011, pp. 1-17.

12. R. Jung, R. Krebbers et al. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, vol. 28, 2018, article e 20.

13. G. Winskel. Event structure semantics for CCS and related languages. Lecture Notes in Computer Science, vol. 140, 1982, pp. 561-576.

14. R. Langerak. Bundle event structures: a non-interleaving semantics for LOTOS. In Proc. of the 5th International Conference on Formal Description Techniques for Distributed Systems and Communications Protocols, 1992, pp. 331-346.

15. G. Boudol and I. Castellani. Flow models of distributed computations: event structures and nets. Research Report RR-1482, INRIA, 1991, 40 p.

16. E. Moiseenko, A. Podkopaev et al. Reconciling event structures with modern multiprocessors. In Proc. of the 34th European Conference on Object-Oriented Programming, 2020, 26 p.

17. A. Mahboubi and E. Tassi. Mathematical components, 2017. Available at http://doi.org/10.5281/zenodo.4457887, accessed 7-May-2021.

18. G. Gonthier, A. Mahboubi, and E. Tassi. A small scale reflection extension for the Coq system. Research Report RR-6455, Inria Saclay Ile de France, 2016, 69 p.

19. G. Gonthier and A. Mahboubi. An introduction to small scale reflection in Coq. Journal of formalized reasoning, vol. 3, no. 2, 2010, pp. 95-152.

20. M. Sozeauand, C. Mangin. Equations reloaded: High-level dependently-typed functional programming and proving in Coq. Proceedings of the ACM on Programming Languages, vol. 3, 2019, article no. 86.

21. D. Kozen. Kleene algebra with tests. ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 19, no. 3,1997, pp. 427-443.

22. D. Pous. Kleene algebra with tests and Coq tools for while programs. Lecture Notes in Computer Science, vol. 7998, 2013, pp. 180-196.

23. L.-y. Xia, Y. Zakowski et al. Interaction trees: representing recursive and impureprograms in Coq. Proceedings of the ACM on Programming Languages, vol. 4, issue POPL, 2019, pp. 1-32.

24. T. Letan and Y. R ́egis Gianas. Freespec: specifying, verifying, and executing impure computations in Coq. In Proc. of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020, pp. 32-46.

25. R. Affeldt, D. Nowak, and T. Saikawa. A hierarchy of monadic effects for program verification using equational reasoning. Lecture Notes in Computer Science, vol. 11825, 2019, pp. 226-254.

26. P. Letouzey. Extraction in Coq: An overview. Lecture Notes in Computer Science, vol. 5028, 2008, pp. 359-369.

27. F. Garillot, G. Gonthier et al. Packaging mathematical structures. Lecture Notes in Computer Science, vol. 5674, 2009, pp. 327-342.

28. O. Lahav, V. Vafeiadis et al. Repairing sequential consistency in C/C++11. In Proc. of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017, pp. 618-632.

29. H.-J. Boehm and B. Demsky. Outlawing ghosts: Avoiding out-of-thin-air results. In Proc. of the Workshop on Memory Systems Performance and Correctness, 2014, article no. 7.

30. L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers, vol. 28, no. 9, 1979, pp. 690-691.

31. R. Milner. A calculus of communicating systems. Springer-Verlag, 1980, 260 p.

32. R. Milner. Communicating and mobile systems: the pi calculus. Cambridge university press, 1999, 176 p.

33. O. Lahav, N. Giannarakis, and V. Vafeiadis. Taming release-acquire consistency. ACM SIGPLAN Notices, vol. 51, no. 1, 2016, pp. 649-662

34. A. Podkopaev, O. Lahav, and V. Vafeiadis. Bridging the gap between programming languages and hardware weak memory models. Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, 2019, pp. 1-31.

35. M. Dodds, M. Batty, and A. Gotsman. Compositional verification of compiler optimizations on relaxed memory. Lecture Notes in Computer Science, vol. 10801, 2018, pp. 1027-1055.

36. M. Nielsen, G. Plotkin, and G. Winskel. Petri nets, event structures and domains, part I. Theoretical Computer Science, vol. 13, no. 1, 1981, pp. 85-108.


Review

For citations:


GLADSTEIN V., MIKHAILOVSKII D., MOISEENKO E., TRUNOV A. Mechanized Theory of Event Structures: A Case of Parallel Register Machine. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2021;33(3):143-154. https://doi.org/10.15514/ISPRAS-2021-33(3)-11



Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)