Poly/ML April 2019

polyml@lists.polyml.org

4 participants
4 discussions

Bug report
by David.Matthews＠prolingua.co.uk 08 Apr '19

08 Apr '19

On 30/03/2019 01:07, Eliot Moss wrote: > > The failure I get with -j4 is a SIGSEGV and ti comes pretty early. > I wonder if it has something to do with page mapping or GC?? It > only happens when multiple polyml instances are requested at the > same time, I believe.? Michael Norrish suspects fork/exec, but > I suspect page mapping -- but I don't know enough about how the > system is constructed ... The problem with Cygwin is that it adds an extra layer between the application and the operating system that makes it very difficult to be sure what exactly is happening. It's not at all clear what Windows calls are being made as a result of calling a "Unix" library function. Some calls, and mmap is among them, have fairly clear Windows equivalents. It's unlikely to be a problem there. fork is notorious because there is no direct equivalent in Windows. The nearest is CreateProcess which combines both fork and exec. Poly/ML uses CreateProcess in native Windows but Unix.execute is implemented using fork and exec. It seems odd that there is a problem with multiple Poly/ML processes since I would expect them to be independent. Are the processes created in a poly executable or is there a top level Makefile? Have you tried building with --disable-shared ? Shared libraries complicate fork in Cygwin so it may be worth trying building with a static library. Regards, David

3 3

fork/exec code in 5.8
by Michael.Norrish＠data61.csiro.au 07 Apr '19

07 Apr '19

HOL4's Holmake tool uses a fork/exec idiom to run scripts in parallel (and to monitor their output file descriptors). Under 5.8 this code is causing signal 11 failures (segmentation faults), as reported by a few users, and apparent also on runs on Travis such as https://travis-ci.org/HOL-Theorem-Prover/HOL/jobs/515996149 (It is apparent from the related Travis pages that the same sources are running to completion perfectly with 5.7.1.) The code for doing the fork/exec stuff is visible at https://github.com/HOL-Theorem-Prover/HOL/blob/8990db3c7743feb190d98f4bce66… This code also works under mlton (although eventually does cause "out of filedescriptor" syscall failures because mlton won't garbage collect my fds after they stop getting used), so I do feel as if the code should work.? The failures all happen when Holmake is first run in this mode. When forced to run single-threaded with its -j1 option, which makes it use OS.Process.system underneath, Holmake can work. Michael

2 2

Issues with 5.8 on ARM and s390x
by loganjerry＠gmail.com 05 Apr '19

05 Apr '19

This weekend, I attempted to build polyml 5.8 for Fedora (Rawhide for now, hopefully Fedora 30 later). I encountered issues with the 32-bit ARM build and the s390x build. On s390x, immediately after the C++ code is compiled, polyimport is executed for the first time: ./polyimport polytemp.txt -I . < ./exportPoly.sml /bin/sh: line 1: 33283 Segmentation fault (core dumped) ./polyimport polytemp.txt -I . < ./exportPoly.sml GDB says: (gdb) bt #0 0x000003fffde56ce6 in PolyObject::Get (this=0x8017c8fcff030000, i=0) at globals.h:311 #1 0x000003fffdebbfce in IntTaskData::SwitchToPoly (this=0x10336d0) at interpret.cpp:761 #2 0x000003fffdec2830 in IntTaskData::EnterPolyCode (this=0x10336d0) at interpret.cpp:2261 #3 0x000003fffde92eea in NewThreadFunction (parameter=0x10336d0) at processes.cpp:1307 #4 0x000003fffdb89da6 in start_thread () from /usr/lib64/libpthread.so.0 #5 0x000003fffdd01b06 in thread_start () from /usr/lib64/libc.so.6 Notice the "this" parameter in frame 0. That is an invalid address ... unless one reverses the bytes to get 0x000003fffcc81780, which is a valid address. The code that produces the argument to indirect_0 has apparently done so in little endian byte order. If you can tell me where to look, I can help debug this further. The presence or absence of --enable-compact32bit makes no difference; the segfault happens either way. On 32-bit ARM, the build succeeds, but one test fails: Tests/Succeed/Test174.ML. The first two failures are on lines 34 and 35: check(Real32.fromLarge IEEEReal.TO_ZERO pm < p32); check(Real32.fromLarge IEEEReal.TO_ZERO mp > m32); Entering those values by hand at the polyml command prompt I get: > Real32.fromLarge IEEEReal.TO_ZERO pm; val it = 3.141592741: Real32.real > p32; val it = 3.141592741: ?.Math.real > Real32.fromLarge IEEEReal.TO_ZERO mp; val it = ~3.141592741: Real32.real Then the tests at lines 40 and 42 fail: check(Real32.fromLarge IEEEReal.TO_POSINF pp > p32); check(Real32.fromLarge IEEEReal.TO_POSINF mp > m32); > Real32.fromLarge IEEEReal.TO_POSINF pp; val it = 3.141592741: Real32.real > Real32.fromLarge IEEEReal.TO_POSINF mp; val it = ~3.141592741: Real32.real Likewise, the tests at lines 48 and 50 fail: check(Real32.fromLarge IEEEReal.TO_NEGINF pm < p32); check(Real32.fromLarge IEEEReal.TO_NEGINF mm < m32); > Real32.fromLarge IEEEReal.TO_NEGINF pm; val it = 3.141592741: Real32.real > Real32.fromLarge IEEEReal.TO_NEGINF mm; val it = ~3.141592741: Real32.real The output of configure on ARM seems okay, although I will note an entirely different problem: configure:17740: checking whether as supports .note.GNU-stack configure:17753: armv7hl-redhat-linux-gnueabi-gcc -c -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -fexceptions -fstack-protector-strong -grecord-gcc-switches -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1 -march=armv7-a -mfpu=vfpv3-d16 -mtune=generic-armv7-a -mabi=aapcs-linux -mfloat-abi=hard -fno-strict-aliasing -D_GNU_SOURCE conftest.c >&5 {standard input}: Assembler messages: {standard input}:552: Error: junk at end of line, first unrecognized character is `,' configure:17753: $? = 1 configure: failed program was: | /* confdefs.h */ [ skip lots of #defines that don't matter] | /* end confdefs.h. */ | __asm__(".section .note.GNU-stack,\"\", at progbits"); | int | main () | { | | ; | return 0; | } Taking a clue from the output of gcc -S conftest.c -fverbose-asm after removing the __asm__ line above, I changed @progbits to %progbits, and then the test worked. Advice on how to proceed w.r.t the floating point issues with the ARM build is much appreciated. Regards, -- Jerry James http://www.jamezone.org/

4 10

Problem with compact32bit
by rda＠lemma-one.com 04 Apr '19

04 Apr '19

I was doing some performance comparisons and found what looks like a bug in Poly/ML when compiled with ?enable-compact32bit. The problem is that ML code that runs to completion when compiled to use native 64 bit addresses, raises Overflow when compiled to 32 bit addressing. The code is a lengthy proof search that explores in excess of 4,000,000,000 blind alleys. It takes about 10 to 20 minutes to find the proof when using 64 bit addressing and it takes 2 or 3 minutes before it raises Overflow when using 32 bit addressing. I don?t really know where to start with narrowing the problem down. I?ve attached a tarball containing cutdown source that demonstrates the problem, but the mailing list software will likely strip it off, hence CC to David. Regards, Rob.

2 6

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

Poly/ML April 2019