Verifying Concurrent Data Structures with Isabelle/HOL

People

Research areas

Description

Background

Formal reasoning for concurrent systems - for example using rely guarantee style reasoning - is complicated as all possible interleavings of the programs running in parallel need to be considered. Concurrent Data Structures (CDSs) are significantly more difficult to design and to verify than their sequential counterparts. The situation becomes even more problematic and verification more intricate (and hence even more indispensable) when the effects of both hardware (e.g. x86-TSO, ARMv8) and software (e.g. C11) weak memory models are considered.

Linearizability-style specification is a standard approach among algorithm designers for deducing correctness when considering weak memory models. However, it has been shown that linearizability does not suffice for this purpose [RDRLV19]. The alternative, called strong linearizability, has its own limitations as not all algorithms satisfy this criterion [RHW11]. We plan to follow the seminal paper [5] and study CDSs structures under weak memory consistency (WMC).

Research Questions and Tasks

The aim of the project is to verify basic concurrent data structures, in particular locks. This could include locks, such as ticket lock, spin lock or the CLH lock. As all locks have identical specifications regarding safety properties, but obviously different implementations, the use of Rely-Guarantee reasoning techniques in combination with a Refinement calculus (RGR) will reveal where the implementations differ. RGR usually guarantees safety (functional correctness), but not liveness properties. These include progress properties and avoidance of starvation, which are of equal importance for CDSs.

To guarantee correctnes and to support proof mechanization, the verification tasks should be carried out in an Isabelle-framework. To guarantee compositionality - an indispensable feature for verifying concurrent systems - a combination of rely-guarantee refinement proofs should be used.

References

[RDRLV19] Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, Viktor Vafeiadis: On Library Correctness under Weak Memory Consistency. POPL 2019: 68:1-68:31
[RHW11] Wojciech Golab, Lisa Higham, Philipp Woelfel: Linearizable Implementations Do Not Suffice for Randomized Distributed Computation. STOCS 2011: 373–382

Requirements: knowledge in the area of interactive theorems proving (e.g. Coq, HOL4 or Isabelle/HOL) is an advantage

Keywords

formal verification, interactive theorem proving, correctness of software

Updated:  1 June 2019/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing