APLAS 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
co-located with SPLASH 2022

This program is tentative and subject to change.

Mon 5 Dec 2022 09:00 - 10:00 at Seminar Room G007 - Keynote

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.

This program is tentative and subject to change.

Mon 5 Dec

Displayed time zone: Auckland, Wellington change