Weakly Consistent Concurrency

Graduate seminar 0368-4192
School of Computer Science
Tel Aviv University

Ori Lahav

Spring 2018

Wednesday 10-12, Schreiber 209

Modern concurrent systems (e.g., multi-core processors and distributed data stores) exhibit fundamental trade-offs between the consistency guarantees they provide to their users and the amount of parallelism they allow. Typically, ensuring strong consistency (that is, maintaining an illusion of a centralized system) severely impacts performance and availability. Thus, system developers resort to "weakly consistent systems", where some behaviors of the system cannot be understood in terms of a centralized system. Formalizing the guarantees provided by such systems and reasoning about their behaviors are highly challenging.

In this seminar, we will explore (some of) the rich landscape of weak consistency, including relaxed memory models in multi-core processors and modern high-level programming languages, correctness criteria for distributed implementations of data structures, and different consistency levels of database transactions.

The seminar will be held as a reading group with student presentations. We will read and discuss classical and recent research papers, and emphasize formal mathematical definitions and clear presentations.

Requirements and grading


Date Speaker Topic (some links require TAU proxy)
March 7


Introduction: Weakly consistent concurrency

March 14


Introduction: C/C++11 concurrency model

March 23

Yoav Kaempfer

Causal memory: definitions, implementation, and programming
Mustaque Ahamad, Gil Neiger, James E. Burns, Prince Kohli, Phillip W. Hutto
Distributed Computing, vol. 9, pp. 37-49, 1995

March 26 (Monday)

Anton Podkopaev
(guest lecture)

Correctness of compilation (tentative)

April 11

Matan Fillus

Efficient and correct execution of parallel programs that share memory
Dennis Shasha, Marc Snir
ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 10, issue 2, pp. 282-312, 1988

April 25

Or Ostrovsky

Don’t sit on the fence: a static analysis approach to automatic fence insertion
Jade Alglave, Daniel Kroening, Vincent Nimal, Daniel Poetzl
ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 39, issue 2, pp. 6:1--6:38, 2017

May 2

Daniel Katzan

Reasoning about the implementation of concurrency abstractions on x86-TSO
Scott Owens
In European Conference on Object-Oriented Programming (ECOOP), pp. 478-503, 2010

May 9

Tomer Raz

Safe optimisations for shared-memory concurrent programs
Jaroslav Ševčík
Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 306-316, 2011

May 16

Ori Saporta

Chasing away RAts: semantics and evaluation for relaxed atomics on heterogeneous systems
Matthew D. Sinclair, Johnathan Alsop, Sarita V. Adve
Proceedings of the 44th Annual International Symposium on Computer Architecture (ISCA), pp. 161-174, 2017

May 23

Daniel Solomon

A framework for transactional consistency models with atomic visibility
Andrea Cerone, Giovanni Bernardi, Alexey Gotsman
Proceedings of the 26th International Conference on Concurrency Theory (CONCUR), pp. 58-71, 2015

May 30

Dima Kuznetsov

Analysing snapshot isolation
Andrea Cerone, Alexey Gotsman
Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing (PODC), pp. 55-64, 2016

June 6

Replicated data types: specification, verification, optimality
Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, Marek Zawirski
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 271-284, 2014

June 13



Additional backgroud