FEVS: a functional equivalence verification suite for high-performance scientific computing. (English) Zbl 1264.68066
Summary: 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.
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.
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68N19 | Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) |
| 65D99 | Numerical approximation and computational geometry (primarily algorithms) |
References:
| [1] | Andrews G.R.: Foundations of Multithreaded, Parallel, and Distributed Programming. Addison-Wesley, Boston (2000) |
| [2] | 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) · Zbl 1081.68606 |
| [3] | 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) |
| [4] | 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) |
| [5] | 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) · Zbl 1108.68422 |
| [6] | 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) · Zbl 1095.68051 |
| [7] | 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) |
| [8] | 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) · Zbl 1077.68615 |
| [9] | Gropp W., Lusk E., Skjellum A.: Using MPI: Portable Parallel Programming with the Message-Passing Interface. MIT Press, Cambridge (1999) · Zbl 0875.68206 |
| [10] | Hatton L.: The T experiments: errors in scientific software. IEEE Comput. Sci. Eng. 4(2), 27–38 (1997) · doi:10.1109/99.609829 |
| [11] | Isaacson E., Keller H.B.: Analysis of Numerical Methods. John Wiley & Sons, New York (1966) · Zbl 0168.13101 |
| [12] | 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) |
| [13] | McCabe, T.J.: A complexity measure. IEEE Transactions on Software Engineering, pp. 308–320 (1976) · Zbl 0352.68066 |
| [14] | Message Passing Interface Forum.: MPI: A Message-Passing Interface Standard, version 2.2, September 4, 2009. http://www.mpi-forum.org/docs/ (2009) |
| [15] | Post, D.E., Votta, L.G.: Computational science demands a new paradigm. Physics Today, pp. 35–41 (2005) |
| [16] | Quinn M.J.: Parallel Programming in C with MPI and OpenMP. McGraw-Hill, New York (2004) |
| [17] | 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) |
| [18] | 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) |
| [19] | 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) · Zbl 1317.68035 |
| [20] | 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) |
| [21] | 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) |
| [22] | 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) · Zbl 1242.68076 |
| [23] | Wilson G.: How do scientists really use computers?. Am Scientist 97, 8–10 (2009) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
