Preview

Труды Института системного программирования РАН

Расширенный поиск

Механизированная теория структур событий: случай параллельной регистровой машины

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

Аннотация

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

Об авторах

Владимир Петрович ГЛАДШТЕЙН
Санкт-Петербургский государственный университет
Россия

Cтудент бакалавриата 



Дмитрий Владимирович МИХАЙЛОВСКИЙ
Санкт-Петербургский государственный университет
Россия

Cтудент бакалавриата 



Евгений Александрович МОИСЕЕНКО
Санкт-Петербургский государственный университет
Россия

Аспирант



Антон Александрович ТРУНОВ
Zilliqa Research
Сингапур

Инженер-исследователь 



Список литературы

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.


Рецензия

Для цитирования:


ГЛАДШТЕЙН В.П., МИХАЙЛОВСКИЙ Д.В., МОИСЕЕНКО Е.А., ТРУНОВ А.А. Механизированная теория структур событий: случай параллельной регистровой машины. Труды Института системного программирования РАН. 2021;33(3):143-154. https://doi.org/10.15514/ISPRAS-2021-33(3)-11

For citation:


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
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


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