Concurrency Theory

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

Ori Lahav

Spring 2021

Wednesday 13-15

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 and interactive presentations, and effective demonstrations and examples.

Requirements and grading (for full details see first lecture)


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

Ori L.

Introduction and guidelines [slides]

March 10

Dvir, Mor

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

March 17

Dor, Topaz

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

April 7

Ricky, Shai

A Very Gentle Introduction to Multiparty Session Types
Nobuko Yoshida, Lorenzo Gher
Distributed Computing and Internet Technology. ICDCIT 2020. Springer.

April 21

Din, Noga

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

April 28

Tomer, Idan

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

May 5

Shalev, Barak

Separation logic: a logic for shared mutable data structures
John C. Reynolds
Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, Copenhagen, Denmark, 2002, pp. 55-74

May 12

Guy, Ido

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

May 19

Tom, May

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

May 26

Grisha, Yaniv

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

June 2


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

June 9

Israel, Shir

FastTrack: efficient and precise dynamic race detection
Cormac Flanagan, Stephen N. Freund
Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '09). ACM, New York, NY, USA, 121–133

June 16

Ori J.

Conflict-free Replicated Data Types: An Overview. 2018
Nuno Preguiça