Adding Concurrency to a Sequential Refinement Tower

Abstract

This paper defines a concept and a verification methodology for adding concurrency to a sequential refinement tower of abstract state machines, that is based on data refinement and a component structure. We have developed such a refinement tower for the Flashix file system earlier, from which we generate executable (C and Scala) Code. The question we answer in this paper, is how to add concurrency based on locks to such a refinement tower, without breaking the initial modular structure. We achieve this by just enhancing the relevant components, and adding intermediate atomicity refinements that complement the data refinements that are already there. We also give a verification methodology for such atomicity refinements.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{SchellhornBPR20,
  author       = {Gerhard Schellhorn and
                  Stefan Bodenm{\"{u}}ller and
                  J{\"{o}}rg Pf{\"{a}}hler and
                  Wolfgang Reif},
  editor       = {Alexander Raschke and
                  Dominique M{\'{e}}ry and
                  Frank Houdek},
  title        = {Adding Concurrency to a Sequential Refinement Tower},
  booktitle    = {Rigorous State-Based Methods - 7th International Conference, {ABZ}
                  2020, Ulm, Germany, May 27-29, 2020, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12071},
  pages        = {6--23},
  publisher    = {Springer},
  year         = {2020},
  url          = {https://doi.org/10.1007/978-3-030-48077-6\_2},
  doi          = {10.1007/978-3-030-48077-6\_2},
  timestamp    = {Sun, 25 Oct 2020 23:07:20 +0100},
  biburl       = {https://dblp.org/rec/conf/asm/SchellhornBPR20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}