Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent Systems

This page documents the KIV formalization of

Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif:
Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent Systems.
Submitted to ABZ 2023.

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 main Hashset specification defines the algorithms for inserting elements and for testing membership in the hashtable. It also defines the necessary assertions and rely conditions to prove an invariant (HashsetInv). The specification text generates data types for global and local states, actions, and predicate logic axioms for steps, consisting of preconditions 'pre' and three functions 'gstepf', 'lstepf', 'pcstepf' that modify the global, local and control state. The generated specifications are all shown after the ';;;END' marker that ends the specification text typed in by the user. Note that the definition of the thread-local invariant HashsetLInv that has to collect all the assertions given is already quite a large formula.
• The specification imports the predicates 'htok', 'allslotsfull' and 'between' as given in the paper. Some simple lemmas are proved over them in the theorembase.
• Specification HashSet also generates step-, rely- and stable- proof obligations (as defined in the paper), that must be discharged to prove the invariant. These are proven here. Some 'definedness' proof obligations (not discussed in the paper) ensure that partial functions (like array access or division/modulo) are always called within their specified domain (for array access the index must be below the array size; divisor must not be zero).
• The abstract canonical automaton is defined in specification Set. Again this specification generates data types and axioms given at the end of the text. The invariant SetInv needed here is rather simple. Again local proof obligations are discharged as shown in this theorembase.
• Specification Hashset-refines-Set contains the necessary definitions that fix the forward simulation 'abs' by defining a global abstraction, assertions that define the abstraction between local state (predicate 'labs'), and by mapping actions of the concrete automaton for the algorithms to actions of the abstract one. The latter mapping is necessary for the technical reason, that the two types of actions of the automata (HashsetAction and SetAction) are different. It is basically identity. The definitions generate the thread-local, step-local proof obligations as given in the paper, that must be proved to ensure a correct forward simulation and therefore refinement, i.e. trace inclusion.
• Because of refinement, most of the tasks given in the description of the VerifyThis2022 challenge can be proved over abstract set operations, instead of proving them for the algorithms. Some properties are proved here, however termination has not been considered yet, and the proofs are not discussed in the paper.
• Finally, this specification provides the instance of the generic refinement theory with the case study.

Used basic libraries:

• The basic KIV library with basic data types.
• KIV formalization of the refinement theory of IO-Automata.

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.

[Imprint] [Data Privacy Statement] [E-Mail]