Division by zero

Posted Jan 3, 2025 21:56 UTC (Fri) by dskoll (subscriber, #1630)
In reply to: Division by zero by Wol
Parent article: Preventing data races with Pony

In IEEE 754 floating point, 0.0 / 0.0 gives you NaN if you don't trap it. Once an expression yields a NaN, the NaN "infects" every other operator... any operator involving a NaN returns the NaN.

But that's floating point. Most CPUs don't have a way to represent a NaN in a variable of integer type. (Nor Inf nor -Inf, though I guess you could co-opt INT_MAX and INT_MIN respectively.)

Division by zero

Posted Jan 3, 2025 22:19 UTC (Fri) by quotemstr (subscriber, #45331) [Link] (20 responses)

Right. NaN is at least "I don't know". It may be imprecise, but it's not wrong. Zero is mathematical nonsense: imagine 60/5, 60/4, 60/3, 60/2, and 60/1: the quotients are 12, 15, 20, 30, and 60. Now you go to 60/0 and get zero? And then 60/-1 goes to -60? Weird discontinuity. I'd rather abort the program if it tries to do something nonsensical like divide an integer by zero.

Division by zero

Posted Jan 3, 2025 22:29 UTC (Fri) by dskoll (subscriber, #1630) [Link] (19 responses)

Yes, I agree. And most CPUs will raise an exception on integer divide by zero. This little C program:

int main()
{
    int x = 0;
    int y = 0;
    int z = x/y;
    return 0;
}

Does this when you run it:

$ ./test
Floating point exception
$ echo $?
136

Division by zero

Posted Jan 4, 2025 9:56 UTC (Sat) by pm215 (subscriber, #98099) [Link] (18 responses)

Well, x86 does that. But the CPU architecture you're next most likely to be running on today (arm) does not. There the division instructions are defined to produce a zero result without generating an exception if you divide by zero. I believe powerpc, mips and riscv also do not generate exceptions for integer division by zero.

Division by zero

Posted Jan 4, 2025 13:06 UTC (Sat) by pizza (subscriber, #46) [Link] (7 responses)

> But the CPU architecture you're next most likely to be running on today (arm) does not.

Historically, Arm processor didn't actually implement a hardware integer divider, so any faults/exceptions had to be triggered by the low-level software runtime library.

But starting with armv7-m and armv8, there are integer divide instructions, and they can generate divide by zero exceptions -- something I can personally attest to triggering numerous times. Here is the documentation on the UDIV/SDIV instructions on armv7-m:

https://developer.arm.com/documentation/ddi0403/d/Applica...

Meanwhile, IIRC the various Arm FPUs always supported faults/exceptions, including for divide-by-zero.

Division by zero

Posted Jan 4, 2025 18:03 UTC (Sat) by khim (subscriber, #9252) [Link] (4 responses)

> But starting with armv7-m and armv8, there are integer divide instructions

Yes.

> and they can generate divide by zero exceptions

No. Take your own link that, with one click, tells us how SDIV works on ARM 7-m. It looks like this:

if ConditionPassed() then
    EncodingSpecificOperations();
    if SInt(R[m]) == 0 then
        if IntegerZeroDivideTrappingEnabled() then
            GenerateIntegerZeroDivide();
        else
            result = 0;
    else
        result = RoundTowardsZero(SInt(R[n]) / SInt(R[m]));
    R[d] = result<31:0&rt;

Now compare that to ARM8 specification:

constant bits(datasize) operand1 = X[n, datasize];
constant bits(datasize) operand2 = X[m, datasize];
constant integer dividend = SInt(operand1);
constant integer divisor = SInt(operand2);
integer result;
if divisor == 0 then
     result = 0;
elsif (dividend < 0) == (divisor < 0) then
     result = Abs(dividend) DIV Abs(divisor); // same signs - positive result
else
     result = -(Abs(dividend) DIV Abs(divisor)); // different signs - negative result
X[d, datasize] = result<datasize-1:0>;

See that call to GenerateIntegerZeroDivide? I don't see it either.

Just why ARM decided that embedded version have to have “division by zero” exception while “big” CPUs have to silently produce zero is good question, but that's how things work currently.

P.S. Of course if you recall that RISC-V does things differently and x86, too… then question of codifying ARM-specific behavior in the language arises… but I guess it one of these “looked good at the time” ideas.

Division by zero

Posted Jan 4, 2025 18:10 UTC (Sat) by dskoll (subscriber, #1630) [Link] (1 responses)

Huh, you are right! Even though my Pi 4 is running an aarch64 kernel, userspace is 32-bit armhf and the test program raised SIGFPE. I tried the test program on a fully 64-bit Pi 4 with 64-bit userspace and it ran without complaint, assigning 0 to z.

Division by zero

Posted Jan 4, 2025 20:34 UTC (Sat) by pm215 (subscriber, #98099) [Link]

My guess is that your compiler is generating code that assumes the CPU doesn't implement the division instructions (because armhf includes v7-without-VE CPUs in its remit) and instead calls into the gcc runtime, and the runtime function is then manually raising a SIGFPE. (Possibly also the compiler figures out that it is a div by zero and generates a call to the div-by-zero runtime function.)

You can probably pass the compiler some kind of -march or -mcpu options to tell it to generate code assuming the v8 CPU you have, and then it ought to emit the udiv or sdiv inline, if you want to look at the behaviour in that situation.

Division by zero

Posted Jan 5, 2025 0:05 UTC (Sun) by pm215 (subscriber, #98099) [Link] (1 responses)

Re "codifying ARM-specific behavior in the language", it isn't necessarily that. The Pony FAQ justifies why you would want it to return *some value*, and having it return a known value rather than a random one is sensible for reproducibility. Then, you could pick anything, so why *not* 0? It makes no difference to the "branch away if divisor is zero" code you need to generate (and if you're really into shaving cycles then 0 has the advantage that you know for certain you already have it in the input value so you can copy it to the output and don't need to emit code to generate a fresh constant value).

Apparently various theorem provers also define their division this way:
https://xenaproject.wordpress.com/2020/07/05/division-by-...
and https://www.ponylang.io/blog/2017/05/an-early-history-of-... suggests that the inventory of Pony has some background in that kind of academic type theory/theorem proving area, so it seems plausible that the motivation for choosing 0 might been influenced by existing languages like that. Early 2010s seems a bit early for it to be very likely that a language designer was much influenced by fine details of codegen for Arm.

Division by zero

Posted Jan 6, 2025 0:38 UTC (Mon) by Heretic_Blacksheep (guest, #169992) [Link]

Mathematical correctness doesn't matter here because division by zero is undefined. You can literally make it anything you want - and I've seen math professors do so as an esoteric joke. However, programmers do not like non-deterministic error states. Pony makes the outcome deterministic, regardless of hardware traps that may or may not exist, allowing for a simple error check state across all architectures which the programmer can define as fatal or non-fatal depending on their program logic then handle it accordingly.

Given the alternatives, I'd much rather have a 'mathematically incorrect' deterministic result that I can take to the bank rather than depending on disparate architectural dependent error states that are really just as mathematically arbitrary as assigning X/0 == 0 but a lot more messy to deal with.

Division by zero

Posted Jan 4, 2025 20:19 UTC (Sat) by pm215 (subscriber, #98099) [Link]

Integer divide in A-profile comes in with the Cortex-A15 and A7, in v7VE, so some v7A cores have it, just not all. V7R requires it for the Thumb insn set but not the Arm one (!)

And yeah, as noted in the sibling comments M-profile has configurable trapping of integer division by zero, but A profile does not. (M profile diverges from A in various more or less obvious ways.) R profile also permits configuring trapping on div by zero. A profile never traps.

The v7A/R Arm ARM has a section that describes the various options:

https://developer.arm.com/documentation/ddi0406/c/Applica...

v8 got to clean this up by just having them be always present.

Division by zero

Posted Jan 4, 2025 20:54 UTC (Sat) by pm215 (subscriber, #98099) [Link]

By the by, on the floating point side of the house Arm has always supported setting the appropriate floating point status flag bit for fp division by zero, since this is a requirement of IEEE 754. Support for trapping (i.e. generating a CPU exception into the kernel instead of setting the status flag bit) is an implementation defined choice, though -- not many implementations choose to implement it (though I'm aware of at least one which does). As far as I know the only way to detect trapping support is to write a 1 to the FPCR/FPSCR "enable traps for this exception" bit and see if it reads back as zero or one -- if the implementation doesn't implement trapping then the bit will be RAZ/WI.

Division by zero

Posted Jan 4, 2025 13:22 UTC (Sat) by dskoll (subscriber, #1630) [Link] (6 responses)

I get the same SIGFPE on a Raspberry Pi 4 with an aarch64 kernel.

Division by zero

Posted Jan 4, 2025 18:09 UTC (Sat) by khim (subscriber, #9252) [Link] (5 responses)

SIGFPE sounds suspiciously like result of floating-point operation. We are talking about integer division here.

Division by zero

Posted Jan 4, 2025 18:12 UTC (Sat) by dskoll (subscriber, #1630) [Link] (2 responses)

Yes, I know. Nevertheless, SIGFPE is the signal that gets raised.

$ cat /tmp/test.c
#include <stdio.h>
int main()
{
    int x = 0;
    int y = 0;
    int z = x/y;
    printf("z = %d\n", z);
    return 0;
}

$ strace /tmp/test
[... bunch of stuff elided ...]
--- SIGFPE {si_signo=SIGFPE, si_code=FPE_INTDIV, si_addr=0x55c090d59153} ---
+++ killed by SIGFPE +++
Floating point exception

Division by zero

Posted Jan 4, 2025 22:56 UTC (Sat) by khim (subscriber, #9252) [Link] (1 responses)

How do you compile that? GCC is smart enough to recognize UB and produce appropriate brk if optimizations are enabled, but that's not related to what CPU is doing. And unoptimized version calls function that can check the divisior.

Try to invoke sdiv directly, then CPU should do what it does. At least for me it produces zero, as CPU manual promised.

Division by zero

Posted Jan 4, 2025 23:18 UTC (Sat) by dskoll (subscriber, #1630) [Link]

I compiled in both cases with make test which simply invoked gcc with no optimization. I checked the assembly output and you are right. On the armhf architecture, it looks like gcc calls into a library function:

        bl      __aeabi_idiv

but on the aarch64 architecture, it calls an assembly instruction:

        sdiv    w0, w1, w0

Division by zero

Posted Jan 4, 2025 19:15 UTC (Sat) by excors (subscriber, #95769) [Link] (1 responses)

glibc says: (https://sourceware.org/glibc/manual/2.40/html_node/Progra...)

> The SIGFPE signal reports a fatal arithmetic error. Although the name is derived from “floating-point exception”, this signal actually covers all arithmetic errors, including division by zero and overflow.

(It notes the integer overflow exception is "impossible in a C program unless you enable overflow trapping in a hardware-specific fashion".)

Division by zero

Posted Jan 4, 2025 22:58 UTC (Sat) by khim (subscriber, #9252) [Link]

I'm surprised not by SIGFPE per see, but by the fact that SDIV suddenly started producing exceptions. Raspberri Pi 4 uses ARM Cortex-A72 which uses ARMv8-A and on ARMv8-A result should be zero, not exception.

If you avoid UB and functions that do manual checks, at least.

Division by zero

Posted Jan 6, 2025 15:52 UTC (Mon) by paulj (subscriber, #341) [Link] (2 responses)

Oh, interesting. Is there any way to enable signal or some exception bit to detect this? (Like FP has, per standard)

Division by zero

Posted Jan 6, 2025 17:39 UTC (Mon) by farnz (subscriber, #17727) [Link] (1 responses)

Not for the integer UDIV and SDIV instructions. You can see in the "Operation" section (which uses Arm Pseudocode to describe the behaviour in abstract terms) that the instruction unconditionally outputs a 0 result if the input divisor is 0.

Division by zero

Posted Jan 7, 2025 11:01 UTC (Tue) by paulj (subscriber, #341) [Link]

Hmm, ouch.

GCC seems to have some useful options to help catch int-div-0 in testing, including for its analyzer and sanitizer, and also a -mcheck-zero-division - which is enabled by default for -O0 and -Og.