Lina4WM Linearizability Proofs for Weak Memory Models

• Applicant: Professorin Dr. Heike Wehrheim
• Subject Area: Software Engineering and Programming Languages
• Term: from 2010 to 2018
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 163003744

• Final Report Year: 2018

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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at 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
  (See online at https://doi.org/10.1007/978-3-319-46750-4_1)