Title: Verification of Concurrent Programs under Release Acquire -- Part I

Speaker: Krishna S    (bio) (bio)

Krishna S is a faculty member in the Department of Computer Science and Engineering at IIT Bombay. Her areas of research are broadly in Automata, Logics, Games and the formal verification of timed and probabilistic systems.

When: Tuesday, 06 December 2022 at 1900 hrs (IST)       

Abstract:
This talk (part I and part II) is an overview of some recent work on the verification of concurrent programs. Traditionally concurrent programs are interpreted under sequential consistency (SC). Eventhough SC is very intuitive and easy to use, modern multiprocessors do not employ SC for performance reasons, and instead use so called "weak memory models". Some of the well known weak memory models in vogue among modern multiprocessor architectures are Intel x-86, IBM POWER and ARM. The use of weak memory is also prevalent in the C11 model, leading to the release acquire fragment of C11. This talk is on the verification of concurrent programs under the release acquire (RA) semantics.

The main focus of the talk will be on non parameterized programs under RA, and I will briefly discuss results in the parameterized setting.

In the non parameterized setting, we show that the reachability problem for RA is undecidable even in the case where the input program is finite-state, closing a long standing open problem. What works well for this class is under approximate reachability, in the form of bounded view switching, an analogue of bounded context switching, relevant to RA. In the parameterized setting, the first observation is that the semantics of RA can be simplified, lending to a better complexity for verification. Further, safety verification is PSPACE-complete for the case where the distinguished threads are loop-free, and jumps to NEXPTIME-complete for the setting where an unrestricted distinguished ego thread interacts with the environment threads.

This talk is based on papers that appeared in PLDI'19 (joint with Parosh Abdulla, Mohamed Faouzi Atig and Jatin Arora), PODC'22 (joint with Roland Meyer, Adwait Godbole and Soham Chakraborty), and Arxiv'21 (with Roland Meyer and Adwait Godbole).