[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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and