Restructuring a concurrent refinement algebra

TL;DR

The paper addresses deriving shared-variable concurrent programs from rely/guarantee specifications by restructuring the Concurrent Refinement Algebra (CRA) around a unified algebraic backbone. It shows that sequential composition, parallel composition, and weak conjunction form common quantale and biquantale structures with weak interchange laws, and that this structure extends consistently to tests, atomic and pseudo-atomic commands. By introducing compatible sets of commands and reusing atomic-algebra lemmas for pseudo-atomic commands, the authors obtain a coherent, reusable toolkit for reasoning about termination, guarantees, and relies within rely/guarantee concurrency, implemented in Isabelle/HOL. The work provides concrete laws for distributing across iterations and fixed points, enabling simplified proofs and practical mechanization for concurrent program refinement from specifications. Overall, it advances a principled, tool-supported foundation for deriving concurrent programs from rely/guarantee specifications with stronger algebraic guarantees.

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.

Figures (2)

• Figure 1: Aczel trace satisfying a specification with precondition $p$, postcondition $q$, rely condition $r$ and guarantee condition $g$. If the initial state, $\sigma_0$, is in $p$ and all environment transitions ($\epsilon$) satisfy $r$, then all program transitions ($\pi$) must satisfy $g$ and the initial state $\sigma_0$ must be related to the final state $\sigma_7$ by the postcondition $q$, also a relation between states.
• Figure 2: Weak interchange law between parallel and sequential. On the left $c_1$ may finish at any of the coloured lines and $d_1$ finish at the correspondingly coloured lines. Hence $c_2$'s execution may overlap with $d_1$ or $c_1$'s execution may over lap with $d_2$. On the right the termination of $c_1$ is synchronised with the termination of $d_1$.

Theorems & Definitions (19)

• definition 1: monoid
• definition 2: quantales
• Lemma 1: finite-to-fixed
• proof
• Corollary 2: finite-to-choice
• Lemma 3: finite-iter-decompose
• proof
• definition 3: biquantale
• definition 4: General Concurrent Refinement Algebra
• definition 5: compatible