AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI   Info

AG Audience

English

60 Minutes

Kaiserslautern

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.

Susanne Girard

+49 631 9303 9605

--email hidden

Yes

Saarbrücken

E1 5

029

Cisco Webex

passcode not visible

logged in users only