Nebenläufigkeitstheorie SS24

News

25. März  - Die Informationen auf dieser Seite sind noch vorläufig.

Organisation

• Die Vorlesung wird von Prof. Dr. Roland Meyer gehalten.
• Vorlesung: Montag und Dienstag 16:45-18:15 Uhr (IZ 358).
• Übung: Mittwoch 13:15-14:45 Uhr (IZ 358).
• Die Vorlesung startet am 08.04.2024.
• Falls Sie die Vorlesung in den Bachelor einbringen möchten, klären Sie dies bitte mit dem Prüfungsamt ab.

Modul

Es handelt sich um eine (4+2) Veranstaltung. Um das Modul erfolgreich abzuschließen, sind zwei Leistungen zu erbringen:

• Prüfungsleistung: Zu erbringen durch Bestehen einer mündlichen Abschlussprüfung zu Beginn des vorlesungsfreien Zeitraums. Das genaue Prüfungsdatum wird zeitnah bekannt gegeben.
• Studienleistung: Zu erbringen durch das erfolgreiche Bearbeiten von mindestens 50% der Übungsaufgaben.

Vorlesungsvideos

Vorlesungsvideos vergangener Semester:

• Woche 1: Einleitung, Treibers-Stack in C++, Programmiertechniken, ABA und Segfaults, Speicherverwaltung in C++, ABA in C++.
• Woche 2: W-- Syntax und Small-Step-Semantik, W-- Big-Step-Semantik, Einführung in die Hoare-Logik.
• Woche 3: Hoare-Logik an einem Beispiel, Korrektheit und Vollständigkeit, Verification-Conditions. 
• Woche 4: Verification-Conditions in C++, Einführung in die Separation-Logik, Programmiersprache W und Separation-Logik-Assertions.
• Woche 5: Assertions (cont.),  Assertions (fin), Separation-Logik. 
• Woche 6: Separation-Logik (fin),  Infer-Tool. 
• Woche 7: Concurrent-Separation-Logik,  Beweisskizzen und Ownership-Transfer. 
• Woche 8: Soundness von CSL,  Rely-Guarantee. 
• Woche 9: RGSep 1, RGSep 2,  RGSep 3. 
• Woche 10: RGSep 4, Lock-Coupling-List 1,  Lock-Coupling-List in C++, Lock-Coupling-List 2, Lock-Coupling-List Beweis, Lock-Coupling-List 3. Linearisierbarkeit 1. Danke an Sebastian Wolff!
• Woche 11: Linearisierbarkeit 2, SC und TSO,  Robustheit.
• Woche 12: Anarchische Semantik, Analytische Semantik und CAT. 

Vorlesungsnotizen

Handschriftliche Notizen der Vorlesung:

• Woche 1: Einleitung, Treiber's stack (.cpp), Programmiertechniken, ABA und Segfaults, Speicherverwaltung (.cpp), ABA in Treibers-Stack (.cpp). 
• Woche 2: W-- Syntax und Small-Step-Semantik,  W-- Big-Step-Semantik, Einführung in die Hoare-Logik.
• Woche 3: Hoare-Logik an einem Beispiel, Korrektheit und Vollständigkeit, Verification-Conditions. 
• Woche 4: Verification-Conditions (.cpp), Einführung in die Separation-Logik,  Programmiersprache W und Separation-Logik-Assertions.
• Woche 5: Assertions (cont.), Assertions (fin),  Separation-Logik. 
• Woche 6: Separation-Logik (fin), Infer-Tool. 
• Woche 7: Concurrent-Separation-Logik,  Beweisskizzen und Ownership-Transfer. 
• Woche 8: Soundness von CSL,  Rely-Guarantee. 
• Woche 9: RGSep 1,  RGSep 2, RGSep 3,  Korrektur (com). 
• Woche 10: RGSep 4,  Lock-Coupling-List, Lock-Coupling-List (.cpp),  Lock-Coupling-List (.wlang),  Lock-Coupling-List (Beweis), Linearisierbarkeit 1. Danke an Sebastian Wolff!
• Woche 11: Linearisierbarkeit 2, SC und TSO, Robustheit, Dekker (.cpp). 
• Woche 12: Anarchische Semantik, Analytische Semantik, CAT.

Übungsblätter

Die Übungsblätter werden während des Semesters hier zur Verfügung gestellt.

Literature

• Maurice Herlihy and Nir Shavit. 2012. The Art of Multiprocessor Programming, Revised Reprint (1st. ed.). Morgan Kaufmann Publishers Inc., San Francisco, CA, USA. ISBN: 978-0-12-397337-5

  Contains interesting information about the theory and practice of parallel programming.

• Glynn Winskel. 1993. The Formal Semantics of Programming Languages: An Introduction. MIT Press. ISBN: 978-0-262-23169-5

  Our presentation of programming languages is based on this. 

• Aaron R. Bradley and Zohar Manna. 2007. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer. ISBN: 978-3-540-74112-1

  Our presentation of verification conditions is based on this text.

• Maged M. Michael and Michael L. Scott. 1996. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In PODC. ACM. DOI: 10.1145/248052.248106
• Simon Doherty, Lindsay Groves, Victor Luchangco, and Mark Moir. 2004. Formal Verification of a Practical Lock-Free Queue Algorithm. In FORTE. LNCS vol. 3235. Springer. DOI: 10.1007/978-3-540-30232-2_7.
• John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS. IEEE. 55-74.

  Our presentation of separation logic is based on this.

• Samin S. Ishtiaq, Peter W. O'Hearn. 2001. BI as an Assertion Language for Mutable Data Structures. In POPL. ACM. 14-26.

  Here you find the axioms for heap-manipulating commands + the statement of completeness as weakest preconditions. 

• Peter W. O'Hearn, John C. Reynolds, Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. In CSL. Springer. 1-19.

  The ''Small Axioms''.

• Hongseok Yang and Peter W. O'Hearn. 2002. A Semantic Basis for Local Reasoning. In FoSSaCS. Springer. 402-416.

  Soundness, Completeness, and Discussion of the Frame-Rule. Contains the semantic lemma about our programming language.

• Hongseok Yang. 2001. Local Reasoning for Stateful Programs. PhD Thesis University of Illinois at Urbana−Champaign. 

  Completeness of the Frame-Rule and foundations of separation logic.

• Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang. 2009. Compositional shape analysis by means of bi-abduction. In POPL. 289-300.

  Our presentation of Infer is based on this paper. 

• Viktor Vafeiadis. 2011. Concurrent Separation Logic and Operational Semantics. In MFPS. ENTCS 276: 335-351.

  Our presentation of concurrent separation logic is based on this paper. 

• Peter W. O'Hearn. 2007. Resources, concurrency, and local reasoning. TCS 375(1-3): 271-307. 

  On concurrent separation logic.

• Viktor Vafeiadis. 2008. Modular fine-grained concurrency verification. PhD Thesis University of Cambridge.

  Our presentation of RGSep is taken from this thesis. It also contains the lock-coupling list.

• Viktor Vafeiadis, Matthew J. Parkinson. 2007. A Marriage of Rely/Guarantee and Separation Logic. In CONCUR. 256-271. 

  The RGSep paper.

• Ahmed Bouajjani, Roland Meyer, Eike Möhlmann. 2011. Deciding Robustness against Total Store Ordering. In ICALP. 428-440. 

  The locality principle.

• Ahmed Bouajjani, Egor Derevenetc, Roland Meyer. 2013. Checking and Enforcing Robustness against TSO. In ESOP. 533-553. 

  From robustness against TSO to reachability under SC.