Information Technology Reference
In-Depth Information
public
class
Example {
1
public
static
void
main( String
args []) {
2
LinkedList
l
= new
LinkedList() ;
3
l . header = new
Node ( ) ;
4
Node
n
= new
Node ( ) ;
5
n . next
= n ;
6
l . addLast(n); }}
7
LinkedList {
class
8
Node
header ;
9
void
addLast(Node n)
{
10
Node newN =
n . c l o n e ( ) ;
11
if
( header ==
null )
{
12
header = newN;
13
}
else
{
14
Node
pointer
=
header . next ;
15
Node
prevPointer
=
header ;
16
while ( pointer
!=
null )
{
17
pointer
=
pointer . next ;
18
prevPointer
=
prevPointer . next ;
}
19
prevPointer . next
= newN;
}}}
20
class
Node {
21
Node
next ;
22
protected
Node
c l o n e ( ) {
23
... }}
24
Listing 1.1. Motivating example: erroneous Singly Linked List addLast method
next
next
header
next
header
next
next
next
...
N 0
N 1
N 0
N 1
N 500
(a)
(b)
Fig. 1. The output of the method of Listing 1.1 on an initial list of (a) one and (b) 500 node(s)
those specifications to check and repair data structures. In addition to data structure in-
variant specifications supported by most repair frameworks [8, 13, 17, 23, 24, 27], some
data structure repair frameworks [23, 24, 27] support pre- and post-conditions of pro-
gram methods too. As an example of specifications, Listing 1.2 displays the invariant
(commonly called repOK [18]) of Singly Linked List and a partial post-condition of the
addLast method in the Alloy [14] specification language 1 . When repair is triggered
on the faulty data structures of Fig. 1, it enforces this specification by breaking the cycle
and setting the next pointer of the last node to null .
Most data structure repair frameworks [8, 13, 17, 23, 24, 27] instantiate a search in
the space of valid data structures to find a close and correct data structure to replace the
faulty one. This search poses a major challenge to scalability of data structure repair,
as the size of the state space increases exponentially with the size of the data structure.
For example, our previous work Cobbler [23] uses a combination of SAT solvers and
heuristics for data structure repair. While Cobbler can break the cycle and repair the
faulty list in Fig. 1 (a) in few hundred milliseconds, it runs out of heap space and a time
out of 500 seconds when there are 500 nodes in the list (Fig. 1 (b)). Yet, the conceptual
1
We use the syntactic sugar of adding back-tick (' ' ') to distinguish post-state from pre-state in
this Alloy specification. More details on Alloy specifications can be found elsewhere [14, 23].
Search WWH ::




Custom Search