Theoretical Computer Science

Lecture: Concurrency Theory

Winter term 2020/21

News

März 08

Die Prüfung findet in Form einer mündlichen Onlineprüfung statt. Dazu ist eine Videokonferenz (Ton- und Bildübertragung) verpflichtend. Für weitere Information siehe unten.

Februar 25

Registrieren Sie sich bie Sebastian Wolff, um an den Prüfungen teilzunehmen. Für weitere Information siehe unten.

Februar 12

Die Prüfungen werden voraussichtlich in der Woche vom 22.03-26.03 (KW12) stattfinden. Genauere Informationen zur Form, Durchführung und Terminvergabe folgen in Kürze.

Dezember 01

Krankheitsbedingt entfallen in dieser Woche leider die Vorlesungen.

November 25

Eine korrigierte Version des vierten Übungsblattes ist online. In Aufgabe 4.3a ist zu zeigen: A*emp impliziert A.

November 22

Das neue Übungsblatt ist online.

November 20

Die Prüfung wird mündlich stattfinden.

November 20

Der Code von Michael&Scott's queue zum ersten Übungsblatt wurde ergänzt.

November 05

Die Vorlesungsunterlagen werden teils neu erstellt, teils überarbeitet. Es mag vorkommen, dass sie erst am Donnerstag online erscheinen. Wir entschuldigen uns für eventuelle Verspätungen.

October 20

Die Vorlesung und Übung wird in digitaler Form angeboten. Ein Chat zur Veranstaltung findet sich hier.

October 13

Es wird eine Vorbesprechung am 20.10 um 11:00 Uhr zur Organisation dieser Veranstaltung geben.

Organisation

• Die Vorlesung wird von Prof. Dr. Roland Meyer gehalten. Die Übung wird von Sebastian Wolff betreut.
• Eintrag im Vorlesungsverzeichnis.
• 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: Dienstags und Mittwochs
  • Übung: Mittwochs
• Ein Präsenzlehre findet vorerst nicht statt. Bei Bedarf an Fragestunden (nach Machbarkeit in Präsenzlehre), wenden Sie sich bitte an Sebastian Wolff.
• 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 Sebastian Wolff per E-Mail. Falls Bedarf an einer physikalischen Abgabe (Abgabekästen im Informatikzentrum) besteht, wenden Sie sich bitte an Sebastian Wolff.
• Als Kommunikationskanal dient https://messenger.tu-bs.de/group/concurrency2021. Um dem Chat beizutreten benötigen Sie einen Invite-Link; um diesen zu erhalten wenden Sie sich bitte an Sebastian Wolff.
• 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üfungen finden zwischen Montag, dem 22.03, und Mittwoch, dem 24.03, statt. Es handelt sich dabei um mündliche Prüfungen, die nach aktuellem Stand online durchgeführt werden. Wer an der Prüfung teilnehmen möchte, muss sich dazu bei Sebastian Wolff registrieren. Schreiben Sie dazu bitte bis zum 05.03 eine kurze Mail mit Ihrem Namen und Ihrer Matrikelnummer sowie ggf. terminlichen Konflikten im obigen Zeitraum. Wir werden die registrierten Personen dann auf Prüfungstermine verteilen, welche Ihnen zusammen mit weiteren Informationen zum Ablauf der Prüfung zeitnah mitgeteilt werden.

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 umgehend bei Sebastian Wolff. 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.

Bei Fragen wenden Sie sich bitte an Sebastian Wolff.

Vorlesungsvideos

Die Vorlesungen werden 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 7: Separation-Logik (fin), Infer-Tool.
• Woche 8: Concurrent-Separation-Logik, Beweisskizzen und Ownership-Transfer.
• Woche 9: Soundness von CSL, Rely-Guarantee.
• Woche 10: RGSep 1, RGSep 2, RGSep 3.
• Woche 11: 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.
• Woche 12: Linearisierbarkeit 2, SC und TSO, Robustheit.
• Woche 13: 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 7: Separation-Logik (fin), Infer-Tool.
• Woche 8: Concurrent-Separation-Logik, Beweisskizzen und Ownership-Transfer.
• Woche 9: Soundness von CSL, Rely-Guarantee.
• Woche 10: RGSep 1, RGSep 2, RGSep 3, Korrektur (com).
• Woche 11: RGSep 4, Lock-Coupling-List, Lock-Coupling-List (.cpp), Lock-Coupling-List (.wlang), Lock-Coupling-List (Beweis), Linearisierbarkeit 1.
• Woche 12: Linearisierbarkeit 2, SC und TSO, Robustheit, Dekker (.cpp).
• Woche 13: 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 (korrigierte Version)
• Übungsblatt 5
• Übungsblatt 6
• Übungsblatt 7 (korrigierte Version)
• Übungsblatt 8
• Übungsblatt 9
• Übungsblatt 10

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

• Übung 1: Video, Michael&Scott's queue (.cpp), Beispiel zum Konsistenz-Check, Beispiel zum ABA Problem
• Übung 2: Video, Notizen
• Übung 3: Video, Notizen
• Übung 4: Video, Notizen, VC Code (.cpp)
• Übung 5: Video, Notizen
• Übung 6: Video, Notizen
• Übung 7: Video, Notizen (korrigierte Version)
• Übung 8: Video, Notizen
• Übung 9: Video, Notizen
• Übung 10: Video, Notizen

Kontaktieren Sie bei Fragen zu den Übungsblättern Sebastian Wolff.

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.