test/waterlevel: Inconsistent test results

[mhaeuser]

The test "waterlevel" outputs different results based on the host CPU architecture (or so it seems). AARCH64 macOS and Linux both output an accumulated number of leaves of 7586, while x86-64 Linux outputs 7671. The currently expected value of 7622 is never hit on my machine. However, the value 7671 output by x86-64 Linux has been hit previously, but was changed with no reason provided: 0a5dfde

This leads me to believe there always has been some bug that causes inconsistent results and that it was simply masked by the commit above. AddressSanitizer and UndefinedBehaviorSanitizer do not report critical issues, only a few indirect memory leaks. All systems use glpk 5.0. Even rolling back to above's commit does not yield the currently expected value.

[christoph-grimm]

It is likely not a bug.
The number of leaves depends on the result of comparison among Double numbers, and in the test the values are often more or less (!!!) the same.
With different architectures and FP implementations and rounding modes this can give different results.

Note that the C++ AADD implementation (which is acceptable for reachability analysis purposes with larger starting ranges) does NOT consider FP roundoff errors; while the Java/Kotlin/Multiplatform one (AADD-MP which targets rather formal methods, constraint propagation) does this accurately.

[mhaeuser]

Hmm. Both x86 and M1 processors should "properly" conform to IEEE 754, I also made sure the rounding mode is the same. In fact, I can observe the difference in values even with Rosetta 2, which should quite literally just translate the float OPs (though I did not verify this)(I’ll have to re-test this later). M1 was also tested to yield equal results for known tricky problems compared to x86 CPUs: https://eclecticlight.co/2021/04/22/can-you-trust-floating-point-arithmetic-on-apple-silicon/

I guess the bit-level equality is mostly true for +, -, *, and /. Is there a particular operation (or location in the code) you have in mind I could verify actually deviates between the architectures?

EDIT: I also just forced -O0 to rule out any level of compiler optimizations (though I think they should not be applied under the standard float model), no change.

EDIT2: Added -ffp-contract=off -fno-fast-math, no change.

EDIT3: I added abort() to many "risky" operations, like AAF:sin(), :log(), etc., but they do not get hit. Looking at the sample, it seems to only use + and - at a high level, I do not see how any complex operations could be invoked from there.

[mhaeuser]

Sorry for the confusion, I made the wrong assumption that the arithmetics in the tool caused the deviation. However, they only appear on code paths involving GLPK. This includes both the min/max prints (one small deviation) and the conditionals (seemingly one deviation, but of course it propagates).

I guess the assert must be adjusted somehow. I’ll leave this open for tracking.