Re: [isabelle] sledgehammer in RC4



Hi Jasmin,

Thanks for your answer.  I'm not sure if it is useful or harmful to
count the hyperthreads (double the number of real cores).  The host OS
(OSX or Windows or Linux) can see the difference between cores and
hyperthreads, and hopefully schedules accordingly (i.e. distributes
threads to different cores before using a hyperthread on a core
already running).

The issue is complicated by the fact that I'm running Ubuntu in a VBox
virtual machine. Probably (but I don't know, and haven't been able to
ascertain from VBox documentation) VBox simply spawns guest threads
and leave it to the host OS to schedule them.  That would imply that
no harm is done by telling isabelle the number of hyperthreads rather
than the number of cores.

Unless someone on the list knows about this, experimentation is required.

Best,
Randy
--

On Thu, Nov 14, 2013 at 3:51 PM, Jasmin Blanchette
<jasmin.blanchette at gmail.com> wrote:
> Hi Randy,
>
> Sorry for the delay in answering.
>
>> BTW, how does Multithreading.max_threads_value get set to 2, can I
>> change it, and would that do any good?  You and Makarius probably
>> understand this point better than I: a modern "dual core" Intel
>> machine has 4 hardware threads.
>
> In Proof General, this should do the trick:
>
>     ML {* Multithreading.max_threads := 4 *}
>
> In jEdit, there appears to be an option called "threads" that one can set (judging from the code in "Pure/PIDE/protocol.ML" -- I'm faster at grepping than at searching my way through GUIs).
>
> I hope this helps. And please let us (or me) know if you run into more issues with Sledgehammer.
>
> Regards,
>
> Jasmin
>
>




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