The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

 

If this is of interest for the community, I could run some benchmark through VTune and publish the statistics. This would give quite some insight into what makes sense in terms of cache size, DRAM size, DRAM bandwidth and CPU clock.

 

The question is what would be an appropriate benchmark.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Timothy Carstens
Sent: Wednesday, June 17, 2015 9:47 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq CPU recommendations

 

Here's a question this thread begs: how cache efficient does Coq wind up being? Like, internally is it just creating tons of copy-on-write structures? How smart is it about reusing objects which are due to fall out of scope (think temp values constructed during reductions)?

Could be the cache barely matters, if the allocation/reuse strategy is too simple.

On Jun 17, 2015 11:52 AM, "Timothy Carstens" <intoverflow AT gmail.com> wrote:

This is why I recommend going with quad-channel DDR. Anything less is gamer/homework grade. If you're doing gigs of symbolic computation, and especially if you're going multi-core, the extra memory bandwidth is a must.

And don't overclock your memory, itll drive up your bandwidth but also wreck you latency. Most of your memory operations will be to/from CPU cache (versus memcopies via PCIe go a peripheral) so you will be doing relatively small burst read/write, and thus need low latency RAS/CAS settings for your memory (hard to do when overclocked).

-t

On Jun 17, 2015 10:49 AM, "Adam Chlipala" <adamc AT csail.mit.edu> wrote:

On 06/16/2015 05:33 PM, George Van Treeck wrote:

But, I would be surprised if anyone is using more than 4G of memory for Coq.

My collaborators (the original poster is one of them) and I work on Coq developments in a fairly unusual style, pushing the limits of proof automation.  In that style, it's not too hard to wind up with one source file that, compiled by Coq without using parallelism, uses 20 GB or more.  We at least need 16 GB of RAM available to avoid needing to waste time on too much memory optimization during the initial exploratory stages of a new proof.