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

Extended deadlines

March 09, 2019

Abstract submission deadline

March 16, 2019

Paper submission deadline

April 27, 2019

Acceptance notification

May 24, 2019

Camera ready copy due

Proceedings

SpringerLNCS

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

Partners & Sponsors

SponsorsNETYS28