Abstract
Scientific computing poses many challenges to formal verification, including the facts that typical programs: (1) are numerically-intensive, (2) are highly-optimized (often by hand), and (3) often employ parallelism in complex ways. Another challenge is specifying correctness. One approach is to provide a very simple, sequential version of an algorithm together with the optimized (possibly parallel) version. The goal is to show the two versions are functionally equivalent, or provide useful feedback when they are not. We present a new verification suite consisting of pairs of programs of this form. The suite can be used to evaluate and compare tools that verify functional equivalence. The programs are all in C and the parallel versions use the Message Passing Interface. They are simpler than codes used in practice, but are representative of real coding patterns (e.g., manager-worker parallelism, loop tiling) and present realistic challenges to current verification tools. The suite includes solvers for the 1-d and 2-d diffusion equations, Jacobi iteration schemes, Gaussian elimination, and N-body simulation.
Similar content being viewed by others
References
Andrews G.R.: Foundations of Multithreaded, Parallel, and Distributed Programming. Addison-Wesley, Boston (2000)
Barrett, C., Fang, Y., Benjamin, G., Hu, Y., Pnueli, A., Zuck, L.: TVOC: A translation validator for optimizing compilers. In: Etessami, K., Rajamani, S.K. (eds.) Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6–10, 2005, Proceedings of LNCS, vol. 3576, pp. 291–295. Springer, Berlin (2005)
Boldo S., Nguyen T.T.: Hardware-Independent Proofs of Numerical Programs. In: Muñoz, C. (eds) Proceedings of the Second NASA Formal Methods Symposium, pp. 14–23. Number NASA/CP-2010-216215 in NASA Conference Publication, Washington, D.C. (2010)
Cadar, C., Dunbar, D., Engler, D.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of 8th USENIX Symposium on Operating Systems Design and Implementation (2008)
Cousot P., Cousot R., Feret J., Mauborgne L., Miné A., Monniaux D., Rival X. : The ASTRÉE Analyser. In: Sagiv, M. (ed.) (eds) Proceedings of European Symposium on Programming (ESOP’05), LNCS, vol. 3444, pp. 21–30, Springer, Edinburgh (2005)
Emerson, E.A., Vineet, K.: Parameterized model checking of ring-based message passing systems. In: Marcinkowski, J., Tarlecki, A. (eds.) Computer Science Logic, Lecture Notes in Computer Science, vol. 3210, pp. 325–339. Springer, Berlin (2004)
Filliâtre J.-C., Marché C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds) CAV 2007, LNCS, vol. 4590, pp. 173–177, Springer, Berlin (2007)
Goubault, E., Martel, M., Putot, S.: Asserting the precision of floating-point computations: a simple abstract interpreter. In: European Symposium on Programming, LNCS, vol. 2305, pp. 209–212. Springer, Berlin (2002)
Gropp W., Lusk E., Skjellum A.: Using MPI: Portable Parallel Programming with the Message-Passing Interface. MIT Press, Cambridge (1999)
Hatton L.: The T experiments: errors in scientific software. IEEE Comput. Sci. Eng. 4(2), 27–38 (1997)
Isaacson E., Keller H.B.: Analysis of Numerical Methods. John Wiley & Sons, New York (1966)
Krammer B., Müller M.S., Resch M.M.: MPI application development using the analysis tool MARMOT. In: Bubak, M., van Albada, G.D., Sloot, P.M.A., Dongarra, J. (eds) International Conference on Computational Science, LNCS, vol. 3038, pp. 464–471, Springer, UK (2004)
McCabe, T.J.: A complexity measure. IEEE Transactions on Software Engineering, pp. 308–320 (1976)
Message Passing Interface Forum.: MPI: A Message-Passing Interface Standard, version 2.2, September 4, 2009. http://www.mpi-forum.org/docs/ (2009)
Post, D.E., Votta, L.G.: Computational science demands a new paradigm. Physics Today, pp. 35–41 (2005)
Quinn M.J.: Parallel Programming in C with MPI and OpenMP. McGraw-Hill, New York (2004)
Siegel, S.F.: Verifying parallel programs with MPI-Spin. In: Cappello, F., Hérault, T., Dongarra, J. (eds.) Recent Advances in Parallel Virtual Machine and Message Passing Interface, 14th European PVM/MPI User’s Group Meeting, Paris, France, September 30–October 3, 2007, Proceedings of the Lecture Notes in Computer Science, vol. 4757, pp. 13–14. Springer, Berlin (2007)
Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Combining symbolic execution with model checking to verify parallel numerical programs. ACM TOSEM, vol. 17(2), pp. 1–34 (2008)
Siegel, S.F., Zirkel, T.K.: Collective assertions. In: Jhala, R., Schmidt, D. (eds.) Verification, Model Checking, and Abstract Interpretation: 12th International Conference, VMCAI 2011, LNCS, vol. 6538, pp. 387–402 (2011)
Snir M., Otto S., Huss-Lederman S., Walker D., Dongarra J.: MPI—The Complete Reference, vol. 1: The MPI Core, 2nd edn. MIT Press, Berlin (1998)
Vakkalanka, S., Sharma, S.V., Ganesh, G., Kirby, R.M.: ISP: A tool for model checking MPI programs. In: Principles and Practices of Parallel Programming (PPoPP), pp. 285–286 (2008)
Verdoolaege, S., Janssens, G., Bruynooghe, M.: Equivalence checking of static affine programs using widening to handle recurrences. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26–July, 2009, Proceedings of Lecture Notes in Computer Science, vol. 5643, pp. 599–613. Springer, Berlin (2009)
Wilson G.: How do scientists really use computers?. Am Scientist 97, 8–10 (2009)
Author information
Authors and Affiliations
Corresponding authors
Additional information
This material is based upon work supported by the National Science Foundation under Grants CCF-0733035 and CCF-0953210, and by the University of Delaware Research Foundation.
Rights and permissions
About this article
Cite this article
Siegel, S.F., Zirkel, T.K. FEVS: A Functional Equivalence Verification Suite for High-Performance Scientific Computing. Math.Comput.Sci. 5, 427–435 (2011). https://doi.org/10.1007/s11786-011-0101-6
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11786-011-0101-6