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

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 a week before the lecture. The material may be uploaded here and made publicly available.
Students are welcome to discuss their presentations with me before they give it.
Students are welcome to use other sources besides the one that will be suggested. In particular, many good presentations (and sometimes videos) of these topics are available online. You may want to 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)
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		No meeting
June 12	Ori	Robustness Against Release/Acquire Semantics Ori Lahav, Roy Margalit To appear in PLDI'19 [1]