Rob Arthan wrote:
On 26 Jul 2009, at 19:37, David Matthews wrote:
Rob Arthan wrote:
We have performance problems with ProofPower when compiled with
Poly/ML using the latest sources as compared with version 5.2.1. The
main problem is with loading a large state. In some of QinetiQ's
tests, it now takes nearly 40 minutes to load a state (occupying
about 150Mb on disc) that previously took about 20 seconds.
Unfortunately, my attempts to create simple examples of this type
problem do not exhibit much difference between 5.2.1 and the latest
sources. I wondered if anyone else has had similar problems or has
any suggestions about how to isolate the problem.
I believe the problem is quite old. It apparently predates the move
from CVS to SVN.
Thanks. The binary chop wasn't very arduous: the problem first shows up
at SVN revision 595. It looks like some changes in exporter.cpp could
be relevant. Let me know if there are any useful sizings that I can
provide.
Rob,
Thanks for narrowing down the problem. That update changed the
calculation of the buffer size used when saving state. Previously both
saving state and exporting calculated the size based on the total active
memory, both that currently used for saved states and also local data.
The effect of that was to grossly overestimate in the case where a
program was saving a succession of states, each a child of the previous.
This was the case when building with the experimental IDE which ended
up running out of memory so I changed it so that a saved state
calculated the space based only on the local data. I suspect that in
your example you are loading a hierarchy of states and then saving a new
top-level state which amalgamates them. Is that right? If so I'll
contact you off-list and try an alternative calculation based on the
actual hierarchy level.
Regards,
David
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
