Poly/ML March 2019

polyml@lists.polyml.org

11 participants
11 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

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

Bug report
by moss＠cs.umass.edu 29 Mar '19

29 Mar '19

Dear developers -- PolyML had been working great for me, but I wanted to move to a more recent version of HOL4, which demands a newer version of PolyML. I run on cygwin and find two issues: 1) Out of the box, 5.7.1 and 5.8 (which, by the way is not advertised as the latest release on polyml.org) do not build. This is because statistics.cpp and statistics.h in libpolyml seem to assume that HAVE_WINDOWS_H means you are building for Windows and does not take Cygwin into account. Cygwin has gettimeofday, etc. I found that the system builds if every #ifdef HAVE_WINDOWS_H is replaced by #if defined(HAVE_WINDOWS_H) && ! defined(__CYGWIN__) It may be easier just to suppress HAVE_WINDOWS_H in the presence of __CYGWIN__, though I have not confirmed that as a proper solution. 2) The system thus built fails to run Holmake properly, crashing with signal B (11) (SEGV, I believe). It works if I run Holmake with -j1 (default is something like -j4), which means that multiple concurrent instances of poly interfere with each other in some way, near as I can tell. Regards - Eliot Moss

5 10

Building an executable that runs the read-eval-print loop
by rda＠lemma-one.com 27 Mar '19

27 Mar '19

I wanted to create an executable that runs the Poly/ML read-eval-print loop with some code of mine precompiled. What I found was that the print part of the read-eval-print loop doesn't work if I compile from source with polyc, but does work if I use PolyML.export to create a .o file and then link it with polyc. For example, if I have a file t.ML containing the following two lines: fun p s = (TextIO.output(TextIO.stdOut, s); s); val main = PolyML.rootFunction and compile it with: polyc -o t t.ML and then run: echo 'val x = p "Boo!\n"' | t the output I see is: Poly/ML 5.7 Release Boo! So it's executed my code, but it hasn't printed the usual report on the new value binding for x. So I copied what I do in ProofPower, which does something similar but doesn't have this problem. I appended the following line to t.ML: val _ = PolyML.export ("t", main); and compiled it with: poly < t.ML polyc -o t t.o Then when I run t as above, I see the output, I'd expected to get: Poly/ML 5.7 Release Boo! val x = "Boo!\n": string The work-around is easy, but it would be nice to be able to compile from source to executable directly (and to minimise the Poly/ML-specific code in my source). Regards, Rob.

2 1

Memory leak when FFI callback and ref value.
by kostirya＠gmail.com 14 Mar '19

14 Mar '19

Hello. I found memory leak when FFI callback and ref value. I checked Poly/ML 5.8 and 5.7. Simple code for reproduce the memory leak is attached. To prevent the memory leak I clean ref value (see comment in example). But It must do the garbage collector, is it? At least MLton have not this problem. Result of run of example code: Without clean ref value (The memory leak is) USER PID %CPU %MEM VSZ RSS TT STAT STARTED TIME COMMAND nick 19855 91,8 9,7 305016 289452 6 S+ 16:53 0:17,94 poly --script cb-po With clean ref value USER PID %CPU %MEM VSZ RSS TT STAT STARTED TIME COMMAND nick 19862 65,3 0,6 32632 17476 6 S+ 16:54 0:10,77 poly --script cb-poly Best, Nick.

2 1

Testing Poly/ML 5.8
by David.Matthews＠prolingua.co.uk 12 Mar '19

12 Mar '19

The current version of Poly/ML is approaching the point of creating a new release, 5.8. Makarius has run a lot of tests with Isabelle and various bugs have been fixed. This has mainly affected the 32-bit object ID version for 64-bits but some of the fixes will also have affected the native-address versions. This is a last chance to test the current git master before release. Don't forget to run "make compiler" at least twice after the initial "make" in order to build the up-to-date compiler and recompile all the code with it. This is particularly important if testing the --enable-compact32bit version. Some extra checking was added during testing and there is a strong chance of getting an assertion failure during the initial "make" or the first "make compiler" due to a bug in the pre-built compiler. If this happens just rerun the step. Once the compiler has been rebuilt it will incorporate a fix. David

6 12

ar cru call
by buday.gergely＠uni-eszterhazy.hu 12 Mar '19

