VaST - Validation of Software Transactional Memory

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

• Final Report Year: 2021

Final Report Abstract

Software transactional memory (STM) algorithms are designed for the purpose of supporting software developers in parallel programming. STMs provide a high-level synchronisation mechanism for parallel access to shared state. Today, numerous proposals for such algorithms exist. They typically allow for a high degree of concurrency while guaranteeing some form of serializability very much alike that of database transactions. The form of serializability most often employed for STMs is opacity. The objective of the project was the development of validation methods for checking a given Software Transactional Memory algorithm for opacity. These methods comprise model checking and testing techniques for a set of fixed transactions as well as mechanized verification of algorithms based on refinement using theorem provers KIV and Isabelle. The techniques have been applied to a number of STMs including NORec, FastLane, TML and RingSTM. A central result of the project furthermore concerns the decidability and complexity of opacity itself which has been shown to be NP-complete for the membership and decidable for the correctness problem.

Publications

• Value-Based or Conflict-Based? Opacity Definitions for STMs. ICTAC 2017: 118-135
  Jürgen König, Heike Wehrheim
  
• FastLane Is Opaque - a Case Study in Mechanized Proofs of Opacity. SEFM 2018: 105-120
  Gerhard Schellhorn, Monika Wedel, Oleg Travkin, Jürgen König, Heike Wehrheim
  
• Mechanized proofs of opacity: a comparison of two techniques. Formal Aspects Comput. 30(5): 597-625 (2018)
  John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim
  
• Data Independence for Software Transactional Memory. NFM 2019: 263-279
  Jürgen König, Heike Wehrheim
  
• On the (Non-) Applicability of a Small Model Theorem to Model Checking STMs. 2021
  Heike Wehrheim
  
• On the Correctness Problem for Serializability, ICTAC 2021: 47-64
  Jürgen König, Heike Wehrheim