Deriving Laws for Developing Concurrent Programs in a Rely-Guarantee Style
Abstract
This paper presents a theory for the refinement of shared-memory concurrent algorithms from specifications. We augment pre and post condition specifications with Jones' rely and guarantee conditions, all of which are encoded as commands within a wide-spectrum language. Program components are specified using either partial or total correctness versions of postcondition specifications. Operations on shared data structures and atomic machine operations (e.g. compare-and-swap) are specified using an atomic specification command. All the above constructs are defined in terms of a simple core language, based on a small set of primitive commands and a handful of operators. A comprehensive set of laws for refining such specifications to code is derived in the theory. The approach supports fine-grained concurrency, avoiding atomicity assumptions on expression evaluation and assignment commands. The theory has been formalised in Isabelle/HOL, and the refinement laws and supporting lemmas have been proven in Isabelle/HOL.
Cite
@article{arxiv.2103.15292,
title = {Deriving Laws for Developing Concurrent Programs in a Rely-Guarantee Style},
author = {Ian J. Hayes and Larissa A. Meinicke and Patrick A. Meiring},
journal= {arXiv preprint arXiv:2103.15292},
year = {2023}
}