Abstract
A floating-point predicate is a routine that returns a boolean value based on a result of a floating-point computation. For example, in computational geometry floating-point predicates determine whether 3 points are collinear or which side of a line a point lies on. Due to floating-point round-off errors, implementing such predicates correctly, while maintaining good performance, requires both domain knowledge and deep understanding of the floating-point standard. Hence, it is usually done by experts that carefully craft them by relying on the floating-point round-off error model and complex mathematical derivations. This paper presents our automatic floating-point predicates synthesis method. Given an input predicate specified over reals, our method synthesizes the corresponding rigorous floating-point predicate by automatically deriving the expression that calculates the round-off error-bound of the input computation. We minimize the number of operations in the error-bound calculation, which is critical to maintain good performance, by judiciously reusing intermediate results, applying absolute-value inequalities, adjusting polynomial coefficients, and performing meta-heuristic grouping. We implemented the method in a prototype tool FPSyn. We evaluated FPSyn on 8 floating-point predicates, and showed that it synthesizes predicates whose performance is on par with optimized manually crafted implementations, while they outperform the straightforward interval arithmetic implementations.
This work was supported in part by the NSF award CCF 1552975.
Z. Rakamarić—The author contributed to this work before joining Amazon Web Services (AWS).
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
Similar content being viewed by others
References
Bartels, T., Fisikopoulos, V.: Fast robust arithmetics for geometric algorithms and applications to GIS. Int. Arch. Photogramm. Remote Sens. Spat. Inf. Sci. 46, 1–8 (2021). https://doi.org/10.5194/isprs-archives-XLVI-4-W2-2021-1-2021
Brönnimann, H., Burnikel, C., Pion, S.: Interval arithmetic yields efficient dynamic filters for computational geometry. Discrete Appl. Math. 109(1–2), 25–47 (2001). https://doi.org/10.1016/S0166-218X(00)00231-6
Darulova, E., Kuncak, V.: Sound compilation of reals. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 235–248. ACM, NY (2014)
Dekker, T.J.: A floating-point technique for extending the available precision. Numer. Math. 18(3), 224–242 (1971). https://doi.org/10.1007/BF01397083
Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., Védrine, F.: Towards an industrial use of FLUCTUAT on safety-critical avionics software. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 53–69. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04570-7_6
Devillers, O., Pion, S.: Efficient exact geometric predicates for Delaunay triangulations. Ph.D. thesis, INRIA (2002)
Glover, F.: Future paths for integer programming and links to artificial intelligence. Comput. Oper. Res. 13(5), 533–549 (1986). https://doi.org/10.1016/0305-0548(86)90048-1
Meyer, A., Pion, S.: FPG: a code generator for fast and certified geometric predicates. In: Real Numbers and Computers, pp. 47–60 (2008)
Moore., R.E.: Interval Analysis. Prentice-Hall (1966)
The GNU MPFR library. https://www.mpfr.org
Nanevski, A., Blelloch, G., Harper, R.: Automatic generation of staged geometric predicates. In: Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming, pp. 217–228 (2001). https://doi.org/10.1145/507669.507662
Pion, S.: Interval arithmetic: an efficient implementation and an application to computational geometry. In: Workshop on Applications of Interval Analysis to systems and Control (MISC) (1999)
Rubio-González, C., et al.: Precimonious: tuning assistant for floating-point precision. In: Gropp, W., Matsuoka, S. (eds.) SC, p. 27. ACM (2013). https://doi.org/10.1145/2503210.2503296
Sanchez-Stern, A., Panchekha, P., Lerner, S., Tatlock, Z.: Finding root causes of floating point error. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 256–269 (2018). https://doi.org/10.1145/3192366.3192411
Shewchuk, J.R.: Adaptive precision floating-point arithmetic and fast robust geometric predicates. Discrete Comput. Geom. 18(3), 305–363 (1997). https://doi.org/10.1007/PL00009321
Solovyev, A., Baranowski, M.S., Briggs, I., Jacobsen, C., Rakamarić, Z., Gopalakrishnan, G.: Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions. ACM Trans. Program. Lang. Syst. 41(1), 20 (2018). https://doi.org/10.1145/3230733
SymPy: A Python library for symbolic mathematics. https://www.sympy.org
Titolo, L., Feliú, M.A., Moscato, M., Muñoz, C.A.: An abstract interpretation framework for the round-off error analysis of floating-point programs. In: VMCAI 2018. LNCS, vol. 10747, pp. 516–537. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-73721-8_24
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Nguyen, T.S., Jones, B., Rakamarić, Z. (2022). Synthesis of Rigorous Floating-Point Predicates. In: Legunsen, O., Rosu, G. (eds) Model Checking Software. SPIN 2022. Lecture Notes in Computer Science, vol 13255. Springer, Cham. https://doi.org/10.1007/978-3-031-15077-7_3
Download citation
DOI: https://doi.org/10.1007/978-3-031-15077-7_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-15076-0
Online ISBN: 978-3-031-15077-7
eBook Packages: Computer ScienceComputer Science (R0)