Automated Reasoning under Weak Memory Consistency
Michalis Kokologiannakis
Max Planck Institute for Software Systems
14 Dec 2023, 4:00 pm - 5:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Student Defense Talks - Thesis Defense
Weak memory consistency models capture the outcomes of concurrent programs that
appear in practice and yet cannot be explained by thread interleavings. Such
outcomes pose two major challenges to formal methods. First, establishing that
a memory model satisfies its intended properties (e.g., supports a certain
compilation scheme) is extremely error-prone: most proposed language models
were initially broken and required multiple iterations to achieve soundness.
Second, weak memory models make verification of concurrent programs much
harder, as a result of which there are no scalable verification techniques
beyond a few that target very simple models. ...
Weak memory consistency models capture the outcomes of concurrent programs that
appear in practice and yet cannot be explained by thread interleavings. Such
outcomes pose two major challenges to formal methods. First, establishing that
a memory model satisfies its intended properties (e.g., supports a certain
compilation scheme) is extremely error-prone: most proposed language models
were initially broken and required multiple iterations to achieve soundness.
Second, weak memory models make verification of concurrent programs much
harder, as a result of which there are no scalable verification techniques
beyond a few that target very simple models.
In this talk, I present solutions to both of these problems. First, I show that the relevant meta-theory of weak memory models can be effectively decided (sparing years of manual proof efforts), and present Kater, a tool that can answer such queries in a matter of seconds. Second, I present GenMC, the first scalable stateless model checker that is parametric in the choice of the memory model, often improving the prior state of the art by orders of magnitude.
Read more
In this talk, I present solutions to both of these problems. First, I show that the relevant meta-theory of weak memory models can be effectively decided (sparing years of manual proof efforts), and present Kater, a tool that can answer such queries in a matter of seconds. Second, I present GenMC, the first scalable stateless model checker that is parametric in the choice of the memory model, often improving the prior state of the art by orders of magnitude.