Scaling up relaxed memory verification with separation logics

Abstract

Reasoning about concurrency in a realistic, non-toy language like C/C++ or Rust, which encompasses many interweaving complex features, is very hard. Yet, realistic concurrency involves relaxed memory models, which are significantly harder to reason about than the simple, traditional concurrency model that is sequential consistency. To scale up verifications to realistic concurrency, we need a few ingredients: (1) strong but abstract reasoning principles so that we can avoid the too tedious details of the underlying concurrency model; (2) modular reasoning so that we can compose smaller verification results into larger ones; (3) reasoning extensibility so that we can derive new reasoning principles for both complex language features and algorithms without rebuilding our logic from scratch; and (4) machine-checked proofs so that we do not miss potential unsoundness in our verifications. With these ingredients in hand, a logic designer can flexibly accommodate the intricacy of relaxed memory features and the ingenuity of programmers who exploit those features. In this dissertation, I present how to develop strong, abstract, modular, extensible, and machine- checked separation logics for realistic relaxed memory concurrency in the Iris framework, using multiple layers of abstractions. I report two main applications of such logics: (i) the verification of the Rust type system with a relaxed memory model, where relaxed memory effects are encapsulated behind the safe interface of libraries and thus are not visible to clients, and (ii) the compositional specification and verification of relaxed memory libraries, in which relaxed memory effects are exposed to clients.

Programmverifikation von nebenläufige Programmen in einer realistischen Programmiersprache wie C/C++ oder Rust, die viele komplexe, miteinander verflochtene Sprachkonstrukte enthält, ist sehr schwierig. Realistische nebenläufige Programme basieren auf schwachen Speicherkonsistenzmodellen, in denen sich die Beweisführung im Vergleich zum traditionellen, sequentiellen Speicherkonsistenzmodell (SC) erheblich schwieriger gestaltet. Um die Verifikation solcher realistischen nebenläufigen Programme zu ermöglichen benötigen wir mehrere Voraussetzungen: (1) starke Beweisregeln die die mühsamen Details des zugrundeliegenden Speicherkonsistenzmodells abstrahieren, (2) modulare Beweistechniken die es erlauben, die Verifikation in kleinere, mundgerechte Beweise aufzuteilen, (3) eine erweiterbare Verifikationslogik, in der neue Beweistechniken hinzugefügt werden können, ohne die Korrektheit der gesamten Logik erneut beweisen zu müseen (4) maschinengeprüfte Beweise, die die Korrektheit der Logik und der durchgeführten Beweise garantiert. Mit diesen Voraussetzungen kann ein Logikdesigner die Komplexität des schwachen Speicherkonsistenzmodells und den Einfallsreichtum der Programmierer, die sich dessen Funktionenen zu Nutze machen, flexibel berücksichtigen. In dieser Dissertation stelle ich vor, wie man starke, abstrakte, modulare, erweiterbare und maschi- nengeprüfte Separationslogiken für realistische schwache Speicherkonsistenz in dem Framework Iris mit Hilfe von mehreren Abstraktionsebenen erstellen kann. Ich berichte über zwei Hauptanwendungen dieser Logiken: (i) die Verifikation des Typsystems von Rust auf Basis eines schwachen Speicherkonsistenzmod- ells, bei dem die Auswirkungen schwacher Speicherkonsistenz hinter der sicheren Programmschnittstelle abstrahiert und somit für Clients unsichtbar sind, und (ii) die modulare Spezifikation und Verifikation von Programmbibliotheken mit schwacher Speicherkonsistenz, bei denen die Auswirkungen schwacher Speicherkonsistenz für Clients sichtbar sind.