Verification of Concurrent Programs under Release-Acquire Concurrency
14/04/2022, 10:30am
Speaker
Abstract
This 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
multiprcessor architectures are
Intel x-86, IBM POWER and ARM. The use of weak memory is also prevelant
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, the reachability problem for RA is
undecidable even inthe case where the input program is finite-state.
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.
Speaker Bio
Krishna is a faculty member in the department of computer science and engineering at IIT Bombay, India. Prior to joining IIT Bombay, she obtained a PhD from IIT Madras, India.Her areas of research span formal verification, with a focus on transducers, logic and games, and more recently on weak memory concurrency.