Flexible Refinement Proofs in Separation Logic

TL;DR

This paper introduces a flexible refinement method using separation logic that enables reasoning about efficient concurrent programs with minimal structural restrictions, broadening applicability and automation in verified system development.

Contribution

It presents a novel, loosely coupled refinement technique in separation logic that overcomes limitations of existing methods, supporting diverse program structures and enabling automation.

Findings

Supports a wide range of program structures and data representations

Proven to preserve properties through formal trace inclusion

Demonstrated effectiveness on multiple case studies

Abstract

Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development of substantial verified systems. Nevertheless, existing refinement techniques have limitations that impede their practical usefulness. Some techniques generate executable code automatically, which generally leads to implementations with sub-optimal performance. Others employ bottom-up program verification to reason about efficient implementations, but impose strict requirements on the structure of the code, the structure of the refinement proofs, as well as the employed verification logic and tools. In this paper, we present a novel refinement technique that removes these limitations. Our technique uses separation logic to reason about efficient concurrent implementations. It prescribes only a loose coupling between an abstract model and the concrete implementation. It thereby supports a wide range of program structures, data representations, and proof structures. We make only minimal assumptions about the underlying program logic, which allows our technique to be used in combination with a wide range of logics and to be automated using off-the-shelf separation logic verifiers. We formalize the technique, prove the central trace inclusion property, and demonstrate its usefulness on several case studies.