If these crashes are happening at the end of the build process I would
suspect that it is something to do with either the data sharing or
writing out the heap image. Writing the heap image does not involve any
concurrency but the data sharing does, so I would suspect the latter.
That has changed recently in 5.7.1 but so too has saving the heap. The
fact that it only occurs on specific hardware points to some error in
the memory model i.e. that the code is assuming something about the
consistency of memory that is not in fact true. It's impossible to be
sure about any of this without running tests on the hardware itself. At
least the problem seems to have gone away with the latest version of
Poly/ML.
David
On 08/11/2017 08:21, Manuel Eberl wrote:
I was not able to find out what exactly crashes and why, but while
trying to do that, I found out that the problem is actually not present
in the development version of Isabelle anymore.
After a lengthy bisection, I found that the first revision where no
crashes occur is this one:
changeset: 66920:aefaaef29c58
user: wenzelm
date: Thu Oct 26 13:44:41 2017 +0200
summary: use Poly/ML 5.7.1 test version as default;
So apparently, something changed in Poly/ML 5.7.1 that made the crashes
go away. Older versions of Isabelle, i.e. Isabelle2016-1, Isabelle2017,
and isabelle-dev up to 66919:1f93e376aeb6 /do/ exhibit the crash. It
thus seems likely that whatever caused it was apparently present in
multiple older Poly/ML versions.
Note that the crash appears to be highly sensitive to the environment:
Having two builds run in parallel with different Isabelle versions seems
to make it considerably less frequent; however, only in Poly/ML 5.7.1
does it appear to not happen at all no matter how I run it.
Does Poly/ML 5.7.1 contain any changes that could plausibly cause this
bad behaviour to go away?
Manuel
On 2017-11-07 09:51, Manuel Eberl wrote:
It seems like this thread is not dead yet.
I had my CPU replaced by a new version that supposedly does not have the
SMD problem on Linux. The problem with Isabelle did not go away.
I still get reproducible crashes of "isabelle build -c Pure", but only
with SMT switched on. However, it is worth noting that the crashes
always seem to happen at the end of the build process. (A successful
build takes about 9 seconds of elapsed and CPU time on my machine and
unsuccessful ones always crash at at least that time) However, it is
worth noting that some of the failed builds look like this:
0:00:30 elapsed time, 0:00:08 cpu time, factor 0.29
Also, the last line that is printed is always
### theory "ML_Bootstrap"
so perhaps that also points to some specific problem. However, I don't
think it's anything specific to Pure, since the crash is also
reproducible with other sessions if I remember correctly (I just use
Pure because it can be built quickly).
To summarise:
- crash happens randomly in about 6% of builds of the "Pure" session
- crash seems specific to my Ryzen or at least my system
- disabling SMT makes problem go away
- crash reproducible on my Arch installation and a fresh install of
Arch, but not on Ubuntu
- RAM passes memtest without errors
- I did not experience instability with any other software
- My conjecture would be that it is somehow related to PolyML and
multithreading
I attached both the console output and the build log.
Manuel
On 04/09/17 15:12, Manuel Eberl wrote:
Alas, it would appear I have spoken too soon!
I experienced a strange build failure with RC1 yesterday and, fearing
the worst, did my experiment from a few weeks ago again, with the
following result:
– building "Pure" fails in around 6 % of the cases
– this does not change even after a cold reboot
– switching SMT off seems to make the problem go away entirely
– switching SMT on makes it reappear
Sounds very much like this might well be the Ryzen bug. AMD has started
replacing affected CPUs, so I shall enquire about that and see what happens.
Cheers,
Manuel
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
