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)

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 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. [1]
April 21	Din, Noga	An axiomatic proof technique for parallel programs I Susan S. Owicki, David Gries Acta Informatica 6: 319-340, 1976 [1]
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 [1]
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 [1]
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 [1]
May 26	Grisha, Yaniv	Wait-free synchronization Maurice Herlihy. ACM Trans. Program. Lang. Syst. 13, 1: 124-149, 1991 [1]
June 2	Yoav	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]
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 [1]
June 16	Ori J.	Conflict-free Replicated Data Types: An Overview. 2018 Nuno Preguiça [1]