Towards program optimization through automated analysis of numerical precision

Reducing the arithmetic precision of a computation has real performance implications, including increased speed, decreased power consumption, and a smaller memory footprint. For some architectures, e.g., GPUs, there can be such a large performance difference that using reduced precision is effectively a requirement. The tradeoff is that the accuracy of the computation will be compromised. In this paper we describe a proof assistant and associated static analysis techniques for efficiently bounding numerical and precisionrelated errors. The programmer/compiler can use these bounds to numerically verify and optimize an application for different input and machine configurations. We present several case study applications that demonstrate the effectiveness of these techniques and the performance benefits that can be achieved with rigorous precision analysis. Categories and Subject Descriptors D.2.4 [Software Engineering]: Program Verification–Validation; D.3.4 [Programming Lan

• Type: Conference
• Year: 2010
• Where: CGO
• Authors: Michael D. Linderman, Matthew Ho, David L. Dill, Teresa H. Y. Meng, Garry P. Nolan
• Keywords: CGO 2010, Large Performance Difference, Real Performance Implications, Smaller Memory Footprint, Software Engineering