Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.



I'd just like to add that this problem can be compounded by some other issues, such as one we mentioned before where a diverging "blast" can slow down jEdit. On rare occasions I've had to go hunting for blasts and fastforces in the future part of my theory just to get enough CPU back to work on the problem I have.

Not sure what else to say about it, but if some improvement to the prioritising of these speculative calculations could be made, I'd be all for it.

Cheers,
    Thomas.

On 22/04/14 23:22, Makarius wrote:
On Tue, 22 Apr 2014, Lars Noschinski wrote:

On 22.04.2014 14:47, Makarius wrote:
That is a relatively weak CPU, but Intel makes it appear stronger via
hyperthreading, thus it gets somewhat overloaded and burns a lot of
CPU cycles (literally, by turning them into heat).
You have now often recommended reducing the number of threads to the
number of real physical cores. Does this hold for interactive mode only?
Because on my machine (a quadcore with 8 virtual cores), there are
several theories in the AFP with a speedup factor around 5 or even 6; so
at least raw throughput sometimes profits from the virtual cores on
Isabelle workload.

I also do systematic "overburning" of CPU cycles in batch mode, it gives me (real) warp factor 9.6 for 8 real cores (Intel Xeon from 2009) -- hyperthreading actually has a purpose. Concerning the "factor" one needs to be careful, though: the figure given in Isabelle build on the spot is merely the relative burn-factor of CPU cycles, and that is a quite distorted version of the true speed-up factor compared to sequential mode.


So yes, one could probably make this a general rule of thumb: interactive mode refers to physical CPU cores and batch more to the maximum number of virtual CPU cores, even more.

I usually get that effect by having the persistent default options as described before, which will be also the default in the next release. For batch builds I then give a generous -j4 to the implicit -o threads=4. In this "4x4" mode (which means "4-wheel drive" in French), I get the "sound of speed" in my office from the CPU fans, and Isabelle + AFP built quite fast.


    Makarius






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