Chengsong Tan (Jun 28 2024 at 13:58): Chengsong Tan (Jun 28 2024 at 13:58):Hi,
I was wondering if anyone encountered similar crashes of Isabelle with the code in the title?
Is this a Java issue or an Isabelle bug? If the latter, do we know any quick fixes?
Some error log text:
#
# A fatal error has been detected by the Java Runtime Environment:
#
# EXCEPTION_ACCESS_VIOLATION (0xc0000005) at pc=0x00007ffbc5571d2f, pid=26860, tid=22256
#
# JRE version: OpenJDK Runtime Environment Zulu17.42+19-CA (17.0.7+7) (build 17.0.7+7-LTS)
# Java VM: OpenJDK 64-Bit Server VM Zulu17.42+19-CA (17.0.7+7-LTS, mixed mode, sharing, tiered, compressed oops, compressed class ptrs, g1 gc, windows-amd64)
# Problematic frame:
# V [jvm.dll+0x2b1d2f]
#
# No core dump will be written. Minidumps are not enabled by default on client versions of Windows
#
# If you would like to submit a bug report, please visit:
# http://www.azul.com/support/
#
--------------- S U M M A R Y ------------
Command Line: -Disabelle.root=C:\Users\Richc\Desktop\Isabelle2023 -Dcygwin.root=C:\Users\Richc\Desktop\Isabelle2023\contrib\cygwin -Dfile.encoding=UTF-8 -Disabelle.threads=0 -Duser.language=en -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle2023 -Xms512m -Xmx4g -Xss16m -Disabelle.jedit_server=Isabelle2023 isabelle.jedit.JEdit_Main
Host: Intel(R) Core(TM) i9-14900HX, 32 cores, 63G, Windows 11 , 64 bit Build 22621 (10.0.22621.3672)
Time: Wed Jun 26 13:11:09 2024 GMT dows 11 , 64 bit Build 22621 (10.0.22621.3672) elapsed time: 43.002788 seconds (0d 0h 0m 43s)
--------------- T H R E A D ---------------
Current thread (0x00000202e7b5be70): JavaThread "C2 CompilerThread0" daemon [_thread_in_native, id=22256, stack(0x000000088d000000,0x000000088d100000)]
Current CompileTask:
C2: 43002 15154 4 org.gjt.sp.jedit.textarea.Gutter::paintLine (770 bytes)
Stack: [0x000000088d000000,0x000000088d100000], sp=0x000000088d0fa970, free space=1002k
Native frames: (J=compiled Java code, j=interpreted, Vv=VM code, C=native code)
V [jvm.dll+0x2b1d2f]
V [jvm.dll+0x585257]
V [jvm.dll+0x2222e2]
V [jvm.dll+0x21b519]
V [jvm.dll+0x218e3b]
V [jvm.dll+0x1a513d]
V [jvm.dll+0x22892a]
V [jvm.dll+0x226a85]
V [jvm.dll+0x7f01dc]
V [jvm.dll+0x7ea73a]
V [jvm.dll+0x67b5c5]
C [ucrtbase.dll+0x29333]
C [KERNEL32.DLL+0x1257d]
C [ntdll.dll+0x5af28]
siginfo: EXCEPTION_ACCESS_VIOLATION (0xc0000005), data execution prevention violation at address 0x00007ffb45571d2f
Crash logs is attached:
hs_err_pid20992.log
hs_err_pid26860.log
Best wishes,
Chengsong
Mathias Fleury (Jun 29 2024 at 07:33):Most likely java issue
Mathias Fleury (Jun 29 2024 at 07:34):Or hardware problem
Mathias Fleury (Jun 29 2024 at 07:37):Before you laugh: I had a bug leading to crashes only in Isabelle after some time (only during isabelle build)... after discovering that it could easily reproduce it with mprime/Prime95 showing that the issue was memory. I finally pinpoint it to the EMP profile for RAM.
Chengsong Tan (Jun 29 2024 at 21:47):Mathias Fleury said:
Before you laugh: I had a bug leading to crashes only in Isabelle after some time (only during isabelle build)... after discovering that it could easily reproduce it with mprime/Prime95 showing that the issue was memory. I finally pinpoint it to the EMP profile for RAM.
What is "EMP profile for RAM"? This does sound quite similar to my crashes (happens when running intensive proof searching), can you elaborate a bit more on how you debugged this (using a power virus if my google search gives me the right idea)?
Mathias Fleury (Jul 01 2024 at 12:28):sorry it is called XMP (not EMP) for intel and DOCP for AMD. It is a setting you activate in the bios
Mathias Fleury (Jul 01 2024 at 12:29):When running mprime, I would get within 1min either a crash (rarely) or errors
Mathias Fleury (Jul 01 2024 at 12:30):those errors were memory related
Mathias Fleury (Jul 01 2024 at 12:30):Then I restarted the computer and changed the XMP timing in the bios (the default was too aggressuve)
Chengsong Tan (Jul 02 2024 at 17:49):Mathias Fleury said:
Then I restarted the computer and changed the XMP timing in the bios (the default was too aggressuve)
I will try this to see if it fix my crashes. Thanks a lot!
Manuel Eberl (Sep 15 2024 at 10:35):I also once had a student whose Isabelle crashed on Windows under heavy load, reproducibly. The issue in that case was CPU overclocking. Finally though, none of the usual benchmarking tools like primes95 triggered it; just Isabelle.
Chengsong Tan (Sep 16 2024 at 15:02):Manuel Eberl said:
I also once had a student whose Isabelle crashed on Windows under heavy load, reproducibly. The issue in that case was CPU overclocking. Finally though, none of the usual benchmarking tools like primes95 triggered it; just Isabelle.
Interestingly the recent gen13/14 intel cpu issues are also exposed by Isabelle: my laptop (using 14900hx) was fine at first running other applications, but every once in a while s/h calls would crash the system and cause a BSOD.
Manuel Eberl (Sep 16 2024 at 16:21):Perhaps we ought to be marketing Isabelle as a benchmarking tool to hardware enthusiasts.
Last updated: Dec 21 2024 at 12:33 UTC