Keynote Talk : On Program Verification under the Release-Acquire Semantics

Parosh Parosh Aziz Abdulla

Uppsala University (Sweden)

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 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 idea at a high level so that it can be followed by non-experts.

BIOGRAPHY: Parosh Aziz Abdulla is a professor at the department of information technology, Uppsala University. His areas of interest include formal methods, automata theory and logic in computer science, program verification and model checking. He has more than 150 publications, and has received more than 10 best paper awards including ones from the European association for software science and technology at ETAPS 2013, the European association for theoretical computer science at ETAPS 2010 and ICALP 2001, and the European association for programming languages and systems at ETAPS 2000. He was a co-recipient of the LICS test-of-time award in 2016, for his paper in 1996 on the verification of well quasi-ordered programs. In 2017, he was a co-recipient of the CAV award for his contributions in the area of verification of programs with infinite state spaces.

Dates

All deadlines are at 23:59 AoE

March 5th, 2021, March 19th, 2021

Abstract submission deadline

March 12th, 2021 March 26th, 2021

Paper submission deadline

April 26th, 2021 April 30th, 2021

Acceptance notification

May 10th, 2021

Camera ready

May 10th, 2021

Pre-recorded talk

Proceedings

Revised selected papers will be published as a post-proceedings in Springer's LNCS "Lecture Notes in Computer Science"

Partners & Sponsors