contracted floating-point expressions

[monniaux]

The C standard allows a compiler to "contract" compound floating-point expressions by removing intermediate rounding points. Concretely, an expression a*b+c may be rewritten into fma(a, b, c).

It has come to my attention that part of CompCert's low performance compared to gcc on certain kinds of programs (matrix and other numerical computations) can be attributed to gcc, by default, contracting expressions.

Since this optimization modifies semantics, it cannot be implemented in the verified parts of CompCert, but I think it could be implemented in the unverified parts of the front-end (those that deal with varargs, structure passing and so on).

On gcc and clang, this optimization may be turned off and on using -ffp-contract=off/on/fast. A similar option could be used. The C standard mandates a #pragma STDC FP_CONTRACT but gcc does not implement it yet.

[xavierleroy]

I'm uneasy about this suggestion.

CompCert prides itself of compiling FP computations exactly as written in the source, without excess precision, "contraction", reassociation, or any of that stuff allowed by the C and Fortran standards that makes it so painful to conduct a precise FP analysis of the code, as you observed previously. To me, this predictability of FP computations is worth more than improving benchmark figures.

Now, you're right that FP contraction can be controlled by the users, and off by default. I also agree that programming with explicit invocations of __builtin_fma is syntactically heavy and unpleasant. I'm still on the fence.

Concering #pragma STDC FP_CONTRACT, CompCert could honor it at the level of whole functions, but not at the statement level. That's because CompCert's C elaborator currently processes pragmas at "top-level" of a source file, but not inside functions.

[andrew-appel]

I have worked on and continue to work on the verification of C programs that use floating point. Indeed I need "precise FP analysis of the code". But I do this analysis at the Clight level, not the Csem level. So indeed, if this transformation were done before Clight (or at least, before Clight2), then it would not substantially interfere with proving programs correct -- especially if it could be turned on or off using the pragma.