Precisely reasoning about internal pointers in containers

What is it about?

This paper is about how to specify container APIs that temporarily expose internal pointers to the outside, and to verify programs that use these APIs. We present logical pinning, a lightweight borrowing model for sequential programs that allows users to selectively track container-internal pointers at the logical level. Because it only changes the way representation predicates and specifications are written, our approach is compatible with most separation logic variants.

Featured Image

Photo by Joanna Kosinska on Unsplash

Photo by Joanna Kosinska on Unsplash

Why is it important?

Most separation logics hide container-internal pointers for modularity. This makes it difficult to specify container APIs that temporarily expose those pointers to the outside, and to verify programs that use these APIs. We demonstrate the practicality of logical pinning by verifying small but representative pointer-manipulating programs, and deriving more precise versions of common container specifications. In doing so, we show that our approach subsumes some well-known proof patterns, simplifies some complex proofs, and enables reasoning about program patterns not supported by traditional specifications. All of our results are mechanized in the Rocq proof assistant, using the CFML library.