[isabelle] Isabelle/jEdit and hyperthreading


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.

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