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

Schedule

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

Ori
[slides]

Introduction: Weakly consistent concurrency

March 14

Ori
[slides]

Introduction: C/C++11 concurrency model

March 23

Yoav Kaempfer
[slides]

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
[slides]

Guest lecture: Correctness of compilation
Code example: http://preshing.com/20120515/memory-reordering-caught-in-the-act/

April 11

Matan Fillus
[slides]

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
[slides]

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
[slides]

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
[slides]

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 23

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 30

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

June 13

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

Additional backgroud