Poly/ML January 2019

polyml@lists.polyml.org

6 participants
5 discussions

32bits addresses in 64-bit mode and other updates to master
by David.Matthews＠prolingua.co.uk 24 Jan '19

24 Jan '19

I've now merged a major piece of development work into GitHub master. This is a variant of 64-bit mode that uses 32-bit values. It was triggered by the observation that Isabelle often peformed better with the 32-bit version than the 64-bit despite the 64-bit version allowing a much larger heap and having more registers. It appears that Isabelle, at any rate, is limited more by the bandwidth between the processors and main memory than by the processors themselves. This may well be the result of the work on parallelising the application and the garbage collector. In effect there are now three versions on the X86: native 64-bit, native 32-bit and 32-bits on 64-bits. The new version can be built with the --enable-compact32bit option to configure. It allows a heap size of up to 16Gbytes by using 31-bit "object ids", essentially indexes into an array of 8-byte cells. This heap contains only the data. Code, thread stacks and other support structures are outside this. It has been extensively tested with Isabelle (thanks to Makarius) and seems to perform better than either of the native address versions. I started the development about a year ago; development of the final stages were supported by Data61 and CSIRO through Gerwin Klein. I would be interested in feedback on this and also the native address versions. Whether it well help other applications may depend on whether the limitation is processor speed or memory bandwidth. It's likely that many applications will continue to perform best with native addressing. The update also includes changes to the X86 code-generator that affect all the variants. These changes improve the way boolean values and conditionals are handled. There also other changes to the IO system. Garbage-collection of streams has been removed and overlapped IO is now used on Windows which should improve performance and responsiveness. There have been changes to the handling of floating point and Real32 has been added. Let me have any feedback. Regards, David

4 8

ASSERTION FAILURE: 0 at src/x86/ffi64.c:302 when --enable-debug
by kostirya＠gmail.com 11 Jan '19

11 Jan '19

Hello. I got FFI error when configure and built poly with --enable-debug *only*: ASSERTION FAILURE: 0 at src/x86/ffi64.c:302 The error happens on Linux and FreeBSD. I use PolyML from git at "Thu Jan 3 14:35:50" date (Linux) and "Fri Jun 22 13:49:32 2018" (FreeBSD): ./configure --with-gmp --enable-debug When I use PolyML *without* debugIt is all right. :-) GDB backtrace on linux: (gdb) bt #0 0x00007f53c3fca1f7 in raise () from /lib64/libc.so.6 #1 0x00007f53c3fcb8e8 in abort () from /lib64/libc.so.6 #2 0x00007f53c4c1295f in ffi_assert () from /home/nick/polyml/lib/libpolyml.so.9 #3 0x00007f53c4c1326a in ffi_prep_cif_machdep () from /home/nick/polyml/lib/libpolyml.so.9 #4 0x00007f53c4be1d31 in poly_ffi (taskData=0x7f53bc01b8c0, args=0x7f53bc01baf8, code=0x7f53bc01baf0) at polyffi.cpp:381 #5 0x00007f53c4be2986 in PolyFFIGeneral (threadId=0x7f53c4f54870, code=..., arg=...) at polyffi.cpp:587 #6 0x0000000000408aa2 in area1 () #7 0x00007f53abe429c0 in ?? () #8 0x00007f53abe42700 in ?? () #9 0x0000000000001000 in ?? () #10 0x00007f53c400f53b in new_heap () from /lib64/libc.so.6 #11 0x0000000000000000 in ?? () GDB backtrace on FreeBSD is more informative ans say "0x6f <Address 0x6f out of bounds>": (gdb) bt #0 0x000000080132a47a in thr_kill () from /lib/libc.so.7 #1 0x000000080132a444 in raise () from /lib/libc.so.7 #2 0x000000080132a3b9 in abort () from /lib/libc.so.7 #3 0x00000008009224a7 in ffi_assert () from /home/nick/polyml_new/lib/libpolyml.so.9 #4 0x0000000800923922 in classify_argument () from /home/nick/polyml_new/lib/libpolyml.so.9 #5 0x000000080092290e in examine_argument () from /home/nick/polyml_new/lib/libpolyml.so.9 #6 0x00000008009227eb in ffi_prep_cif_machdep () from /home/nick/polyml_new/lib/libpolyml.so.9 #7 0x000000080091b2d8 in ffi_prep_cif_core () from /home/nick/polyml_new/lib/libpolyml.so.9 #8 0x000000080091b54d in ffi_prep_cif () from /home/nick/polyml_new/lib/libpolyml.so.9 #9 0x00000008008e9cd8 in poly_ffi (taskData=0x802218200, args=0x80221c008, code=0x80221c000) at polyffi.cpp:379 #10 0x00000008008e8df0 in PolyFFIGeneral (threadId=0x8006b2208, code= {contents = {signedInt = 111, unsignedInt = 111, objectPtr = 0x6f, codePtr = 0x6f <Address 0x6f out of bounds>, stackAddr = 0x6f}}, arg= {contents = {signedInt = 34366811360, unsignedInt = 34366811360, objectPtr = 0x8006bece0, codePtr = 0x8006bece0 "\005", stackAddr = 0x8006bece0}}) at polyffi.cpp:585

2 2

Assertion `markCount == bitCount' failed
by gbuday＠gmail.com 04 Jan '19

04 Jan '19

Hi, in a CakeML compilation I got explorerProgTheory FAILED! <Signal 6> GC: Count error mark count 205399344, bitCount 205372170 GC: Count error mark count 205267608, bitCount 205240434 buildheap: gc.cpp:178: bool doGC(POLYUNSIGNED): Assertion `markCount == bitCount' failed. GC: Count error mark count 205267608, bitCount 205240434 What could cause this? Unsuccessful memory allocation attempt? Signal 6 is ABRT. I am using the 5.7.1 release. - Gergely

2 3

Too many passes raised while compiling
by gbuday＠gmail.com 04 Jan '19

04 Jan '19

Hi, using HEAD version of polyml I got the following error message building HOL: error in quse /home/gbuday/Desktop/HOL/src/1/TypeBasePure.sml : Fail "Exception- InternalError: Too many passes raised while compiling" The InternalError error message is in this file of polyml: ./mlsource/MLCompiler/COMPILER_BODY.ML: "Exception- InternalError: " ^ String.toString s ^ " raised while compiling" and the exception comes from ./mlsource/MLCompiler/CodeTree/X86Code/X86ICodeTransform.ML: val _ = passes < maxTotalPasses orelse raise InternalError "Too many passes" The error does not occur with the 5.7.1 release. Michael could comment on why TypeBasePure.sml is so special that the error is exhibited here. Large datatypes probably? What is this error? - Gergely

2 1

Smackage changes for Poly/ML
by mark.clements＠ki.se 04 Jan '19

04 Jan '19

I have had a pull request accepted for using Poly/ML with Smackage. However, the default Poly/ML executable in the Smackage Makefile is currently `POLYML=polyml`? Who would be affected if we changed the default to `POLYML=poly`, which seems to be the default on Debian and Mac? Any guidance here would be appreciated. Kindly, Mark. N?r du skickar e-post till Karolinska Institutet (KI) inneb?r detta att KI kommer att behandla dina personuppgifter. H?r finns information om hur KI behandlar personuppgifter<https://ki.se/medarbetare/integritetsskyddspolicy>. Sending email to Karolinska Institutet (KI) will result in KI processing your personal data. You can read more about KI?s processing of personal data here<https://ki.se/en/staff/data-protection-policy>.

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