The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Just to be clear on the reason that Coq's native integers are 31 bits.

Obviously the integers Coq uses have to be machine independent, out of concern for consistency. We chose 31-bit because they fit in a machine word of every (reasonable?) machine (the runtime reserves the last bit of every word to tell the garbage collector whether we are in the presence of a pointer or not).

Of course, it would be arguably better to have 63bit integers and emulate them on the 32bit architecture. However, there is a trick to Coq: since it must evaluate open terms, there is a representation of variables in the bytecode values. The integer operation are nonsense on variables*. As it happens, variables (and more generally terms with a variable in head position) are represented as blocks (aka pointers), and so we use the gc-bit to discrimate: if we see a pointer, the operations are done inefficiently, if we see a simple value, we use the efficient processor arithmetic. We would need to replace this trick with a more complex one for bigger integers to be emulated on a 32-bit architecture. Currently there has been some effort in having a more efficient implementation of native integers into Coq. As it is more complex, it still hasn't been integrated, I don't actually know where this prototype stands on the issue of integer size.


[*] in fact, native integers are compiled from actual Coq terms which can have variables in them, not necessarily in head position. So there is an extra case which we have to handle: that of a constructed term. Fortunately, the constructed terms with non-nullary constructors are also pointers, and the catch-all case for pointers handle them properly.

On 24 March 2014 08:46, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

On 24/03/2014 07:10, Moshe Tenenbaum wrote:

Gabriel and Enrico, thank you very much for your responses! Good step
forward for me.

My next question regards if there is any possible way to go a bit
further with the code. FOr example, in the coq_interp.c code you
mention, on line 1300, there is an instruction that looks like this:

Instruct (TAIL0INT31) {
     int r = 0;
         uint32 x;
         print_instr("TAIL0INT31");
     x = (((uint32) accu >> 1) | 0x80000000);
         if (!(x & 0xFFFF)) { x >>= 16; r += 16; }
         if (!(x & 0x00FF)) { x >>= 8;  r += 8; }
         if (!(x & 0x000F)) { x >>= 4;  r += 4; }
         if (!(x & 0x0003)) { x >>= 2;  r += 2; }
         if (!(x & 0x0001)) { x >>=1;   r += 1; }
         if (!(x & 0x0001)) {           r += 1; }
         accu = value_of_uint32(r);
         Next;
       }

Can this be transformed using mnemonics like uint64 instead of uint32?

Sure, you can declare x of static type uint64. But presumably, any optimizing compiler is already doing this transformation behind the scenes when it is beneficial for performances.

You can even go further with mnemonics and substitute all of this code with __builtin_ctz(x) (assuming this construct is portable enough) and let the compiler do its black magic. That said, I doubt that it would bring any noticeable speed-up.

(By the way, I am noticing that the last test is pointless, since it always evaluates to false.)

And can it be extended for TAIL0INT63 for proper memory allocation?

No, it can't. Keep in mind that this is just the tiny C part of a huge Coq development about 31-bit integers. If you change the width of integers there, you will have to modify some Coq theories in depth and deal with the fallout of breaking user formalizations.

I am not saying it is a bad idea. In fact, I whole-heartedly support switching Coq native integer from 31 bits to 63 bits in the long run. I am just saying that this is a much more massive endeavor than the code might suggest.

Best regards,

Guillaume