Separating Separation Logic - Modular Verification of a Pointer Implementation of Red-Black Trees

This page gives a description of the modular verification of red-black trees with KIV as described in [Rbtree22]. The version verified uses a pointer structure with parent pointers and a while-loop based algorithm, it is very close to [Cormen09], the version in the stdc++-library, and many C implementations that can be found on the internet. There is one small difference that exists with many other implementations: we do not use a single pre-allocated sentinel-node for leaves (that has all the fields of regular nodes), but simply the null pointer. Therefore, leaf nodes do no have a parent pointer. Using the null pointer does not require any changes for the insert algorithm. However, removeFixup cannot start with the replacement node of the deleted node, since this could be a leaf and traversing upwards would be impossible. Instead it starts with its parent. and gets the additional (boolean) information of whether the left or right child has been deleted. Starting this way allows to avoid certain calls to removeFixup at all, and simplifies its loop test (as a leaf would be possible in the original algorithm in the first iteration only).

KIV's code generator produces the C code contained in this file. All code in subfolders except string/to_string.c is generated, the main algorithms are in asm/rbtree.c. The toplevel contains a Makefile for building the generated C code. The archive also contains a recursive (non-verified) implementation (asm/rrbtree.c) that was generated from KIV models realizing the algorithm used by [Zhan18] to evaluate the Auto2 prover (our implementation is an adaption of the imperative version published in the Isabelle AFP). Making will create a program 'bench' from 'main.cpp' that can be run to execute some performance tests, which show that the KIV code has run times very similar to the C++ code (and runs faster than the recursive implementation).

The general approach for splitting up the correctness proof into two parts is described in [Rbtree22] (submitted; a copy can be obtained by mailing the authors) and it is assumed the reader has already understood the basic idea. Here we give a more technical description of the specifications:

The effort to do the case study was ca. 4 person months for two students that had participated in our course on KIV. A first student needed 2 months to set up the specifications and to verify the first refinement except remove. A second student needed another two months to verify remove and the second refinement.

Bibliography

[Rbtree22] G. Schellhorn, S. Bodenmüller, M. Bitterlich, W. Reif
Separating Separation Logic - Modular Verification of Red-Black Trees
accepted at VSTTE 2022
[Cormen09] T. Cormen, C. Leiserson, R. Rivest, C. Stein
Introduction to Algorrithms, Third Edition, MIT 2009
[Zhan18] B. Zhan
Efficient Verification of Imperative Programs Using Auto2
Proc. of TACAS 2018

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.


[Imprint] [Data Privacy Statement]