Ahmed Bouajjani (IRIF, Paris 7 & CNRS)

Constantin Enea (LIX, Ecole Polytechnique)

Lectures will be given on Thursdays from 16:15 to 19:15, room 1004.

TBD

Concurrency is omnipresent at all levels of computer systems (multi-core hardware architectures, libraries of concurrent data structures, network protocols, distributed databases, concurrent and distributed applications, etc.). Concurrent systems are notoriously hard to design and to implement. This is due to the complexity of their behaviors resulting from intricate and difficult to apprehend interactions between their components. Several aspects contribute to this complexity: (1) the combinatorial explosion due to the interleaving of action sequences issued by different components, (2) the infinite number of possible configurations due to dynamic creation of processes, (3) the interaction between recursion and synchronization, (4) the out-of-order executions allowed by optimizations (both at the hardware and the compiler levels), (5) the consistency relaxations in implementations of concurrent objects and distributed databases, etc.

This course presents the basic concepts, approaches, and techniques for the verification of concurrent systems. It covers several aspects related to the complexity and the decidability of verification problems of different types of such programs, and the design of efficient methods and algorithms for their automated verification.

1-4. See https://www.irif.fr/~abou/cours-mpri.html

5. Introduction. Concurrent/distributed data types. Slides

• Correctness criteria: quiescent/sequential consistency, linearizability
• Examples of concurrent data structure implementations,

6. Checking linearizability: Theoretical Limits Slides

• Complexity results
• Deciding linearizability for implementations with fixed linearization points, and fixed number of threads, respectively.
• References: Model-Checking of Correctness Conditions for Concurrent Objects On the complexity of Linearizability Verifying Concurrent Programs Against Sequential Specifications

7. Reducing Linearizability to Classic Verification Problems Slides

• References: Reducing Linearizability to State Reachability for Queues and Stacks Obs. Ref. and Lin. Proving Lin. using For. Sim. Forward Simulation Proof for Snapshots (Section 6 and Appendix D)

7. Weak Consistency Slides

• References: Principles of Eventual Consistency On Verifying Causal Consistency

2022-2023 Subject

2023-2024 Subject

Internships in the area of Program Verification are available. Please contact one of the teachers or a member of the Modeling and Verification group of IRIF.