This is an overview of some recent work on the verification of concurrent programs. Traditionally concurrent programs are interpreted under sequential consistency (SC). Even though 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, the reachability problem for RA is undecidable even in the 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 EXPTIME-complete for the setting where an unrestricted distinguished ego thread interacts with the environment threads.