Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing



Here is the next one. Putting Isabelle under heavy load seems not to be
a good idea nowadays :( 

A few years ago, Isabelle used to be very stable, even on big stuff ...


Welcome to Isabelle/HOL (Isabelle2014: August 2014)
poly: gc_mark_phase.cpp:439: virtual void
MTGCProcessMarkPointers::ScanAddressesInObject(PolyObject*,
POLYUNSIGNED): Assertion `baseAddr > (PolyWord*)obj && baseAddr <
((PolyWord*)obj)+length' failed.

Malformed message:
bad chunk (unexpected EOF after 3012 of 4431 bytes)
message_output terminated
/home/lammich/opt/Isabelle2014/lib/scripts/run-polyml-5.5.2: line 84:
7861 Aborted                 (core dumped) "$POLY" -q -i $ML_OPTIONS
--eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")"
--error-exit < /dev/null

standard_error terminated
standard_output terminated
process terminated
command_input terminated
process_manager terminated
Return code: 134


--
  Peter



On Do, 2015-01-08 at 21:58 +0100, Makarius wrote:
> On Tue, 30 Dec 2014, Peter Lammich wrote:
> 
> >> OK, I recommend to apply the tiny change from
> >> http://isabelle.in.tum.de/repos/isabelle/rev/f4e9bd04e1d5 by editing
> >> Isabelle2014/src/Pure/General/table.ML accordingly, and rebooting (which
> >> will cause an automatic rebuild of logic images).
> >>
> >> If anything like that happens again, just keep me informed.
> >>
> >
> > Again, a permanent grayout, which did not recover itself.
> 
> Thanks for reporting that.  As always, it is important for me get an 
> impression about two things:
> 
>    (1) What kind of crashes can happen.
> 
>    (2) The approximate frequency they happen.
> 
> In that sense, just keep me informed if you see something like this again.
> 
> Anyone else who sees the same or similar breakdowns is welcome to say so, 
> too.
> 
> 
> > This time, syslog sais:
> >
> > Welcome to Isabelle/CAVA_Base (Isabelle2014: August 2014)
> > Isabelle protocol command failure: "Document.update"
> > exception Thread "Thread creation failed" raised (line 48 of "ML-Systems/polyml.ML")
> 
> > Isabelle protocol command failure: "Document.update"
> > Undefined document version: -60998
> > Isabelle protocol command failure: "Document.remove_versions"
> > Attempt to remove execution version -60993
> 
> Here I was first distracted by the latter part, which would have been an 
> integrity problem within the PIDE protocol state, i.e. in my own 
> department.
> 
> The relevant bit is "Thread creation failed", though, which is produced by 
> the Poly/ML runtime system, when the system function pthread_create fails 
> (according to libpolyml/processes.cpp).  The man page for that function 
> says about error situations:
> 
>         EAGAIN Insufficient resources to create another thread,  or  a  system-
>                imposed  limit  on  the  number of threads was encountered.  The
>                latter case  may  occur  in  two  ways:  the  RLIMIT_NPROC  soft
>                resource  limit  (set via setrlimit(2)), which limits the number
>                of process for a real user ID, was reached; or the kernel's sys‐
>                tem-wide   limit   on  the  number  of  threads,  /proc/sys/ker‐
>                nel/threads-max, was reached.
> 
> We can probably ignore the explicit /proc/sys/kernel/threads-max -- it is 
> a very high value on my Ubuntu system.
> 
> 
> In other words, we are back to the usual guess of insufficient resources 
> -- unless your application was unexpectedly tiny.
> 
> It should be explicitly noted that stack space was already sucessfully 
> allocated -- there is a different exception for that: "Unable to allocate 
> thread stack".
> 
> 
> Maybe we are slowly moving out of the 32-bit era, but there might be a 
> completely different reason.
> 
> 
>  	Makarius






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