Poly/ML

polyml@lists.polyml.org

698 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

Segmentation fault on get_stream
by kostirya＠gmail.com 31 Dec '18

31 Dec '18

Hello. I got sometimes Segmentation fault. The GDB backtrace of core file is bellow. It is multi thread server. I call Socket.bind and Socket.listen in main thread and then I create worker threads. If server have one worker thread then error is not occur. OS is CentOS, Poly/ML 5.7.2 Testing (Git version v5.7.1-161-g33045f8) #0 0x00007fbf878faa87 in get_stream(PolyWord) () from /home/nick/polyml/lib/libpolyml.so.9 #1 0x00007fbf878fac32 in writeArray(TaskData*, SaveVecEntry*, SaveVecEntry*, bool) [clone .isra.7] () from /home/nick/polyml/lib/libpolyml.so.9 #2 0x00007fbf878fc0be in IO_dispatch_c(TaskData*, SaveVecEntry*, SaveVecEntry*, SaveVecEntry*) () from /home/nick/polyml/lib/libpolyml.so.9 #3 0x00007fbf878fd2a1 in PolyBasicIOGeneral () from /home/nick/polyml/lib/libpolyml.so.9 #4 0x000000000041406d in area1 () #5 0x0000000000002001 in ?? () #6 0x00007fbf87b57320 in ?? () from /home/nick/polyml/lib/libpolyml.so.9 #7 0x00007fbf81e49e30 in ?? () #8 0x0000000000006001 in ?? () #9 0x0000000000010008 in ?? () #10 0x00007fbf879171ed in Processes::FindAllocationSpace(TaskData*, unsigned long, bool) () from /home/nick/polyml/lib/libpolyml.so.9 #11 0x00007fbf7c00a4d0 in ?? () #12 0x00007fbf81e4a660 in ?? () #13 0x00007fbf8792c9f1 in X86TaskData::SwitchToPoly() () from /home/nick/polyml/lib/libpolyml.so.9 #14 0x00007fbf8792cbcc in X86TaskData::EnterPolyCode() () from /home/nick/polyml/lib/libpolyml.so.9 #15 0x00007fbf87916fc9 in NewThreadFunction(void*) () ============================================================== This one more backtrace. #0 0x00007ff5a378ba87 in get_stream(PolyWord) () from /home/nick/polyml/lib/libpolyml.so.9 #1 0x00007ff5a379ef08 in getSelectResult(TaskData*, SaveVecEntry*, int, WaitSelect*) () from /home/nick/polyml/lib/libpolyml.so.9 #2 0x00007ff5a379f481 in selectCall(TaskData*, SaveVecEntry*, int) () from /home/nick/polyml/lib/libpolyml.so.9 #3 0x00007ff5a37a03ed in Net_dispatch_c(TaskData*, SaveVecEntry*, SaveVecEntry*) () from /home/nick/polyml/lib/libpolyml.so.9 #4 0x00007ff5a37a12f7 in PolyNetworkGeneral () from /home/nick/polyml/lib/libpolyml.so.9 #5 0x00000000004078a2 in area1 () #6 0x0000000000002001 in ?? () #7 0x00007ff5a39e8320 in ?? () from /home/nick/polyml/lib/libpolyml.so.9 #8 0x00007ff59d4d9e30 in ?? () #9 0x000000000000a001 in ?? () #10 0x0000000000010008 in ?? () #11 0x00007ff5a37a81ed in Processes::FindAllocationSpace(TaskData*, unsigned long, bool) () from /home/nick/polyml/lib/libpolyml.so.9 #12 0x00007ff59800c980 in ?? () #13 0x00007ff59d4da660 in ?? () #14 0x00007ff5a37bd9f1 in X86TaskData::SwitchToPoly() () from /home/nick/polyml/lib/libpolyml.so.9 #15 0x00007ff5a37bdbcc in X86TaskData::EnterPolyCode() () ---Type <return> to continue, or q <return> to quit--- from /home/nick/polyml/lib/libpolyml.so.9 #16 0x00007ff5a37a7fc9 in NewThreadFunction(void*) () from /home/nick/polyml/lib/libpolyml.so.9 #17 0x00007ff5a2968e25 in start_thread () from /lib64/libpthread.so.0 #18 0x00007ff5a2c7534d in clone () from /lib64/libc.so.6 ============================================================== This one more backtrace. #0 0x00007f88d2be3a87 in get_stream(PolyWord) () from /home/nick/polyml/lib/libpolyml.so.9 #1 0x00007f88d2be5b85 in IO_dispatch_c(TaskData*, SaveVecEntry*, SaveVecEntry*, SaveVecEntry*) () from /home/nick/polyml/lib/libpolyml.so.9 #2 0x00007f88d2be62a1 in PolyBasicIOGeneral () from /home/nick/polyml/lib/libpolyml.so.9 #3 0x000000000040580d in area1 () #4 0x0000000000002001 in ?? () #5 0x00007f88d2e40320 in ?? () from /home/nick/polyml/lib/libpolyml.so.9 #6 0x00007f88cc931e30 in ?? () #7 0x000000000000a001 in ?? () #8 0x0000000000010008 in ?? () #9 0x00007f88d2c001ed in Processes::FindAllocationSpace(TaskData*, unsigned long, bool) () from /home/nick/polyml/lib/libpolyml.so.9 #10 0x00007f88c800c980 in ?? () #11 0x00007f88cc932660 in ?? () #12 0x00007f88d2c159f1 in X86TaskData::SwitchToPoly() () from /home/nick/polyml/lib/libpolyml.so.9 #13 0x00007f88d2c15bcc in X86TaskData::EnterPolyCode() () from /home/nick/polyml/lib/libpolyml.so.9 #14 0x00007f88d2bfffc9 in NewThreadFunction(void*) () from /home/nick/polyml/lib/libpolyml.so.9 #15 0x00007f88d1dc0e25 in start_thread () from /lib64/libpthread.so.0 #16 0x00007f88d20cd34d in clone () from /lib64/libc.so.6 ===================================================================== This one more backtrace. #0 0x00007f1ed86fca87 in get_stream(PolyWord) () from /home/nick/polyml/lib/libpolyml.so.9 #1 0x00007f1ed8710209 in selectCall(TaskData*, SaveVecEntry*, int) () from /home/nick/polyml/lib/libpolyml.so.9 #2 0x00007f1ed87113ed in Net_dispatch_c(TaskData*, SaveVecEntry*, SaveVecEntry*) () from /home/nick/polyml/lib/libpolyml.so.9 #3 0x00007f1ed87122f7 in PolyNetworkGeneral () from /home/nick/polyml/lib/libpolyml.so.9 #4 0x00000000004078a2 in area1 () #5 0x0000000000002001 in ?? () #6 0x00007f1ed8959320 in ?? () from /home/nick/polyml/lib/libpolyml.so.9 #7 0x00007f1ecdffae30 in ?? () #8 0x000000000000a001 in ?? () #9 0x0000000000010008 in ?? () #10 0x00007f1ed87191ed in Processes::FindAllocationSpace(TaskData*, unsigned long, bool) () from /home/nick/polyml/lib/libpolyml.so.9 #11 0x00007f1ed000c980 in ?? () #12 0x00007f1ecdffb660 in ?? () #13 0x00007f1ed872e9f1 in X86TaskData::SwitchToPoly() () from /home/nick/polyml/lib/libpolyml.so.9 #14 0x00007f1ed872ebcc in X86TaskData::EnterPolyCode() () from /home/nick/polyml/lib/libpolyml.so.9 #15 0x00007f1ed8718fc9 in NewThreadFunction(void*) ()

