This Article 
 Bibliographic References 
 Add to: 
Goal-Directed Reasoning for Specification-Based Data Structure Repair
December 2006 (vol. 32 no. 12)
pp. 931-951
Software errors and hardware failures can cause data structures in running programs to violate key data structure consistency properties. As a result of this violation, the program may produce unacceptable results or even fail. We present a new data structure repair system. This system accepts a specification of data structure consistency properties stated in terms of an abstract set- and relation-based model of the data structures in the running program. It then automatically generates a repair algorithm that, during the execution of the program, detects and repairs any violations of these constraints. The goal is to enable the program to continue to execute acceptably in the face of otherwise crippling data structure corruption errors. We have applied our system to repair inconsistent data structures in five applications: CTAS (an air traffic control system), AbiWord (an open source word processing program), Freeciv (an interactive multiplayer game), a parallel x86 emulator, and a simplified Linux file system. Our results indicate that the generated repair algorithms can effectively repair inconsistent data structures in these applications to enable the applications to continue to operate successfully in cases where the original application would have failed. Without repair, all of the applications fail.

[1] “Center-Tracon Automation System,” http:/www.ctas.arc.nasa. gov/, 2006.
[2] “Changelog in Reiserfsprogs Distribution,” http://ftp.namesys. com/pubreiserfsprogs /, 2006.
[3] “Chkdsk,” documentation/ windows/XP/all/proddocs/en-us chkdsk. mspx?mfr=true, 2006.
[4] “E2fsprogs Release Notes,” http://e2fsprogs.sourceforge.nete2fsprogs-release.html , 2006.
[5] “Ext2 fsck Manual Page,” http:/, 2006.
[6] M. Accetta, R. Baron, W. Bolosky, D. Golub, R. Rashid, A. Tevanian, and M. Young, “Mach: A New Kernel Foundation for UNIX Development,” Proc. USENIX Summer Conf., 1986.
[7] T. Anderson and R. Kerr, “Recovery Blocks in Action: A System Supporting High Reliability,” Proc. Second Int'l Conf. Software Eng., pp. 447-457, 1976.
[8] A. Avizienis, “The Methodology of N-Version Programming,” Software Fault Tolerance, M.R. Lyu, ed., pp. 23-46, Wiley, 1995.
[9] A. Avizienis, J.-C. Laprie, B. Randell, and C. Landwehr, “Basic Concepts and Taxonomy of Dependable and Secure Computing,” IEEE Trans. Dependable and Secure Computing, vol. 1, no. 1, pp. 11-33, Jan.-Mar. 2004.
[10] G. Candea and A. Fox, “Recursive Restartability: Turning the Reboot Sledgehammer into a Scalpel,” Proc. Workshop Hot Topics in Operating Systems (HotOS-VIII), pp. 110-115, May 2001.
[11] S. Ceri, P. Fraternali, S. Paraboschi, and L. Tanca, “Automatic Generation of Production Rules for Integrity Maintenance,” ACM Trans. Database Systems, vol. 19, no. 3, Sept. 1994.
[12] S. Ceri and J. Widom, “Deriving Production Rules for Constraint Maintenance,” Proc. Int'l Conf. Very Large Data Bases, pp. 566-577, 1990.
[13] K. Chandy and C. Ramamoorthy, “Rollback and Recovery Strategies,” IEEE Trans. Computers, vol. 21, no. 2, pp. 137-146, Feb. 1972.
[14] J.C. Corbett, M.B. Dwyer, J. Hatcliff, S. Laubach, C.S. Pasareanu, Robby, and H. Zheng, “Bandera : Extracting Finite-State Models from Java Source Code,” Proc. 22nd Int'l Conf. Software Eng., 2000.
[15] B. Demsky, “Data Structure Repair Using Goal-Directed Reasoning,” PhD thesis, Massachusetts Inst. of Tech nology, Jan. 2006.
[16] B. Demsky and M. Rinard, “Automatic Detection and Repair of Errors in Data Structures,” Proc. 18th Ann. Conf. Object-Oriented Programming Systems, Languages and Applications, Oct. 2003.
[17] B. Demsky and M. Rinard, “Static Specification Analysis for Termination of Specification-Based Data Structure Repair,” Proc. 14th IEEE Int'l Symp. Software Reliability Eng., Nov. 2003.
[18] B. Demsky and M. Rinard, “Data Structure Repair Using Goal-Directed Reasoning,” Proc. 2005 Int'l Conf. Software Eng., May 2005.
[19] E.W. Dijkstra, “Self-Stabilization in Spite of Distributed Control,” Comm. ACM, vol. 17, no. 11, pp. 643-644, 1974.
[20] S. Dolev, Self-Stabilization. MIT Press, 2000.
[21] R. Ghiya and L.J. Hendren, “Is It a Tree, a Dag, or a Cyclic Graph? A Shape Analysis for Heap-Directed Pointers in C,” Proc. 23rd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, 1996.
[22] A.L. Goel, “Software Reliability Models: Assumptions, Limitations, and Applicabity,” IEEE Trans. Software Eng., vol. 11, no. 12, Dec. 1985.
[23] J. Gray and A. Reuter, Transaction Processing: Concepts and Techniques. Morgan Kaufmann, 1993.
[24] T. Griffin, H. Trickey, and C. Tuckey, “Generating Update Constraints from PRL 5.0 Specifications,” Preliminary Report Presented at AT&T Database Day, Sept. 1992.
[25] N.K. Gupta, L.J. Jagadeesan, E.E. Koutsofios, and D.M. Weiss, “Auditdraw: Generating Audits the FAST Way,” Proc. 19th Int'l Conf. Software Eng., 1997.
[26] S. Hallem, B. Chelf, Y. Xie, and D. Engler, “A System and Language for Building System-Specific, Static Analyses,” Proc. SIGPLAN '02 Conf. Program Language Design and Implementation, 2002.
[27] G. Haugk, F. Lax, R. Royer, and J. Williams, “The 5ESS(TM) Switching System: Maintenance Capabilities,” AT&T Technical J., vol. 64, no. 6,part 2, pp. 1385-1416, July-Aug. 1985.
[28] R. Hoover, “Incremental Computation as a Programming Abstraction,” Proc. SIGPLAN '92 Conf. Program Language Design and Implementation, 1992.
[29] K. Huang, J. Wu, and E.B. Fernandez, “A Generalized Forward Recovery Checkpointing Scheme,” Proc. 1998 Ann. IEEE Workshop Fault-Tolerant Parallel and Distributed Systems, Apr. 1998.
[30] Y. Huang, C. Kintala, N. Kolettis, and N.D. Fulton, “Software Rejuvenation: Analysis, Module and Applications,” Proc. 25th Int'l Symp. Fault-Tolerant Computing, 1995.
[31] D. Jackson, “Alloy: A Lightweight Object Modeling Notation,” Technical Report 797, Laboratory for Computer Science, Massachusetts Inst. of Tech nology, 2000.
[32] D.A. Ladd and J.C. Ramming, “Two Application Languages in Software Production,” USENIX 1994 Very High Level Languages Symp. Proc., Oct. 1994.
[33] C.-C.J. Li, P. Cheng, and W.K. Fuchs, “Local Concurrent Error Detection and Correction in Data Structures Using Virtual Backpointers,” IEEE Trans. Computers, vol. 38, no. 11, pp. 1481-1492, Nov. 1989.
[34] J. Lions, “Ariane 5 Flight 501 Failure: Report by the Inquiry Board,” 1996.
[35] D. Litman, P.F. Patel-Schneider, and A. Mishra, “Modeling Dynamic Collections of Interdependent Objects Using Path-Based Rules,” Proc. 12th Ann. Conf. Object-Oriented Programming Systems, Languages and Applications, Oct. 1997.
[36] G. Lopez, “The Design and Implementation of Kaleidoscope, a Constraint Imperative Programming Language,” PhD thesis, Univ. of Washington, Apr. 1997.
[37] T. May and M. Woods, “Alpha-Particle-Induced Soft Errors in Dynamic Memories,” IEEE Trans. Electron Devices, vol. 26, no. 1, 2-9 Jan. 1979.
[38] A. Mishra, J.P. Ros, A. Singhal, G. Weiss, D. Litman, P.F. Patel-Schneider, D. Dvorak, and J. Crawford, “R++: Using Rules in Object-Oriented Designs,” Proc. 11th Ann. Conf. Object-Oriented Programming Systems, Languages and Applications, July 1996.
[39] S. Mourad and D. Andrews, “On the Reliability of the IBM MVS/XA Operating System,” IEEE Trans. Software Eng., Sept. 1987.
[40] D. Patterson, A. Brown, P. Broadwell, G. Candea, M. Chen, J. Cutler, P. Enriquez, A. Fox, E. Kcman, M. Merzbacher, D. Oppenheimer, N. Sastry, W. Tetzlaff, J. Traupman, and N. Treuhaft, “Recovery-Oriented Computing (ROC): Motivation, Definition, Techniques, and Case Studies,” Technical Report UCB//CSD-02-1175, Computer Science, Univ. of California Berkeley, Mar. 2002.
[41] J.S. Plank, M. Beck, G. Kingsley, and K. Li, “Libckpt: Transparent Checkpointing Under Unix,” Proc. Usenix Winter Technical Conf., pp. 213-223, Jan. 1995.
[42] “The Unified Modeling Language,” Rational Inc., http://www. rational.comuml, 2006.
[43] M. Rinard, “Probabilistic Accuracy Bounds for Fault-Tolerant Computations that Discard Tasks,” Proc. 20th ACM Int'l Conf. Supercomputing, 2006.
[44] M. Rosenblum and J.K. Ousterhout, “The Design and Implementation of a Log-Structured File System,” Proc. 13th ACM Symp. Operating Systems Principles, Oct. 1991.
[45] P. Shirvani, N.R. Saxena, and E.J. McCluskey, “Software-Implemented EDAC Protection against SEUs,” IEEE Trans. Reliability, vol. 49, no. 3, pp. 273-284, Sept. 2000.
[46] D. Taylor and J. Black, “Principles of Data Structure Error Correction,” IEEE Trans. Computers, vol. 31, no. 7, pp. 602-608, July 1982.
[47] D. Taylor, D. Morgan, and J. Black, “Redundancy in Data Structures: Improving Software Fault Tolerance,” IEEE Trans. Software Eng., vol. 6, no. 6, pp. 585-594, Nov. 1980.
[48] D. Taylor, D. Morgan, and J. Black, “Redundancy in Data Structures: Some Theoretical Results,” IEEE Trans. Software Eng., vol. 6, no. 6, pp. 595-602, Nov. 1980.
[49] D. Taylor, D. Morgan, and J. Black, “A Compendium of Robust Data Structures,” Proc. 11th Int'l Symp. Fault Tolerant Computing, June 1981.
[50] M. Taylor, J. Kim, J. Miller, D. Wentzlaff, F. Ghodrat, B. Greenwald, H. Hoffman, P. Johnson, J.-W. Lee, W. Lee, A. Ma, A. Saraf, M. Seneski, N. Shnidman, V. Strumpen, M. Frank, S. Amarasinghe, and A. Agarwal, “The Raw Microprocessor: A Computational Fabric for Software Circuits and General-Purpose Programs,” IEEE Micro, Mar./Apr. 2002.
[51] S.D. Urban and L.M. Delcambre, “Constraint Analysis: A Design Process for Specifying Operations on Objects,” IEEE Trans. Knowledge and Data Eng., vol. 2, no. 4, Dec. 1990.
[52] E.J. Weyuker, “Using the Consequence of Failures for Testing and Reliability Assessment,” Proc. Third ACM SIGSOFT Symp. Foundations of Software Eng., 1995.
[53] T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard, “Field Constraint Analysis,” Proce. Int'l Conf. Verification, Model Checking, and Abstract Interpratation, 2006.
[54] S.S. Yau and R.C. Cheung, “Design of Self-Checking Software,” Proc. Int'l Conf. Reliable Software, pp. 450-455, 1975.
[55] J.W. Young, “A First Order Approximation to the Optimum Checkpoint Interval,” Comm. ACM, vol. 17, no. 9, pp. 530-531, 1974.
[56] Y. Zhang, D. Wong, and W. Zheng, “User-Level Checkpoint and Recovery for LAM/MPI,” ACM SIGOPS Operating Systems Rev., vol. 39, no. 3, pp. 72-81, 2005.

Index Terms:
Testing and debugging, language constructs and features.
Brian Demsky, Martin C. Rinard, "Goal-Directed Reasoning for Specification-Based Data Structure Repair," IEEE Transactions on Software Engineering, vol. 32, no. 12, pp. 931-951, Dec. 2006, doi:10.1109/TSE.2006.122
Usage of this product signifies your acceptance of the Terms of Use.