Re: [isabelle] Isabelle/jEdit and hyperthreading

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.
On 29 Jun 2015 09:08, "Matthew Fernandez" <matthew.fernandez at>

> Hi,
> 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.
> Thanks,
> Matt
> ________________________________
> 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 MHonArc.