Concurrency, Theory & Practice – Summer 2024

• Lecturer: Prof. Dr. Peter Thiemann
• Assistant: Dr. Bas van den Heuvel

Course planning

We plan to discuss the following topics (subject to change):

• Go: language overview
• Go: concurrency
• Dynamic data race prediction
• Dynamic deadlock prediction
• Futures
• Model checking: a short introduction
• Low-level concurrent data structures
• The pi-calculus
• Session types

We have one lecture and one tutorial each week:

• Lecture: Wednesday, 4:15 pm - 5:45 pm, SR 00 031 (G.-Köhler-Allee 051)
• Tutorials: Friday, 12:15 pm - 1:45 pm, R 04 007 Videokonferenz (G.-Köhler-Allee 106)

Note that some tutorials will be held online, so keep an eye on the schedule.

Examination and Studienleistung

To pass the course, you need a passing grade on the written exam. Additionally, you need to pass the Studienleisting, which entails actively participating in the Ilias quizzes.

Announcements

2024-09-16:

• We will hold an exam review session:

  • on Tuesday 24.09 from 14:00 to 16:00,
  • at Werthmannstr. 4 in the same room as the exam,
  • you will need your Ilias login credentials.

  Let Bas know if this doesn’t work for you, so we can find a different solution.

2024-08-14:

• The exam is Tuesday 20 August, 10-12 at Werthmannstr. 4.
• Make sure you know the credentials (username and password) for your uni account.
• Besides the Ilias exam, you will have access to Notepad++. On request, we can provide paper for note-taking, but all material will have to remain in the room after the exam.
• There is no Studienleistung; a passing grade on the exam will award you your ECTS.
• The last tutorial recording only has audio. To follow along, use the material here.
• We will use the following syntax for the exam (will be provided during the exam as well):
  • LTL, given formulas 𝜑 and 𝜓:
    • forever 𝜑: □𝜑 -> []𝜑 (left and right square brackets)
    • eventually 𝜑: ⬦𝜑 -> <>𝜑 (less than and greater than)
    • next 𝜑: 🞅𝜑 -> X𝜑 (capital letter X)
    • 𝜑 until 𝜓: 𝜑 ∪ 𝜓 -> 𝜑 U 𝜓 (capital letter U)
    • 𝜑 and 𝜓: 𝜑 ∧ 𝜓 -> 𝜑 ^ 𝜓 (hat symbol)
    • 𝜑 or 𝜓: 𝜑 ∨ 𝜓 -> 𝜑 v 𝜓 (small letter v)
    • 𝜑 implies 𝜓: 𝜑 → 𝜓 -> 𝜑 -> 𝜓 (dash and greater than)
    • not 𝜑: ¬𝜑 -> ~𝜑 (tilde)
    • p and q are atomic propositions
  • Traces:
    • nodes: ( p,q ) (parentheses, with comma-separated list of atomic propositions satisfied)
    • edge: ---> (dashes followed by greater than, or different symbols depending on direction)
    • initial node -> ( .. )
  • Pi-calculus:
    • send y over x: ̅x〈y〉 -> x<y> (no overline, less than and greater than)
    • receive y over x: x(y) -> x(y) (left and right parentheses)
    • unobservable: 𝜏 -> tau (word tau)
    • choice: P + Q -> P + Q (plus)
    • parallel: P | Q -> P | Q (vertical bar)
    • restriction: (𝜈x)P -> (nu x)P (word nu and space)
    • replication: !P -> !P (exclamation mark)
    • substitution: P [x := y] -> P [x := y] (square brackets, colon and equals)
  • Session types:
    • process syntax as above, except restriction: (𝜈xy)P -> (nu x y) (space also between names)
    • select: x ◃ j -> x < j (less than)
    • branch: x ▹ {…} -> x > {...} (greater than and curly brackets)
    • types as usual, except select: ⊕{…} -> +{...} (plus symbol)
    • duality: ̅T -> dual(T) (word dual and parentheses)
    • typing judgments: Γ ⊦ P -> Gamma |- P (capitalized word Gamma, vertical bar and dash)
    • context split: Γ₁ ○ Γ₂ -> Gamma1 o Gamma2 (small letter o)

2024-08-05:

Trace examples now available here.

2024-07-26:

Exam format:

• Exam pool, through Ilias.
• 120 minutes, ~10 questions.
• A single handwritten two-sided A4 cheat sheet is allowed.

Exam topics and additional study pointers:

• Go concurrency here here here.
• Concurrency traces to practice data race and deadlock detection will be provided soon.
• For Futures, try to recreate the examples from the slides.
• There will be no exam questions about transition systems.
• Traces and LTL here.
• Pi-calculus and session types study the tutorial and examples of Sepi.
• Further material may be found in other concurrency lectures, such as here and here.

2024-07-19:

1. Unfortunately, the recording software failed on me, so the recording of today’s tutorial has only audio. My apologies.
2. Early next week, there will be additional study material available here.

2024-07-03:

After today’s lecture, the Ilias quiz on the pi-calculus will be available. Other than usual, you only have until next Friday (July 5) at noon to finish the quiz. This way, we can discuss the exercises during the tutorial.

2024-06-28:

1. Please check today’s tutorial for clarifications on notation.
2. Next Ilias quiz will be released after next Wednesday’s lecture.

2024-06-20:

1. A new quiz is available on Ilias, on transition systems and LTL.
2. The deadline of this quiz is Friday June 28 at noon (12:00 CEST).
3. There is no tutorial this Friday (June 21).
4. Next week’s tutorial (Friday June 28) will be online.

Schedule

If the schedule says “Tutorial”, there is a tutorial. Only if the schedule says “No tutorial” will there be no tutorial.

Additional consulting

Besides tutorials, Bas will be available for consulting on Tuesdays 10-11 (with the exception of 2024-04-30, 2024-05-28, 2024-06-18, 2024-06-25). If you cannot make it and have urgent questions, email Bas and ask the question directly or make an appointment.