Concurrency Theory

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

Ori Lahav

Spring 2019

Wednesday 10-12, Kaplun 324

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)
February 27


Introduction and guidelines [slides]
My research: weak memory concurrency in programming languages [slides]

March 13


Transition systems and behavioral equivalences
[Chapter 2 in Introduction to Concurrency Theory by Gorrieri&Versari]

March 20


Calculus of communicating systems (CCS)
[Chapter 3 in Introduction to Concurrency Theory by Gorrieri&Versari]

March 27


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

April 3


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

April 10


Resources, concurrency and local reasoning
Peter W. O’Hearn
Theoretical Computer Science 375, 1-3: 271-307, 2007
[1] [recent CACM article]

May 1


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

May 15


Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated
Hagit Attiya, Rachid Guerraoui, Danny Hendler, Petr Kuznetsov, Maged M. Michael, Martin Vechev
In Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL '11). ACM, New York, NY, USA, 487-498

May 22


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

May 29


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 5

No meeting

June 12


Robustness Against Release/Acquire Semantics
Ori Lahav, Roy Margalit
To appear in PLDI'19