Lina4WM Linearizability Proofs for Weak Memory Models
Final Report Abstract
Das Projekt hat sich in seiner zweiten Förderphase mit dem Nachweis von Linearisierbarkeit von nebenläufigen Datenstrukturen beschäftigt. Der wesentliche Schwerpunkt lag dabei auf der Untersuchung des Einflusses von schwachen Speichermodellen auf die Korrektheit und auf der Entwicklung entsprechend passender Beweisverfahren. In dem Projekt sind dafür mehrere Forschungsarbeiten durchgeführt worden: • die Entwicklung einer zu schwachen Speichermodellen passenden Definition von Linearisierbarkeit, • der Entwurf sowohl mechanisierter Beweisverfahren fär Linearisierbarkeit mittels Simulation als auch eines Modelchecking-Ansatzes, und • der Nachweis der Korrektheit der Beweisverfahren selber. Mit Hilfe des Werkzeuges Weak2SC ist die Behandlung der schwachen Speichermodelle automatisiert möglich; die Simulationsbeweise selber verbleiben interaktiv. In einer Reihe von Fallstudien sind die Beweisverfahren erprobt worden. Dabei ist für zwei Algorithmen ein Nachweis der Linearisierbarkeit unter dem Speichermodell TSO erreicht worden, für die es bisher keinen entsprechenden formalen Korrektheitsbeweis gab.
Publications
-
Mechanized proofs of opacity: a comu parison of two techniques. Formal Aspects of Computing
John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
-
TSO to SC via Symbolic Execution. Haifa Verification Conference 2015: 104-119
Heike Wehrheim, Oleg Travkin
-
Verifying Opacity of a Transactional Mutex Lock. FM 2015: 161-177
John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
-
Proving Opacity of a Pessimistic STM. OPODIS 2016: 35:1-35:17
Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
-
Towards a Thread-Local Proof Technique for Starvation Freedom. IFM 2016: 193-209
Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
-
Verification of Concurrent Programs on Weak Memory Models. ICTAC 2016: 3-24
Oleg Travkin, Heike Wehrheim
