Title: Stateless Model Checking under the Release-Acquire Semantics
Speaker: Parosh Aziz Abdulla
Abstract:
Program verification methodologies need to consider new challenges for which we currently lack solutions. The principal reason is that such methods are often conducted under the fundamental assumption of strong (or sequential) consistency (SC) where all components are strongly synchronized so that they all have a uniform view of the global state of the system. However, nowadays, most parallel software runs on platforms that do not guarantee SC. More precisely, to satisfy demands on efficiency and energy saving, such platforms implement optimizations that lead to the relaxation of the inter-component synchronization, hence offering only weak consistency guarantees. Weakly consistent platforms are found at all levels of system design, e.g., multiprocessor architectures, Cache protocols, Language level concurrency, and distributed data stores.
To illustrate the types of challenges that may arise, and the solutions that we can provide, I will consider the Release-Acquire (RA) fragment of the C11 language. RA is a useful and well-behaved fragment of the C11 memory model, which strikes a good balance between performance and programmability. In RA, all writes are release accesses, while all reads are acquire accesses. I will explain how classical stateless model checking algorithms, based on partial order reductions, that have been developed to work under the SC semantics can be adapted so that they can be applied to a concurrent program running under the RA semantics.
The lecture will present the ideas at a high level so that it can be followed by non-experts.