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

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

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 me...

Full description

Bibliographic Details
Main Authors: Evgenii A. Moiseenko, Vladimir P. Gladstein, Anton V. Podkopaev, Dmitry V. Koznov
Format: Article
Language:English
Published: Saint Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO University) 2022-06-01
Series:Naučno-tehničeskij Vestnik Informacionnyh Tehnologij, Mehaniki i Optiki
Subjects:
memory models
pomset languages
formal semantics
interactive theorem proving
Online Access:https://ntv.ifmo.ru/file/article/21262.pdf

Internet

https://ntv.ifmo.ru/file/article/21262.pdf

Similar Items