Hal Wasserman
Manuel Blum
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.
- ALON, N., SPENCER, J., AND ERD6S, P. 1992. The Probabilistic Method. Wiley, New York.Google Scholar
- AR, S., BLUM, M., CODENOTTI, B., AND GEMMELL, P. 1993. Checking approximate computations over the reals. In Proceedings of the 25th Annual ACM Symposium on the Theory of Computing (San Diego, Calif., May 16-18). ACM, New York, pp. 786-795. Google Scholar
- 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.Google Scholar
- BABAI, L., FORTNOW, L., AND LUND, C. 1991. Non-deterministic exponential time has two-prover interactive protocols. Comput. Comp. 1, 1, 3-40.Google Scholar
- BABAI, L., AND FORTNOW, L. 1991. Arithmetization: a new method in structural complexity theory. Comput. Comp. 1, 1, 41-46.Google Scholar
- BABAI, L., FORTNOW, L., LEVIN, L., AND SZEGEDY, M. 1991. Checking computations in polylogarithmic time. In Proceedings of the 23rd Annual ACM Symposium on the Theory of Computing (New Orleans, La., May 6-8). ACM, New York, pp. 21-31. Google Scholar
- BEAVER, D., AND FEIGENBAUM, J. 1990. Hiding instances in multioracle queries. In Proceedings of the 7th Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 415, Springer-Verlag, New York, pp. 37-48. Google Scholar
- BEIGEL, R., AND FEIGENBAUM, J. 1992. On being incoherent without being very hard. Comput. Comp. 2, 1, pp. 1-17. Google Scholar
- BENTLEY, J. 1986. Programming Pearls. Addison-Wesley, Reading, Mass. Google Scholar
- BLUM, M. 1988. Designing programs to check their work. International Computer Science Institute Tech. Report TR-88-009.Google Scholar
- BLUM, M., EVANS, W., GEMMELL, P., KANNAN, S., AND NAOR, M. 1994. Checking the correctness of memories. Algorithmica 12, 2-3, 225-244.Google Scholar
- BLUM, M., AND KANNAN, S. 1989. Designing programs that check their work. In Proceedings of the 21st Annual ACM Symposium on the Theory of Computing (Seattle, Wash., May 15-17). ACM, New York, pp. 86-97. Google Scholar
- BLUM, M., LUBY, M., AND RUBINFELD, R. 1993. Self-testing/correcting with applications to numerical problems: J. Comput. Syst. Sci. 47, 3, 549-595. Google Scholar
- BLUM, M., AND WASSERMAN, H. 1996. Reflections on the Pentium division bug. IEEE Trans. Comput. 45, 4, 385-393. Google Scholar
- BOETTcHER, C., AND MELLEMA, D.J. 1995. Program checkers: Practical applications to real-time software. Test Facility Working Group Conf.Google Scholar
- BUTLER, R., AND FINELLI, G. 1993. The infeasibility of quantifying the reliability of life-critical real-time software. IEEE Trans. Sofiw. Eng. 19, 1, 3-12. Google Scholar
- CLEVE, R., AND LUBY, M. 1990. A note on self-testing/correcting methods for trigonometric functions. International Computer Science Institute Tech. Report 90-032.Google Scholar
- ERGON, F. 1995. Testing multivariate linear functions: Overcoming the generator bottleneck. In Proceedings of the 27th Annual ACM Symposium on the Theory of Computing (Las Vegas, Nev., May 29-Jun. 1). ACM, New York, pp. 407-416. Google Scholar
- FORTNOW, L., AND SIPSER, M. 1988. Are there interactive protocols for co-NP languages? Inf. Proc. Lett. 28, 5, 249-251. Google Scholar
- 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.Google Scholar
- GEMMELL, P., LIPTON, R., RUBINFELD, R., SUDAN, M., AND WIGDERSON, A. 1991. Self-testing/ correcting for polynomials and for approximate functions. In Proceedings of the 23rd Annual ACM Symposium on the Theory of Computing (New Orleans, La., May 6-8). ACM, New York, pp. 32-42. Google Scholar
- GEMMELL, P., AND SUDAN, M. 1992. Highly resilient correctors for polynomials. Inf. Proc. Lett. 43, 4, 169-174. Google Scholar
- 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.Google Scholar
- KANNAN, S. 1990. Program result-checking with applications. Ph.D. dissertation. Computer Science Division. University of California, Berkeley, Berkeley, Calif.Google Scholar
- LIPTON, R. 1990. Efficient checking of computations. In Proceedings of the 7th Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 415. Springer- Verlag, New York, pp. 207-215. Google Scholar
- LIPTON, R. 1991. New directions in testing, distributed computing and cryptography. DIMACS Series Disc. Math. Theoret. Comput. Sci. 2, 191-202.Google Scholar
- LUND, C., FORTNOW, L., KARLOFF, H., AND NISAN, N. 1992. Algebraic methods for interactive proof systems. J. ACM 39, 4, 859-868. Google Scholar
- 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.Google Scholar
- NISAN, N. 1989. Co-SAT has multi-prover interactive proofs, e-mail message.Google Scholar
- RAVIKUMAR, S., AND SIVAKUMAR, D. 1995. On self-testing without the generator bottleneck. In Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science. pp. 248-262. Google Scholar
- RUBINFELD, R. 1990. A mathematical theory of self-checking, self-testing, and self-correcting programs. Ph.D. dissertation. Computer Science Division, University of California, Berkeley, Berkeley, Calif. Google Scholar
- RUBINFELD, R. 1992. Batch checking with applications to linear functions. Inf. Proc. Lett. 42, 2, 77-80. Google Scholar
- 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.Google Scholar
- RUBINFELD, R., AND SUDAN, M. 1992. Self-testing polynomial functions efficiently and over rational domains. In Proceedings of the 3rd ACM-SIAM Symposium on Discrete Algorithms. (Orlando, Fla., Jan. 27-29). ACM, New York, pp. 23-32. Google Scholar
- RUBINFELD, R., AND SUDAN, M. 1996. Robust characterizations of polynomials with applications to program testing. SIAM J. Comput. 25, 2, 252-271. Google Scholar
- SCHWARTZ, J. 1980. Fast probabilistic algorithms for verification of polynomial identities. J. ACM 27, 4, 701-717. Google Scholar
- SHAMIR, A. 1990. IP = PSPACE. In Proceedings of the 31st Annual IEEE Symposium on Foundations of Computer Science. IEEE, New York, pp. 11-15.Google Scholar
- VAINSTEIN, F. 1991. Error detection and correction in numerical computations by algebraic methods. In Proceedings of the 9th International Symposium on Applied Algebra, Algebraic Algorithms and Error-Correcting Codes. Lecture Notes in Computer Science, vol. 539. Springer-Verlag, New York, pp. 456-464. Google Scholar
- VAINSTEIN, F. 1993. Algebraic methods in hardware/software testing. Ph.D. dissertation. EECS Department, Boston University, Boston, Mass. Google Scholar
- VALIANT, L. 1979. The complexity of computing the permanent. Theoret. Comput. Sci. 8, 2, 189-201.Google Scholar
- 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.Google Scholar
- YAO, A. 1990. Coherent functions and program checkers. In Proceedings of the 22nd AnnualACM Symposium on the Theory of Computing (Baltimore, Md., May 14-16). ACM, New York, pp. 84-94. Google Scholar
Index Terms
- Software reliability via run-time result-checking
Recommendations
Program result-checking: a theory of testing meets a test of theory
SFCS '94: Proceedings of the 35th Annual Symposium on Foundations of Computer ScienceWe 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 reliable functionality. We consider how to modify ...
Reflections on the Pentium Division Bug
We review the field of result-checking and suggest that it be extended to a methodology for enforcing hardware/software reliability. We thereby formulate a vision for "self-monitoring" hardware/software whose reliability is augmented through embedded ...
Integrating Software Testing and Run-Time Checking in an Assertion Verification Framework
ICLP '09: Proceedings of the 25th International Conference on Logic ProgrammingWe present a framework that unifies unit testing and run-time verification (as well as static verification and static debugging). A key contribution of our overall approach is that we preserve the use of a unified assertion language for all of these ...
Reviews
Jaak Tepandi
The approach to runtime result-checking presented in this paper is based on three main ideas. The first is the asymmetry of many functions with respect to their inverse from the computational complexity point of view. This asymmetry is widely used, for example, in public-key encryption systems, and can be exploited to check the result of a computation. The second idea is to use random values to generate multiple versions of the same result. These multiple values can then be compared, in order to select the majority answer. Repetition of this process can lead to an arbitrarily small probability of error. The third idea is to use stored randomness to reduce computing time. The authors begin with an overview of result-checking and its applications, proceed with a nontrivial case study on checking real-number linear transformations, and finish by stating conclusions. The key ideas are well presented and fully detailed, and the examples are realistic. The authors consider several problems of checker-based debugging, such as performance loss, real number issues, and testing checkers. I would add that the area of direct application of checkers seems to be limited to well-defined functions and that the formal machinery for justifying and implementing the checkers is complex. The complexity level is comparable to that used in formal verification, although the methodology itself is different. But who has said that things must be simple__?__ The paper presents an inventive combination of ideas and may provide useful hints for many researchers and engineers in the fields<__?__Pub Caret> of software, hardware, or reliability.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments