Abstraction-guided Runtime Checking of Assertions on Lists

We investigate ways to specify and check, at runtime, assertions that express properties of dynamically manipulated linked-list data structures. Checking an assertion involving whether pointers point to a valid linked list and separation 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 orders 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.

Joint work with Garg, P., Pek, E. and Madhusudan, P.

Alex Gyori is a second year PhD student in Computer Science at the University of Illinois at Urbana Champaign. His research interests are at the intersection of Software Engineering, Formal Methods, and Programming Languages; his main goal is to design automated techniques that improve software reliability and programmer productivity. His research so far has explored Regression Testing, Runtime Assertion Checking for Separation Logic, and Program Transformations. He was awarded the Saburo Muroga Fellowship(2014) and the General Electric Foundation Scholar Leaders Award(2011). He interned at Google(2014), ITI(2012) and Continental AG(2011, 2010). Alex has a BS(2013) in Computer Science from The Polytechnic University of Timisoara, Romania.

Hosted jointly with Philippa Gardner’s group.