The Coq mailing list

[Jim Fehrle <jfehrle AT sbcglobal.net>]

>> Why is 32-bit Coq faster, if the 64-bit instructions are faster, and the system

>> is not RAM-limited?  I conjecture that the reason is *cache locality.*  That is,
>> you can fit a lot more 32-bit pointers into the 6 megabyte cache than you can
>> fit 64-bit pointers.

> So the idea is, the cache is effectively only half the size because all the data

> is twice as big?  Makes sense.  (Well I hope not *all* the data is pointers, but

> OCaml is pretty pointer-heavy after all.)  I am wondering if maybe memory
> bandwidth also plays a role, or is that usually way faster than anything like
> Coq needs?

That should be measurable.  The x86 has extensive performance measurement

counters.  One tool that uses them is Intel's VTune

(https://software.intel.com/en-us/intel-vtune-amplifier-xe/try-buy).

A sample output at https://software.intel.com/en-us/vtune-amplifier-cookbook-frequent-dram-accesses#HS

shows a breakdown of clock ticks spent waiting for L1, L2, L3 caches and DRAM.