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

Schedule

Date Speaker Topic (some links require TAU proxy)
February 27

Ori

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

March 13

Tomer

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

March 20

Maxim

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

March 27

Inbar

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

April 3

Karam

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
[1]

April 10

Muhammed

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

May 1

Ron

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

May 15

Yuval

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
[1]

May 22

Shahar

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

May 29

Roee

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
[1]

June 5

Alon

Conflict-free replicated data types
Marc Shapiro, Nuno Preguiça, Carlos Baquero, Marek Zawirski
[1] [2]

June 12

TBD