4 6

Compilation of dynamically loaded code
by vijay.the.lisper＠gmail.com 27 Dec '18

27 Dec '18

Hi, I am new to PolyML and this question is a basic one. Is a file loaded by the top-level `use` function compiled to machine code or is it compiled to the instructions of a VM? Thanks, Vijay

2 1

Handle Interrupt exception
by kostirya＠gmail.com 14 Dec '18

14 Dec '18

Hello. Do Interrupt exception is special exception? I got warning "Pattern 2 is redundant" for this code: doit () handle Interrupt => NONE | exc => raise exc Why? If one use other exception, then it is all right. Warning is missing. doit () handle Option => NONE | exc => raise exc Nick.

2 2

Strange system calls when one use Socket.select or OS.IO.poll
by kostirya＠gmail.com 14 Dec '18

14 Dec '18

Hello. My application use select or poll before accept socket. I trace system calls and found that too many select or poll calls occur. When I use select: select(1024,{ },{ },{ },{ 0.010000 }) = 0 (0x0) select(1024,{ 3 },{ },{ },{ 0.000000 }) = 0 (0x0) select(1024,{ },{ },{ },{ 0.010000 }) = 0 (0x0) select(1024,{ 3 },{ },{ },{ 0.000000 }) = 0 (0x0) select(1024,{ },{ },{ },{ 0.010000 }) = 0 (0x0) ... select(1024,{ 3 },{ },{ },{ 0.000000 }) = 1 (0x1) accept(3,{ AF_INET 127.0.0.1:54121 },0xbb9f9c5c) = 4 (0x4) When I use poll and do *not* select: poll({ 3/POLLIN },1,0) = 0 (0x0) select(1024,{ },{ },{ },{ 0.010000 }) = 0 (0x0) poll({ 3/POLLIN },1,0) = 0 (0x0) select(1024,{ },{ },{ },{ 0.010000 }) = 0 (0x0) poll({ 3/POLLIN },1,0) = 0 (0x0) select(1024,{ },{ },{ },{ 0.010000 }) = 0 (0x0) poll({ 3/POLLIN },1,0) = 1 (0x1) ... accept(3,{ AF_INET 127.0.0.1:48659 },0xbb9f9c5c) = 4 (0x4) My application wait incoming connection and do nothing but use 1-2% CPU. What is it and why it is? By the way. When I use kevent (epoll on linux) via FFI it is all right. Nick.

2 4

Run out of store - interrupting threads
by buday.gergely＠uni-eszterhazy.hu 05 Dec '18

05 Dec '18

Hi, https://polyml.inf.ed.ac.narkive.com/c53BJE4q/run-out-of-store-interrupting- threads says that setting --maxheap with polyml can fix this problem. Does this memory allocation necessarily mean _physical_ memory allocation or the operating system can use swap space to have the necessary memory? I have set maxheap as twice the physical memory size in a CakeML compilation and I still got this error message (8G/16G). - Gergely

3 5

← Newer
1
...
6
7
8
9
10
11
12
...
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