Restructuring a concurrent refinement algebra

TL;DR

This paper presents a restructured version of the concurrent refinement algebra, enhancing its mathematical properties and implementation in Isabelle/HOL to better support reasoning about concurrent programs.

Contribution

It introduces a reorganized algebraic structure that exploits commonalities among operations and implements it in Isabelle/HOL for improved reasoning capabilities.

Findings

Enhanced algebraic structure with common biquantale properties

Implementation of the algebra in Isabelle/HOL

Improved support for rely/guarantee reasoning in concurrency

Abstract

The concurrent refinement algebra has been developed to support rely/guarantee reasoning about concurrent programs. The algebra supports atomic commands and defines parallel composition as a synchronous operation, as in Milner's SCCS. In order to allow specifications to be combined, the algebra also provides a weak conjunction operation, which is also a synchronous operation that shares many properties with parallel composition. The three main operations, sequential composition, parallel composition and weak conjunction, all respect a (weak) quantale structure over a lattice of commands. Further structure involves combinations of pairs of these operations: sequential/parallel, sequential/weak conjunction and parallel/weak conjunction, each pair satisfying a weak interchange law similar to Concurrent Kleene Algebra. Each of these pairs satisfies a common biquantale structure. Additional structure is added via compatible sets of commands, including tests, atomic commands and pseudo-atomic commands. These allow stronger (equality) interchange and distributive laws. This paper describes the result of restructuring the algebra to better exploit these commonalities. The algebra is implemented in Isabelle/HOL.