Re: [isabelle] Useful number of cores for running Isabelle (was: running Isabelle on a Mac)



On 17/06/2019 17:00, Eugene W. Stark wrote:
> 
> My main machine has been a 4-core i5-4670K @ 3.40GHz.

Currently the high end for home machines is something like 8-core i7 /
i9 @ 3.60 GHz. It also helps to have extra-fast RAM and SSD.


> I did some experiments using cloud servers on Digital Oceanhe maintenance level.
> 
> The vCPUS identify as the following:
> 
> model name	: Intel(R) Xeon(R) Gold 6140 CPU @ 2.30GHz
> cpu MHz		: 2294.608
> cache size	: 25344 KB
> 
> I tried doing "isabelle build" of my projects using configurations with various numbers of vCPUs
> and watching the load average, CPU utilization, number of threads, and so on.  I found that it
> was difficult to find situations where more than about 8 CPUs were in use and the overall average
> speedup factor was more like about 3x.

For a single session, 8 cores is indeed the optimal number for most
applications. Typical speedup is in the range of 3..7.

For full-scale maintenance of many (parallel) sessions, notably AFP, it
makes sense to have 80 cores around. Usually these are arranged in a
non-uniform manner. Often, server hardware is actually just a
single-board cluster of 8-core nodes.


> Also, the 2.30GHz Xeon CPUs on the cloud server are somewhat slower than my 3.40GHz i5 CPU at home,
> so it actually turns out that I still get stuff done faster on my home system than if I use the
> cloud server with double the number of cores.

Yes, I guess this is normal for most clouds.


> A question that comes to mind is what is it that usually limits the amount of concurrency when
> using Isabelle?  Although obviously the source has to be parsed and type-checked before anything else
> can be done, and that seems to occur in a initial pass over the code that runs ahead of the actual
> proof checking, once that has been done it seems like as many of the basic proof steps as you like
> ought to be doable in parallel.  So I wonder why that doesn't happen.

Processing of Isabelle document sources (not "code") has many aspects.
It depends a lot on the structure of the application how much implicit
parallelism is in there by default. Scalable parallel executation is one
of the big challenges of computer-science. Isabelle is already quite
advanced in this respect, but we now also see the limits of hardware:
parallel shared-memory access is a typical bottle-neck.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.