Verification of Parallel Programs

Verification of Parallel Programs (VPP)

Lecturer: Prof. Dr. Marie-Christine Jakobs

Typically, the course is offered each winter term.

Current Course Information

Self-study

Tu 2:00pm-3:00pm, Zoom, Question & Answering session

  • VPP in TUCaN
  • VPP material in Moodle

Course Content

The course deals with mostly automatic verification approaches for multi-threaded programs with shared memory. Topics of the course are:

  • Semantics of parallel programs, e.g., interleaving semantics
  • Static and dynamic approaches for data race detection
  • Techniques for deadlock detection
  • Verification of program properties (e.g., with sequentialization, bounded model checking, etc.)
  • Partial Order Reduction
  • Thread-modular verification

At the end of the course, students can name a number of techniques for the verification of parallel programs, especially in the area of data race and deadlock detection as well as for verification of safety properties. They should be able to explain the underlying formalisms of the techniques, to describe the work flow of the different techniques, and to apply the techniques on examples. Moreover, the students know the strengths and weaknesses of the techniques.

Recommended Previous Knowledge

Knowledge according to the first four bachelor terms in computer science that is ideally supplemented by knowledge of automatic software verification techniques for sequential programs as taught in the course Automatic Software Verification.

Literature

Program Semantics

  • K. R. Apt, F. S. de Boer, E.-R. Olderog: Verification of Sequential and Concurrent Programs. Springer 2009.

Data Race Detection

  • S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, T. E. Anderson: Eraser: A Dynamic Data Race Detector for Multi-Threaded Programs. SOSP 1997.
  • E. Poznianski, A. Schuster: Efficient On-the-Fly Data Race Detection in Multithreaded C++ Programs. IPDPS 2003.
  • C. Flanagan, S. N. Freund: FastTrack: efficient and precise dynamic race detection. PLDI 2009.

Deadlock Detection

  • Dawson R. Engler, Ken Ashcraft: RacerX: effective, static detection of race conditions and deadlocks. SOSP 2003.
  • Mayur Naik, Chang-Seo Park, Koushik Sen, David Gay: Effective static deadlock detection. ICSE 2009.

Sequentialization

  • Akash Lal, Thomas W. Reps: Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. CAV 2008.
  • Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato: Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. CAV 2014.

Bounded Model Checking

  • L. C. Cordeiro, B. Fischer: Verifying multi-threaded software using SMT-based context-bounded model checking. ICSE 2011

Thread-modular Verification

  • C. Flanagan, S. N. Freund, S. Qadeer: Thread-Modular Verification for Shared-Memory Programs. ESOP 2002

Partial Order Reduction

  • D. Peled: Partial-Order Reduction. Handbook of Model Checking 2018.
  • P. Godefroid, D. Pirottin: Refining Dependencies Improves Partial-Order Verification Methods (Extended Abstract). CAV 1993.
  • P. Godefroid, P. Wolper: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. Formal Methods in System Design 2(2) 1993.

Atomicity Checking

  • C. Flanagan, S. N. Freund: Atomizer: a dynamic atomicity checker for multithreaded programs. POPL 2004