Nebenläufigkeitstheorie SS25

Prüfungstermine

Die Prüfungen zur Vorlesung Nebenläufigkeitstheorie sollen am 15.09.2025 und 16.09.2025 stattfinden.
Um einen Prüfungstermin zu vereinbaren, schreiben Sie eine Mail (ggf. mit Ihren zeitlichen Einschränkungen) an Natalia Gacek.

Das genaue Datum und die Uhrzeit Ihrer Prüfung werden Ihnen dann zu einem späteren Zeitpunkt mitgeteilt.

Bitte beachten Sie, dass Sie sich unabhängig von der Vereinbarung eines Prüfungstermins beim Prüfungsamt/ im TUconnect-Portal für die Prüfung anmelden müssen!

News

30. April - Die meisten Vorlesungsvideos sind wieder verfügbar!

15. April - Die erste große Übung findet am 24.04. statt. Sollten Sie sich nach den ersten beiden Vorlesungen noch zur Übung anmelden wollen, schreiben Sie eine Mail an n.gacek(at)tu-braunschweig.de.

20. Februar  - 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: Donnerstag 15:00-16:30 Uhr (IZ 358).
  • Falls Sie die Vorlesung in den Bachelor einbringen möchten, klären Sie dies bitte mit dem Prüfungsamt ab.
  • Die Vorlesung beginnt am 14.04.

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.

Übungsblätter

Literatur

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

Letzte Aktualisierung: 25.06.2025