Poly/ML

polyml@lists.polyml.org

695 discussions

chasing an intermittent allocation failure
by cannam＠all-day-breakfast.com 02 Aug '19

02 Aug '19

I have an SML program which sometimes fails while trying to allocate an array of 3 million ints, with the message Run out of store - interrupting threads and an exception. This happens on one of the first substantial allocations in the program, near the start of its run, so there should be space available - and it only happens on occasional runs, and if it doesn't fail, then the rest of the program (which does a lot more work) runs fine. The exact size of the array being allocated doesn't seem to matter so long as it's reasonably large, but despite this and the fact that it's so early in the program, I haven't yet managed to make a simple test program with a similar allocation pattern that fails. The situation seems to be the same regardless of whether I use Poly/ML 5.7, 5.8, or current git. I compared a successful run with an unsuccessful one based on logging in the runtime. In both cases this allocation gets sent for a "quick GC", which returns failure, followed by a full GC, which runs and then either succeeds or fails to establish that there is enough memory available afterwards (via CheckForAllocation). In the "good" case, when this check comes to AllocHeapSpace, the test "if (space->allocationSpace)" never succeeds and we fall out of the first loop with currentAllocSpace == 0, defaultSpaceSize == 131072, spaceBeforeMinorGC == 120608, and our request for minWords == 3000001 is successfully fielded in the following conditional block. In the "bad" case, when this check comes to AllocHeapSpace, the "if (space->allocationSpace)" test succeeds once (available == 131070), then we fall out of the first loop with currentAllocSpace == 131072, defaultSpaceSize == 131072, spaceBeforeMinorGC == 120608, the following conditional is not entered, and we return failure from the line at the end of the function, causing the GC to return failure as well. If I comment out the check if (currentAllocSpace/* + minWords */ < spaceBeforeMinorGC) then it apparently always succeeds, but I can see that this is no solution because no GC is happening at all without it... Any suggestions for what I might look at next? Chris

2 4

Non-blocking socket functions called without MSG_DONTWAIT flag
by kostirya＠gmail.com 20 Jun '19

20 Jun '19

Hello. I have question. Why Non-blocking socket functions called without MSG_DONTWAIT flag? Nick.

2 2

[RFC] move to C++11
by matthew.fernandez＠gmail.com 21 May '19

21 May '19

Hello PolyMLers, Some time ago I proposed PolyML switch to building with the C++11 standard [0]. The main blocking issue that surfaced was Isabelle supporting Ubuntu 12.04 which ships without a C++11-enlightened compiler. In January 2019, Makarius bumped the supported Linux release to Ubuntu 14.04 [1] which has a C++11 compiler. Are there any remaining issues preventing a migration to C++11? Do people feel strongly for or against this? The immediate benefits are similar to what I listed in my original posting: - PLock, PLocker, PCondVar implementations could all be deleted and dropped with std::mutex, std::lock_guard, std::condition_variable respectively - NORETURNFN could be replaced with [[noreturn]] - Bitmap could be dropped and replaced with std::vector<bool> The general motivation here is reducing the maintenance overhead and allowing performance to evolve with libstdc++/libc++. I expect we could get a lot of mileage out of code clarity wins too (e.g. range-based for loops). I haven?t CCed isabelle-dev because I think they would have no opinion on this topic, but Makarius if you think it?s relevant please loop them into this thread as well. Thanks, Matt [0]: http://lists.inf.ed.ac.uk/pipermail/polyml/2017-December/002125.html [1]: http://isabelle.in.tum.de/repos/isabelle/rev/88b8bc6a6e5f

3 7

`Exception- Overflow raised' during functor application
by ldbeth＠sdf.org 16 May '19

16 May '19

Hi Poly/ML members: I???m porting MLPolyR from SML/NJ to Poly/ML, and after getting smlnj-lib, ml-yacc and ml-lex loaded with Poly/ML I try to load the parser but the following error occurs: ``` Exception- Overflow raised Exception- Overflow raised ``` and `poly` quits. Here's a minimal setup that can reproduce the issue: https://github.com/owo-lang/MLPolyR/tree/polyml_debug Clone the tree and checkout `polyml_debug` branch, ``` poly --use load.sml ``` It already contains smlnj-lib, ml-yacc and ml-lex from MLton 20180207 releases. My platform is macOS Mojave 10.14.4, Poly/ML version is 5.8 Release. With the same setup MLton can compile the source without such an issue. (via `mlton mlpolyr.mlb`) Hints on what could be the cause? Thank you for any help you can offer. LdBeth.

2 1

Berkeley DB binding for Standard ML
by kostirya＠gmail.com 03 May '19

03 May '19

Hello. Let me introduce you the Berkeley DB binding for Standard ML (MLton and Poly/ML): https://github.com/kni/sml-bdb Nick. -- Also there are: https://github.com/kni/sml-net-server - Standard ML server engine https://github.com/kni/sml-net-server-ev - asynchronous Standard ML server engine https://github.com/kni/sml-http-server - Standard ML http server https://github.com/kni/sml-http-server-ev - asynchronous Standard ML http server https://github.com/kni/sml-gumbo-parser - bindings for Google's Gumbo HTML5 parser library https://github.com/kni/sml-uri - URI with IDN and IRI support.

1 0

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

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

← Newer
1
...
4
5
6
7
8
9
10
...
70
Older →

Jump to page:

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