data strutcher

ABSTRACT
Data structure repair is a promising technique for enabling
programs to execute successfully in the presence of otherwise
fatal data structure corruption errors. Previous research in
this field relied on the developer to write a specification to
explicitly translate model repairs into concrete data structure
repairs, raising the possibility of 1) incorrect translations
causing the supposedly repaired concrete data structures
to be inconsistent, and 2) repaired models with no
corresponding concrete data structure representation.
We present a new repair algorithm that uses goal-directed
reasoning to automatically translate model repairs into concrete
data structure repairs. This new repair algorithm eliminates
the possibility of incorrect translations and repaired
models with no corresponding representation as concrete
data structures.
Categories and Subject Descriptors
D.2.5 [Software Engineering]: Testing and Debugging;
D.3.3 [Programming Languages]: Language Constructs
and Features
General Terms
Design, Languages, Reliability
Keywords
Data Structure Repair, Data Structure Invariants
computer science engineering
1. INTRODUCTION
Programs usually assume that the data structures that
they manipulate are consistent. A software error or some
other event may cause the data structures to become inconsistent.
Data structure repair is a useful technique that can
This research was supported in part by a fellowship from
the Fannie and John Hertz Foundation, DARPA Cooperative
Agreement FA 8750-04-2-0254, DARPA Contract
33615-00-C-1692, the Singapore-MIT Alliance, and the NSF
Grants CCR-0341620, CCR-0325283, and CCR-0086154.
Permission to make digital or hard copies of all or part of this work for
personal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. To copy otherwise, to
republish, to post on servers or to redistribute to lists, requires prior specific
permission .
restore the consistency properties and enable the program
to continue to execute successfully. Our previous work [7]
introduced a model-based approach in which the developer
writes a specification to identify the required data structure
consistency properties.
This model-based approach involves two views: a concrete
view of the data structures as they are represented
in the memory and an abstract view that models the data
structures as sets of objects and relations between objects.
A set of model definition rules translates the concrete data
structures to the sets and relations in the abstract model.
The key consistency constraints are expressed using the sets
and relations in this model. This approach provides several
key benefits: 1) it provides a mechanism for separating objects
that play different conceptual roles in a computation
into different sets — the developer can then specify different
constraints to apply to each of these different sets, 2) the
model definition rules provide a clean, simple mechanism to
specify a traversal of a data structure, and 3) it provides a
means to manage the complexity of data structure consistency
properties — the model definition rules encapsulate
the data structure representation complexity and the model
consistency constraints encapsulate the complexity inherent
in the consistency property. There are three challenges in
making this approach effective: 1) maintaining a correspondence
between the abstract model and the concrete data
structures, 2) generating a set of repairs that is sufficient to
repair any error, and 3) ensuring that all repairs terminate.
Our previous work [7] performed repairs on the abstract
model and relied on a set of user-defined external consistency
constraints to faithfully translate the repaired model state to
the data structures. While this approach automates much of
the repair process, the presence of the external consistency
constraints has several undesirable properties:
• An error in the external consistency constraints may
cause the repair algorithm to incorrectly translate the
model repair to the data structures. In this case the
data structures would remain inconsistent after the repair.
• The repair algorithm may generate abstract models
that cannot be represented as concrete data structures.
To avoid this possibility, the developer may need to
add additional model constraints that prevent the repair
process from constructing such a model.