Theoretical Computer Science

Lecture: Concurrency Theory

Winter term 2021/2022

News

06. Oktober

Die Veranstaltung beginnt mit einem Kick-Off Termin am 26. Oktober 11:30 Uhr im BBB.

26. Oktober

Der Kick-Off findet heute um 11:30 im BBB statt.

08. November

Die Übungsvideos werden mittwochs hochgeladen, da die Deadline der Aufgabenblätter dienstags ist.

27. Januar

Am Fr, 28. Januar um 10:00 Uhr, findet eine Fragestunde im BBB statt.

01. Februar

Für einen Prüfungstermin bitte eine E-Mail an Sören van der Wall schreiben. Prüfungstage sind der 23. und 24. Februar.

Organisation

• Die Vorlesung wird von Prof. Dr. Roland Meyer gehalten. Die Übung wird von Sören van der Wall betreut.
• Aufgrund der momentanen Situation und nach Absprache im Kickoff-Meeting, werden Videos der Vorlesung bzw. der Übung auf dieser Webseite online gestellt. Voraussichtlich werden Videos an folgenden Tagen veröffentlicht:
  • Vorlesung: Montags
  • Übung: Mittwochs
• Ein Präsenzlehre findet aufgrund der aktuellen Lage nicht statt. Bei Bedarf an Fragestunden (nach Machbarkeit in Präsenzlehre), wenden Sie sich bitte an Sören van der Wall.
• Die Hausaufgabenabgabe und Korrektur erfolgt online. Scannen Sie dazu ihre handschriftlichen Hausaufgaben ein oder erstellen Sie diese direkt in digitaler Form als .pdf (z.B. mit LateX), und senden Sie diese an Sören van der Wall per E-Mail. Falls Bedarf an einer physikalischen Abgabe (Abgabekästen im Informatikzentrum) besteht, wenden Sie sich bitte an Sören van der Wall.
• Als Kommunikationskanal dient Rocket Chat.
• Falls Sie die Vorlesung in den Bachelor einbringen möchten, klären Sie dies bitte mit dem Prüfungsamt ab.

Modul

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 findet mündlich über das BBB der Universität statt. Für einen Prüfungstermin bitte eine E-Mail an Sören van der Wall schreiben. Prüfungstage sind der 23. und 24. Februar.

Wichtig: während der Prüfung muss eine ständige Ton- und Videoübertragung stattfinden (Videokonferenz). Es werden weder Ton- noch Videoaufnahmen gespeichert. Falls Sie nicht entsprechend ausgestattet sind, so melden Sie sich bei Sören van der Wall. Falls Sie nicht mit der Ton- oder Videoübertragung einverstanden sind, so kann die Prüfung nicht durchgeführt werden! In diesem Falle können Sie sich wie üblich von der Prüfung abmelden.

Vorlesungsvideos

Die Vorlesungen werden jeden Montag als Videos hier angeboten.

• 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.

  Bitte benennen Sie Kapitel 5 um in ''Pointer-Programme 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. Bitte benennen Sie Kapitel 5 um in ''Pointer-Programme 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 (korrigiert)
• Übungsblatt 8 (korrigiert)
• Übungsblatt 9
• Übungsblatt 10

Die kleinen Übungen mit der Besprechung der Übungsblätter werden im Videoformat hier bereitgestellt.

• Übung 1: Video, Code.
• Übung 2: Video
• Übung 3: Video
• Übung 4: Video, Code.
• Übung 5: Vidieo
• Übung 6: Video
• Übung 7: Video
• Übung 8: Video
• Übung 9: Video
• Übung 10: Video

Kontaktieren Sie bei Fragen zu den Übungsblättern Sören van der Wall.

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.