Michail Kokologiannakis

• 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. This thesis presents solutions to both of these problems. First, it shows that the relevant metatheory of weak memory models can be effectively decided (sparing years of manual proof efforts), and presents Kater, a tool that can answer metatheoretic queries in a matter of seconds. Second, it presents GenMC, the first (and only) 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.
• Modelle mit schwacher Speicherkonsistenz erfassen die Ergebnisse nebenläufiger Programme, die in der Praxis auftreten und dennoch nicht durch Thread-Verschachtelungen erklärt werden können. Solche Ergebnisse stellen formale Methoden vor zwei großen Herausforderungen. Erstens ist die Feststellung, dass ein Speichermodell seine beabsichtigten Eigenschaften erfüllt (z. B. ein bestimmtes Kompilierungsschema unterstützt), äußerst fehleranfällig: Die meisten vorgeschlagenen Sprachmodelle waren anfangs fehlerhaft und erforderten mehrere Iterationen, um Solidität zu erreichen. Zweitens erschweren Modelle mit schwacher Speicherkonsistenz die Verifizierung nebenläufiger Programme erheblich, weshalb es keine skalierbaren Verifizierungstechniken außer einigen wenigen gibt, die auf sehr einfache Modelle abzielen. In dieser Arbeit präsentiere ich Lösungen für beide Probleme. Zunächst zeige ich, dass die relevante Metatheorie schwacher Speicherkonsistenzmodellen effektiv entschieden werden kann (wodurch jahrelanger manueller Beweisaufwand eingespart wird), und präsentiere Kater, ein Tool, das metatheoretische Fragen in Sekundenschnelle beantworten kann. Zweitens präsentiere ich GenMC, den ersten (und einzigen) skalierbaren zustandslosen Modellprüfer, der bei der Wahl des Speichermodells parametrisch ist und den bisherigen Stand der Technik oft um Größenordnungen verbessert.