Re: [isabelle] Any way to deactivate multithreading in Isabelle 2009-1?



On Wed, 24 Feb 2010, Thomas Sewell wrote:

Multithreading seems to be mildly useful on my desktop machine at work, with cpu usage of 110-150% of one core being reported.

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





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