Re: [isabelle] sledgehammer in RC4



On 11/10/2013 11:36 AM, Randy Pollack wrote:
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.

Randy,

I didn't see that anyone answered this, and it was of interest to me, because of how Sledgehammer used to deal with virtual cores (# of threads), but things have changed to how I wanted them. It ceased to be an issue for me because I currently use an older quad core with no virtual threads.

I have a laptop with an i3-330m:

http://ark.intel.com/products/47663/

As the Intel web page shows, it has 2 hardware cores and 4 virtual threads. My use of "ML {* Multithreading.max_threads_value () *}" for that laptop returns "it = 4". For the older quad core that I use, which has no virtual threads, it returns "it = 4". For a newer i7 with 4 cores, and 8 threads, I assume it would return "it = 8".

For the i3-330m, when I run sledgehammer with "e spass z3_tptp z3", on a theorem it can't prove, with a 60 second timeout, I see 4 processes start up, SPASS.exe, eprover.exe, and two copies of z3-solver.exe, all taking up to about 25% of the CPU.

That's good, because with Isabelle2012 (or whatever I was using at the time), it would only run 2 provers at a time on that laptop. So when I get an i7, it hopefully will run 8 at a time.

I guess if you get "it = 2", it means you have an older dual core that has no virtual threads.

Regards,
GB






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