Re: [isabelle-dev] [158c513a39f5] JVM crash
> You could try with a fresh build of Poly/ML: Okay, I rebuilt Poly/ML (not libsha1 and libgmp though; apparently your build script does not build those). The crashes still occured though. I think I did everything correctly, because when I delete the files that the compilation created, isabelle build fails immediately with some ML-related error message, so it must have been using them. > It should be sufficient to remove the is_pure() here: That does indeed seem to make the problem go away completely. At least I got about 50 consecutive builds without any crashes now. Manuel On 2017-11-08 15:35, Makarius wrote: > On 08/11/17 09:21, Manuel Eberl wrote: >> 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; >> Does Poly/ML 5.7.1 contain any changes that could plausibly cause this >> bad behaviour to go away? > One side-condition that has also changed is the build platform: for the > various Poly/ML 5.6 Isabelle components it was still Ubuntu 10.04 LTS, > for current Poly/ML 5.7.1 test versions it is Ubuntu 12.04 LTS. > > Sometimes there are problems in the C/C++ compiler that disappear over > time. You could try with a fresh build of Poly/ML: the README in the > component contains brief instructions how to operate on the included src > directory. > > > Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
On 08/11/17 15:45, Manuel Eberl wrote: > Is there an easy way to disable that for testing purposes? Some line I > have to remove from a .scala file or something? It should be sufficient to remove the is_pure() here: http://isabelle.in.tum.de/repos/isabelle/annotate/3ff88fece1f6/src/Pure/Tools/build.scala#l522 Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
Is there an easy way to disable that for testing purposes? Some line I have to remove from a .scala file or something? Manuel On 2017-11-08 15:44, Makarius wrote: > On 08/11/17 15:39, Manuel Eberl wrote: >>> 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. >> Does writing out of the heap happen also when I just do "isabelle build >> Pure" as opposed to "isabelle build -b Pure"? Because the "-b" has no >> influence on whether it crashes or not. > Yes, Pure always produces a heap, independently of the -b option. > > > Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
On 08/11/17 15:39, Manuel Eberl wrote: >> 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. > > Does writing out of the heap happen also when I just do "isabelle build > Pure" as opposed to "isabelle build -b Pure"? Because the "-b" has no > influence on whether it crashes or not. Yes, Pure always produces a heap, independently of the -b option. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
> 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. Does writing out of the heap happen also when I just do "isabelle build Pure" as opposed to "isabelle build -b Pure"? Because the "-b" has no influence on whether it crashes or not. > It's impossible to be sure about any of this without running tests on > the hardware itself. I would gladly run any tests that you propose on my hardware. I could even give you SSH access to a live-CD-like system. Manuel ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
On 08/11/17 09:21, Manuel Eberl wrote: > > 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; > Does Poly/ML 5.7.1 contain any changes that could plausibly cause this > bad behaviour to go away? One side-condition that has also changed is the build platform: for the various Poly/ML 5.6 Isabelle components it was still Ubuntu 10.04 LTS, for current Poly/ML 5.7.1 test versions it is Ubuntu 12.04 LTS. Sometimes there are problems in the C/C++ compiler that disappear over time. You could try with a fresh build of Poly/ML: the README in the component contains brief instructions how to operate on the included src directory. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
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
Re: [isabelle-dev] [158c513a39f5] JVM crash
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
Re: [isabelle-dev] [158c513a39f5] JVM crash
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 On 20/08/17 14:31, Manuel Eberl wrote: > Addendum: I did a system upgrade (including a major kernel upgrade) > around the same time when I first noticed the problem and I don't think > I rebooted afterwards, so one very plausible explanation is that Linux > introduced some workarounds/bug fixes in the kernel within the last few > weeks that solved whatever issue I was having, and, of course, it took a > reboot for it to kick in. > > On 20/08/17 14:14, Manuel Eberl wrote: >> Okay I have no idea what is going on anymore. >> >> I know have the following new data points: >> – 2500 iterations on my Intel Core i7 laptop. No failures. >> >> So it must be the Ryzen issue after all, I thought. I recalled that some >> people said the problem was less pronounced with SMT disabled, so I >> disabled it. >> – 100 iterations on Ryzen 1800X after a reboot with SMT disabled. No >> failures. >> – 100 iterations on Ryzen 1800X after another reboot with SMT enabled >> again. No failures. >> >> So it seems the problem went away as mysteriously as it appeared and it >> probably has something to do with the hardware or software constellation >> on my computer. Or perhaps I should check my flat for radiation sources. >> >> Cheers, >> >> Manuel >> >> >> On 20/08/17 11:24, Lars Hupel wrote: Lars, maybe you can run the same test on your machine and see what happens there. >>> >>> I did, and nothing happened for about 100 iterations. I have a Core >>> i7-2600. OS is otherwise identical to Manuel (Arch Linux). >>> As for Scala, could a problem in the Scala compiler really lead to the JVM segfaulting? I would have thought if the JVM segfaults, that's a bug in the JVM. (unless it's a hardware-related issue, of course) >>> >>> I've seen it happening, but it is very rare. Still, the coincidence of >>> crashes during compilation could be explained by random chance (even if >>> very unlikely). A quick look over Scala's issue tracker reveals no >>> documented JVM segfaults after 2011. >>> >>> Cheers >>> Lars >>> ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
Addendum: I did a system upgrade (including a major kernel upgrade) around the same time when I first noticed the problem and I don't think I rebooted afterwards, so one very plausible explanation is that Linux introduced some workarounds/bug fixes in the kernel within the last few weeks that solved whatever issue I was having, and, of course, it took a reboot for it to kick in. On 20/08/17 14:14, Manuel Eberl wrote: > Okay I have no idea what is going on anymore. > > I know have the following new data points: > – 2500 iterations on my Intel Core i7 laptop. No failures. > > So it must be the Ryzen issue after all, I thought. I recalled that some > people said the problem was less pronounced with SMT disabled, so I > disabled it. > – 100 iterations on Ryzen 1800X after a reboot with SMT disabled. No > failures. > – 100 iterations on Ryzen 1800X after another reboot with SMT enabled > again. No failures. > > So it seems the problem went away as mysteriously as it appeared and it > probably has something to do with the hardware or software constellation > on my computer. Or perhaps I should check my flat for radiation sources. > > Cheers, > > Manuel > > > On 20/08/17 11:24, Lars Hupel wrote: >>> Lars, maybe you can run the same test on your machine and see what >>> happens there. >> >> I did, and nothing happened for about 100 iterations. I have a Core >> i7-2600. OS is otherwise identical to Manuel (Arch Linux). >> >>> As for Scala, could a problem in the Scala compiler really lead to the >>> JVM segfaulting? I would have thought if the JVM segfaults, that's a bug >>> in the JVM. (unless it's a hardware-related issue, of course) >> >> I've seen it happening, but it is very rare. Still, the coincidence of >> crashes during compilation could be explained by random chance (even if >> very unlikely). A quick look over Scala's issue tracker reveals no >> documented JVM segfaults after 2011. >> >> Cheers >> Lars >> ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
Okay I have no idea what is going on anymore. I know have the following new data points: – 2500 iterations on my Intel Core i7 laptop. No failures. So it must be the Ryzen issue after all, I thought. I recalled that some people said the problem was less pronounced with SMT disabled, so I disabled it. – 100 iterations on Ryzen 1800X after a reboot with SMT disabled. No failures. – 100 iterations on Ryzen 1800X after another reboot with SMT enabled again. No failures. So it seems the problem went away as mysteriously as it appeared and it probably has something to do with the hardware or software constellation on my computer. Or perhaps I should check my flat for radiation sources. Cheers, Manuel On 20/08/17 11:24, Lars Hupel wrote: >> Lars, maybe you can run the same test on your machine and see what >> happens there. > > I did, and nothing happened for about 100 iterations. I have a Core > i7-2600. OS is otherwise identical to Manuel (Arch Linux). > >> As for Scala, could a problem in the Scala compiler really lead to the >> JVM segfaulting? I would have thought if the JVM segfaults, that's a bug >> in the JVM. (unless it's a hardware-related issue, of course) > > I've seen it happening, but it is very rare. Still, the coincidence of > crashes during compilation could be explained by random chance (even if > very unlikely). A quick look over Scala's issue tracker reveals no > documented JVM segfaults after 2011. > > Cheers > Lars > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
> Lars, maybe you can run the same test on your machine and see what > happens there. I did, and nothing happened for about 100 iterations. I have a Core i7-2600. OS is otherwise identical to Manuel (Arch Linux). > As for Scala, could a problem in the Scala compiler really lead to the > JVM segfaulting? I would have thought if the JVM segfaults, that's a bug > in the JVM. (unless it's a hardware-related issue, of course) I've seen it happening, but it is very rare. Still, the coincidence of crashes during compilation could be explained by random chance (even if very unlikely). A quick look over Scala's issue tracker reveals no documented JVM segfaults after 2011. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
The following seems to be the most reliable way to trigger the problem: while true isabelle build -b -c Pure end I did that and about 6% of builds with Scala 2.12.3 failed with something like the attached log. I then tried the same thing with Scala 2.12.2 (double-checked "isabelle scala -version" to be sure) and the same thing happened. I got 9 failures in 152 iterations; however, I never got a JVM segfault with either Scala version; only these "silent failures". That was on my Ryzen 1800X. I then did the exact same thing on my laptop (with Scala 2.12.3 though) and haven't gotten a single failure in over 100 iterations. So maybe this is the Ryzen bug after all? Lars, maybe you can run the same test on your machine and see what happens there. Manuel On 19/08/17 21:29, Makarius wrote: > On 19/08/17 21:27, Makarius wrote: >> I propose to try the previous Scala release locally, e.g. as follows in >> $ISABELLE_HOME_USER/etc/settings: >> >> init_component "$HOME/.isabelle/contrib/scala-2.12.2" > > Do not forget "isabelle jedit -b -f" after flipping Scala versions (that > is not required for changes of the Java version). > > > Makarius > Cleaning Pure ... Building Pure ... Pure FAILED (see also /home/manuel/.isabelle/heaps/polyml-5.6_x86-linux/log/Pure) val warning_message: string -> unit val writeln_message: string -> unit end structure Debugger: DEBUGGER val it = (): unit signature NAMED_THEOREMS = sig val add: string -> attribute val add_thm: string -> thm -> Context.generic -> Context.generic val check: Proof.context -> string * Position.T -> string val clear: string -> Context.generic -> Context.generic val declare: binding -> string -> local_theory -> string * local_theory val del: string -> attribute val del_thm: string -> thm -> Context.generic -> Context.generic val get: Proof.context -> string -> thm list val member: Proof.context -> string -> thm -> bool end structure Named_Theorems: NAMED_THEOREMS val it = (): unit signature JEDIT = sig val check_action: string * Position.T -> string end structure JEdit: JEDIT val it = (): unit Loading theory "Pure" ### theory "Pure" ### 0.436s elapsed time, 0.436s cpu time, 0.016s GC time Loading theory "ML_Bootstrap" structure Output_Primitives: OUTPUT_PRIMITIVES structure Thread_Data: THREAD_DATA val ML_system_pp = fn: (int -> 'a -> 'b -> PolyML.pretty) -> unit val it = (): unit val it = (): unit structure PolyML: sig structure IntInf: sig val gcd: int * int -> int val lcm: int * int -> int end end val it = (): unit val it = (): unit ### theory "ML_Bootstrap" ### 0.006s elapsed time, 0.006s cpu time, 0.000s GC time Unfinished session(s): Pure 0:00:32 elapsed time, 0:00:10 cpu time, factor 0.31 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
On 19/08/17 21:27, Makarius wrote: > I propose to try the previous Scala release locally, e.g. as follows in > $ISABELLE_HOME_USER/etc/settings: > > init_component "$HOME/.isabelle/contrib/scala-2.12.2" Do not forget "isabelle jedit -b -f" after flipping Scala versions (that is not required for changes of the Java version). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
On 19/08/17 21:14, Manuel Eberl wrote: > > As for Scala, could a problem in the Scala compiler really lead to the > JVM segfaulting? I would have thought if the JVM segfaults, that's a bug > in the JVM. (unless it's a hardware-related issue, of course) > > So, all in all, my money would be on the JVM. The JVM is indeed the weakest link in the chain, but I've seen situations in the past where the Scala compiler has triggered a JVM problem by producing certain byte code: the problem disappeared again after another update of Scala. I propose to try the previous Scala release locally, e.g. as follows in $ISABELLE_HOME_USER/etc/settings: init_component "$HOME/.isabelle/contrib/scala-2.12.2" If that crashes again, we can be quite sure that it is jdk-8u144. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
The Ryzen thing was also on my mind, but I have not experienced any of those instability issues. From what I read, they are extremely rare under normal use and the error occured a few seconds after initiating isabelle build. Besides, I know that Lars does not have a Ryzen CPU, and it would be a very strange coincidence that he ran into a different issue that also leads to a JVM crash. As for Scala, could a problem in the Scala compiler really lead to the JVM segfaulting? I would have thought if the JVM segfaults, that's a bug in the JVM. (unless it's a hardware-related issue, of course) So, all in all, my money would be on the JVM. Manuel On 19/08/17 21:04, Makarius wrote: > On 19/08/17 20:31, Manuel Eberl wrote: >>> If you still have that, can you send it to me? >> >> Sure. >> >>> Since the JVM crash happened during scalac compilation, I recommend to >>> enforce a fresh build, e.g. like this: > > The log says "java_command: isabelle.Isabelle_Tool build -b > HOL-Analysis" so this was really the "isabelle build", after scalac > compilation was finished. > > Reading the tea leaves further, I see the following potential reasons of > the crash: > > * jdk-8u144 (see Isabelle/98afae4308f5) > > * scala-2.12.3 (see Isabelle/96ad7d5ff613) > > * hardware: AMD Ryzen 7 1800X Eight-Core Processor > > I've seen occasional press articles discussing problems of AMD Ryzen, > e.g. > https://www.phoronix.com/scan.php?page=news_item=Ryzen-Compiler-Issues > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
On 19/08/17 17:19, Lars Hupel wrote: >> on 158c513a39f5, I just had a JVM crash during "isabelle build" when it >> was building Isabelle/Scala. (Log attached). > > I had a similar problem today. Unfortunately I didn't save the logfile. Can you say anything about the system? Hardware, OS etc. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
On 19/08/17 20:31, Manuel Eberl wrote: >> If you still have that, can you send it to me? > > Sure. > >> Since the JVM crash happened during scalac compilation, I recommend to >> enforce a fresh build, e.g. like this: The log says "java_command: isabelle.Isabelle_Tool build -b HOL-Analysis" so this was really the "isabelle build", after scalac compilation was finished. Reading the tea leaves further, I see the following potential reasons of the crash: * jdk-8u144 (see Isabelle/98afae4308f5) * scala-2.12.3 (see Isabelle/96ad7d5ff613) * hardware: AMD Ryzen 7 1800X Eight-Core Processor I've seen occasional press articles discussing problems of AMD Ryzen, e.g. https://www.phoronix.com/scan.php?page=news_item=Ryzen-Compiler-Issues Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
> If you still have that, can you send it to me?
Sure.
> Since the JVM crash happened during scalac compilation, I recommend to
> enforce a fresh build, e.g. like this:
That seems to have worked. The only output I got was this:
### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...
Manuel
#
# A fatal error has been detected by the Java Runtime Environment:
#
# SIGSEGV (0xb) at pc=0x7f25a57c5b6c, pid=13339, tid=0x7f256066c700
#
# JRE version: Java(TM) SE Runtime Environment (8.0_144-b01) (build 1.8.0_144-b01)
# Java VM: Java HotSpot(TM) 64-Bit Server VM (25.144-b01 mixed mode linux-amd64 compressed oops)
# Problematic frame:
# J 2075 C2 scala.util.parsing.combinator.Parsers$Parser$$Lambda$107.apply(Ljava/lang/Object;)Ljava/lang/Object; (16 bytes) @ 0x7f25a57c5b6c [0x7f25a57c5b00+0x6c]
#
# Core dump written. Default location: /home/manuel/hg/afp-devel/core or core.13339
#
# If you would like to submit a bug report, please visit:
# http://bugreport.java.com/bugreport/crash.jsp
#
--- T H R E A D ---
Current thread (0x7f25b5e99800): JavaThread "pool-1-thread-5" daemon [_thread_in_Java, id=13390, stack(0x7f256026c000,0x7f256066d000)]
siginfo: si_signo: 11 (SIGSEGV), si_code: 1 (SEGV_MAPERR), si_addr: 0xf21517da
Registers:
RAX=0x0007c0061210, RBX=0x7f25622e2870, RCX=0xe404fdd3, RDX=0x0007947664a0
RSP=0x7f256066a898, RBP=0xe4000482, RSI=0xf21517ca, RDI=0xf28ece10
R8 =0x0007c01b3230, R9 =0xf1dfb1a3, R10=0xf21517ca, R11=0x0007c01b3230
R12=0x, R13=0x00072027ee98, R14=0xf803c74e, R15=0x7f25b5e99800
RIP=0x7f25a57c5b6c, EFLAGS=0x00010202, CSGSFS=0x002b0033, ERR=0x0004
TRAPNO=0x000e
Top of Stack: (sp=0x7f256066a898)
0x7f256066a898: 7f25a573cae8 f2152037
0x7f256066a8a8: 7f25a573cae8 e4000482
0x7f256066a8b8: e4000482 0007f21517d3
0x7f256066a8c8: 000790a8eb00 000794766dd8
0x7f256066a8d8: 7f25a5af59b8 e4000482
0x7f256066a8e8: 7f25a573cae8 000794766e78
0x7f256066a8f8: 000794766e78 e4000482
0x7f256066a908: 7f25a57bd270 0007f2151765
0x7f256066a918: 7f25a5af5b0c 0007c01b1650
0x7f256066a928: 7f25a5b01884 e4000482
0x7f256066a938: 7f25a573cae8 e40de09c
0x7f256066a948: 7f25a573cae8 e4000482
0x7f256066a958: 7f25a57bd270 e40de09c
0x7f256066a968: 7f25a57bd270 000794765550
0x7f256066a978: 7f25a5af5b0c e40d8883
0x7f256066a988: 7f25a57bd270 e40de0a2
0x7f256066a998: 7f25a573cae8 f21519e3
0x7f256066a9a8: 7f25a573cae8 e40de0a2
0x7f256066a9b8: 7f25a57bd270 f21519e3
0x7f256066a9c8: 7f25a5af59b8 f21519e6e40db48e
0x7f256066a9d8: 0007947664a0 f2152177
0x7f256066a9e8: 7f25a5af5a58 f215199f
0x7f256066a9f8: 7f25a573cae8 000794765f60
0x7f256066aa08: 0007c00d41e0 f21519ec
0x7f256066aa18: 7f25a5af5a58 f21519a3947655f0
0x7f256066aa28: 0007947664a0 000794766fa8
0x7f256066aa38: 7f25a5af5a58 f2151e2b6066aa80
0x7f256066aa48: 000794764c40 0007947656f8
0x7f256066aa58: 7f25bc2f28b0 f21519ac
0x7f256066aa68: 7f25a573cae8 7f256066aac0
0x7f256066aa78: 7f25bbcd0e20 f21519ac
0x7f256066aa88: 7f25a5af59b8 f21519afb5e99800
Instructions: (pc=0x7f25a57c5b6c)
0x7f25a57c5b4c: 5b 30 49 b8 30 32 1b c0 07 00 00 00 4d 3b d8 75
0x7f25a57c5b5c: 30 49 8b f2 48 c1 e6 03 90 48 b8 ff ff ff ff ff
0x7f25a57c5b6c: ff ff ff e8 14 d9 d7 ff 44 8b 58 08 41 81 fb 27
0x7f25a57c5b7c: 64 03 f8 75 24 48 83 c4 20 5d 85 05 74 14 74 17
Register to memory mapping:
RAX=0x0007c0061210 is pointing into metadata
RBX={method} {0x7f25622e2870} 'apply' '(Ljava/lang/Object;)Ljava/lang/Object;' in 'scala/util/parsing/combinator/Parsers$Parser$$Lambda$107'
RCX=0xe404fdd3 is an unknown value
RDX=0x0007947664a0 is an oop
scala.util.parsing.input.CharSequenceReader
- klass: 'scala/util/parsing/input/CharSequenceReader'
RSP=0x7f256066a898 is pointing into the stack for thread: 0x7f25b5e99800
RBP=0xe4000482 is an unknown value
RSI=0xf21517ca is an unknown value
RDI=0xf28ece10 is an unknown value
R8 =0x0007c01b3230 is pointing into metadata
R9 =0xf1dfb1a3 is an unknown value
R10=0xf21517ca is an unknown value
R11=0x0007c01b3230 is pointing into metadata
R12=0x is an unknown value
R13=0x00072027ee98 is an oop
scala.util.DynamicVariable$$anon$1
- klass: 'scala/util/DynamicVariable$$anon$1'
R14=0xf803c74e is an unknown value
Re: [isabelle-dev] [158c513a39f5] JVM crash
On 19/08/17 17:16, Manuel Eberl wrote: > > on 158c513a39f5, I just had a JVM crash during "isabelle build" when it > was building Isabelle/Scala. Since the JVM crash happened during scalac compilation, I recommend to enforce a fresh build, e.g. like this: isabelle jedit -b -f > Log attached This refers to a separate log file /home/manuel/hg/afp-devel/hs_err_pid13339.log If you still have that, can you send it to me? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [158c513a39f5] JVM crash
> on 158c513a39f5, I just had a JVM crash during "isabelle build" when it > was building Isabelle/Scala. (Log attached). I had a similar problem today. Unfortunately I didn't save the logfile. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
