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.
The tarball did survive the mailing list and I've just unpacked it and tried the test on my MacBook. The problem does not occur on a MacBook running Mac OS High Sierra 10.13.6 but does occur on an iMac running Mac OS Mojave 10.14.4.
I'll try it on some Linux VMs tomorrow.
Regards,
Rob.
On 30 Mar 2019, at 16:50, Rob Arthan <rda at lemma-one.com> wrote:
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. <fordavidm20190330.tgz>_______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
I have done some further experiments. I can reproduce the problem on
Mac OS Mojave 10.14.4 Fedora 24 Kubuntu 18.10
The above were all run an iMac using VirtualBox VMs for the Linux distros.
I also tried running poly under a debugger and found that the problem doesn?t occur when run under lldb on Mac OS Mojave. It does occur when run under gdb on the two Linux distros.
Regards,
Rob
On 31 Mar 2019, at 00:04, Rob Arthan <rda at lemma-one.com> wrote:
The tarball did survive the mailing list and I've just unpacked it and tried the test on my MacBook. The problem does not occur on a MacBook running Mac OS High Sierra 10.13.6 but does occur on an iMac running Mac OS Mojave 10.14.4.
I'll try it on some Linux VMs tomorrow.
Regards,
Rob.
On 30 Mar 2019, at 16:50, Rob Arthan <rda at lemma-one.com> wrote:
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. <fordavidm20190330.tgz>_______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Rob, Have you tried using the Poly debugger? PolyML.Compiler.debug := true; open PolyML.Debug; breakEx Overflow; then compile your code.
This won't help if the problem is a code-generator bug because adding the debugging code may well change the code and avoid the bug but if it's a library function this may narrow it down.
Regards, David
On 31/03/2019 13:31, Rob Arthan wrote:
I have done some further experiments. I can reproduce the problem on
Mac OS Mojave 10.14.4 Fedora 24 Kubuntu 18.10
The above were all run an iMac using VirtualBox VMs for the Linux distros.
I also tried running poly under a debugger and found that the problem doesn?t occur when run under lldb on Mac OS Mojave. It does occur when run under gdb on the two Linux distros.
Regards,
Rob
On 31 Mar 2019, at 00:04, Rob Arthan <rda at lemma-one.com> wrote:
The tarball did survive the mailing list and I've just unpacked it and tried the test on my MacBook. The problem does not occur on a MacBook running Mac OS High Sierra 10.13.6 but does occur on an iMac running Mac OS Mojave 10.14.4.
I'll try it on some Linux VMs tomorrow.
Regards,
Rob.
On 30 Mar 2019, at 16:50, Rob Arthan <rda at lemma-one.com> wrote:
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. <fordavidm20190330.tgz>_______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
David,
On 2 Apr 2019, at 11:34, David Matthews <David.Matthews at prolingua.co.uk> wrote:
Rob, Have you tried using the Poly debugger? PolyML.Compiler.debug := true; open PolyML.Debug; breakEx Overflow; then compile your code.
This won't help if the problem is a code-generator bug because adding the debugging code may well change the code and avoid the bug but if it's a library function this may narrow it down.
It ran to completion after about 6 hours. So compiling for debugging does avoid the bug. Is there anything I can do with gdb? I?ll have a think about instrumenting my code with exception handlers to try to pinpoint the problem.
Regards,
Rob.
Regards, David
On 31/03/2019 13:31, Rob Arthan wrote:
I have done some further experiments. I can reproduce the problem on Mac OS Mojave 10.14.4 Fedora 24 Kubuntu 18.10 The above were all run an iMac using VirtualBox VMs for the Linux distros. I also tried running poly under a debugger and found that the problem doesn?t occur when run under lldb on Mac OS Mojave. It does occur when run under gdb on the two Linux distros. Regards, Rob
On 31 Mar 2019, at 00:04, Rob Arthan <rda at lemma-one.com> wrote:
The tarball did survive the mailing list and I've just unpacked it and tried the test on my MacBook. The problem does not occur on a MacBook running Mac OS High Sierra 10.13.6 but does occur on an iMac running Mac OS Mojave 10.14.4.
I'll try it on some Linux VMs tomorrow.
Regards,
Rob.
On 30 Mar 2019, at 16:50, Rob Arthan <rda at lemma-one.com> wrote:
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. <fordavidm20190330.tgz>_______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
David,
Apologies! This was all down to a simple misunderstanding on my part. I hadn't appreciated that --enable-compact32bit gives you 31-bit ints. My proof search explores in excess of 2^32 blind alleys and it tries to count them.
The confusion about Mac OS versions and lldb was caused by me doing the tests with the compiler built with --enable-intinf-as-int as well as --enable-compact32bit.
Regards,
Rob.
On 3 Apr 2019, at 18:41, Rob Arthan <rda at lemma-one.com> wrote:
David,
On 2 Apr 2019, at 11:34, David Matthews <David.Matthews at prolingua.co.uk> wrote:
Rob, Have you tried using the Poly debugger? PolyML.Compiler.debug := true; open PolyML.Debug; breakEx Overflow; then compile your code.
This won't help if the problem is a code-generator bug because adding the debugging code may well change the code and avoid the bug but if it's a library function this may narrow it down.
It ran to completion after about 6 hours. So compiling for debugging does avoid the bug. Is there anything I can do with gdb? I?ll have a think about instrumenting my code with exception handlers to try to pinpoint the problem.
Regards,
Rob.
Regards, David
On 31/03/2019 13:31, Rob Arthan wrote:
I have done some further experiments. I can reproduce the problem on Mac OS Mojave 10.14.4 Fedora 24 Kubuntu 18.10 The above were all run an iMac using VirtualBox VMs for the Linux distros. I also tried running poly under a debugger and found that the problem doesn?t occur when run under lldb on Mac OS Mojave. It does occur when run under gdb on the two Linux distros. Regards, Rob
On 31 Mar 2019, at 00:04, Rob Arthan <rda at lemma-one.com> wrote:
The tarball did survive the mailing list and I've just unpacked it and tried the test on my MacBook. The problem does not occur on a MacBook running Mac OS High Sierra 10.13.6 but does occur on an iMac running Mac OS Mojave 10.14.4.
I'll try it on some Linux VMs tomorrow.
Regards,
Rob.
On 30 Mar 2019, at 16:50, Rob Arthan <rda at lemma-one.com> wrote:
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. <fordavidm20190330.tgz>_______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Rob, I'm glad that's sorted. --enable-compact32bit uses 32-bit quantities for both addresses and ints. It's necessary to use the same size for both in order to be able to compile polymorphic functions. LargeWord.word is 64-bits (i.e. two "words") to allow it to handle native values in SysWord.word.
Regards, David
On 04/04/2019 11:38, Rob Arthan wrote:
David,
Apologies! This was all down to a simple misunderstanding on my part. I hadn't appreciated that --enable-compact32bit gives you 31-bit ints. My proof search explores in excess of 2^32 blind alleys and it tries to count them.
The confusion about Mac OS versions and lldb was caused by me doing the tests with the compiler built with --enable-intinf-as-int as well as --enable-compact32bit.
Regards,
Rob.
-
David.Matthews＠prolingua.co.uk -
rda＠lemma-one.com