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

• Students are required to attend all meetings.
• Each student (or pair of students, depending on the number of participants) will be assigned one subject to present in a 70-90 minute talk, based on a research paper or a chapter from a book.
• Students will prepare slides and/or handouts for their presentation (in English), and send them to me two weeks before the lecture. The material may be uploaded here and made publicly available.
• Students should discuss their presentations with me before they give it.
• Students are very welcome to use other sources besides the one that will be suggested. In particular, many good presentations (sometimes videos) of these topics are available online. You can learn from them, but, clearly, you should prepare your own presentation and lecture. All materials used should be clearly cited.
• The grade will be based on the understanding of the paper, quality and clarity of presentation in class and of the slides/handouts.

Schedule

Date	Speaker	Topic (some links require TAU proxy)
March 9	Ori Lahav	Introduction and guidelines [slides]
April 20	Harel	An axiomatic proof technique for parallel programs I Susan S. Owicki, David Gries Acta Informatica 6: 319-340, 1976 [1] [2]
May 11	Chen	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 18	Inbar	Wait-free synchronization Maurice Herlihy. ACM Trans. Program. Lang. Syst. 13, 1: 124-149, 1991 [1]
May 25	Roee	Well (and better) quasi-ordered transition systems Parosh Aziz Abdulla Bulletin of Symbolic Logic 16.4: 457-515, 2010 [1]
June 1	Hosni	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 8	Izzideen	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]