[isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

[Lars Hupel]

Dear list,

the good news is that we have just received new hardware (Dual Epyc 
7601).

The bad news is that a current development snapshot 
(Isabelle/410818a69ee3) exhibits a problem on this hardware. In 
particular, the session HOL-Corec_Examples doesn't appear to terminate.

$ cat .isabelle/etc/settings
init_components "$USER_HOME/.isabelle/contrib" 
"$ISABELLE_HOME/Admin/components/main"

ML_OPTIONS="-H 4000 --maxheap 8G"
ML_PLATFORM="$ISABELLE_PLATFORM64"

ML_HOME="$POLYML_HOME/$ML_PLATFORM"

ISABELLE_GHC=ghc
ISABELLE_POLYML="$ML_HOME/poly"
ISABELLE_SCALA="$SCALA_HOME/bin"
ISABELLE_OCAMLC=ocamlc
ISABELLE_OCAML=ocaml
ISABELLE_MLTON=mlton
ISABELLE_SWIPL=swipl
ISABELLE_SMLNJ=sml

The precise invocation is:

$ ./isabelle/bin/isabelle build -cbv -a -o threads=2 -j 16

Isabelle2017 "build -bva" works fine. This qualifies the problem as a 
regression, I suppose.

I've done some preliminary tracing; here are my findings:

- The "poly" process gets stuck at 100% CPU load and keeps calling 
"mmap"
- When trying to build the nonterminating session without "-b", it 
terminates
- GDB tells me the following stack trace when "mmap" is called (which 
corroborates that it happens during heap dumping):

#0  0x00007f8dab80ba13 in __GI___mmap64 (addr=0x0, len=32768, prot=7, 
flags=34, fd=-1, offset=0) at ../sysdeps/unix/sysv/linux/mmap64.c:52
#1  0x0000000000879d56 in OSMem::Allocate(unsigned long&, unsigned int) 
()
#2  0x0000000000871c6e in MemMgr::NewExportSpace(unsigned long, bool, 
bool, bool) ()
#3  0x000000000085f020 in CopyScan::ScanAddressAt(PolyWord*) ()
#4  0x000000000088c2b6 in 
ScanAddress::ScanAddressesInObject(PolyObject*, unsigned long) ()
...
#24 0x000000000088c335 in 
ScanAddress::ScanAddressesInObject(PolyObject*, unsigned long) ()
#25 0x000000000088c8c1 in ScanAddress::ScanAddressesInRegion(PolyWord*, 
PolyWord*) ()
#26 0x00000000008890a1 in SaveRequest::Perform() ()
#27 0x0000000000882717 in Processes::BeginRootThread(PolyObject*) ()
#28 0x0000000000874a9c in polymain ()
#29 0x00007f8dab711b97 in __libc_start_main (main=0x405720 <main>, 
argc=16, argv=0x7fffe693d4d8, init=<optimized out>, fini=<optimized 
out>, rtld_fini=<optimized out>, stack_end=0x7fffe693d4c8) at 
../csu/libc-start.c:310
#30 0x0000000000405e01 in _start ()

I'm open to any suggestions for how to diagnose this. Happy to give out 
SSH access to the machine.

Cheers
Lars