Re: [isabelle] Isabelle/jEdit and hyperthreading
On 29/06/15 14:22, Harry Butterworth wrote:
I think the behaviour has changed between 2014 and 2015 as 2014 used to use 100% of CPU with
hyperthreading turned on and 2015 now peaks only just above 50%.
I've been running with hyperthreading disabled in the BIOS anyway as I did some benchmarking (using
run_tests from seL4) with 2014 and the fastest configuration I found (for my x5680) was with
hyperthreading disabled. Some of the tests were a bit faster at the same clock speed with
hyperthreading disabled but the main benefit was that by disabling hyperthreading I could run with a
higher clock speed for the same CPU temperature at max load.
I also benchmarked the difference between speedstep on and off (on an i7 5820k this time) and see a
10% improvement by turning speedstep off which will be useful in the winter when I need a heater.
Thanks, Harry, informative to hear your results. I don't have the same processor, but I suspect mine
behaves the same in limiting the clock frequency with hyperthreading enabled. I don't want to
disable it or speedstep, so I'll just live with my current setup.
On 29 Jun 2015 09:08, "Matthew Fernandez" <matthew.fernandez at nicta.com.au
<mailto:matthew.fernandez at nicta.com.au>> wrote:
Isabelle/jEdit has an option to configure the number of threads in use for parallel proofs:
Plugins > Plugin options > Isabelle > General > Parallel processing > Threads
By default, this is set to 0 which indicates the "hardware max." I find on machines with
hyperthreading, this means the
number of physical cores, not the number of logical hardware threads. E.g. on a machine I have
here with 2 hyperthreaded
cores, Isabelle/jEdit appears to use 2 threads when I would prefer 4. I realise I can set this
manually, but I was
wondering if the default behaviour is deliberate? Perhaps the assumption is that the shared
resources on the cores are
kept busy enough by Isabelle that the extra threads won't help. I'm just asking out of
curiosity, more than anything
else. The host environment is 64-bit Linux by the way.
The information in this e-mail may be confidential and subject to legal professional privilege
and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by
this email or its attachments.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
This archive was generated by a fusion of
Pipermail (Mailman edition) and