Moving the Needle on Rigorous Floating-point Precision Tuning


Marek Baranowski, Ian Briggs, Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamaric, Alexey Solovyev. 6th Automated Formal Methods Workshop (AFM 2017), Moffett Field, CA, USA.
[pdf] [bib]

Abstract: Virtually all real-valued computations are carried out using floating-point data types and operations. With increasing emphasis on overall computational efficiency, compilers are increasingly attempting to optimize floating-point expressions. Practical reasoning about the correctness of these optimizations requires error analysis procedures that are rigorous (ideally, they can generate proof certificates), can handle a wide variety of operators (e.g., transcendentals), and handle all normal programmatic constructs (e.g., conditionals and loops). Unfortunately, none of today’s approaches can achieve this entire combination. This position paper summarizes recent progress achieved in the community on this topic. It then showcases the component techniques present within our own rigorous floating-point precision tuning framework called FPTuner – essentially offering a collection of “grab and go” tools that others can benefit from. Finally, we present FPTuner’s limitations and describe how we can exploit contemporaneous research to improve it.


  author = {Marek Baranowski and Ian Briggs and Wei-Fan Chiang and
    Ganesh Gopalakrishnan and Zvonimir Rakamari\'c and Alexey Solovyev},
  title = {Moving the Needle on Rigorous Floating-Point Precision Tuning},
  booktitle = {Proceedings of the 6th Automated Formal Methods Workshop (AFM 2017)},
  series = {Kalpa Publications in Computing},
  volume = {5},
  publisher = {EasyChair},
  editor = {Natarajan Shankar and Bruno Dutertre},
  year = {2018},
  pages = {19--30},
  doi = {10.29007/f4f3},