Lina4WM Linearizierbarkeitsbeweise für schwache Speichermodelle
Zusammenfassung der Projektergebnisse
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.
Projektbezogene Publikationen (Auswahl)
- 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
(Siehe online unter https://doi.org/10.1007/s00165-017-0433-3) - TSO to SC via Symbolic Execution. Haifa Verification Conference 2015: 104-119
Heike Wehrheim, Oleg Travkin
(Siehe online unter https://doi.org/10.1007/978-3-319-26287-1_7) - Verifying Opacity of a Transactional Mutex Lock. FM 2015: 161-177
John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
(Siehe online unter https://doi.org/10.1007/978-3-319-19249-9_11) - Proving Opacity of a Pessimistic STM. OPODIS 2016: 35:1-35:17
Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim
(Siehe online unter https://dx.doi.org/10.4230/LIPIcs.OPODIS.2016.35) - Towards a Thread-Local Proof Technique for Starvation Freedom. IFM 2016: 193-209
Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
(Siehe online unter https://doi.org/10.1007/978-3-319-33693-0_13) - Verification of Concurrent Programs on Weak Memory Models. ICTAC 2016: 3-24
Oleg Travkin, Heike Wehrheim
(Siehe online unter https://doi.org/10.1007/978-3-319-46750-4_1)
