Poly/ML

polyml@lists.polyml.org

720 discussions

Memory consumption profiling in PolyML
by Thomas.Sewell＠nicta.com.au 24 Sep '11

24 Sep '11

Hello to the PolyML users mailing list. I'm an Isabelle/HOL user from the L4.verified project at NICTA, and we're having some issues with Isabelle using far too much memory. I have a feature request that would be useful in diagnosing the problem. The current implementation of PolyML provides an object profiling mechanism PolyML.objProfile which analyses memory consumed by a given object, decomposed by size. As a trivial issue, there doesn't seem to be a good way to profile all the heap, since threading may make some objects inaccessible from the current root function. The big issue is that the profile doesn't tell me anything useful at all. ML> PolyML.objProfile (Thy_Info.get_theory "Nat"); Immutable object sizes and counts 1 229872 2 2557083 3 756596 4 1283875 5 811230 6 24521 7 102914 8 9200 9 9452 10 20660 ... The development is too big for me to have a chance of identifying which objects of size 2, 4 and 5 are consuming all the memory. By comparison, an object profile could be really valuable if it were decomposed by type (or possible type and/or closure). This would hopefully make it straightforward to hunt down the worst-offending modules. On a related note, Don Stewart gave a talk about his experience in Haskell working at Galois recently, and pointed out that profiling by types in their runtime effectively eliminated their problems with the famous Haskell space-leak issue. It seems to me this would be roughly compatible with the existing objProfile algorithm. I had a look at the code and got as far as realising I had no hope of understanding how PolyML encodes types internally. Does this seem like a reasonable feature request? Yours, Thomas.

2 2

Memory consumption profiling in PolyML
by Thomas.Sewell＠nicta.com.au 23 Sep '11

23 Sep '11

I may have overstated Don's point. I didn't mean that it was no longer a problem with the language - I was saying that this was an effective way to eliminate the problem within a given program. Space leaks are certainly a huge problem with the language. For novice/casual users the runtime is effectively a black box and space leaks are a showstopper. Don was pointing out that if your process involves using these tools routinely (such as at Galois) then the problem diminishes greatly. Yours, Thomas. On 23/09/11 16:10, Paul A. Steckler wrote: > On Fri, Sep 23, 2011 at 2:58 PM, Thomas Sewell > <Thomas.Sewell(a)nicta.com.au> wrote: >> On a related note, Don Stewart gave a talk about his experience in Haskell >> working at Galois recently, and pointed out that profiling by types in their >> runtime effectively eliminated their problems with the famous Haskell >> space-leak issue. > Do you mean, they now have a good idea where to stuff seq's in their code? > > Still a bother to have to routinely run the memory profiler on your code. > > -- Paul

1 0

Pretty printing of functor arguments
by phil.clayton＠lineone.net 03 Sep '11

03 Sep '11

Just a minor observation: when I enter e.g. functor F () = struct end; Poly/ML prints back functor F (sig end) : sig end Generally, when Functor_Arguments is a Specification, it prints back with an enclosing sig ... end. Even if the whole response is not a valid piece of syntax, it would seem nice to have a valid Functor_Arguments printed back. (I made exactly the same mistake initially!) Phil

1 0

Order of evaluation of arguments to a function
by ivan.tomac＠gmail.com 20 Aug '11

20 Aug '11

Is the following code supposed to print 1 followed by 2 or 2 followed by 1? val _ = (fn () => (print "1\n"; fn x => x)) () (print "2\n"; ()) In SML/NJ, MLton and PolyML it does the former, while in Moscow ML it does the latter. Is this specified somewhere in the standard? I noticed equivalent code in OCaml behaves the way Moscow ML does which is not very surprising seeing how Moscow ML was based on Caml Light. Could this be a bug in Moscow ML? The following code works the same in all 4 SML compilers (but different in OCaml): val _ = (print "1\n"; 1) + (print "2\n"; 2) It seems to me like SML/NJ, MLton and PolyML evaluate all function arguments left to right, OCaml evaluates them right to left, and Moscow ML seems inconsistent.

6 6

Re: [MLton-user] Order of evaluation of arguments to a function
by ivan.tomac＠gmail.com 19 Aug '11

19 Aug '11

