Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations

TL;DR

This paper introduces resource morphisms and simulations in separation logic, enabling the adaptation of verified concurrent programs across different resource models for improved proof reuse.

Contribution

It presents a novel concept of resource morphisms and integrates them into separation logic, enhancing modularity and reusability of proofs in concurrent program verification.

Findings

Resource morphisms preserve resource structure.

Morphisms enable compositionally adapting programs to different resources.

Enhanced proof reuse in concurrent program verification.

Abstract

In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of resources---a form of state transition system---to describe the state-based program invariants that must be preserved, and to record the permissible atomic changes to program state. In this paper we introduce a novel notion of resource morphism, i.e. structure-preserving function on resources, and show how to effectively integrate it into separation logic, using an associated notion of morphism-specific simulation. We apply morphisms and simulations to programs verified under one resource, to compositionally adapt them to operate under another resource, thus facilitating proof reuse.