Email Gateway (Aug 18 2022 at 14:37): Email Gateway (Aug 18 2022 at 14:37):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Is there any simple way to deactivate multithreading in Isabelle? I'm using Isabelle 2009-1 with PolyML 5.3, and I'm seeing multithreading for the first time.
Multithreading seems to be mildly useful on my desktop machine at work, with cpu usage of 110-150% of one core being reported. On my desktop machine at home, though, it seems to cause random and unrepeatable build failures. More than 5 different attempts to build the HOL image failed 5 different ways, sometimes with a meaningful but unexpected exception being reported and sometimes with no explanation.
I've discovered the way to make progress is to tie up the other cores with useless work. These days I use a busy loop written in 10 lines of C code, although the original discovery involved Unreal Tournament. Interestingly PolyML's CPU usage still peaks at around 120% of one core - it must be getting CPU quota for 2 or 3 threads while my busy loop gets less. Curiously, this does not seem to create a problem, or at least, it's not so likely.
Anyway, is there an environment variable or ML reference I can tweak to disable threading for more reliable builds?
Yours,
Thomas.
Email Gateway (Aug 18 2022 at 14:37):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
I've seen it done as follows:
ML {* Multithreading.max_threads := 1 *}
ML {* Goal.parallel_proofs := 0 *}
Jasmin
Email Gateway (Aug 18 2022 at 14:37):From: Gerwin Klein <gerwin.klein@nicta.com.au>
The options -M and -q in isabelle usedir govern the settings for multithreading.
Putting in your ~/.isabelle/etc/settings
ISABELLE_USEDIR_OPTIONS="-M 1 -q 0"
should do what you want. Random crashes on HOL are still disconcerting, though.
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 14:38):From: Makarius <makarius@sketis.net>
Indeed, and it should not happen. (Which does not mean that I did not see
all kinds of weird crashes in earlier versions of the system.)
Can you give some details about your hardware and operating system? It
might be even a strange C library that is dynamically linked against our
prebuilt Poly/ML binaries.
Since multithreading is already commonplace -- and the next version of the
toplevel will not work without it -- one really needs to isolate the
remaining problems now.
Makarius
Email Gateway (Aug 18 2022 at 14:38):From: Makarius <makarius@sketis.net>
On a dual-core machine you should normally see 160-180% CPU usage, unless
the theories are pathologically sequential. There is also a correllation
with available heap space, and providing an adequate initial default can
make a big difference, e.g. like this:
ML_OPTIONS="-H 1000"
This assumes you have something like 2 GB of real memory. The official
default is still targeting 512 MB, and it is probably time to adjust it to
1 GB real memory for the next release, or make the installation somehow
smarter in detecting hardware resources. (So far there is still the basic
assumption that power users understand Isabelle settings, which are
explained in the Isabelle system manual.)
Makarius
Last updated: Apr 23 2024 at 20:15 UTC