Re: [polyml] [isabelle-dev] PolyML crashes

2014-03-03 Thread David Matthews
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

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


Re: [polyml] [isabelle-dev] PolyML crashes

2014-03-03 Thread Makarius

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-Systems/compiler_polyml.ML#l40

  (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_compiler_polyml.ML#l184

In both cases, the critical bit is the two-stage invocation of 
PolyML.compiler: first the static then the dynamic phase.



Makarius

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


Re: [polyml] [isabelle-dev] PolyML crashes

2014-03-03 Thread 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-Systems/compiler_polyml.ML#l40

  (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_compiler_polyml.ML#l184

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
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml


Re: [polyml] [isabelle-dev] PolyML crashes

2014-02-26 Thread Michael Norrish
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-...@in.tum.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
 ___
 isabelle-dev mailing list
 isabelle-...@in.tum.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




signature.asc
Description: OpenPGP digital signature
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml