VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.
Exploiting and Reasoning about Concurrency
Last Updated: 2026-06-03 00:07:33
Abstract
A large percentage of modern applications is concurrent: from cache protocols, filesystems and operating systems, to networking,distributed systems and cloud services. Exploiting concurrency in these systems is highly non-trivial, as they often experiencebehaviors that cannot be expressed as plain process interleavings.
Objective
By the end of the course, students should (1) have a good working understanding of the concurrency semantics in various domains (e.g., shared-memory, distributed systems, non-volatile memory, filesystems), (2) be able to design applications that exploit concurrency effectively, and (3) understand a variety of concurrency reasoning principles techniques, and also apply them to concurrent programs.
Content
The course is organized in three parts. In the first part, we will describe common concurrency patterns that appear in various different domains (e.g., shared-memory programs, distributed protocols, RDMA), discuss defensive programming techniques that can be used to mitigate these effects along with proposed correctness criteria, and introduce automated tools that can be used to reason about program correctness. In the second part, we will formally introduce memory consistency models (i.e., models that describe the behaviors that can arise in concurrent systems), as well as memory-model properties that enable effective program reasoning. In the third part, we will discuss manual and automated reasoning techniques (e.g., program logics, model checking, testing) that can be used to prove program correctness.
Resources
Lecture Notes
Will be made available online.
Literature
Will be announced in the lectures.
General Information
- Language
- English
- Levels
- MSC , WBZ
- Frequency
- Yearly recurring
Examination
- Type
- session examination
- Mode
- written 180 minutes
- Aids
- One handwritten paper sheet (A4).
Registration & Places
- Max Places
- 40
Course Components
| Type | Title | Time & Place | Hours |
|---|---|---|---|
| lecture | Exploiting and Reasoning about Concurrency | No time listed | 2 h weekly |
| exercise | Exploiting and Reasoning about Concurrency | No time listed | 2 h weekly |
| independent project | Exploiting and Reasoning about Concurrency | No time listed | 1 h weekly |