Reducing Lookups for Invariant Checking
Venue
Proceedings of ECOOP 2013 (to appear)
Publication Year
2013
Authors
Jakob G. Thomsen, Christian Clausen, Kristoffer J. Andersen, Erik Ernst, John Danaher
BibTeX
Abstract
This paper helps reducing the cost of invariant checking in cases where access to
data is expensive. Assume that a set of variables satisfy a given invariant and a
request is received to update a subset of them. We reduce the set of variables to
inspect, in order to verify that the invariant is still satised. We present a
formal model of this scenario, based on a simple query language for the expression
of invariants that covers the core of a realistic query language. We present an
algorithm which simplies a representation of the invariant, along with a mechan-
ically veried proof of correctness. We also investigate the underlying invariant
checking problem in general and show that it is co-NP hard, i.e., that solutions
must be approximations to remain tractable. We have seen more than an order of
magnitude performance improvement using these techniques in a case study
