We address the issue of verifying the correctness of libraries of shared data structures (such as concurrent stacks, queues, etc.). Such a library provides a number of operations for the abstract manipulation of the data structure (e.g., push, pop, is-empty, etc.) The users of the library assume that these operations are executed atomically, in some interleaving order between operations issued by different threads. While implementations based on coarse-grained locking allow to ensure easily correctness (w.r.t. the abstract, sequential specification of the data structure), they are not satisfactory due to their poor performances. In general, efficient implementations employ lock-free synchronization techniques instead in order to maximise parallelism while minimizing contention between concurrent operations. However, these implementations are quite complex and hard to get right. The conformance of these implementation to the abstract specification of the data structure is captured by the concept of linearizability. In this talk, we overview the decidability and complexity of the problem of verifying linearizability w.r.t. a sequential specification, and we provide reductions of this problem to reachability problems under various assumptions (on the implementation and on the specification). These reductions are presented following a generic schema that consists in defining monitors (state machines) for detecting linearization violations that implementations may generate.

This talk is based on joint work with Michael Emmi, Constantin Enea, and Jad Hamza.

 

Ahmed Bouajjani got a PhD and a Habilitation in CS from the Univ. of Grenoble (1990, 1999). He was associate prof. at the Univ. of Grenoble/Verimag lab. (1990-99). He is full professor at Paris Diderot Univ./LIAFA-IRIF lab. since 1999, head of the ``Modeling and Verification'' team from 2004 to 2017, and head of the ``Automata, Structures, and Verification’’ research group since 2017. He is senior member of the ``Institut Universitaire de France’’ (IUF) since 2013. He was visiting professor in several institutions including TU~Munich, Uppsala~Univ., Chennai Mathematical Institute, and Microsoft Research. His research interests include formal specification and verification methods, model checking algorithms, verification of infinite-state systems, program analysis and verification, concurrency, automata and logics. He published more that 115 articles in international conferences and journals. He co-chaired the program committees of 5 international conferences, he is in the editorial boards of 2 journals, in the steering conferences of 2 international conferences.