Automating Deductive Verification for Weak-Memory Programs

TL;DR

This paper presents the first automated deductive verification approach for weak-memory programs, encoding advanced program logics into existing tools to improve correctness proofs.

Contribution

It introduces novel encoding techniques to automate proofs in weak memory program logics using the Viper infrastructure, enabling practical verification.

Findings

Successfully encoded three recent program logics into Viper

Automated verification demonstrated on real-world examples including Facebook's Folly library

First implementation of automated deductive verification for weak-memory programs

Abstract

Writing correct programs for weak memory models such as the C11 memory model is challenging because of the weak consistency guarantees these models provide. The first program logics for the verification of such programs have recently been proposed, but their usage has been limited thus far to manual proofs. Automating proofs in these logics via first-order solvers is non-trivial, due to reasoning features such as higher-order assertions, modalities and rich permission resources. In this paper, we provide the first implementation of a weak memory program logic using existing deductive verification tools. We tackle three recent program logics: Relaxed Separation Logic and two forms of Fenced Separation Logic, and show how these can be encoded using the Viper verification infrastructure. In doing so, we illustrate several novel encoding techniques which could be employed for other logics. Our work is implemented, and has been evaluated on examples from existing papers as well as the Facebook open-source Folly library.