On Fri, Aug 19, 2011 at 1:32 AM, <rossberg(a)mpi-sws.org> wrote: >> Is the following code supposed to print 1 followed by 2 or 2 followed by 1? >> >> val _ = (fn () => (print "1\n"; fn x => x)) () (print "2\n"; ()) >> >> In SML/NJ, MLton and PolyML it does the former, while in Moscow ML it >> does the latter. Is this specified somewhere in the standard? I >> noticed equivalent code in OCaml behaves the way Moscow ML does which >> is not very surprising seeing how Moscow ML was based on Caml Light. >> Could this be a bug in Moscow ML? > > It is specified, and the deviation a (known) bug/limitation of Moscow ML. > It's due to its implementation being based on the Caml VM, which chose this > semantics in order to be able to implement curried functions more > efficiently. > Interesting and very useful to know. > (Note that in OCaml, evaluation order actually depends on whether you are > using byte code or native code compilation.) > That sounds bad.

1 0

PolyML with OS X 10.7 Lion?
by palantir＠trustworthytools.com 13 Aug '11

13 Aug '11

I have just recently updated my MacBook Pro from Snow Leopard to Lion (Mac OS X 10.7), and now I am regretting it. Poly/ML has stopped working for building the HOL theorem prover. When I try to run the configuration script for HOL using my current version of Poly/ML, I see . . . Making tools/mllex/mllex.exe. Poly/ML 5.3 Release > # ld: library not found for -lcrt1.10.6.o collect2: ld returned 1 exit status Failed to build mllex. In fact this library was present in prior versions of Mac OS X, like 10.6, but is not present in 10.7. So I tried downloading and building the current version of Poly/ML, 5.4.1. I have the current version of the Developer tools, Xcode version 4.1 for Lion. When trying ./configure I see -bash-3.2$ ./configure checking for a BSD-compatible install... /usr/bin/install -c checking whether build environment is sane... yes checking for a thread-safe mkdir -p... ./install-sh -c -d checking for gawk... no checking for mawk... no checking for nawk... no checking for awk... awk checking whether make sets $(MAKE)... yes checking build system type... x86_64-apple-darwin11.0.0 checking host system type... x86_64-apple-darwin11.0.0 checking for style of include used by make... GNU checking for gcc... gcc checking whether the C compiler works... no configure: error: in `/Users/palantir/sml/polyml/polyml.5.4.1': configure: error: C compiler cannot create executables See `config.log' for more details When I look at the end of the config.log file, I see ## ----------- ## ## confdefs.h. ## ## ----------- ## /* confdefs.h */ #define PACKAGE_NAME "Poly/ML" #define PACKAGE_TARNAME "polyml" #define PACKAGE_VERSION "5.4" #define PACKAGE_STRING "Poly/ML 5.4" #define PACKAGE_BUGREPORT "polyml AT polyml DOT org" #define PACKAGE_URL "" #define PACKAGE "polyml" #define VERSION "5.4" configure: exit 77 Are there any suggestions on how to get Poly/ML working under Lion? Thanks. Peter V. Homeier -- "In Your majesty ride prosperously because of truth, humility, and righteousness; and Your right hand shall teach You awesome things." (Psalm 45:4)

1 0

Experiences with Lion
by aleks0＠gmail.com 24 Jul '11

24 Jul '11

Hi folks, I'm considering updating my system to OS X 10.7, though I'm wondering if it will torpedo poly (cf. Snow leopard). Has anyone had success/struggles running poly/ML under Lion? Aleks

1 0

Bug fixes and 5.4.1
by David.Matthews＠prolingua.co.uk 14 Jul '11

14 Jul '11

There have been a few bugs fixed since the release of 5.4. I've now back-ported the fixes to the 5.4-fixes branch and updated the pre-built compilers for all the architectures. The two issues that seem to have caused particular problems are the divide instruction bug that caused an assertion fault in the garbage collector and the failure to pass floating point rounding control that meant that IEEEReal.setRoundingMode didn't have any effect. I'm planning to release this as a bug-fix release in the next week or so unless anyone reports any problems. Because the pre-built compilers have been updated it should only be necessary to run ./configure make in the fixes branch. Run "make distclean" if necessary to get a clean directory. David

2 1

measuring/profiling memory consumption
by kleing＠cse.unsw.edu.au 07 Jul '11

