Deriving Laws for Developing Concurrent Programs in a Rely-Guarantee Style

TL;DR

This paper develops a formal theory for refining shared-memory concurrent algorithms using rely-guarantee conditions, supporting fine-grained concurrency and formalized in Isabelle/HOL.

Contribution

It introduces a new refinement theory for concurrent programs with rely-guarantee conditions, formalized in Isabelle/HOL, enabling precise development of concurrent algorithms.

Findings

Derived a comprehensive set of refinement laws for concurrent algorithms.

Formalized the theory and laws in Isabelle/HOL.

Supports fine-grained concurrency without atomicity assumptions.

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.