In the final project,
the local proof applications are applied to verify an implementation of
the three standard set operations adding an element, removing an element and membership test.
The implementation is the lazy set algorithm described in [Helleretal05]. Like the (pessimistic) version we
verified earlier,
it uses a singly-linked list to represent a set of integers. The version verified here
has three essential new problems:
- It has linearization points outside the current thread.
- It may linearize several operations simultaneously.
- Its algorithms may step through list cells, which have already been removed from the list representation.
Therefore it is necessary to prove properties for these cells too.
The following list gives some details on the specifications and proofs:
- The list is sorted in strictly ascending order. The initial and the final cell are used as sentinels. They
contain -infinity and infinity. A fine-grained locking scheme is used to lock single list cells.
Cells in the list aremarked to indicate deletion atomically, before the actual removal. Therefore the type of memory cells is a
four-tuple, consisting of a boolean mark,
an integer or +/-infinity as the data value,
process id or none for locking,
and a next pointer. The
heap
is again an instance of the generic specification
store, where keys are references and data are memory cells.
- The
definition of the status function makes use of the new status INOUT for the contains function. The status is INOUT(e,bv)
during the main loop of this function, when it is called with element e, where the boolean value bv is true iff
the element e would be found (unmarked), when the contains program would run to completion uninterrupted.
- The
abstraction function is defined to collect all unmarked elements reachable from the Head pointer.
- The invariant needed
for each process is similar to the one used in the earlier case study, but there is a new global invariant LISTINV
that always holds. This invariant ensures the existence of a (unique) tail cell with value infinite, and next-pointer = null.
For this tail reference and every reference r in the heap H the predicate NODEINV(r,Head,Tail,H) must hold. This states, that
each cell falls into one of four disjoint classes:
- If it is marked, then Tail is reachable from it.
- If it is unmarked and there is an pointer to the cell in the heap, then it must be a cell of the current set representation,
i.e. it must lie between Head and Tail.
- If it is unmarked and there is no ingoing pointer, then it can be the head cell with value -infinity.
- Otherwise, it must be a newly allocated cell with a value different from -infinity. In this case either the next-pointer is null
(the cell has just been allocated), or the Tail pointer is reachable (the next pointer has been set to point into
the current set representaion, but the cell itself has not been inserted).
NODEINV also guarantees, that the value stored in the cell pointed to by r is strictly smaller
than the value stored in the next cell (if it exists, i.e. if the next-pointer is non-null).
- Finally,
the local proof obligations are verified. The ones for invoke and return operations are simple (as well as the inialization
conditions). The three main interesting proofs are
Although the three proofs look big, their structure is simple: all three proofs split immediately
into branches for each program step (indicated by the value of the program counter) of
the add, remove and contains routine. The most complex proof is for the second proof obligation,
which requires another systematic case split according to the various properties required for the other process,
so it essentially distinguishes between the various program steps of the other process too.
Among the program steps the five main interesting steps of add (allocating a cell, setting its next pointer, adding it to the list)
and remove (marking the cell to remove and actually removing it) require some interactive steps, usually to apply
standard lemmas about linking or unlinking cells. These lemmata, like
this one about linking a cell into a chain of cells are from the library and used in many case studies that have linked lists.
Used basic libraries:
Here you can find all our publications.
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.