Efficient search for inputs causing high floating-point errors

ABSTRACT

Tools for floating-point error estimation are fundamental to program understanding and optimization. In this paper, we focus on tools for determining the input settings to a floating point routine that maximizes its result error. Such tools can help support activities such as precision allocation, performance optimization, and auto-tuning. We benchmark current abstraction-based precision analysis methods, and show that they often do not work at scale, or generate highly pessimistic error estimates, often caused by non-linear operators or complex input constraints that define the set of legal inputs. We show that while concrete-testing-based error estimation methods based on maintaining shadow values at higher precision can search out higher error-inducing inputs, suit able heuristic search guidance is key to finding higher errors. We develop a heuristic search algorithm called Binary Guided Random Testing (BGRT). In 45 of the 48 total benchmarks, including many real-world routines, BGRT returns higher guaranteed errors. We also evaluate BGRT against two other heuristic search methods called ILS and PSO, obtaining better results.

References

1. E. Anderson, Z. Bai, C. Bischof, L. S. Blackford, J. Demmel, J. J. Dongarra, J. Du Croz, S. Hammarling, A. Greenbaum, A. McKenney, and D. Sorensen. LAPACK Users? Guide (3rd Ed.). SIAM: Society for Industrial and Applied Mathematics, 1999.
2. J. Ansel, C. Chan, Y. L. Wong, M. Olszewski, Q. Zhao, A. Edelman, and S. Amarasinghe. Petabricks: a language and compiler for algorithmic choice. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 38--49, 2009.
3. D. H. Bailey and J. M. Borwein. Highly parallel, high-precision numerical integration, 2005.
4. E. T. Barr, T. Vo, V. Le, and Z. Su. Automatic detection of floating-point exceptions. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 549--560, 2013.
5. F. Benz, A. Hildebrandt, and S. Hack. A dynamic program analysis to find floating-point accuracy problems. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 453--462, 2012.
6. S. Boldo and G. Melquiond. Flocq: A unified library for proving floating-point algorithms in Coq. In IEEE Symposium on Computer Arithmetic, pages 243--252, 2011.
7. S. Boldo, J.-C. Filliâtre, and G. Melquiond. Combining Coq and Gappa for certifying floating-point programs. In Intelligent Computer Mathematics, pages 59--74. Springer-Verlag, 2009.
8. C. Cadar and K. Sen. Symbolic execution for software testing: three decades later. Communications of the ACM, 56(2):82--90, Feb. 2013.
9. W.-F. Chiang, G. Gopalakrishnan, Z. Rakamari, D. H. Ahn, and G. L. Lee. Determinism and reproducibility in large-scale HPC systems. In Workshop on Determinism and Correctness in Parallel Programming (WoDet), 2013.
10. Coq. The Coq proof assistant. http://coq.inria.fr/.
11. E. Darulova and V. Kuncak. Trustworthy numerical computation in Scala. In Conference on Object-Oriented Programming Systems (OOPSLA), pages 325--344, 2011.
12. F. de Dinechin, C. Q. Lauter, and G. Melquiond. Assised verification of elementary functions using Gappa. In ACM Symposium on Applied computing (SAC), pages 1318--1322, 2006.
13. L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 337--340, 2008.
14. D. Delmas, E. Goubault, S. Putot, J. Souyris, K. Tekkal, and F. Vdrine. Towards an industrial use of FLUCTUAT on safety-critical avionics software. In Workshop on Formal Methods for Industrial Critical Systems (FMICS), pages 53--69, 2009.
15. J. Demmel and H. D. Nguyen. Numerical reproducibility and accuracy at exascale. In IEEE Symposium on Computer Arithmetic, pages 235--237, 2013.
16. J. W. Demmel. Trading off parallelism and numerical stability. Technical Report UCB/CSD-92--702, EECS Department, University of California, Berkeley, 1992.
17. A. Goodloe, C. Munoz, F. Kirchner, and L. Correnson. Verification of numerical programs: From real numbers to floating point numbers. In NASA Formal Methods Symposium (NFM), pages 441--446, 2013.
18. M. Harris. Optimizing parallel reduction in CUDA. NVIDIA Developer Technology, 2007.
19. M. Heideman, D. Johnson, and C. Burrus. Gauss and the history of the fast Fourier transform. ASSP Magazine, IEEE, 1(4):14--21, 1984.
20. N. J. Higham. Accuracy and Stability of Numerical Algorithms (2nd Ed.). SIAM: Society for Industrial and Applied Mathematics, 2002.
21. C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576--580, 1969.
22. F. Hutter, H. H. Hoos, and T. Stutzle. Automatic algorithm configuration based on local search. In National Conference on Artificial Intelligence, pages 1152--1157, 2007.
23. IEEE Task P754. ANSI/IEEE 754--1985, Standard for Binary Floating-Point Arithmetic. IEEE, 1985.
24. F. Ivancic, M. K. Ganai, S. Sankaranarayanan, and A. Gupta. Numerical stability analysis of floating-point computations using software model checking. In IEEE/ACM Intl. Conference on Formal Methods and Models for Codesign (MEMOCODE), pages 49--58, 2010.
25. W. Kahan. Pracniques: Further remarks on reducing truncation errors. Communications of the ACM, 8(1):40--, Jan. 1965.
26. J. Kennedy. Particle swarm optimization. In Encyclopedia of Machine Learning, pages 760--766. Springer-Verlag, 2010.
27. A. B. Kinsman and N. Nicolici. Finite precision bit-width allocation using SAT-modulo theory. In Conference on Design, Automation and Test in Europe (DATE), pages 1106--1111, 2009.
28. M. O. Lam, J. K. Hollingsworth, B. R. de Supinski, and M. P. LeGendre. Automatically adapting programs for mixed-precision floating-point computation. In International Conference on Supercomputing (ICS), pages 369--378, 2013.
29. M. O. Lam, J. K. Hollingsworth, and G. W. Stewart. Dynamic floating-point cancellation detection. Parallel Computing, 39(3):146--155, 2013.
30. P. Li, G. Li, and G. Gopalakrishnan. Parametric flows: automated behavior equivalencing for symbolic analysis of races in CUDA programs. In Proc. of the Intl. Conf. on High Performance Computing, Networking, Storage and Analysis (SC), pages 29:1--29:10, 2012.
31. M. D. Linderman, M. Ho, D. L. Dill, T. H. Y. Meng, and G. P. Nolan. Towards program optimization through automated analysis of numerical precision. In IEEE/ACM International Symposium on Code Generation and Optimization (CGO), pages 230--237, 2010.
32. H. R. Lourenco, O. C. Martin, and T. Stutzle. Iterated local search. arXiv preprint math/0102188, 2001.
33. J. Luitjens, B. Worthen, M. Berzins, and T. C. Henderson. Petascale Computing Algorithms and Applications, chapter Scalable parallel AMR for the Uintah multiphysics code, pages 67--82. Chapman and Hall/CRC, 2007.
34. MAGMA. The MAGMA library. http://icl.cs.utk.edu/ magma/index.html.
35. NPB. The NAS parallel benchmarks (NPB). http://www.nas. nasa.gov/publications/npb.html.
36. C. Rubio-Gonz - lez, C. Nguyen, H. D. Nguyen, J. Demmel, W. Kahan, K. Sen, D. H. Bailey, C. Iancu, and D. Hough. Precimonious: Tuning assistant for floating-point precision. In Proc. of the Intl. Conf. on High Performance Computing, Networking, Storage and Analysis (SC), pages 27:1--27:12, 2013.
37. S3FP. Guided random testing for floating-point error estimation. https://sites.google.com/site/grt4fperror/.
38. M. Souza, M. Borges, M. d'Amorim, and C. S. Psreanu. CORAL: Solving complex constraints for symbolic Pathfinder. In NASA Formal Methods Symposium (NFM), pages 359--374, 2011.
39. J. A. Stratton, C. Rodrigues, I.-J. Sung, N. Obeid, L.-W. Chang, N. Anssari, G. D. Liu, and W.-m. W. Hwu. Parboil: A revised benchmark suite for scientific and commercial throughput computing. Center for Reliable and High-Performance Computing, 2012.

Index Terms

• Computing methodologies