A discipline for program verification based on backpointers and its use in observational disjointness

Abstract

In the verification of programs that manipulate the heap, logics that emphasize localized reasoning, such as separation logic, are being used extensively. In such logics, state conditions may only refer to parts of the heap that are reachable from the stack. However, the correct implementation of some data structures is based on state conditions that depend on unreachable locations. For example, reference counting depends on the invariant that "the number of nodes pointing to a certain node is equal to its reference counter". Such conditions are cumbersome or even impossible to formalize in existing variants of separation logic. In the first part of this paper, we develop a minimal programming discipline that enables the programmer to soundly express backpointer conditions, i.e., state conditions that involve heap objects that point to the reachable part of the heap, such as the above-mentioned reference counting invariant. In the second part, we demonstrate the expressiveness of our methodology by verifying the implementation of concurrent copy-on-write lists (CCoWL). CCoWL is a data structure with observational disjointness, i.e., its specification pretends that different lists depend on disjoint parts of the heap, so that separation logic reasoning is made easy, while its implementation uses sharing to maximize performance. The CCoWL case study is a very challenging problem, to which we are not aware of any other solution. © 2013 Springer-Verlag.