Data reification in a concurrent rely-guarantee algebra

TL;DR

This paper extends data reification techniques to concurrent systems using an algebraic approach, enabling clearer development and reasoning about concurrent programs with abstract data types.

Contribution

It introduces a concurrent rely-guarantee algebraic framework for data reification, adapting sequential refinement concepts to concurrent settings.

Findings

Develops an algebraic theory for concurrent data reification

Applies the theory to a concurrent Galler-Fischer data structure

Demonstrates clearer reasoning about concurrent program 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.