Does not work on Apple M1 CPU

[BrunoDutertre]

The code does not compile on MacOS but that can be fixed.

But after fixing the compilation issues, the test fails for max and min.

The reference implementation does this:

• min(-zero,+zero) = -zero
• min(+zero,-zero) = -zero
• min(x,NaN) = NaN
• min(NaN,x) = NaN

The computed values don't agree with this. I'm not sure who is right.

Here are some of the failed tests (for min):

vector[1 -> (1,0)] input1 = 0x80000000, input2 = 0x0, computed = 0x0, reference = 0x80000000
vector[1316165 -> (1659,0)] input1 = 0xff800001, input2 = 0x0, computed = 0x0, reference = 0xffc00001
vector[1316166 -> (1658,1)] input1 = 0x7f800001, input2 = 0x80000000, computed = 0x80000000, reference = 0x7fc00001
vector[1316172 -> (1658,2)] input1 = 0x7f800001, input2 = 0x3f800000, computed = 0x3f800000, reference = 0x7fc00001
vector[1316173 -> (1659,2)] input1 = 0xff800001, input2 = 0x3f800000, computed = 0x3f800000, reference = 0xffc00001

The compiler is clang++:

Apple clang version 12.0.5 (clang-1205.0.22.11)
Target: arm64-apple-darwin20.5.0

and here are the compilation flags I used:

CXXFLAGS+=-std=c++17 -g -Wall -W -ffp-model=strict -pedantic

But it looks like -ffp-model=strict is ignored by this compiler.

[martin-cs]

Sorry to hear you are having issues. I will see if I can work through them...

• Compilation with clang : I haven't tried but I will when next working on this (likely to be September). I hope it is a simple enough fix.
• Compilation on MacOS : I have never tried as I don't own a Mac but I think cvc5 has this working so it feels like it should be straight-forward.
• Running on M1 : if you can point me to where I can run code on one or are willing to test stuff out for me then this should be do-able.
• max(+0,-0) : a little harder to explain and needs some context, see below.
• max(NaN,x) : a separate issue but also see below.

So, max and min have a slightly ... chequered history in IEEE-754. They are not in 1985/1989 at all, which meant that people implemented various different things. For example, in C, whether you pick (a < b) ? a : b or (a <= b) ? a : b will change the zeros case. Older ISAs date back to this era and so x86 just returns the left zero in the two zeros case (which, of course, means that max is not commutative).

C99 (ISO-9899:1999 specifically) adds the fmax and fmin functions and variants. The important bit is in the footnote to 7.12.12.2 :

The fmax functions determine the maximum numeric value of their arguments.204)

204) NaN arguments are treated as missing data: if one argument is a NaN and the other numeric, then the
     fmax functions choose the numeric value. See F.9.9.2.

( Appendix F is the binding between the C standard and IEEE-754 ) which has the following to say:

F.9.9.2 The fmax functions

1 If just one argument is a NaN, the fmax functions return the other argument (if both
  arguments are NaNs, the functions return a NaN).

2 The body of the fmax function might be 314)
          { return (isgreaterequal(x, y) || isnan(y)) ? x : y; }

314) Ideally, fmax would be sensitive to the sign of zero, for example fmax(−0. 0, +0. 0) would
     return +0; however, implementation in software might be impractical.

So, in ISO-9899:1999, fmax(x,NaN) = x and fmax(+0,-0) = one of them but it's sort of up to what you find easiest.

The next revision of IEEE-754 in 2008 adds (5.3.1) the following:

maxNum(x, y) is the canonicalized number y if x < y, x if y < x, the canonicalized number if one
operand is a number and the other a quiet NaN. Otherwise it is either x or y, canonicalized (this
means results might differ among implementations). When either x or y is a signalingNaN, then the
result is according to 6.2.

6.2.3 NaN propagation
6.2 3.0
An operation that propagates a NaN operand to its result and has a single NaN as an input should produce a
NaN with the payload of the input NaN if representable in the destination format.

So, in IEEE-754:2008 maxNum(x,qNaN) = x, maxNum(x,sNaN) = qNaN and maxNum(+0,-0) = +0 OR -0.

ISO-9899:2011 is exactly the same as ISO-9899:1999 in this regard and still binds to IEEE-754:1989.

