Data reification in a concurrent rely-guarantee algebra
Logic in Computer Science
2024-05-10 v1 Software Engineering
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.
Cite
@article{arxiv.2405.05546,
title = {Data reification in a concurrent rely-guarantee algebra},
author = {Larissa A. Meinicke and Ian J. Hayes and Cliff B. Jones},
journal= {arXiv preprint arXiv:2405.05546},
year = {2024}
}