07 Jul '11

What is the best way to measure memory consumption in polyml? Background: we're running out of memory after porting some of our tools and proofs to Isabelle-2011. It seems that the main problem is that we are now producing more objects that can later be shared, i.e. we think we were able to get memory consumption down by sharing more often (using PolyML.shareCommonData PolyML.rootFunction, not sure if this is the sane thing to do). It's still too much for saving the state at the end of the session on a 32bit system, though. On 64bit systems, we seem to need about 12GB for something that fit into about 2G on 32bit before. We tried various measurements and tried to bisect where in Isabelle or our code the problem was introduced, but we're only getting strange results - seemingly completely unrelated changes. My guess is that we didn't measure right. We used PolyML.objSize PolyML.rootFunction as an approximation of the overall memory consumption, but that doesn't always seem to correspond. What is the best way to figure out more precisely what is going? More specifically, I'd like to figure out: - maximum total memory consumption of the polyml process in a complete program run - current non-garbage heap consumption at a given point in the program - more detailed view of which type of object is how big and occurs how often at a given point Does anyone have more experience with this kind of thing? Cheers, Gerwin

2 1

Assertion `val.IsDataPtr()' failed
by alex.merry＠cs.ox.ac.uk 01 Jul '11

01 Jul '11

I think Lucas has probably mentioned this problem that we keep running into with quantomatic. I'm using Poly/ML 5.4 (ie: the lastest version of the 5.4 branch from subversion). Occasionally (or, in my case, frequently) we get the following error: poly: scanaddrs.cpp:107: PolyWord ScanAddress::ScanStackAddress(PolyWord, StackObject*, bool): Assertion `val.IsDataPtr()' failed. There appears to be no rhyme or reason to it. Re-running poly with the same code another time will not necessarily produce this assertion, or may produce it in a different place. It happens regardless of compiler optimisations (I've tried -O3, -O2 and -O0). I managed to get a backtrace: #0 0x0000003ff54330c5 in raise () from /lib64/libc.so.6 #1 0x0000003ff5434a76 in abort () from /lib64/libc.so.6 #2 0x0000003ff542b905 in __assert_fail () from /lib64/libc.so.6 #3 0x00007ffff7dc357e in ScanAddress::ScanStackAddress (this=0x7fffffffde10, val=..., base=0x7fffed6b56c0, isCode=false) at scanaddrs.cpp:107 #4 0x00007ffff7dc3811 in ScanAddress::ScanAddressesInObject (this=0x7fffffffde10, obj=0x7fffed6b56c0, lengthWord=4827858800541175088) at scanaddrs.cpp:146 #5 0x00007ffff7d9b4e2 in ProcessMarkPointers::ScanAddressesInObject (this=0x7fffffffde10, base=0x7fffed6b56c0, L=4827858800541175088) at gc.cpp:509 #6 0x00007ffff7dc42c8 in ScanAddress::ScanAddressesInObject (this=0x7fffffffde10, base=0x7fffed6b56c0) at scanaddrs.h:86 #7 0x00007ffff7dc3d48 in ScanAddress::ScanAddressesInRegion (this=0x7fffffffde10, region=0x7fffed6a3af0, end=0x7fffed6c3000) at scanaddrs.cpp:252 #8 0x00007ffff7d9ad12 in OpMutables (process=0x7fffffffde10) at gc.cpp:348 #9 0x00007ffff7d9d2cc in doGC (doFullGC=false, wordsRequiredToAllocate=3) at gc.cpp:1341 #10 0x00007ffff7d9f473 in QuickGCRequest::Perform (this=0x7fffeaa10cc0) at gc.cpp:1955 #11 0x00007ffff7da732c in Processes::BeginRootThread (this=0x7ffff7ffa8e0, rootFunction=0x605278) at processes.cpp:1253 #12 0x00007ffff7d9a472 in polymain (argc=3, argv=0x7fffffffe218, exports=0xf72a00) at mpoly.cpp:205 #13 0x0000000000400659 in main (argc=3, argv=0x7fffffffe218) at polystub.c:43 I don't know how useful that is, though. Alex

2 4

← Newer
1
...
39
40
41
42
43
44
45
...
72
Older →

Jump to page:

2026

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