Subjective Simulation as a Notion of Morphism for Composing Concurrent Resources

TL;DR

This paper introduces a new notion of morphism between state transition systems (STSs) that allows for modular composition and linking of concurrent program specifications without the need for reverification, enhancing the verification process.

Contribution

It develops a constructive simulation-based morphism for STSs, enabling modular composition and linking of concurrent resources in separation logic verification.

Findings

Morphism enables lifting of STSs in composition

Proof system is concise and general

Illustrated on readers/writers lock and quiescence proofs

Abstract

Recent approaches to verifying programs in separation logics for concurrency have used state transition systems (STSs) to specify the atomic operations of programs. A key challenge in the setting has been to compose such STSs into larger ones, while enabling programs specified under one STS to be linked to a larger one, without reverification. This paper develops a notion of morphism between two STSs which permits such lifting. The morphisms are a constructive form of simulation between the STSs, and lead to a general and concise proof system. We illustrate the concept and its generality on several disparate examples, including staged construction of a readers/writers lock and its proof, and of proofs about quiescence when concurrent programs are executed without external interference.