The SMT-LIB 2.* floating-point is based on IEEE-754:2009 and says:

                  { f   if gt(f,g) or g = NaN
max (f,g) = { g  if gt(g,f) or f = NaN
                  { h  h \in {f,g} if eq(g,f)

So max(x,NaN) = x and max(+0,-0) = +0 OR -0. I have suggested that all partially specified functions in SMT-LIB gain an extra argument for the partially specified case and I hope this will allow clear specification of what behaviour people want from max(+0,-0).

During the discussions in updating IEEE-754, it was discussed that the semantics for max and min in IEEE-754:2008 are a mistake. This includes a fairly comprehensive survey of what people actually do.

https://754r.ucbtest.org/minutes/2017-01-19-minutes.txt
https://grouper.ieee.org/groups/msc/ANSI_IEEE-Std-754-2019/background/minNum_maxNum_Removal_Demotion_v3.pdf

In IEEE-754:2019 minNum and maxNum have been removed from the definitive part of the standard and Section 9 "Recommended Operations" has gained the following:

9.6 Minimum and maximum operations
9.6 0
Language standards should define the following homogeneous general-computational operations for all
supported arithmetic formats:
    sourceFormat maximum(source, source)
    sourceFormat maximumNumber(source, source)

maximum(x, y) is x if x > y, y if y > x, and a quiet NaN if either operand is a NaN, according to 6.2.
For this operation, +0 compares greater than −0. Otherwise (i.e., when x = y and signs are the
same) it is either x or y.

maximumNumber(x, y) is x if x > y, y if y > x, and the number if one operand is a number and the
other is a NaN. For this operation, +0 compares greater than −0. If x = y and signs are the same it
is either x or y. If both operands are NaNs, a quiet NaN is returned, according to 6.2. If either
operand is a signaling NaN, an invalid operation exception is signaled, but unless both operands
are NaNs, the signaling NaN is otherwise ignored and not converted to a quiet NaN as stated in
6.2 for other operations.

So maximum(x,NaN) = x and maximum(+0,-0) = +0.

So that is the standard point of view, but what about what SymFPU implements? The encoding

symfpu/core/compare.h

Line 202 in c3acaf6

return ITE(left.getNaN() || ordering(format, left, right, zeroCase),

fixes max(x,NaN) = x but makes the sign of zero configurable in the mixed zero case. For the test program we use the platform fmax for reference and mix the behaviour of the split case to be Intel SSE-like.

symfpu/applications/implementations.h

Line 119 in c3acaf6

return fmaxf(f,g);

symfpu/applications/implementations.h

Line 779 in c3acaf6

uf max(symfpu::max<traits>(*format, unpacked1, unpacked2, INTELSSEMAXSTYLE));

So, my guess as to what is going on:

1. ARM hardware handles the mixed zero case differently to Intel. If I replace INTELSSEMAXSTYLE with something more intelligent and platform specific then I think I can get this test to pass.
2. Mac OS / ARM M1 returns fmax(x,NaN) = NaN for reasons I don't fully understand. This feels like it could be a bug.

HTH and sorry for the rant. I'm aiming a new SymFPU version for September and will try to fix as much of this as possible.

[florianschanda]

I have only a tiny bit to add to Martin's excellent answer, just to illustrate the point, which is the behaviour on Intel (when using the built-in min/max) generally gives you the first parameter back in the case of +/- 0 (i.e. max(-0, +0) = -0 and max(+0, -0) = +0).

[florianschanda]

Actually, one more thing to add: if you do want a 3rd extremely independent test oracle that very precisely follows IEEE-754:2008 consider looking at https://github.com/florianschanda/PyMPF which we wrote to validate all this; specifically because it'll throw you an exception if you enter an area where the answer is unspecified.

[BrunoDutertre]

Thanks for the feedback.

Here's more detail on what's going on:

• the fmax function is compiled to the ARM instruction fmaxnm
• the fmin function is compiled to the ARM instruction fminnm
• the ARM doc says that fmaxnm and fminnm are compatible with IEEE754-2008:

The minNum(x,y) and maxNum(x,y) operations follow the IEEE 754-2008 standard and return the numerical operand when one operand is numerical and the other a quiet NaN. Apart from this additional handling of a single quiet NaN the result is then identical to min(x,y) and max(x,y).

The min(x,y) and max(x,y) operations return a quiet NaN when either x or y is NaN

[BrunoDutertre]

It also fails on my intel machine (with the same behavior for max/min when one argument is
a signaling NaN).