Information Technology Reference
In-Depth Information
sig
LinkedList
{
1
header :
lone
Node ,
2
header ' :
lone
Node
}
3
s i g
Node
{
4
next :
lone
Node ,
5
next ' :
lone
Node
}
6
pred
repOk( l :
LinkedList)
{
//
class
invariant
of
LinkedList
7
l . header.
∗
next
|
n!inn.ˆnext
}
all
n:
//
acyclicity
8
pred
add postcondition( This :
LinkedList ,
n:
Node)
{
9
repOk [ This ]
10
This . header .
∗
next
+ n =
This . header '.
∗
next '
}
11
Listing 1.2.
Alloy specification for the
addLast
method
action required to break the cycle is the same, no matter how many nodes are present in
the list. Indeed, it is enough to set the
next
pointer of the last node to
null
.
Our key insight is to abstract out repair actions and use them as possible repair action
candidates in the future, before opting into searching the state space. The idea is that
if an error in the data structure is due to a fault in software or hardware, a similar
error may occur again, for example when the same buggy code segment is executed
again or when the same faulty memory location is accessed again. Repair abstractions
capture the essence of how certain data structure corruptions are repaired by specific
actions of a data structure repair routine, such as Cobbler [23], Juzi [8], PBnJ [27] or
any other repair framework. Conceptually, a repair abstraction is a tuple
(condition;
action)
where action is an abstract repair action performed when condition is met on a
program state that needs repair.
Consider the example of repairing the faulty output of
addLast
shown in Fig 1 (a).
The concrete repair action suggested by any repair framework should include the as-
signment
N
1
.next = null
. We abstract out this concrete repair action to the ab-
stract action
[LAST NODE](in post-state).next = null
. Suppose that a
similar error occurs again, now on a list of 500 nodes as shown in Fig 1 (b). Before
starting to search the state space of correct data structures, we first try the previous ab-
straction in the hope of finding a quick fix. Concretizing the abstract repair action on
the current data structures gives
N
500
.next = null
which is a correct fix.
Repair abstractions offer two key advantages. One, they allow summarizing concrete
repair actions into intuitive descriptions of how certain errors in data structures were
fixed, which helps users understand and debug faulty program behaviors (when the
errors in state were due to bugs in code). Two, they allow a direct reuse of repair actions
without the need for a systematic exploration of a large number of data structures when
the same error appears in a future program execution. The cost of repair, in cases that
we do perform a search, will now be amortized over many repairs.
3
DREAM Framework
In this section, we explain the fundamentals of DREAM in abstracting and reusing
repair actions. DREAM sits on top of an external data structure repair framework
(Fig. 2). When a data structure repair framework is in place, specifications are periodi-
cally checked to make sure that data structure invariants and/or method post-conditions
