Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Wrong semantics for fmul_add in afp/IEEE_Float...

view this post on Zulip Email Gateway (Oct 29 2021 at 18:23):

From: Peter Lammich <lammich@in.tum.de>
Hi List (cc Fabian who's to hg-blame for this),

when trying to prove properties of the IEEE fused-multiply-add
operation as formalized in the AFP entry IEEE_Floating_Point, I came
across an oddity in the corner
case of rounding to -\infinity, where a positive actual result
(resulting from non-negative operands) gets rounded down to zero.
In this case, the formalized operation returns -0, but I believe it
must be 0 (and so does Intel's AVX512 _mm_fmadd_round_sd instruction).

I'm writing this lengthy mail, as the formalization looks like this
behaviour has been built in on purpose. The relevant code in IEEE.thy
is:

float_round mode
(if (r1 = 0) ∧ (r2 = 0) ∧ (signP = sign z) then
signP = 1
else mode = To_ninfinity) (r1 + r2))

This will explicitly select a negative zero for To_ninfinity rounding
mode!

Any comments?
What was the intention behind this?
Am I (and Intel-AVX) interpreting the standard wrongly? Or should I try
to fix this?

view this post on Zulip Email Gateway (Mar 18 2022 at 16:57):

From: Peter Lammich <lammich@in.tum.de>
Hi Fabian,

I have now fixed the issue.

I have also built an executable result checker, which will check the
semantics against a proposed result. With this, the fixed semantics (see
attached) now passes the IBM fpgen test suite
(https://research.ibm.com/haifa/projects/verification/fpgen/ieeets.shtml)
and coincides with the output of AVX512f, and std::fma in C++ (however
that gets translated on my laptop ;) ). I have also tested the
+,-,/,*,sqrt operations, which also pass fpgen.

Shall I commit a patch to afp-devel?
IEEE.thy

view this post on Zulip Email Gateway (Mar 18 2022 at 20:07):

From: Fabian Immler <cl-isabelle-users@lists.cam.ac.uk>

On 18. Mar 2022, at 17:54, Peter Lammich <lammich@in.tum.de> wrote:

Hi Fabian,

I have now fixed the issue.

I have also built an executable result checker, which will check the semantics against a proposed result. With this, the fixed semantics (see attached) now passes the IBM fpgen test suite (https://research.ibm.com/haifa/projects/verification/fpgen/ieeets.shtml <https://research.ibm.com/haifa/projects/verification/fpgen/ieeets.shtml>) and coincides with the output of AVX512f, and std::fma in C++ (however that gets translated on my laptop ;) ). I have also tested the +,-,/,*,sqrt operations, which also pass fpgen.

Nice!
Shall I commit a patch to afp-devel?

Yes, looks good to me.

Best wishes,
Fabian

Last updated: Apr 20 2024 at 08:16 UTC