Seminars on Concurrent Data-Structure Verification
Title of the Talk: Seminars on Concurrent Data-Structure Verification
Host Faculty: Prof.Sathya Peri
Speaker: Prof.Sathya Peri & Narayanan
Date: 10 August - 14 August 2026
Time: 10:00 am
Abstract
Modern computer systems are by nature concurrent, consisting of a number of cores/processors executing threads in parallel. To exploit this concurrency, programming on such models must avoid unnecessary sequentialization. Using locks to ensure mutually exclusive access to (parts of) the data-structure, unless done very carefully, can lead to sequentialization and poor performance.
Over the years, several Concurrent Data-Structures (CDS) have been developed) with carefully calibrated use of locks as well as avoiding locks altogether by using hardware/OS provided operations such as test-and-set or compare-and-swap.
However, proving the correctness of CDS is very challenging. Even the notion of correctness for concurrent data structures, linearizability, is not immediate. The concurrent setting also obliges us to establish liveness properties. Classical notions such a deadlock-freedom/starvation-freedom assume properties of the underlying scheduler. While this is reasonable while dealing with OS primitives, something weaker is needed for CDS which are likely to run at user level. The corresponding notions are lock-free/wait-free and establishing linearizability under such liveness conditions is usually very involved.
In this seminar series we will study techniques for proving Linearizability of CDS under such liveness obligations.