Re: [isabelle] RC4: sledgehammer on Cygwin crashed once; temp file not removed



On Tue, 26 Aug 2014, Gottfried Barrow wrote:

Finally another crash.

This is following a pattern. The crash doesn't happen until after I terminate the sledgehammer command, and then it's not immediate.

In this case, I haven't changed threads back to threads=4, it's still at 12, with the 17 provers.

About 30 seconds after I terminated a sledgehammer command, I was staring at the screen thinking about what I wanted to do, and it terminated. The "Isabelle Syslog" message is below:

Welcome to Isabelle/HOL (Isabelle2014-RC4: August 2014)
assertion "baseAddr > (PolyWord*)obj && baseAddr < ((PolyWord*)obj)+length" failed: file "gc_mark_phase.cpp", line 439, function: virtual void MTGCProcessMarkPointers::ScanAddressesInObject(PolyObject*, POLYUNSIGNED)

This one is already quite well-known in internal circles.

It can happen when the Poly/ML runtime system and memory management is under high pressure -- we've increased that pressure on the application side significantly since the last release. Trying to hunt it down and pin it up, I have found out that Windows has a much higher chance to expose that bad behaviour, presumably due to more narrow memory resources on Cygwin. The situation might become better again, after switching to Cygwin x86_64, but I have not tried it yet.

Note that David Matthews did not manage to eradicate the source of the problem, because it never happened on any of his machines, and the people who have seen it elsewhere could not repeat it reliably.


	Makarius




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