Reasoning about distributive laws in a concurrent refinement algebra

TL;DR

The paper addresses the challenge of deriving strong, equality-based distributive laws for reasoning about concurrent programs, extending beyond prior partial-correctness results. It develops a concurrent refinement algebra built on synchronous algebra, an abstract synchronisation operator $⊗$, and a class of pseudo-atomic fixed points that enable equalities such as $d ⊗ c_1 ; c_2 = (d ⊗ c_1) ; (d ⊗ c_2)$. These results are then applied to rely/guarantee concurrency by encoding program and environment transitions as atomic steps and proving distributivity across sequential, parallel, and iterative constructs, including fixed points and generalized invariants like $ ext{inv} p$. The framework supports total correctness and data refinement through invariant coupling, with formalization implications in Isabelle/HOL and potential future work on broader distributivity and Cap-operators. This work offers a robust algebraic toolset for compositional, scalable reasoning about concurrent systems.

Abstract

Distributive laws are important for algebraic reasoning in arithmetic and logic. They are equally important for algebraic reasoning about concurrent programs. In existing theories such as Concurrent Kleene Algebra, only partial correctness is handled, and many of its distributive laws are weak, in the sense that they are only refinements in one direction, rather than equalities. The focus of this paper is on strengthening our theory to support the proof of strong distributive laws that are equalities, and in doing so come up with laws that are quite general. Our concurrent refinement algebra supports total correctness by allowing both finite and infinite behaviours. It supports the rely/guarantee approach of Jones by encoding rely and guarantee conditions as rely and guarantee commands. The strong distributive laws may then be used to distribute rely and guarantee commands over sequential compositions and into (and out of) iterations. For handling data refinement of concurrent programs, strong distributive laws are essential.

Figures (1)

• Figure 1: An execution trace (of a program in an environment) consisting of states $\sigma_0$ through $\sigma_7$. Transitions of the program are labeled $\pi$ and transitions of its environment are labeled $\epsilon$. A trace satisfies a specification with pre-condition $p$, post-condition $q$, rely condition $r$ and guarantee condition $g$, if whenever the initial state satisfies $p$ and all environment transitions satisfy $r$, the post-condition $q$ (a binary relation between states) holds between the initial and final states, and every program transition satisfies $g$. Importantly, a trace of a thread includes transitions of both itself ($\pi$) and its environment ($\epsilon$) Aczel83.

Theorems & Definitions (32)

• theorem 1: distrib-fixed-iter
• proof
• theorem 2: distrib-finite-iter
• proof
• Lemma 3: pafp-basic-properties
• proof
• Lemma 4: pseudo-atomic-distrib-length
• proof
• Lemma 5: pseudo-atomic-distrib-fin
• proof