Hi,
when trying to run polyml 4.2.0 on Linux, I get a segmentation fault. I am trying to run this old version, because I want to use Isabelle (http://isabelle.in.tum.de/ seems to be down currently). On that website, a precompiled binary is available. However, it's crashing on startup with a SIGSEGV. So I downloaded the source code of polyml 4.2.0, extracted driver.420.tar.gz, ran configure and make and tried to run poly. But also in this version I get a segmentation fault.
my kernel: uname -rm 2.6.22-gentoo-r2 i686
gdb shows this backtrace:
#0 0xa7f21410 in __kernel_vsyscall () #1 0x410d4038 in mmap () from /lib/libc.so.6 #2 0x08059b34 in ReserveAddressSpace (addr=0x98000000 "", len=268435456) at mmap.c:363 #3 0x08059a41 in ReserveMLSpace (bottom=0x98000000 "", top=0xa8000000 <Address 0xa8000000 out of bounds>) at mmap.c:376 #4 0x08059b82 in ReserveMLSpaces () at mmap.c:403 #5 0x08052741 in main (argc=1, argv=0xafc18304) at mpoly.c:726
The mmap call in line 362/363 is
caddr_t pa = mmap((caddr_t)addr, len, PROT_NONE, MAP_PRIVATE | MAP_FIXED | MAP_NORESERVE | MAP_ANONYMOUS, -1, 0L);
when removing MAP_PRIVATE from the flags, it seems to work. I am not really in the code. Maybe you can tell me: will I run into trouble, when using this as a fix?
Has anybody an idea why this call to mmap results in a segmentation fault and how to fix this properly? I played a bit with the len argument. When setting it to 267500000, sometimes it's crashing and sometimes not. len=260000000 seems to be stable.
Thank you in advance Martin Walch
walch.martin@web.de wrote:
when trying to run polyml 4.2.0 on Linux, I get a segmentation fault. I am trying to run this old version, because I want to use Isabelle (http://isabelle.in.tum.de/ seems to be down currently). On that website, a precompiled binary is available. However, it's crashing on startup with a SIGSEGV. So I downloaded the source code of polyml 4.2.0, extracted driver.420.tar.gz, ran configure and make and tried to run poly. But also in this version I get a segmentation fault.
when removing MAP_PRIVATE from the flags, it seems to work. I am not really in the code. Maybe you can tell me: will I run into trouble, when using this as a fix?
Martin, Problems like these were one of the big motivating factors behind the changes that were made in Poly/ML version 5. Version 4 and earlier required the database to be mapped at a specified address otherwise it would not work. This was fine except that changes to the kernel could mean that the address range was already in use for something else, such as shared libraries.
Isabelle has worked with version 5 for some time and I would strongly advise you to use that version if you can. You may be able to get version 4.2 to work by changing the mapping address in addresses.h and running "poly -d" (the database garbage collector) to remap the database. You may find it easier to use an older kernel which may lay out memory differently. I don't know why removing MAP_PRIVATE works. You really need to include this flag otherwise changes to references will be written back to the database even if you don't commit.
Regards, David.
-
David.Matthews＠prolingua.co.uk -
walch.martin＠web.de