Theoretical Computer Science

Lecture: Concurrency Theory

Sommer term 2023

News

13. März

Die Informationen auf dieser Seite sind noch vorläufig.

24. Mai

Aufgrund von Problemen mit der Website wird Aufgabenblatt 3 nicht gewertet.

13. Juni

Die Vorlesung am 13. Juni findet nicht statt. Sie wird während der Übung am 14. Juni nachgeholt.

Organisation

• Die Vorlesung wird von Prof. Dr. Roland Meyer gehalten. Die Übung wird von Anton Opaterny betreut.
• Die Termine der Veranstaltung sind
  • Vorlesung: Montag und Dienstag 16:45-18:15 Uhr (IZ358).
  • Übung: Mittwoch 13:15-14:45 Uhr (IZ358).
• Die Vorlesung startet am 17.04.2023.
• 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.

Prüfung

Die Prüfung wird am 01.09. in mündlicher Form stattfinden. Für einen Prüfungstermin bitte eine E-Mail an Anton Opaterny schreiben.

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.

• Übungsblatt 1
• Übungsblatt 2
• Übungsblatt 3
• Übungsblatt 4
• Übungsblatt 5
• Übungsblatt 6
• Übungsblatt 7

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.