This page documents the KIV formalization of
Gerhard Schellhorn, Stefan Bodenmüller, Jörg Pfähler, Wolfgang Reif:
Adding Concurrency to a Sequential Refinement Tower.
Presented to ABZ 2020.
Project Overview gives an overview of the entire specification hierarchy.
KIV-Projects always link to an overview which gives the dependency graph of specifications. Clicking on one specification gives its text, and links to a theorem base summary (which lists names of theorems) and a theorem base listing (which shows the full sequent for each theorem). From there individual theorems and the full details of each proof are accessible.
The erase block management interface is defined by the ASM specification ebm-asm. It defines interface operations for reading and writing individual blocks. The initial state is given by an initialization operation.
The sequential implementation of EBM is given in the ASM specification wl-seq-asm which uses the specification block-seq-asm as a submachine. It introduces the mapping LMap from logical to physical blocks as well as an internal operation for wear leveling. Proof obligations for the sequential invariants injective, blockslmap and lmapblocks, which are defined in wl-base, were generated and proved here.
The data refinement of ebm-asm to wl-seq-asm is proved by a regular forward simulation in ebm-refine using the abstraction relation abs. The refinement proof of the wear leveling operation shows that this operation is actually internal, i.e., it is a refinement of the program skip.
The concurrent implementation of EBM is given in the ASM specification wl-asm. It uses the submachine block-asm, which results from expanding block-seq-asm by ownership properties (determined by an ownership hierarchy) and ownership acquire and release operations. Thus mover types for the interface operations of blocks-asm can be inferred, yielding atomic-block-asm
wl-asm specifies an ownership hierarchy for its local (volatile) state and is augmented with locking instructions as well as calls to ownership acquire/release operations of atomic-blocks-asm. Here the concurrent invariants and assertions, which are necessary for atomicity refinement, are proved using rely-guarantee reasoning.
The atomicity refinement is performed in two reduction steps.
First, in wl-asm-reduction the mover types for locking and acquire/release instructions are given and proved by commutation proof obligations. This reduction allows for establishing the invariant that all Locks are free in reduced-wl-asm.
Second, with this invariant bigger atomic blocks can be inferred in wl-asm-reduction2 which in turn yields the completely atomic ASM atomic-wl-asm.
Finally, the trivial refinement in wl-refine shows that the abstraction from locking/unlocking and acquire/release instructions in atomic-wl-asm is feasible.
Used basic libraries:
Back to the overview of all KIV projects.
For general informations on KIV and a download site for the whole system refer to this page.