Excellent! Thanks for tracking this down, that was way more involved than I had anticipated. I'll do some more explicit testing of the AFP over the weekend to confirm.
Cheers, Gerwin On 08/12/2012, at 9:50 AM, Makarius <[email protected]> wrote: > On Thu, 6 Dec 2012, Tobias Nipkow wrote: > >> Am 06/12/2012 12:57, schrieb Makarius: >>> This does not say anything yet. We need to collect further details and >>> hypotheses and test them. I will also try again to reproduce it myself. >> >> One point may (or may not) have got lost. The problem seems to be independent >> from the AFP. Remember that I had the situation where even HOLCF hung. It >> turned >> out that trying to load any theory based on HOL hung. I eventually forced >> HOL to >> be recompiled and then things were more normal again. Yes, it sounds strange. > > The situation should be under control again. > > I've introduced this problem myself in a recent cleanup of the future task > scheduler, probably around 262c36fd5f26 from 18-Oct-2012. Since we are > lagging behind with the testing infrastructure itself, we often get delays in > exposing issues of the systems being tested. > > > So this is the explanation for the empirical observations on this thread: > > * AFP uses document_variants=document:outline=/proof,/ML which means > 1 > document preparation jobs in the end; thus it had the future task > scheduler and potentially some worker threads still running when the > image was saved. > > * After reloading the image to build another session on top, the old > tasks were revived by the Poly/ML runtime system, but a fresh instance > of the scheduler + workers forked by Isabelle/ML as usual. The old > threads could still hold locks or access critical variables in a way > that interferes with the fresh crew. > > What is also funny in the persistent thread model is that the thread equality > changes but physically the threads operate on the same data space as before > the dump. This makes it hard to check explicitly against such mistakes > inside ML. > > Anyway, in such a situations of Isabelle/ML threading problems (not Poly/ML > threading problems nor Scala/JVM threading problems) setting > Multithreading.trace := 5 gives an idea what is wrong. Since it was all in my > own machine room it was easy to isolate and address -- problems by Oracle or > EPFL take much longer. > > > So here is my changeset to conclude this mail thread (hopefully): > > # HG changeset patch > # User wenzelm > # Date 1354918479 -3600 > # Node ID 702278df3b57aff4c55fec3bffb0206ace927432 > # Parent f8cd5e53653b98df3433356a94bbb3810042c626 > make double-sure that the future scheduler is properly shutdown, otherwise > its threads are made persistent and will deadlock with the fresh instance > after reloading the image (NB: Present.finish involves another Par_List.map > over document_variants and thus might fork again); > > diff -r f8cd5e53653b -r 702278df3b57 src/Pure/System/session.ML > --- a/src/Pure/System/session.ML Fri Dec 07 23:11:01 2012 +0100 > +++ b/src/Pure/System/session.ML Fri Dec 07 23:14:39 2012 +0100 > @@ -79,6 +79,7 @@ > Keyword.status (); > Outer_Syntax.check_syntax (); > Options.reset_default (); > + Future.shutdown (); > session_finished := true); > > > Makarius > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
