Generating Rely-Guarantee Conditions with the Conditional-Writes Domain

TL;DR

This paper introduces a new domain called the conditional-writes domain for generating rely-guarantee conditions in concurrent program verification, using a modular abstract interpretation framework.

Contribution

It formalizes a novel approach to generate rely-guarantee conditions based on conditional writes, enhancing modularity and extensibility in verification techniques.

Findings

Effective generation of rely-guarantee conditions for concurrent programs.

Modular abstract interpretation framework facilitates extension to other structures.

Evaluation demonstrates practical applicability on a simple programming language.

Abstract

Abstract interpretation has been shown to be a promising technique for the thread-modular verification of concurrent programs. Central to this is the generation of interferences, in the form of rely-guarantee conditions, conforming to a user-chosen structure. In this work, we introduce one such structure called the conditional-writes domain, designed for programs where it suffices to establish only the conditions under which particular variables are written to by each thread. We formalise our analysis within a novel abstract interpretation framework that is highly modular and can be easily extended to capture other structures for rely-guarantee conditions. We formalise two versions of our approach and evaluate their implementations on a simple programming language.