Abstraction-guided Runtime Checking of Assertions on Lists

Abstract. We investigate ways to specify and check, at runtime, assertions that express properties of dynamically manipulated linked-list data structures. Check-ing an assertion involving whether pointers point to a valid linked list and sepa-ration properties of these lists typically requires linear or even quadratic time on the size of the heap. Our main contribution is a way to scale this checking by or-ders of magnitude, using a novel idea called abstraction-guided runtime checking, whereby we maintain an accurate abstraction of the dynamic heap by utilizing the evolving runtime state, and where the abstraction helps in checking the runtime assertions much faster. We develop this synergistic combination of abstractions and runtime checking for lists, list-segments, and their separation, implement it, and show the tremendous performance gains it yields. In particular, when lists are manipulated using library functions, maintenance of the abstraction is within the libraries and yields constant runtime checking of assertions in the client code. We show that, as the number of assertions get frequent and the data structures get large, abstraction-guided runtime checking, which includes maintenance of the abstraction and the runtime checks, gives close to constant-time per assertion overhead in practice.