Abstract
We introduce FPBench, a standard benchmark format for validation and optimization of numerical accuracy in floating-point computations. FPBench is a first step toward addressing an increasing need in our community for comparisons and combinations of tools from different application domains. To this end, FPBench provides a basic floating-point benchmark format and accuracy measures for comparing different tools. The FPBench format and measures allow comparing and composing different floating-point tools. We describe the FPBench format and measures and show that FPBench expresses benchmarks from recent papers in the literature, by building an initial benchmark suite drawn from these papers. We intend for FPBench to grow into a standard benchmark suite for the members of the floating-point tools research community.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Not shown in the grammar: FPBench uses “;” to indicate that the remainder of a line is a comment.
- 2.
- 3.
We are using |S| to denote the number of elements in a set S.
- 4.
Where n is the number of arguments.
- 5.
Where N is the number of valid inputs, and n is the number of arguments.
- 6.
We use the negative variant here, as in the Herbie paper; the positive variant is analogous.
References
DIMACS challenge. Satisfiability. Suggested format (1993). http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/satformat.ps
Adjé, A., Garoche, P.-L., Werey, A.: Quadratic zonotopes. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 127–145. Springer, Cham (2015). doi:10.1007/978-3-319-26529-2_8
Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.5. Technical report, Department of Computer Science, The University of Iowa (2015). www.SMT-LIB.org
Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Static analysis and verification of aerospace software by abstract interpretation. Found. Trends Program. Lang. 2(2–3), 71–190 (2015)
Bessey, A., Block, K., Chelf, B., Chou, A., Fulton, B., Hallem, S., Henri-Gros, C., Kamsky, A., McPeak, S., Engler, D.: A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53(2), 66–75 (2010)
Cadar, C., Dunbar, D., Engler, D.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI 2008), Berkeley, CA, USA, pp. 209–224. USENIX Association (2008)
Chapoutot, A.: Interval slopes as a numerical abstract domain for floating-point variables. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 184–200. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15769-1_12
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24730-2_15
Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Log. Comput. 2(4), 511–547 (1992)
Damouche, N., Martel, M., Chapoutot, A.: Intra-procedural optimization of the numerical accuracy of programs. In: Núñez, M., Güdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 31–46. Springer, Cham (2015). doi:10.1007/978-3-319-19458-5_3
Darulova, E., Kuncak, V.: Sound compilation of reals. In: Jagannathan, S., Sewell, P., (eds.), POPL 2014, pp. 235–248. ACM (2014)
Goubault, E.: Static analysis by abstract interpretation of numerical programs and systems, and FLUCTUAT. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 1–3. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38856-9_1
Goubault, E., Martel, M., Putot, S.: Some future challenges in the validation of control systems. In: European Congress on Embedded Real Time Software (ERTS 2006), Proceedings (2006)
Goubault, E., Putot, S.: Static analysis of finite precision computations. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 232–247. Springer, Heidelberg (2011). doi:10.1007/978-3-642-18275-4_17
Griewank, A., Walther, A.: Evaluating derivatives - principles and techniques of algorithmic differentiation (2 ed.). SIAM (2008)
Hamming, R.: Numerical Methods for Scientists and Engineers, 2nd edn. Dover Publications, New York (1987)
Henning, J.L.: SPEC CPU2006 benchmark descriptions. SIGARCH Comput. Archit. News 34(4), 1–17 (2006)
Holzmann, G.J.: Mars code. Commun. ACM 57(2), 64–73 (2014)
Lee, W., Sharma, R., Aiken, A.: Verifying bit-manipulations of floating-point. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2016), New York, NY, USA. ACM (2016)
Martel, M.: An overview of semantics for the validation of numerical programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 59–77. Springer, Heidelberg (2005). doi:10.1007/978-3-540-30579-8_4
Wilcox, J.-R., Panchekha, P., Sanchez-Stern, A., Tatlock, Z.: Automatically improving accuracy for floating point expressions. In: Grove, D., Blackburn, S., (eds.), PLDI 2015, pp. 1–11. ACM (2015)
Sankaranarayanan, S.: Static analysis in the continuously changing world. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 4–5. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38856-9_2
Schkufza, E., Sharma, R., Aiken, A.: Stochastic optimization of floating-point programs with tunable precision. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2014), New York, NY, USA. ACM (2014)
Solovyev, A., Jacobsen, C., Rakamarić, Z., Gopalakrishnan, G.: Rigorous estimation of floating-point round-off errors with symbolic taylor expansions. In: Bjørner, N., de Boer, F. (eds.) FM 2015: Formal Methods. Programming and Software Engineering, vol. 9109. Springer, Heidelberg (2015)
Woo, S.C., Ohara, M., Torrie, E., Singh, J.P., Gupta, A.: The SPLASH-2 programs: characterization and methodological considerations. In: Proceedings of the 22nd Annual International Symposium on Computer Architecture (ISCA 1995), pp. 24–36, New York, NY, USA. ACM (1995)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Damouche, N., Martel, M., Panchekha, P., Qiu, C., Sanchez-Stern, A., Tatlock, Z. (2017). Toward a Standard Benchmark Format and Suite for Floating-Point Analysis. In: Bogomolov, S., Martel, M., Prabhakar, P. (eds) Numerical Software Verification. NSV 2016. Lecture Notes in Computer Science(), vol 10152. Springer, Cham. https://doi.org/10.1007/978-3-319-54292-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-54292-8_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-54291-1
Online ISBN: 978-3-319-54292-8
eBook Packages: Computer ScienceComputer Science (R0)