We don’t guarantee canonicalization for non-strictfp operations (except for llvm.canonicalize). So fsub -0, x for a signaling nan can return either an snan or a qnan. I also do not expect guaranteed consistency for payload bits on canonicalizing operations.
So, fneg %s can return a bitwise pattern that fsub can’t. Hence refinement (of fsub 0, x => fneg x) doesn’t hold.
The issue is substitution of a non-canonicalizing operation with a canonicalizing one. Per the current rules, fsub -0, x → fneg is OK, but fneg → fsub -0, x is not OK. As implemented some places are arbitrarily stricter and should be cleaned up for consistency.
But it cannot produce any SNaN. It can only produce the input SNaN, right?
From my reading of LangRef, the samentics of fsub -0.0, %x is:
if (%x is NaN)
return non-determistic-choice(%x, some QNaN)
return -%x
LangRef forbids fsub from creating a new SNaN.
Hence, either there’s some additional rule that’s missing in LangRef, or I’m not seeing how we can justify the fsub → fneg transformation.
I suppose I said this imprecisely, I would generally expect IEEE payload propagation in practice, but the LangRef doesn’t have an explicit note on this. If you read between the lines by looking at the llvm.canonicalize definition, it vaguely hints that this isn’t a property held for other operations. The payload bits aren’t supposed to matter to program meaning.
Other than for canonicalize, LangRef doesn’t have written rules for payload bits. I would assume it can only produce the original sNaN, that would be consistent with the regular payload propagation rules in IEEE. Not sure I understand the “two exceptions” note on llvm.canonicalize though (I assume this is some weird x87 thing)
You’re also missing possible a denormal flush in here. A more precise definition might be return either -x or llvm.canonicalize(-x). It can’t be a fully non-deterministic choice, at worst it would be drop the input payload bits in favor of a generic/preferred/canonical/whatever you want to name it nan.
If the IR semantic is relaxed payload propagation, picking whatever payload bits happened to be in %x to begin with is a fine choice.
The IEEE spec view is anything you do with the sign or payload bits of a nan are semantic preserving for the program. Section 11 states if you want reproducible results on different platforms, you should not depend on these bits.
But then we are back to the previous NaN semantics, where the output is any NaN payload if the input is NaN.
I’m specifically trying to follow this paragraph in LangRef:
Floating-point math operations are allowed to treat all NaNs as if they were quiet NaNs. For example, “pow(1.0, SNaN)” may be simplified to 1.0. This also means that SNaN may be passed through a math operation without quieting. For example, “fmul SNaN, 1.0” may be simplified to SNaN rather than QNaN. However, SNaN values are never created by math operations. They may only occur when provided as a program input value.
Can be interpreted in at least 2 ways:
An operation doesn’t create a new SNaN, only does a passthrough of the arguments
An operation returns an SNaN with a non-deterministic pay-load if and only if one of the inputs is an SNaN
Option 1) makes fsub → fneg invalid. Option 2) works, but is that what you had in mind? Is that the semantics LLVM wants to offer?
My understanding of LLVM’s NaN propagation rules is that the logic looks this:
if (any argument is sNaN)
return non-deterministic-choice(any sNaN or qNaN value)
if (any argument is qNaN)
return non-deterministic-choice(any qNaN value)
return op, with a NaN result being replaced with non-deterministic-choice(any qNaN)
(constrained intrinsics would combine the first two rules into one that returns non-deterministic-choice(any qNaN value)).
The largely intended effect of these rules is that most operations only consider there two be two NaN values, sNaN and qNaN, with even the distinction between sNaN and qNaN largely that LLVM optimizations cannot magic sNaN out of thin air.
In principle, you could extend the rules for optimization further and say instead that the result of a floating point operation that returns NaN is non-deterministic-choice(preferred qNaN ∪ any input NaN ∪ { quieted(x) | any input NaN x}) (where quieted(x) means set the sNaN/qNaN bit but otherwise do not adjust the payload–this turns an sNaN into a qNaN with a well-defined payload, while just returning the input unchanged for a qNaN). However, it needs to be recognized that some of our targets do not implement this propagation rule, which means that we can’t properly operationalize this optimization rule.
As I understand it for several targets, the hardware rules are as follows:
ARM: NaN propagates according to above rule (preferred qNaN has positive sign)
MIPS: pre-2008, qNaN/sNaN has wrong bit direction (we don’t really support this right now anyways); post-2008, NaN propagates as above (don’t know sign off the top of my head)
RISC-V: NaN does not propagate, unconditionally return preferred qNaN (don’t know sign off the top of my head)
SPARC: NaN propagates, but preferred qNaN has all 1’s bits but positive sign (i.e., different from LLVM’s preferred qNaN)
WASM: weaker NaN propagation rules (if any NaN is non-preferred-qNaN, result is non-deterministic-choice(any qNaN)).
x86: NaN propagates according to above rule (preferred qNaN has negative sign)
I think it’s a good quality-of-implementation decision for the optimizer to pick a NaN payload that propagates its input in the nondeterministic choices, but given the hardware diversity in NaN propagation rules, it’s hard to come up with semantics that guarantees this decision that would avoid making extra work to implement those rules on some hardware targets. And NaN payloads are not important enough to justify doing that extra work.
Thank you for the detailed answer. I think I understand it now.
I’ll implement that in Alive2 and report back.
I think this bit is not documented. Doesn’t that mean that it’s not possible to emulate the standard LLVM instructions with the constrained ones? There’s no metadata to control the NaN behavior.
Not sure about the “non-deterministic” payload when quieting, I’d have to re-check the spec. It is quite useful to be able to drop canonicalizations, so I’d like to try to preserve that property
IEEE 754-2019 allows for what you state but does not mandate.
FNEG is allowed to quiet the signaling NaN or allowed to negate the NaN and leave it signaling.
A given architecture will choose one way or the other and stick with that choice.
I should also point out that there are architectures for which FNEG is not an instruction (95% of the time) but a sign changing operation as the operand is routed to the computational unit for processing.
an sNaN is allowed to remain after a calculation that would have consumed it is eliminated by optimization.
a calculation is not allowed to return an sNaN which arrived as an operand, and indeed must quiet an Operand sNaN if the calculation requires a NaN result.
but if the calculation is removed by optimization, the sNaN is allowed to remain.
{{By the way; FMOV FNEG, FABS are not considered calculations merely data movement}}
pow(1.0, sNaN) is special cased to 1.0
From IEEE 754-2019
For the pow operation:
pow(x, ±0) is 1 if x is not a signaling NaN <=======
pow(±0, y) is ±∞ and signals the divideByZero exception for y an odd integer <0
pow(±0, −∞) is +∞ with no exception
pow(±0, +∞) is +0 with no exception
pow(±0, y) is ±0 for finite y>0 an odd integer
pow(−1, ±∞) is 1 with no exception
pow(+1, y) is 1 for any y (even a quiet NaN) <=======
pow(x, +∞) is +0 for −1<x<1
pow(x, +∞) is +∞ for x<−1 or for 1<x (including ±∞)
pow(x, −∞) is +∞ for −1<x<1
pow(x, −∞) is +0 for x<−1 or for 1<x (including ±∞)
pow(+∞, y) is +0 for a number y < 0
pow(+∞, y) is +∞ for a number y > 0
pow(−∞, y) is −0 for finite y < 0 an odd integer
pow(−∞, y) is −∞ for finite y > 0 an odd integer
pow(−∞, y) is +0 for finite y < 0 and not an odd integer
pow(−∞, y) is +∞ for finite y > 0 and not an odd integer
pow(±0, y) is +∞ and signals the divideByZero exception for finite y<0 and not an odd integer
pow(±0, y) is +0 for finite y>0 and not an odd integer
pow(x, y) signals the invalid operation exception for finite x<0 and finite non-integer y
fmul sNaN,1.0 allows the ×1 to be “optimized away” leaving the sNaN still present because it has not yet been consumed by a calculation. It is the consumption of the sNaN in a calculation which causes sNaN → qNaN transformation. {{ +0, /1, … and other calculation identities are allowed to be optimized away leaving sNaNs in their wake.}}
FWIW, I’ve implemented this semantics in Alive2 and I see no regression on the test suit.
I didn’t differentiate the constrained intrinsics. But I guess there aren’t many optimizations with those.
Something’s wrong because it’s being so strict about payload bits it’s impossible to do anything. The payload bits are a quantum state that’s only collapsed by inspection by a non-FP observer. I’ve replaced canonicalizing fmuls operations with a different canonicalizing operation, and it’s complaining about random payload bits which were never observed
This is overly constricted, as there are calculations which can take an aNaN as an operand and still return a deterministic result MAX/MIN from the 2008 standard morphed into IEEE maximumNUMBER and minimumNUMBE where:: maximumNUMBER( x, NaN ) → x.
There are a small number of IEEE defined functions which can take NaNs and deliver normal FP results.
Perhaps::
if (any argument is sNaN && SNaNkillsCalculation( op, argumentList ) )
return non-deterministic-choice(any sNaN or qNaN value)
…
or something a bit more complicated.
I guess the issue is that I’m hearing different things from different people. I’m happy to implement whatever semantics you guys want in Alive2. But I need a specification, or pseudo-code, or something I can work with
Your example reduces to %x -> fmul %x, 1.0. According to the pseudo-code of @jcranmer, this transformation is invalid because when %x is NaN, fmul produces a new NaN with a non-deterministic payload.
So, unless the rules are different or we define refinement to allow any two NaNs to compare equal (or any two QNaNs or whatever), then the above transformation can’t be proven correct.
According to the LLVM docs, LLVM could return arbitrary (quiet) non-preferred NaNs from any addition that has NaN inputs. So there is nothing telling SM that the output of an addition will be either a non-NaN or a preferred NaN. Without such a promise, SM must do a fixup to ensure all NaNs are preferred NaNs.
The entire point of this thread is to get LLVM to document that this won’t happen, so that code like SM doesn’t need to do fixup. (Well, SM is written in C++, so this would also still require a C++ spec or clang doc change. I’m coming here as a member of the Rust project and we hope to allow the things SM does in Rust, but the way LLVM is currently specified, we cannot.)
That’s not the current LangRef semantics. The current LangRef semeantics are that for “true” ops, they return non-deterministically any quiet NaN (except if there is a signaling NaN input, then they return non-deterministically any NaN).
That’s at least not currently documented.
denormal flush surely isn’t allowed in general?
Some operations have non-NaN output for NaN inputs though, such as pow (and min/max were mentioned by others). So I would re-phrase this by starting with “if the result is a NaN, it is picked as follows:”
if (any argument is sNaN)
return non-deterministic-choice(any sNaN or qNaN value)
return non-deterministic-choice(any qNaN value)
But I would prefer if instead we had (at least for the majority of operations on the majority of targets)
if (any argument is sNaN)
return non-deterministic-choice(any sNaN or qNaN value)
if (any argument is non-preferred qNaN)
return non-deterministic-choice(any qNaN value)
return non-deterministic-choice(any preferred qNaN value)
Where there are exactly 2 “preferred qNaN” values: those with the payload having the signaling/quiet bit set and no other bit set. (That leaves the sign bit unspecified, hence there are 2.)
Note that for the effective semantics on x86 that are implemented by LLVM, your rule is not correct: 0.0/0.0 will be optimized to a positive preferred qNaN.
So to account for this, the rule should probably be non-deterministic-choice(positive or negative preferred qNaN ∪ any input NaN ∪ { quieted(x) | any input NaN x}). (Or maybe that’s what you meant.)
This isn’t the best example, this is one of the combines I’m looking into adding and was trying out variants to figure out what exactly alive understands. Previously I saw complaints about snan payload bits, but with today’s build it’s now producing a more sensible error (but wrong in the same sense that signaling nan quieting). For the denormal flush, it’s seemingly mandating canonicalization which is not required
If you’re talking about IEEE. As soon as you talk about denormal flushing you’ve completely left the world of standards. IEEE doesn’t acknowledge this at all, but real hardware either doesn’t support denormals or has controls to disable denormal input or output handling. The IR has denormal-fp-math to express the expectations of what denormal mode the code will execute with. We do not mandate output flushing / canonicalizaton (except at llvm.canonicalize as an observer). The problematic half of this is really the implicit flushing of inputs, denormals-are-zero acts like a constraint since now you need to guard against observing 0s that aren’t real.
So from the IR rules, denormal flush is in the same bucket as signaling nan quieting (an optional canonicalization except at llvm.canonicalize). With the added twist that for inputs it’s a constraint that a denormal may be treated as 0.
My general feeling is if you have expectations for nan payload bits, we could consider a canonicalize-like intrinsic for observing payload bits which could provide any expected platform fixups.
As far as I know, at least 64bit x86 and 64bit ARM handle denormals perfectly IEEE-compliant by default. It would be quite bad if LLVM would interfere here and introduce flushing when the hardware has proper support.
No, not at all. Failing to quite a signaling NaN is introduced by LLVM optimizations. Denormal flushing is introduced by some hardware. Those are very different situations. LLVM should promise to never do denormal flushing unless the hardware does denormal flushing.
Consider the instruction fuml %x,1.0 where %x is a NaN
case 1) %x is an sNaN : converting fmul %z,%x,1.0 => %z ← %x preserves the signaling of the NaN and the consumption of %x in its next calculations uses the signaling property of this NaN.
case 2) %x is a qNaN : converting fmul %z,%x,1.0 => %z ← %x preserves the non-signaling of the NaN and the consumption of %x in its next calculations uses the non-signaling property of this NaN.
{Both without needing to know anything about the payload of the NaN}
Thus my reading of IEEE 754-2019 allows for the transformation of fmul %x,1.0 into just %x for all of the standard calculations {and for certain intrinsics too called “additional mathematical operations” in the standard.}
Until someone links your library into an executable compiled with -ffast-math, and suddenly you now have the wrong floating point mode register setting when your code didn’t expect it.
It is the same. Flushing doesn’t just happen, the optimizer can just know if the expectation is the lowering will treat it as such. You aren’t guaranteed a flush will happen, just like you aren’t guaranteed a signaling nan will be quieted. Nowhere goes out of its way to force a flush where one would not occur.
This is not standards-compliant. When inspecting the bits of %z, IEEE would provide a guarantee that this is a quiet NaN, but after the transformation that property is not upheld.
Modifying the floating point environment is commonly considered UB in C (and we will probably consider it UB in Rust). The reason it is UB is that compilers will optimize code assuming a flush does not occur, so if a flush then does occur, inconsistent results can arise.
Just because hardware has some non-standard modes doesn’t mean the vast overwhelming majority of code that works in the standard mode suddenly has to bear the cost of not knowing whether subnormals work as expected.
I should be guaranteed that a subnormal flush never happens (on common hardware, in the common case). LLVM must never introduce flushing by itself.
