CSAIL Research Abstracts - 2005 link to http://publications.csail.mit.edu/abstracts/abstracts05/index.html link to http://www.csail.mit.edu
bullet Introduction bullet Architecture, Systems
& Networks
bullet Language, Learning,
Vision & Graphics
bullet Physical, Biological
& Social Systems
bullet Theory bullet

horizontal line

Specification-Based Data Structure Repair

Brian Demsky & Martin C. Rinard

Introduction

To correctly represent the information that a program manipulates, its data structures must satisfy key consistency constraints. If a software error or some other anomaly causes the data structures to become inconsistent, the basic assumptions under which the software was developed no longer hold. In this case, the software typically behaves in an unpredictable manner and may even fail catastrophically.

Our work explores a new approach for attacking the data structure inconsistency problem [1]. Instead of attempting to increase the reliability of the code that manipulates the data structures, our system accepts a specification of key data structure consistency constraints. It then dynamically detects and repairs data structures that violate these constraints. Our goal is not necessarily to restore the data structures to the state in which a hypothetical correct program would have left them (although in some cases our system may do this). Our goal is instead to deliver repaired data structures that satisfy the basic consistency assumptions of the program, enabling the program to continue to operate successfully within its designed operating envelope. We have identified two kinds of data structures that are especially appropriate for this approach: 1) long-lived, persistent data structures (such as file systems, application data files, or serialized data structures), and 2) data structures for critical systems in which continued operation even in the face of errors is a paramount concern.

Approach

Our approach involves two data structure views: a concrete view at the level of the bits in memory and an abstract view at the level of relations between abstract objects. The abstract view facilitates both the specification of higher level data structure constraints (especially constraints of linked data structures) and the reasoning required to repair any inconsistencies.

Each specification contains a set of model definition rules and a set of consistency constraints. Given these rules and constraints, our tool automatically generates algorithms that build the model, inspect the model and the data structures to find violations of the constraints, and repair any such violations.

Experience

We have used our tool to repair inconsistencies in three applications: a simplified Linux file system, an interactive game, and Microsoft Word files. In this context, we have used our tool to repair bitmaps identifying free and allocated disk blocks, correct reference counts, eliminate inappropriate sharing in linked data structures, correct illegal values stored in arrays, resolve inconsistencies in correlated values stored in different data structures, and ensure that recorded data structure sizes match the size of the corresponding actual data structure. In addition to these repairs, our tool is also able to correct out of bounds pointers in linked data structures, repair incomplete data structures by allocating and linking in new structures, repair back links (such as parent pointers in trees) in linked data structures, and enforce inequality constraints between multiple values.

We found that the specifications for our applications were relatively straightforward to develop once we understood the underlying data structures and that the automatically generated repair algorithms were able to produce data structures that enabled the corresponding programs to continue to operate successfully. In the absence of this repair, the programs usually failed. Our results therefore indicate that our technique may significantly enhance the ability of applications to recover from data structure errors.

Contributions

This research makes the following contributions:

  • Specification-Based Approach: It introduces the concept of using specifications for the automatic detection and repair of inconsistent data structures. It also introduces the concept of using an abstract model of the data structures to facilitate specification development and reasoning in the repair algorithm.
  • Inconsistency Detection and Repair System: It presents an implemented system and algorithms that, given a specification, automatically detect and repair violations of the specification.
  • Experience: It presents our experience using our tool for several applications. This experience indicates that it is relatively straightforward to develop the consistency conditions and that the use of our tool enhanced the ability of the applications to continue to operate in the face of errors.
Research Support

This research was supported in part by a fellowship from the Fannie and John Hertz Foundation, DARPA Contract F33615-OO-C-1692, NSF Grant CCROO-86154, and NSF Grant CCROO63513.

References

[1] Brian Demsky and Martin C. Rinard. Automatic detection and repair of errors in data structures. In 18th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, October 2003.

[2] Brian Demsky and Martin C. Rinard. Data Structure Repair Using Goal-Directed Reasoning. To appear in Proceedings of the 2005 International Conference on Software Engineering, May 2005.

horizontal line

MIT logo Computer Science and Artificial Intelligence Laboratory (CSAIL)
The Stata Center, Building 32 - 32 Vassar Street - Cambridge, MA 02139 - USA
tel:+1-617-253-0073 - publications@csail.mit.edu
(Note: On July 1, 2003, the AI Lab and LCS merged to form CSAIL.)