Lina4WM Linearizierbarkeitsbeweise für schwache Speichermodelle

• Antragstellerin: Professorin Dr. Heike Wehrheim
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2010 bis 2018
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 163003744

• Erstellungsjahr: 2018

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
  
• 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