Concurrency Theory

Undergraduate seminar 0368-3114
School of Computer Science
Tel Aviv University

Ori Lahav

Spring 2020

Monday 14-16, Dan David 204

In this seminar, we will explore different topics in concurrency theory, such as different formal models of concurrency (e.g., labeled transition systems and the calculus of communicating systems), correctness criteria for concurrent objects, logics for reasoning about concurrent programs, and verification and testing of concurrent systems.

The seminar will be held as a reading group with student presentations. We will emphasize formal mathematical definitions, clear presentations, and effective demonstrations and examples.

Requirements and grading


Date Speaker Topic (some links require TAU proxy)
March 9

Ori Lahav

Introduction and guidelines [slides]

April 20


An axiomatic proof technique for parallel programs I
Susan S. Owicki, David Gries
Acta Informatica 6: 319-340, 1976
[1] [2]

May 11


Linearizability: a correctness condition for concurrent objects
Maurice P. Herlihy, Jeannette M. Wing
ACM Trans. Program. Lang. Syst. 12, 3: 463-492, 1990

May 18


Wait-free synchronization
Maurice Herlihy.
ACM Trans. Program. Lang. Syst. 13, 1: 124-149, 1991

May 25


Well (and better) quasi-ordered transition systems
Parosh Aziz Abdulla
Bulletin of Symbolic Logic 16.4: 457-515, 2010

June 1


A load-buffer semantics for total store ordering
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
Logical Methods in Computer Science, January 23, 2018, Volume 14, Issue 1

June 8


The rely-guarantee method for verifying shared variable concurrent programs
Qiwen Xu, Willem-Paul de Roever, Jifeng He
Formal Aspects of Computing 9: 149-174, 1997