Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Data reification in a concurrent rely-guarantee algebra

Larissa A. Meinicke, Ian J. Hayes, Cliff B. Jones

TL;DR

This work addresses the challenge of proving that concurrent refinements of abstract data structures preserve correctness when moved from specification to efficient implementation. It extends data reification with a concurrent rely-guarantee algebra, introducing coupling invariants and Aczel traces to model environment and program transitions, and uses local variable blocks to manage scoped state. The primary contributions are a formal data-reification framework for concurrent commands, distribution rules for invariants across composition, and a detailed concurrent Galler–Fischer example including a reification of a local operation (clean_up). The results enable modular, scalable reasoning about concurrent data structures with formal guarantees, aligning with prior work on invariants and localisation while offering a concrete pathway for practical refinement.

Abstract

Specifications of significant systems can be made short and perspicuous by using abstract data types; data reification can provide a clear, stepwise, development history of programs that use more efficient concrete representations. Data reification (or "refinement") techniques for sequential programs are well established. This paper applies these ideas to concurrency, in particular, an algebraic theory supporting rely-guarantee reasoning about concurrency. A concurrent version of the Galler-Fischer equivalence relation data structure is used as an example.

Data reification in a concurrent rely-guarantee algebra

TL;DR

This work addresses the challenge of proving that concurrent refinements of abstract data structures preserve correctness when moved from specification to efficient implementation. It extends data reification with a concurrent rely-guarantee algebra, introducing coupling invariants and Aczel traces to model environment and program transitions, and uses local variable blocks to manage scoped state. The primary contributions are a formal data-reification framework for concurrent commands, distribution rules for invariants across composition, and a detailed concurrent Galler–Fischer example including a reification of a local operation (clean_up). The results enable modular, scalable reasoning about concurrent data structures with formal guarantees, aligning with prior work on invariants and localisation while offering a concrete pathway for practical refinement.

Abstract

Specifications of significant systems can be made short and perspicuous by using abstract data types; data reification can provide a clear, stepwise, development history of programs that use more efficient concrete representations. Data reification (or "refinement") techniques for sequential programs are well established. This paper applies these ideas to concurrency, in particular, an algebraic theory supporting rely-guarantee reasoning about concurrency. A concurrent version of the Galler-Fischer equivalence relation data structure is used as an example.
Paper Structure (14 sections, 9 theorems, 49 equations, 1 figure)

This paper contains 14 sections, 9 theorems, 49 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Wide-spectrum language
  3. Language primitives
  4. Naming and syntactic precedence conventions.
  5. Derived commands
  6. Local variable blocks
  7. Invariants
  8. Data reification under coupling a coupling invariant
  9. Data refinement of a local variable block
  10. Example
  11. Specification.
  12. Implementation.
  13. Reifying $clean\_up$.
  14. Conclusion

Key Result

lemma 1

Figures (1)

  • Figure 1: An 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.

Theorems & Definitions (19)

  • definition 1: inv
  • lemma 1: inv-distribute
  • definition 2: data-refines
  • lemma 2: reify-operators
  • proof
  • lemma 3: reify-commands
  • proof
  • lemma 4: reify-rgspec
  • proof
  • lemma 5: reify-expr
  • ...and 9 more