I seem to be able to pretty reliably produce the following:
Exception- InternalError: indirect - invalid constant address raised while compiling
Exception- InternalError: indirect - invalid constant address raised while compiling
Unfortunately, it takes hours to get there...
Switching to --gcthreads=1 may have fixed another error we were having, relating to unwarranted pointer-equality tests.
Michael
On 21/02/14 22:30, David Matthews wrote:
Hi, I'm aware of a number of assertion failures that seem to occur intermittently. This is one of the ones on my list. I suspect they are all symptoms of the same bug but I have never been able to narrow it down or reproduce it. It does seem to occur when the memory management is under heavy load.
Thanks for reporting it and if anyone manages to reproduce it more consistently I would be very interested.
Regards, David
On 20/02/2014 14:21, Ond?ej Kun?ar wrote:
Hi! In the past couple of months I've gotten a crash of PolyML always with the same error message. I cannot reproduce the problem reliably but because it has already happened, let say, six times in the past three months, I am reporting the problem here:
Unofficial version of Isabelle/HOL (unidentified repository version) poly: gc_mark_phase.cpp:432: virtual void MTGCProcessMarkPointers::ScanAddressesInObject(PolyObject*, POLYUNSIGNED): Assertion `baseAddr > (PolyWord*)obj && baseAddr < ((PolyWord*)obj)+length' failed.
This refers to any changeset in the past three months.
Best, Ondrej _______________________________________________ isabelle-dev mailing list isabelle-dev at in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
isabelle-dev mailing list isabelle-dev at in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
InternalError exceptions are assertions within the compiler. I would expect them to be deterministic unlike assertions in the GC which depend a lot on timing of threads. It should be possible to get to the bottom of this if I'm able to get the ML code that is causing the problem. I appreciate this may be easier said than done.
Just to check: is this with the release, with the current fixes branch or with SVN trunk? I seem to remember fixing something a bit like this.
David
On 27/02/2014 03:44, Michael Norrish wrote:
I seem to be able to pretty reliably produce the following:
Exception- InternalError: indirect - invalid constant address raised while compiling
Exception- InternalError: indirect - invalid constant address raised while compiling
Unfortunately, it takes hours to get there...
Switching to --gcthreads=1 may have fixed another error we were having, relating to unwarranted pointer-equality tests.
Michael
On Mon, 3 Mar 2014, David Matthews wrote:
InternalError exceptions are assertions within the compiler. I would expect them to be deterministic unlike assertions in the GC which depend a lot on timing of threads. It should be possible to get to the bottom of this if I'm able to get the ML code that is causing the problem.
Over the years I have seen Poly/ML compiler crashes occasionally, but rather rarely. Usually I managed to point David to some spots in his ML sources, by putting the PolyML.exception_trace combinator just in the right place of the system.
Since Isabelle/ML invokes PolyML.compiler on its own, this often works relatively easily, but sometimes I went through the actual Poly/ML sources and made educated guesses where to make a trace.
Maybe the following may serve as an example how to invoke and manage the PolyML compiler under program control:
(1) short version (Isabelle/Pure bootstrap): http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-2/src/Pure/ML-Sys...
(2) long version (full Isabelle/ML managed compilation with IDE markup) http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-2/src/Pure/ML/ml_...
In both cases, the critical bit is the two-stage invocation of PolyML.compiler: first the static then the dynamic phase.
Makarius
On Mon, 3 Mar 2014, Makarius wrote:
(1) short version (Isabelle/Pure bootstrap): http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-2/src/Pure/ML-Sys...
(2) long version (full Isabelle/ML managed compilation with IDE markup) http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-2/src/Pure/ML/ml_...
In both cases, the critical bit is the two-stage invocation of PolyML.compiler: first the static then the dynamic phase.
That was 1 second too quick: PolyML.Compiler.CPCompilerResultFun is where the two phases can be intercepted.
David can explain better what is what in PolyML.Compiler, if this is required here.
Makarius
-
David.Matthews＠prolingua.co.uk -
makarius＠sketis.net -
michael.norrish＠nicta.com.au