Reducing Lookups for Invariant Checking

In this project we developed a simple algorithm to simplify boolean expressions and we used it in a case study for Google Maps for optimizing its invariant checking mechanism.

Coq Source Code

The Coq source code is available online.  More information about the structure of the Coq source code and how to compile it can be found in the README file.

Research paper

"Reducing Lookups for Invariant Checking" with  Christian ClausenKristoffer Andersen,  John Danaher (Google), & Erik Ernst. In proceedings of ECOOP'13: European Conference on Object-Oriented Programming. : [ paper ]

Abstract

This paper helps reduce 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 satisfied. 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 simplifies a representation of the invariant, along with a mechan- ically verified 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 a factor of thirty performance improvement using this algorithm in a case study.