Negative zero causes different results for interpreter mode and compiler mode

[DerZc]

Hi,

This problem related to #1378 . But I find that negative zero causes different results for interpreter mode and compiler mode (with -c).

This is the dl file and input:
orig.zip

In interpreter mode, the result is 0 and -0. In compiler mode, the result is -0. Maybe these shouldn't be different.

Souffle version is 2.3, the newest release version.

[DerZc]

Hi,

I find another example that zero not equals to negative zero in both interpreter mode and compiler mode.

The datalog file is:

.decl pnlj(A:float, B:float)   
.decl sxnr(A:float, B:float)  

.input pnlj  

sxnr(A, A) :- pnlj(A, A).  
.output sxnr  

The input of pnlj is:
-0.0 0.0

The result of them are both empty.
But in the previous example, in compiler mode, if zero equals to negative zero, the result should be 0 0 or -0 0.

I found this bug in the release version 2.3. Under this version, in compiler mode, if inputs comes from facts file, 0 not equals to -0. but if inputs comes from datalog file. 0 equals to -0. I tested it in the last commit version 3cd802d and found it vas fixed.

[DerZc]

I guess the reason is that if there is (0.0, -0.0) in a fact abc, and abc is a subgoal of a rule abc(A, A), in this case 0.0 not equals to -0.0. But in other comparison 0.0 equals to -0.0.

[b-scholz]

The problem is that the interpreter uses a bitwise comparison, and the compiler uses a proper floating-point comparison. A fix is possible but requires dealing with corner cases, i.e. weakening/strengthening the bitwise comparison to become functional equivalent with a floating point comparison. The bottom line is that the interpreter must use bit equivalence (no other way due to de-specialization - see PLDI paper).

Have a look here:

https://codingnest.com/the-little-things-comparing-floating-point-numbers/

Do you have time to fix this issue? I am happy to guide you. The first step is to build a comparison based on bit comparison that deals with the corner cases as an additional constraint.

[DerZc]

I have a question that whether all comparisons under the compiler mode are float-point comparisons? But in compiler mode, in the first example, 0 equals to -0, and in second example, 0 not equals to -0.

[b-scholz]

The problem is that Souffle synthesizes relational data structures for the compiler. Hence, the floating-point comparison works for the compiler. However, we cannot do the synthesis perfectly for the interpreter because it would require an exponential number of pre-compiled data structures. To overcome the exponential blowout, we compare floating-point numbers bitwise, which works most of the time.

To fix this problem, we would need an extension to bitwise comparison for mimicking floating-point comparison. Something like this:
bitmap(a,b) && magic1(a, b) || magic2(a,b)
which is semantically equivalent to fcmp(a,b).

What are the predicates magic1/2 without using fcmp?

I am happy to expand more.

[DerZc]

It is interesting! But I'm afraid I don't have time to fix this bug. We are primarily interested in designing and evaluating a new testing approach, I wonder whether it is useful if we report this and other bugs?

[b-scholz]

Numerous issues were reported on the same problem, i.e., comparing two floating-point numbers does not work in the interpreter. We need to summarise all previously found issues that relate to this problem.

The giveaway is

• Compiler works
• Interpreter does not work
• Floating point numbers have strange values (NaN, -0.0, 0.0, oo etc)

Would you like to review the issue list and summarise/link the issues?

[quentin]

Could we have a non-specialized btree for situations like this one? It would probably be a bit slower, but sound.

The kind of comparison (signed/unsigned/float-direct/float-margin/float-epsilon/...) of each field would be somehow encoded so that the non-specialized comparator could perform an accurate tuple comparison.

This would also allow the interpreter to index inequalities on non-signed values, something that is not allowed yet and has significant impact on the performance:

souffle/src/ram/transform/MakeIndex.cpp

Lines 100 to 107 in 429676c

	// don't index FEQ in interpreter mode
	if (op == BinaryConstraintOp::FEQ && interpreter) {
	return {mk<UndefValue>(), mk<UndefValue>()};
	}
	// don't index any inequalities that aren't signed
	if (isIneqConstraint(op) && !isSignedInequalityConstraint(op) && interpreter) {
	return {mk<UndefValue>(), mk<UndefValue>()};
	}

And it would also support arbitrary large arities to allow for relations beyond the current limits of the interpreter:

souffle/src/interpreter/Util.h

Lines 81 to 84 in 4226e49

	func(Btree, 18, __VA_ARGS__) \
	func(Btree, 19, __VA_ARGS__) \
	func(Btree, 20, __VA_ARGS__)

[b-scholz]

The problem is that we don't know which attributes are floating point numbers ahead of time.
Even if we reshuffle the floating point numbers to the beginning, we would have a quadratic number of specialized relations.

Let's assume a relation that has an arity of five. Then, we would require the following specializations for this relation:

n,n,n,n,n
f,n,n,n,n
f,f,n,n,n
f,f,f,n,n
f,f,f,f,n
f,f,f,f,f

where f stands for floating-point and n stands for bitwise-comparison (numeric).

The other option is to provide the comparator as a function pointer with pre-compiled comparators. However, previous experiments showed that this is slow.

[quentin]

For the sake of soundness, at the cost of the performance, I suggest we add a non-specialized version of the btree where we don't specialize anything:

• The arity of the btree tuple is given by a member variable of the btree instance: size_t arity.
• Each tuple of the btree is sequence of RamDomain elements.
• Maybe each btree node contains a fixed-size array of N RamDomain elements where tuples are stored consecutively, so each node can store up to N/arity tuples.
• The logical types of each element of a tuple are stored in an array member of the btree instance: ElemType elemTypes[].
• enum ElemType { Signed, Unsigned, Float }.
• The actual value of a tuple element requires a conversion from RamDomain to the appropriate RamSigned/Unsigned/Float.
• The comparator function is a non-specialized function that takes the arity and the logical types array of the btree and perform a tuple comparison accordingly. Each couple of elements is first converted from RamDomain according to its logical type and then compared.

[b-scholz]

Quentin - I think you are right here. We should switch to slow data structures when we see floating point numbers as attributes and/or the number of arities exceeds. The suggestion would be to have a b-tree data structure with a generic comparator (we provide a relational signature) and arbitrary arity so that the interpreter can fall back to such a data structure if the specialized versions fail to suffice the instance requirements. We had something similar in the past. Either we check out the data structures for the old interpreter or create a new one.

[DerZc]

Hi,

I meet another situation that have the same issue as this, but not the same reason. I guess the reason is there is difference in input handler between interpreter.

There is an example:

.decl a(A: float, B:float)
.decl b(A: float)
.input a

b(A):-a(A, 0.0)
.output b

The input of a is:

0.0         -0.0

As in the interpreter, 0.0 not equal to -0.0, so result should be empty. But result is 0.0.

So I think this might be a different situation with the one discussed above.

[b-scholz]

@ohamel-softwaresecure reported these issues a while ago. Please check old issues.

[DerZc]

Hi,

I find another case, I don't know whether they are the same case:

.decl a(A:float)
.decl b(A:float)

a(-0).

b(A) :- a(A), 0.0 = A.

.output b

I run with souffle simple.dl, then the result is -0. As 0 not equals to -0, so the result should be empty?

[DerZc]

I found another case, not sure if they have the same reason, so just report here.
In interpreter mode, the following program return 0, but if I remove inline or replace it with magic, it returns -0.

.decl olkw(A:float)
.decl kkcb(A:float) inline
.decl nvuk(A:float)
.output nvuk

olkw(-0).
kkcb(A) :- olkw(A).
nvuk(A) :- kkcb(A), 0.0 = A.