DITTO: Automatic Incrementalization of Data Structure InvariantChecks (in Java)AbstractModern languages have constricted many classes of programmingerrors, such as memory and type errors. As a result, algorithmic andsemantic errors now present a proportionally greater challenge dur-ing the development cycle. Many static tools exist to track down sucherrors, but data structure bugs, an important class of semantic bugs,resist these tools because scalable heap analysis is very challenging.Dynamic solutions do not fare much better, as user-written or au-tomatically generated data structure invariant checks are often pro-hibitively slow, commonly incurring at least a ten-fold slowdown.We present DITTO, an automatic incrementalizer for read-onlydata structure invariant checks in modern imperative languages likeJava and C#; such checks include verifying the properties of a red-black tree or that the elements in each bucket of a hash have the righthash code. Incrementalization speeds up function execution by usingprevious execution results and only performing anew the portions ofcomputation that correspond to new input. DITTO exploits propertiesspecific to invariant checks to automate and simplify the processwithout constraining the kinds of mutations that can be performed.The source-to-source implementation of DITTO, for Java, is auto-matic, portable, and efficient, providing speedups on data structureswith as few as 100 elements. On larger data structures, it providesthe asymptotic speedups characteristic of incrementalizers, roughly5x at n=5000 and growing linearly with n thereafter.1. IntroductionModern imperative languages such as Java and C# contain a numberof powerful features: automatic memory management, a strong typesystem, and dynamic type, pointer, and bounds checks. These fea-tures reduce or eliminate many types of programming errors, suchas buffer overflows and doubly-freed memory. As a result, algorith-mic and semantic errors present a proportionately greater challengeduring the development cycle.One such class are data structure bugs. Many data structuresrespect high-level invariants not expressible in the base language,such as “the elements of this list are ordered”, “no elements in thispriority queue can be in that priority queue”, or “in a red-black tree,the number of black nodes on any path from the root node to a leafis the same”. Because the heap is persistent over the course of anexecution and globally accessible, bugs that violate these invariantsmay only expose themselves long after the buggy lines of code havebeen executed.Research in static analysis and verification has provided preemp-tive solutions to a number of algorithmic and semantic problems, butdata structure bugs are particularly difficult for static tools to tacklebecause scalable static heap analysis is very challenging. As a result,with current technology, invariants either require extensive annota-tions to verify statically, or are simply unverifiable.Another approach is to execute the invariant checks. Becausethey operate on the concrete data structure, such dynamic checks arePermission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.Copyrightc ACM [to be supplied]. . .$5.00often simple to write and easy to validate. This approach has gainedsupport recently with tools like jmlc [5] that aid in creating suchchecks.However, dynamic checks can slow a program down tremen-dously, hindering the development process. Since checks are exe-cuted frequently and commonly traverse an entire data structure,a program with checks may easily run 10-100 times slower, pro-hibitively slow for all but the most patient programmer. Conse-quently, dynamic checks are rarely employed, even in debugging.This paper introduces DITTO, an optimizer for a class of dy-namic data structure invariant checks written in modern imperativelanguages like Java and C#. These checks can be written in the lan-guage itself by a programmer, or generated by a tool. DITTO auto-matically incrementalizes such checks, rewriting them (with the aidof a support library) so that they only re-check the parts of a datastructure that have been modified since the last check. These incre-mental checks can run linearly faster than the original (10x or moreat 10000 elements), rendering them practical in a development envi-ronment.Incrementalization modifies an algorithm to compute anew onlyon changed data, ideally reusing existing computation results when-ever possible. Traditionally, incrementalization has been designedand implemented by hand for algorithms where reuse was prof-itable [19]. An algorithm was modified to be aware of modificationsas well as to cache and reuse its previous results.While hand-incrementalization of invariant checks can pro-duce the desired speedups, manual incrementalization has severalpractical limitations. First, the programmer may overlook possi-ble modifications to the data structure (as in the infamous Java 1.1getSigners() bug [10]) and thus omit necessary incremental up-dates. This would result in incorrect invariant checks that may fail todetect violations of checked invariants. Next, some invariant checksmay be difficult to incrementalize by hand. For example, after someeffort, we gave up on incrementalizing red-black tree invariants.Furthermore, having to optimize checks manually does not appeareconomical: programmers may want to develop a large number ofsmall checks and optimizing each seems prohibitive. Programmersmay also want to obtain an efficient check rapidly, for example whenwriting custom checks to serve as data breakpoints for explainingsymptoms of a bug. Most importantly, perhaps, the complexity ofmaintaining incremental code scattered throughout the program maybe harder than verifying correctness of the original data structure,which defeats the purpose of relying on invariant checks that aresimple and thus correct by inspection.Recent research by Acar, et al [1] developed a powerful general-purpose framework for incrementalization, based on memoizationand change propagation. The framework provides an efficient incre-mentalization mechanism while