[isabelle] Parallelism in Isabelle 2009-1



Hey Isabelle users.

I've been playing with Isabelle 2009-1's parallelism features for a while now, and have come to the conclusion that I can never get quite what I want from them. There are two problems. On my desktop machine at work, I can't safely enable parallelism. On my desktop machine at home, I can't completely disable parallelism.

The first problem is that the L4.verified proof repository I work on is huge (tens of thousands of lemmas and hundreds of thousands of lines of proof). This exposes a problem with parallel proof checking. CPU usage looks good to begin with but then our systems very rapidly run out of memory and start thrashing. I suspect the problem here is that for every proof saved for later checking the relevant context needs to saved as well. Our contexts get quite large, so the theory-parsing thread doesn't have to get far ahead of the proof-checking threads for memory to run out. The solution to this is to turn off parallel proof checking.

Furthermore, although Isabelle 2009-1 loads theories in parallel this does not seem to translate to CPU parallelism. It is clear from the log chatter that multiple theories are being loaded at once, however, when parallel proofs are disabled CPU usage remains at one core's worth. Running UNIX top and showing thread decompositions (press "H") reveals that there are multiple polyml threads running but their CPU usage always adds to exactly one core. It looks a lot like there's a lock somewhere all the threads need to run. This prevents me getting any parallel execution on my work machine.

Finally, on my machine at home, which seems to act up in the context of parallelism, I can't disable it. I can turn off parallel proof checking and set the maximum thread count to 1. UNIX top confirms that this reduces the number of polyml threads created from 7 to 2, which then share the CPU between them in exactly the same way. This prevents me disabling real parallelism on my home machine. I can still run a busy loop on the other core, which seems to hide the mysterious issues.

Do other users see the same behaviour? Do the developers know what's going on? Could it be easily fixed?

Yours,
   Thomas.





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