Information Technology Reference
In-Depth Information
embody this approach remain computationally expensive and the promise of the ap-
proach remains largely unfulfilled for real applications. The key issue is that finding a
sequence of repair actions, which produces a desired state necessitates trasmuting the
specification into a partial implementation, say using a backtracking search over a large
state space - an inherently complex operation.
This paper introduces
repair abstraction
, a novel mechanism for more efficient data
structure repair. Our key insight is that specific repair actions that are performed to re-
cover from an error may be required again in the future when the same error occurs
again, e.g., when a particular faulty line of code is re-executed to create a new state
with an error similar to the erroneous state created when that line of code was executed
in the past. Conceptually, repair abstraction provide a form of memoization, which cap-
tures the essence of how erroneous program executions in specific error scenarios are
repaired using concrete repair actions and allow replaying similar actions in future,
thereby enabling substantially faster repair of errors that recur.
We make the following contributions:
- Repair abstraction.
We introduce a novel abstraction mechanism - repair abstrac-
tion - for runtime error recovery using data structure repair;
- Abstract repair actions.
We present a representation for abstract repair actions,
which provides the foundations of our work;
- Framework.
We present our framework DREAM (Data structure Repair using Ef-
ficient Abstraction Methods) for repair abstraction. DREAM provides a generic
framework that can be embodied by different data structure repair techniques.
- Embodiment.
We present two techniques that embody DREAM. Our first tech-
nique utilizes specifications in Alloy [14], a first-order, relational language, and its
accompanying SAT-based tool-set. Our second technique utilizes specifications in
Java and an algorithm for solving constraints using Java predicates [3].
- Evaluation.
We present an experimental evaluation using a suite of small programs
that perform intricate operations on the program heap to evaluate the efficacy of
repair abstraction in the context of complex data structure properties. Experimental
results show that the use of repair abstraction enables significantly faster repair than
previous techniques.
2
Running Example: Faulty Singly Linked List
In this section, we provide a motivating example. The example shows how DREAM
efficiently finds and fixes a subtle error and helps the program recover from an otherwise
fatal state. Listing 1.1 shows an implementation of the
addLast
method for a Singly
Linked List data structure in Java. This method, which is supposed to add a node to
the end of a list while maintaining acyclicity, works well when it receives a newly
generated node that has
null
as its
next
pointer. However, it produces a wrong (i.e.,
cyclic) list if provided with an input node that already has a self loop. While the logic
of the implementation is correct, missing to check the input causes an incorrect output.
Such a wrong output list is shown in Fig. 1 (a).
Data structure repair can be utilized to fix this wrong output list and similar erro-
neous states. The basic idea is to augment the program with specifications, and use
