Information Technology Reference
In-Depth Information
Ta b l e 1 .
Description of the Singly Linked List errors used for experimental evaluation
Err. # Description
1
Sets the header to null
2
Fails to update the size
3
Deletes a node with a non-matching element
4
Introduces a cycle after performing correct remove
5
Breaks the list to retain only the first two nodes
6
Deletes the matching element but adds it again
7
Fails to remove the element and updates the size incorrectly
8
Fails to remove the element
9
Fails to update the size because of a missing left hand side in an assignment
5.1
Evaluation: DREAM with Alloy Back-End
We used our tool Cobbler, a data structure repair framework that utilizes SAT and
heuristics, for the first set of experiments with DREAM. In order to improve the per-
formance of SAT solving for data structure repair, Cobbler iteratively calls SAT and
gradually increases the size of the search space. To guesstimate the size of the search
space (i.e., to find out which fields it should include for a possible change when calling
SAT), Cobbler uses program execution history, obtained via reads and writes performed
to the heap, as a source of identifying corrupt fields of data structures and fixes for them.
Furthermore, it uses unsatisfiable cores that SAT solvers provide after a failing call, to
further prune the search space.
The first data structure we looked at was a basic Singly Linked List that also keeps its
size. To minimize threats to validity, we used independently written errors we used to
evaluate Cobbler in our previous work [23]. In that work, we included seven erroneous
remove methods for Singly Linked List. We used the same seven errors plus two new
ones here. Table 1 shows the errors and a brief description of each of them. Some of the
errors violate the invariants of Singly Linked List (e.g., Error 4), some violate the post-
condition of the remove method (e.g., Error 1), and some violate both (e.g., Error 7).
We started by repairing a Singly Linked List of ten nodes. Upon the very first error,
no repair abstraction is available, so DREAM has to use the underlying repair routine
which is Cobbler here. Then DREAM abstracts out the set of concrete repair actions
taken by Cobbler and memorizes them for future use. In the next experiment, we used
a Singly Linked List of 500 nodes with each error. DREAM applies the abstract repair
actions which fix the problem without calling Cobbler in 8 out of 9 errors. Table 2 shows
the abstractions that DREAM extracted for each error. Some abstractions, e.g., the first
and second abstraction for Error 9, are unnecessary but harmless since they change now
unreachable nodes. These unnecessary actions exist because SAT suggested them as
concrete repair actions.
Table 3 displays the time performance of Cobbler repairing lists of size 10 and 500, as
well as DREAM repairing the same lists. For the case of calling Cobbler, an initial call is
made to SAT to discover the problem and trigger repair (the check column in Table 3).
Hence, the total time for repair with Cobbler includes the initial check time plus the
