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