The Laboratory carries out weekly global Seminar, where both classic and recent accomplishments in the area of programming languages and tools are discussed. The seminar is open to everyone – join the mailing list for announcements.
Attending the seminar is mandatory for Lab faculty and post-graduates, and highly recommended for all students. In the autumn semester of 2019, the seminar takes place on Mondays at 17:15, auditorium 3248, at the Faculty of Mathematics and Mechanics at SPbSU.
2020Model Checking under Weak Memory Models
Model checking is a method of automatic formal verification. Most of the existing model checkers are either do not consider effects arising due to a weak memory model or assume some fixed memory model. Among these tools stands out the GenMC model checker which is parametric in the choice of the memory model. GenMC covers a wide class of models (among them are RC11 and IMM). Yet the most challenging ones (Promising, Weakestmo) are not yet supported, since in these models some properties assumed by GenMC are no longer valid. Besides that, the models itself are too weak, so the problem of model checking seems intractable in practice for them.
In this talk, an overview of the GenMC algorithm and its assumptions about the memory model will be given. Also, a modified version of the Weakestmo model will be proposed. The proposed fix makes the model checking problem easier and at the same time preserves all of the desired properties of the model. Finally, a prototype of the modified GenMC algorithm that supports the Weakestmo model will be presented.
Kokologiannakis, Michalis, Azalea Raad, and Viktor Vafeiadis. "Model checking for weakly consistent libraries." Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2019.
Kokologiannakis, Michalis, and Viktor Vafeiadis. "HMC: Model Checking for Hardware Memory Models." Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems. 2020.