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

[Makarius]

On 18/06/18 21:30, Lars Hupel wrote:
> 
> 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.
> 
> 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.

Isabelle2017 still uses Poly/ML 5.6, but for the coming release we are
on 5.7.1, which is quite different in many respects.


> - 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 ()

David Matthews is the only one who can address this.

Maybe the problem is even related to the non-termination we've seen
recently on HOL-Proofs.


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

Of course, I have also use for such a machine for testing Isabelle + AFP
as usual.


	Makarius