Software reliability via run-time result-checking

ABSTRACT

We review the field of result-checking, discussing simple checkers and self-correctors. We argue that such checkers could profitably be incorporated in software as an aid to efficient debugging and enhanced reliability. We consider how to modify traditional checking methodologies to make them more appropriate for use in real-time, real-number computer systems. In particular, we suggest that checkers should be allowed to use stored randomness: that is, that they should be allowed to generate, preprocess, and store random bits prior to run-time, and then to use this information repeatedly in a series of run-time checks. In a case study of checking a general real-number linear transformation (e.g., a Fourier Transform), we present a simple checker which uses stored randomness, and a self-corrector which is particularly efficient if stored randomness is employed.

REFERENCES

• 1: ALON, N., SPENCER, J., AND ERD6S, P. 1992. The Probabilistic Method. Wiley, New York.
• 2: S. Ar , M. Blum , B. Codenotti , P. Gemmell, Checking approximate computations over the reals, Proceedings of the twenty-fifth annual ACM symposium on Theory of computing, p.786-795, May 16-18, 1993, San Diego, California, United States [doi>10.1145/167088.167288]
• 3: ARORA, S., AND SAFRA, S. 1992. Probabilistic checking of proofs; a new characterization of NP. In Proceedings of the 33rd Annual IEEE Symposium of Foundations of Computer Science. IEEE, New York, pp. 2-13.
• 4: BABAI, L., FORTNOW, L., AND LUND, C. 1991. Non-deterministic exponential time has two-prover interactive protocols. Comput. Comp. 1, 1, 3-40.
• 5: BABAI, L., AND FORTNOW, L. 1991. Arithmetization: a new method in structural complexity theory. Comput. Comp. 1, 1, 41-46.
• 6: László Babai , Lance Fortnow , Leonid A. Levin , Mario Szegedy, Checking computations in polylogarithmic time, Proceedings of the twenty-third annual ACM symposium on Theory of computing, p.21-32, May 05-08, 1991, New Orleans, Louisiana, United States [doi>10.1145/103418.103428]
• 7: Donald Beaver , J. Feigenbaum, Hiding instances in multioracle queries, Proceedings of the seventh annual symposium on Theoretical aspects of computer science, p.37-48, February 1990, Rouen, France
• 8: Richard Beigel , Joan Feigenbaum, On being incoherent without being very hard, Computational Complexity, v.2 n.1, p.1-17, 1992 [doi>10.1007/BF01276436]
• 9: Jon Bentley, Programming pearls, ACM Press, New York, NY, 1986
• 10: BLUM, M. 1988. Designing programs to check their work. International Computer Science Institute Tech. Report TR-88-009.
• 11: BLUM, M., EVANS, W., GEMMELL, P., KANNAN, S., AND NAOR, M. 1994. Checking the correctness of memories. Algorithmica 12, 2-3, 225-244.
• 12: M. Blum , S. Kanna, Designing programs that check their work, Proceedings of the twenty-first annual ACM symposium on Theory of computing, p.86-97, May 14-17, 1989, Seattle, Washington, United States [doi>10.1145/73007.73015]
• 13: Manuel Blum , Michael Luby , Ronitt Rubinfeld, Self-testing/correcting with applications to numerical problems, Journal of Computer and System Sciences, v.47 n.3, p.549-595, Dec. 1993 [doi>10.1016/0022-0000(93)90044-W]
• 14: Manuel Blum , Hal Wasserman, Reflections on the Pentium Division Bug, IEEE Transactions on Computers, v.45 n.4, p.385-393, April 1996 [doi>10.1109/12.494097]
• 15: BOETTcHER, C., AND MELLEMA, D.J. 1995. Program checkers: Practical applications to real-time software. Test Facility Working Group Conf.
• 16: R. W. Butler , G. B. Finelli, The Infeasibility of Quantifying the Reliability of Life-Critical Real-Time Software, IEEE Transactions on Software Engineering, v.19 n.1, p.3-12, January 1993 [doi>10.1109/32.210303]
• 17: CLEVE, R., AND LUBY, M. 1990. A note on self-testing/correcting methods for trigonometric functions. International Computer Science Institute Tech. Report 90-032.
• 18: Funda Ergün, Testing multivariate linear functions: overcoming the generator bottleneck, Proceedings of the twenty-seventh annual ACM symposium on Theory of computing, p.407-416, May 29-June 01, 1995, Las Vegas, Nevada, United States [doi>10.1145/225058.225167]
• 19: Lance Fortnow , Michael Sipser, Are there interactive protocols for CO-NP languages?, Information Processing Letters, v.28 n.5, p.249-251, Aug. 12, 1988 [doi>10.1016/0020-0190(88)90199-8]
• 20: FREIVALDS, R. 1979. Fast probabilistic algorithms. In Mathematical Foundations of Computer Science. Lecture Notes in Computer Science, vol. 74. Springer-Verlag, New York, pp. 57-69.
• 21: Peter Gemmell , Richard Lipton , Ronitt Rubinfeld , Madhu Sudan , Avi Wigderson, Self-testing/correcting for polynomials and for approximate functions, Proceedings of the twenty-third annual ACM symposium on Theory of computing, p.33-42, May 05-08, 1991, New Orleans, Louisiana, United States [doi>10.1145/103418.103429]
• 22: Peter Gemmell , Madhu Sudan, Highly resilient correctors for polynomials, Information Processing Letters, v.43 n.4, p.169-174, Sept. 28, 1992 [doi>10.1016/0020-0190(92)90195-2]
• 23: GOLDREICH, O., MICALI, S., AND WIGDERSON, A. 1986. Proofs that yield nothing but their validity and a methodology of cryptographic protocol design. In Proceedings of the 27th Annual IEEE Symposium on Foundation of Computer Science. IEEE, New York, pp. 174-187.
• 24: KANNAN, S. 1990. Program result-checking with applications. Ph.D. dissertation. Computer Science Division. University of California, Berkeley, Berkeley, Calif.
• 25: Richard J. Lipton, Efficient checking of computations, Proceedings of the seventh annual symposium on Theoretical aspects of computer science, p.207-215, February 1990, Rouen, France
• 26: LIPTON, R. 1991. New directions in testing, distributed computing and cryptography. DIMACS Series Disc. Math. Theoret. Comput. Sci. 2, 191-202.
• 27: Carsten Lund , Lance Fortnow , Howard Karloff, Algebraic methods for interactive proof systems, Journal of the ACM (JACM), v.39 n.4, p.859-868, Oct. 1992 [doi>10.1145/146585.146605]
• 28: MICALI, S. 1992/1994. CS proofs and error-detecting computation. HIT Lab for Computer Science Tech. Report, 1992, and CS proofs. HIT Lab for Computer Science Tech. Report TM-510, 1994.
• 29: NISAN, N. 1989. Co-SAT has multi-prover interactive proofs, e-mail message.
• 30: Ravi Kumar , D. Sivakumar, On Self-Testing without the Generator Bottleneck, Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science, p.248-262, December 18-20, 1995
• 31: Ronitt A. Rubinfeld, A mathematical theory of self-checking, self-testing and self-correcting programs, University of California at Berkeley, Berkeley, CA, 1991
• 32: Ronitt Rubinfeld, Batch checking with applications to linear functions, Information Processing Letters, v.42 n.2, p.77-80, May 11, 1992 [doi>10.1016/0020-0190(92)90093-B]
• 33: RUBINFELD, R. 1994. On the robustness of functional equations. In Proceedings of the 35th Annual IEEE Symposium on Foundations of Computer Science. IEEE, New York, pp. 288-299.
• 34: Ronitt Rubinfeld , Madhu Sudan, Self-testing polynomial functions efficiently and over rational domains, Proceedings of the third annual ACM-SIAM symposium on Discrete algorithms, p.23-32, September 1992, Orlando, Florida, United States
• 35: Ronitt Rubinfeld , Madhu Sudan, Robust Characterizations of Polynomials withApplications to Program Testing, SIAM Journal on Computing, v.25 n.2, p.252-271, February 1996 [doi>10.1137/S0097539793255151]
• 36: J. T. Schwartz, Fast Probabilistic Algorithms for Verification of Polynomial Identities, Journal of the ACM (JACM), v.27 n.4, p.701-717, Oct. 1980 [doi>10.1145/322217.322225]
• 37: SHAMIR, A. 1990. IP = PSPACE. In Proceedings of the 31st Annual IEEE Symposium on Foundations of Computer Science. IEEE, New York, pp. 11-15.
• 38: Feodor S. Vainstein, Error Detection and Correction in Numerical Computations by Algebraic Methods, Proceedings of the 9th International Symposium, on Applied Algebra, Algebraic Algorithms and Error-Correcting Codes, p.456-464, October 07-11, 1991
• 39: Feodor Vainstein, Algebraic methods in hardware/software testing, Boston University, Boston, MA, 1992
• 40: VALIANT, L. 1979. The complexity of computing the permanent. Theoret. Comput. Sci. 8, 2, 189-201.
• 41: WEGMAN, M., AND CARTER, J. 1981. New hash functions and their use in authentication and set equality. J. Comput. Syst. Sci. 22, 3, 265-279.
• 42: A. C.-C. Yao, Coherent functions and program checkers, Proceedings of the twenty-second annual ACM symposium on Theory of computing, p.84-94, May 13-17, 1990, Baltimore, Maryland, United States [doi>10.1145/100216.100226]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.1 Numerical Algorithms and Problems
          Subjects: Computation of transforms (e.g., fast Fourier transform)
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Reliability, Verification

Keywords:
Fourier transform, built-in testing, concurrent error detection, debugging, fault tolerance, result-checking, self-correcting