Concurrency Theory

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

Ori Lahav

Spring 2023

Wednesday 13-15

In this seminar, we will explore different topics in concurrency theory, such as different formal models of concurrency, correctness criteria for concurrent objects, logics for reasoning about concurrent programs, and verification and dynamic 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) will be assigned one subject to present in a 90 minute talk, based on research papers or chapters 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 22	Ori	Introduction and guidelines [slides]
April 19	Tal, Nittai	Transition systems and behavioral equivalences [Chapter 2 in Introduction to Concurrency Theory by Gorrieri&Versari]
May 10	Roy, Bar	An axiomatic proof technique for parallel programs I Susan S. Owicki, David Gries Acta Informatica 6: 319-340, 1976 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 17	Yoav, Razi	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 Dynamic race prediction in linear time Dileep Kini, Umang Mathur, Mahesh Viswanathan Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '17). ACM, New York, NY, USA, 157–170
June 7	Itay, Yonatan	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 Resources, concurrency and local reasoning Peter W. O’Hearn Theoretical Computer Science 375, 1-3: 271-307, 2007 Separation logic Peter O'Hearn Communications of the ACM, 62(2), pp.86–95, 2019
June 14	Ahmad, Yousef	Linearizability: a correctness condition for concurrent objects Maurice P. Herlihy, Jeannette M. Wing ACM Trans. Program. Lang. Syst. 12, 3: 463-492, 1990 A Linearizability-based Hierarchy for Concurrent Specifications Armando Castañeda, Sergio Rajsbaum, Michel Raynal Communications of the ACM, 66(1), pp.86-97, 2023
June 28	Somaya, Tamer	Foundations of the C++ Concurrency Memory Model Hans-J. Boehm, Sarita V. Adve Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '08) ACM, New York, NY, USA, 68–78 Memory models: a case for rethinking parallel languages and hardware Sarita V. Adve, Hans-J. Boehm Communications of the ACM, 53(8), pp.90-101, 2010 You don't know jack about shared variables or memory models Hans-J. Boehm, Sarita V. Adve Communications of the ACM, 55(2), pp.48-54, 2012