12 Mar '19

> How can I make polyml to use "ar cr" instead of "ar cru"? The problem was only in the libffi directory. I edited the files with AR_FLAGS setting there, I guess the configure is the source of the others and then make in this directory worked, and then make in the main polyml directory went through. ar manual writes u Normally, ar r... inserts all files listed into the archive. If you would like to insert only those of the files you list that are newer than existing members of the same names, use this modifier. The u modifier is allowed only for the operation r (replace). In particular, the combination qu is not allowed, since checking the timestamps would lose any speed advantage from the operation q. So omitting the u has no real effect other than compile time. The learning is that in MobaXterm, probably due to Busybox using a limited version of ar, option u is not understood. Fixing libffi/configure to have option cr instead of cru for AR_FLAGS makes the compilation possible. Would it be possible to test with autoconf whether a system understands the u option of ar and use cr then? - Gergely

3 2

ar cru call
by buday.gergely＠uni-eszterhazy.hu 08 Mar '19

08 Mar '19

Hi, I try to compile polyml on MobaXterm, which is a cygwin-based distribution for Windows. Once I have a warning libtool: compile: gcc -DHAVE_CONFIG_H -I. -I. -I./include -Iinclude -I./src -O3 -fomit-frame-pointer -fstrict-aliasing -ffast-math -march=core2 -Wall -fexceptions -MT src/closures.lo -MD -MP -MF src/.deps/closures.Tpo -c src/closures.c -DDLL_EXPORT -DPIC -o src/.libs/closures.o src/closures.c: In function 'open_temp_exec_file_name': src/closures.c:273:8: warning: implicit declaration of function 'mkostemp'; did you mean 'mkstemp'? [-Wimplicit-function-declaration] fd = mkostemp (name, flags); ^~~~~~~~ mkstemp and then an error: /bin/sh ./libtool --tag=CC --mode=link gcc -O3 -fomit-frame-pointer -fstrict-aliasing -ffast-math -march=core2 -Wall -fexceptions -o libffi_convenience.la src/prep_cif.lo src/types.lo src/raw_api.lo src/java_raw_api.lo src/closures.lo src/x86/ffi.lo src/x86/win32.lo libtool: link: ar cru .libs/libffi_convenience.a src/.libs/prep_cif.o src/.libs/types.o src/.libs/raw_api.o src/.libs/java_raw_api.o src/.libs/closures.o src/x86/.libs/ffi.o src/x86/.libs/win32.o ar: unknown option -- u BusyBox v1.22.1 (2015-11-10 11:07:12 ) multi-call binary. Usage: ar [-o] [-v] [-p] [-t] [-x] ARCHIVE FILES Extract or list FILES from an ar archive -o Preserve original dates -p Extract to stdout -t List -x Extract -v Verbose ar version is 2.29.1 here. I tried this on another platform, where ar, or, better say binutils has version 2.22.52 and there is no problem. I tried to compile binutils 2.22.52 with binutils 2.29.1 but but that failed with the same error. How can I make polyml to use "ar cr" instead of "ar cru"? - Gergely

2 1

'make compiler' resulting in slow compilation
by David.Matthews＠prolingua.co.uk 06 Mar '19

06 Mar '19

Phil, Thank you for testing this and reporting the problem. It actually turned out to be a bug in the compact 32-bit version. The compilation happened to allocate an array of a particular size that was wrongly copied in the minor garbage collection resulting in a crash either in the GC itself or later on. I've pushed a fix to master and I'm copying this message to the mailing list since this represents a change that others may need to be aware of. Regards, David On 03/03/2019 00:27, Phil Clayton wrote: > David, > > I have been trying out the latest candidate for Poly/ML 5.8 (c3a630f) > with --enable-compact32bit and have not found any issues.? I was pleased > to see a space saving with saved state files, which appear to be around > 62-68% of their size compared with not using compact32bit.? I haven't > measured any other performance though. > > In one obscure respect, compact32bit fails where the full 64 bit version > does not: the exponential blow-up described in this example from a few > years ago now fails to compile code where the full 64 bit version would > take around 8 s on my machine.? Presumably some internal limit is hit > sooner with 32 bits.? I have seen two different failure messages as > shown in the following log. > > Regards, > Phil

1 0

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 March 2019