coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Timothy Carstens <intoverflow AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Coq CPU recommendations
- Date: Wed, 17 Jun 2015 12:47:14 -0700
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.
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.
- Re: [Coq-Club] Coq CPU recommendations, (continued)
- Re: [Coq-Club] Coq CPU recommendations, Eric Mullen, 06/16/2015
- Re: [Coq-Club] Coq CPU recommendations, Timothy Carstens, 06/16/2015
- Re: [Coq-Club] Coq CPU recommendations, Adam Chlipala, 06/16/2015
- Re: [Coq-Club] Coq CPU recommendations, Timothy Carstens, 06/16/2015
- Re: [Coq-Club] Coq CPU recommendations, George Van Treeck, 06/16/2015
- RE: [Coq-Club] Coq CPU recommendations, Soegtrop, Michael, 06/17/2015
- RE: [Coq-Club] Coq CPU recommendations, Soegtrop, Michael, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Enrico Tassi, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Matthieu Sozeau, 06/17/2015
- RE: [Coq-Club] Coq CPU recommendations, Soegtrop, Michael, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Adam Chlipala, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Timothy Carstens, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Timothy Carstens, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Pierre-Marie Pédrot, 06/18/2015
- Re: [Coq-Club] Coq CPU recommendations, David MENTRE, 06/18/2015
- RE: [Coq-Club] Coq CPU recommendations, Soegtrop, Michael, 06/18/2015
- Re: [Coq-Club] Coq CPU recommendations, Adam Chlipala, 06/18/2015
- RE: [Coq-Club] Coq CPU recommendations, Soegtrop, Michael, 06/19/2015
- Re: [Coq-Club] Coq CPU recommendations, Pierre-Marie Pédrot, 06/18/2015
- Re: [Coq-Club] Coq CPU recommendations, Timothy Carstens, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Timothy Carstens, 06/17/2015
- RE: [Coq-Club] Coq CPU recommendations, Soegtrop, Michael, 06/17/2015
- Re: [Coq-Club] Coq CPU recommendations, Eric Mullen, 06/16/2015
Archive powered by MHonArc 2.6.18.