Verifikation paralleler Programme (VPP)
Dozentin: Prof. Dr. Marie-Christine Jakobs
Der Kurs wird nicht mehr angeboten. Das letzte Mal wurde der Kurs im Wintersemester 2022/23 gehalten.
Lerninhalte und -ziele
Die Veranstaltung befasst sich mit überwiegend automatischen Techniken zur Verifikation von parallelen Programmen, insbesondere multi-threaded Programmen mit gemeinsamen Speicher. Die Veranstaltung behandelt dabei folgende Themenbereiche:
- Semantik von parallelen Programmen (z.B. Interleaving-Semantik)
- Statische und dynamische Techniken zur Erkennung von Data Races
- Techniken der Deadlockanalyse
- Analyse von Programmeigenschaften (z.B. mittels Sequentialisierung, Bounded Model Checking, etc.)
- Partial Order Reduction
- Thread-modulare Verifikation
Nach erfolgreicher Teilnahme an der Veranstaltung können die Studierenden Verfahren zur Verifikation von parallelen Programmen, insbesondere Verfahren zur Analyse von Data Races, Deadlocks und Sicherheitseigenschaften (Safety) benennen. Sie können die den Verfahren zugrunde liegenden Formalismen wiedergeben, die Funktionsweise der Verfahren beschreiben und die Verfahren auf Beispielen anwenden. Außerdem können die Studierenden die Stärken und Schwächen der Verfahren beurteilen.
Vorkenntnisse
Informatikkenntnisse entsprechend der ersten vier Semester des Bachelorstudiengangs Informatik werden erwartet. Vorteilhaft, aber nicht erforderlich ist der Besuch der Veranstaltung Automatische Software Verifikation .
Literaturempfehlungen
Programmsemantik
- K. R. Apt, F. S. de Boer, E.-R. Olderog: Verification of Sequential and Concurrent Programs. Springer 2009.
Data Race Detektion
- 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 Detektion
- 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.
Sequentialisierung
- 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 modulare Verifikation
- 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 Prüfung
- C. Flanagan, S. N. Freund: Atomizer: a dynamic atomicity checker for multithreaded programs. POPL 2004
