[isabelle] Any way to deactivate multithreading in Isabelle 2009-1?
- To: Isabelle Users ML <cl-isabelle-users at lists.cam.ac.uk>
- Subject: [isabelle] Any way to deactivate multithreading in Isabelle 2009-1?
- From: Thomas Sewell <Thomas.Sewell at nicta.com.au>
- Date: Wed, 24 Feb 2010 13:01:38 +1100
- Accept-language: en-US
- Acceptlanguage: en-US
- Thread-index: AQHKtPVMJ1Y0Ad99rEeYXtg/RsA2lw==
- Thread-topic: Any way to deactivate multithreading in Isabelle 2009-1?
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and