Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

[David Matthews]

On 28/01/2019 09:20, Bertram Felgenhauer wrote:

I've made sure that the machine is mostly idle; things will be much
different if several processes start competing for the ressources.

I intended to experiment with smaller numbers but have not yet done so.
On another, similar machine, --gcthreads=2 was just as fast as 6.



It is increasingle clear that the limiting factor is the bandwidth 
between main memory and the processors.  There needs to be sufficient 
parallelism to saturate this channel; more than that will not help and 
may well make things worse.


How many threads are needed to saturate the memory channel depends on 
the processor speed, the memory speed and the application so there's no 
single answer to this.  Garbage collection can be particularly bad. 
Each word in the live data is read in and if it is a pointer it is 
followed.  There's no reuse so caching doesn't help.


The idea behind developing the 32-bit value model for the 64-bit 
processor was that by reducing the size of an ML cell more cells could 
be transferred through the memory channel in a given time.  That seems 
to have been borne out by the results.


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

[David Matthews]

On 23/01/2019 21:08, Makarius wrote:

On 23/01/2019 12:05, David Matthews wrote:


I've had a look at this under Windows and the problem seems to be with
calls to IntInf.divMod from generated code, not from IntInf.pow.  The
underlying RTS call used by IntInf.quotRem has changed in the 32-in-64
version.  It previously returned the pair of values by passing in a
stack location and having the RTS update this.  That isn't possible in
the 32-in-64 version so now it allocates a pair on the heap.  For
simplicity this is now used for the native code versions as well.  From
what I can tell nearly all the threads are waiting for mutexes and I
suspect that the extra heap allocation in IntInf.quotRem is causing some
of the problem.  Waiting for a contended mutex can cost a significant
amount of processor time both in busy-waiting and in kernel calls.

I'm not sure what to suggest except not to use concurrency here.  There
doesn't seem to be a way to avoid allocating a pair in IntInf.quotRem.


In the meantime David has produced Poly/ML a444f281ccec and I can
confirm that it works very well:


I had another look and it was a mutex contention problem, just not 
exactly where I'd thought.  Most calls to the run-time system involved 
taking a lock for a very short period in order to get the thread's C++ 
data structure.  This wasn't a problem in the vast majority of cases but 
this example involves very many calls to the long-format arbitrary 
precision package.  That resulted in contention on the lock.  I've 
changed this so the lock is no longer needed and it seems to have solved 
the problem.


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

[David Matthews]

On 22/01/2019 23:01, Makarius wrote:

On 22/01/2019 23:08, Fabian Immler wrote:

On 1/22/2019 4:00 PM, Fabian Immler wrote:

On 1/22/2019 2:28 PM, Makarius wrote:

On 22/01/2019 20:05, Fabian Immler wrote:

These numbers look quite extreme:
The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as
it seems to be the case with polyml-test-0a6ebca445fc).

The following is isabelle/ab5a8a2519b0 afp/f49f0b0ead38 on lxcisa0:

ML_PLATFORM="x86-linux"
ML_OPTIONS="--minheap 2000 --maxheap 4000"
Finished HOL-ODE-Numerics (0:25:27 elapsed time, 1:07:49 cpu time,
factor 2.66)
Finished HOL-ODE-ARCH-COMP (0:18:01 elapsed time, 0:26:19 cpu time,
factor 1.46) > (I am testing HOL-ODE-ARCH-COMP with

polyml-test-0a6ebca445fc/x86_64_32-linux right now, but that does take
some time...)

HOL-ODE-ARCH-COMP looked fine (2-3 times slower). But I realized that
this was the case with your computations, too. Unlike Lorenz_C0:


x86_64_32-linux -minheap 1500
Finished Lorenz_C0 (3:46:03 elapsed time, 28:01:18 cpu time, factor 7.44)
x86_64-linux --minheap 3000
Finished Lorenz_C0 (0:06:52 elapsed time, 0:51:44 cpu time, factor 7.52)

Lorenz_C0 had the most significant slowdown, it has the biggest number
of parallel computations, so I thought this might be related.

And indeed, if you try the theory at the end:
Par_List.map (with 6 cores, on Windows) is 12 times slower on _64_32
whereas the sequential evaluation is only 2 times slower.

All of this reminds me of the discussion we had in November 2017:
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2017-November/thread.html#7643


Back in Nov-2017, I made the following workaround that is still active:
http://isabelle.in.tum.de/repos/isabelle/rev/5da20135f560

Looking at the profiles of the included Float_Test.thy I now see a lot
of IntInf.divMod, but it is qualitatively similar to former IntInf.pow.

Maybe David can revisit both of these operations, so that we can  get
rid of the workarounds.


I've had a look at this under Windows and the problem seems to be with 
calls to IntInf.divMod from generated code, not from IntInf.pow.  The 
underlying RTS call used by IntInf.quotRem has changed in the 32-in-64 
version.  It previously returned the pair of values by passing in a 
stack location and having the RTS update this.  That isn't possible in 
the 32-in-64 version so now it allocates a pair on the heap.  For 
simplicity this is now used for the native code versions as well.  From 
what I can tell nearly all the threads are waiting for mutexes and I 
suspect that the extra heap allocation in IntInf.quotRem is causing some 
of the problem.  Waiting for a contended mutex can cost a significant 
amount of processor time both in busy-waiting and in kernel calls.


I'm not sure what to suggest except not to use concurrency here.  There 
doesn't seem to be a way to avoid allocating a pair in IntInf.quotRem.


By the way I updated IntInf.pow with
https://github.com/polyml/polyml/commit/c2a296122426f5a6205cf121218e3f38415d2b06

David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: support for GHC

[David Matthews]

On 22/10/2018 14:05, Lars Hupel wrote:

The binary provided by Homebrew does not exhibit that problem. I have no
other information beyond that.


I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there.

Interestingly enough, I get Poly/ML warnings of the form:

14:11:19 poly(50366,0xb042) malloc: *** mach_vm_map(size=8388608)
failed (error code=3)
14:11:19 *** error: can't allocate region
14:11:19 *** set a breakpoint in malloc_error_break to debug



This is an Apple bug.  It produces this message if it can't allocate 
memory in certain situations.  That's a perfectly normal case and other 
operating systems just silently, and correctly, return zero from malloc. 
 Poly/ML deals with that.  Just ignore it.


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [158c513a39f5] JVM crash

[David Matthews]

If these crashes are happening at the end of the build process I would 
suspect that it is something to do with either the data sharing or 
writing out the heap image.  Writing the heap image does not involve any 
concurrency but the data sharing does, so I would suspect the latter. 
That has changed recently in 5.7.1 but so too has saving the heap.  The 
fact that it only occurs on specific hardware points to some error in 
the memory model i.e. that the code is assuming something about the 
consistency of memory that is not in fact true.  It's impossible to be 
sure about any of this without running tests on the hardware itself.  At 
least the problem seems to have gone away with the latest version of 
Poly/ML.


David

On 08/11/2017 08:21, Manuel Eberl wrote:

I was not able to find out what exactly crashes and why, but while
trying to do that, I found out that the problem is actually not present
in the development version of Isabelle anymore.

After a lengthy bisection, I found that the first revision where no
crashes occur is this one:

changeset:   66920:aefaaef29c58
user:    wenzelm
date:    Thu Oct 26 13:44:41 2017 +0200
summary: use Poly/ML 5.7.1 test version as default;

So apparently, something changed in Poly/ML 5.7.1 that made the crashes
go away. Older versions of Isabelle, i.e. Isabelle2016-1, Isabelle2017,
and isabelle-dev up to 66919:1f93e376aeb6 /do/ exhibit the crash. It
thus seems likely that whatever caused it was apparently present in
multiple older Poly/ML versions.

Note that the crash appears to be highly sensitive to the environment:
Having two builds run in parallel with different Isabelle versions seems
to make it considerably less frequent; however, only in Poly/ML 5.7.1
does it appear to not happen at all no matter how I run it.

Does Poly/ML 5.7.1 contain any changes that could plausibly cause this
bad behaviour to go away?

Manuel


On 2017-11-07 09:51, Manuel Eberl wrote:

It seems like this thread is not dead yet.

I had my CPU replaced by a new version that supposedly does not have the
SMD problem on Linux. The problem with Isabelle did not go away.

I still get reproducible crashes of "isabelle build -c Pure", but only
with SMT switched on. However, it is worth noting that the crashes
always seem to happen at the end of the build process. (A successful
build takes about 9 seconds of elapsed and CPU time on my machine and
unsuccessful ones always crash at at least that time) However, it is
worth noting that some of the failed builds look like this:

 0:00:30 elapsed time, 0:00:08 cpu time, factor 0.29

Also, the last line that is printed is always

 ### theory "ML_Bootstrap"

so perhaps that also points to some specific problem. However, I don't
think it's anything specific to Pure, since the crash is also
reproducible with other sessions if I remember correctly (I just use
Pure because it can be built quickly).

To summarise:
- crash happens randomly in about 6% of builds of the "Pure" session
- crash seems specific to my Ryzen or at least my system
- disabling SMT makes problem go away
- crash reproducible on my Arch installation and a fresh install of
Arch, but not on Ubuntu
- RAM passes memtest without errors
- I did not experience instability with any other software
- My conjecture would be that it is somehow related to PolyML and
multithreading

I attached both the console output and the build log.

Manuel


On 04/09/17 15:12, Manuel Eberl wrote:

Alas, it would appear I have spoken too soon!

I experienced a strange build failure with RC1 yesterday and, fearing
the worst, did my experiment from a few weeks ago again, with the
following result:

– building "Pure" fails in around 6 % of the cases
– this does not change even after a cold reboot
– switching SMT off seems to make the problem go away entirely
– switching SMT on makes it reappear

Sounds very much like this might well be the Ryzen bug. AMD has started
replacing affected CPUs, so I shall enquire about that and see what happens.

Cheers,

Manuel

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Slow builds due to excessive heap images

[David Matthews]

On 03/11/2017 19:07, Makarius wrote:

On 03/11/17 19:26, Fabian Immler wrote:

I looked at it once more: profiling told me that IntInf.pow (in combination 
with Par_List.map) seems to be the culprit.

The following snippet shows similar behavior:
ML ‹
fun powers [] = []
  | powers (x::xs) = IntInf.pow (2, x mod 15)::powers xs;
Par_List.map (fn i => powers (i upto 10 * i)) (0 upto 31)
›

polyml-5.6-1/x86_64-linux: 0:00:08 elapsed time, 0:00:35 cpu time, factor 4.02
polyml-test-e8d82343b692/x86_64-linux: 0:00:36 elapsed time, 0:03:26 cpu time, 
factor 5.70
polyml-5.6-1/x86_64-darwin:  0.570s elapsed time, 1.748s cpu time, 0.000s GC 
time
polyml-test-e8d82343b692/x86_64-darwin: 522.080s elapsed time, 568.676s cpu 
time, 42.602s GC time


I have discovered the same and have now pushed a workaround:
http://isabelle.in.tum.de/repos/isabelle/rev/17eb23e43630

Somehow the IntInf.pow implementation in Poly/ML e8d82343b692 is a bit
wasteful, maybe during the bit vector operation instead of our
IntInf.divMod (_, 2) used here: see
http://isabelle.in.tum.de/repos/isabelle/annotate/17eb23e43630/src/Pure/General/integer.ML#l43


I've had a look at this and pushed a change to IntInf.pow to Poly/ML 
master (c2a2961).  It now uses Word.andb rather than IntInf.andb which 
avoids a call into the run-time system (RTS).


However, this code hadn't changed since 5.6 and when I tested it using 
List.map with 5.6 and 5.7.1 I didn't notice much difference; certainly 
not the massive differences you found with Par_List.map.  The only thing 
I can think of is that there were so many calls into the RTS that there 
was some contention on a mutex and that was causing problems.


Anyway, try the new version and let me know the results.

David

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Failure in AFP when switching from polyml-5.6-1 to polyml-test-7a7b742897e9

[David Matthews]

On 08/12/2016 15:01, Florian Haftmann wrote:

Hi all,

when testing polyml-test-7a7b742897e9 I found out that this breaks
session Algebraic_Numbers in the AFP:

*** At command "value" (line 42 of
"/mnt/home/haftmann/data/tum/afp/devel/thys/Algebraic_Numbers/Algebraic_Number_Tests.thy")
*** exception Div raised (line 302 of "./basis/InitialBasis.ML")

It looks like a change in the semantics of integer division in PolyML,
but this is entirely speculative.



No, it was a bug in the testing version of Poly/ML.  Thanks for pointing 
it out and in particular including the line number which allowed me to 
see immediately what was wrong.  Hopefully the commit I've just pushed 
will have fixed it.


David

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Proper sign of gcd / lcm on type int

[David Matthews]

On 02/06/2016 08:19, Manuel Eberl wrote:

I do think that we should enforce the same thing in the ML
implementation of gcd/lcm. Any definition of gcd/lcm for integers where
either of them may be negative does not make much sense to me. My guess
would be that lcm can be negative in the implementation you mentioned
because the author defined "lcm a b = a * b / gcd a b" with the unstated
assumption that it is only called for non-negative numbers. Or perhaps
they thought the sign does not matter.


The Poly/ML implementation was based on the idea that something called a 
"multiple" ought to follow the usual rules of multiplication; nothing 
stronger than that.  I don't think I found anything that indicated what 
the sign should be.  The GCD code uses GMP's GCD if possible; the LCM 
code is just derived from that.


I have no strong opinions on this and I'm happy to change it.  There's 
also the question of whether to add it to the IntInf structure and 
signature despite the incompatibility with the "official" library 
definition.


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

[David Matthews]

On 22/02/2016 07:58, Lars Hupel wrote:

Another possibility is to set the maximum heap size with --maxheap e.g.
ML_OPTIONS="--maxheap 28G"
If the application needs it Poly/ML will try to grow the heap to avoid
doing a lot of garbage collection.  That can result in it crowding out
other parts of the system that also need memory.  The "Unable to
increase stack" probably results from it being unable to grow an ML
stack if the application recurses very deeply.  I'm guessing that you
don't have any swap space configured so there's no leeway there.  You
may have to experiment with the setting.  You don't need --stackspace if
you set the maximum heap size.


Thanks for the hint. Indeed, there's no swap space configured, because
all the build boxes have 32 GB of RAM.

I've tried setting the --maxheap to 4 GB, but here's the error I'm getting:

   Value of --maxheap option is too large

(Relevant build log:
)


That suggests that you're running the 32-bit version of Poly/ML in which 
case the heap is limited to around 3-3.5G by the system and the problem 
you're having is the total 4G memory limit.  Switch to the 64-bit 
version as a starting point.  I was assuming that with 32G of memory you 
were running the 64-bit version already.


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

[David Matthews]

On 20/02/2016 00:08, Lars Hupel wrote:

Thanks for the suggestion. I've deployed that change on all our build
boxes. We'll see how it works out.


The problem still persists, as can be witnessed from this log:

   

This time, there are additional messages:

   Warning - Unable to increase stack - interrupting thread
   Warning - Unable to increase stack - interrupting thread
   Warning - Unable to increase stack - interrupting thread
   *** Interrupt
   Algebraic_Numbers FAILED

Oddly enough this is not reproducible. If I run just the failing sessions
on an identical build box, it works fine.


Another possibility is to set the maximum heap size with --maxheap e.g.
ML_OPTIONS="--maxheap 28G"
If the application needs it Poly/ML will try to grow the heap to avoid 
doing a lot of garbage collection.  That can result in it crowding out 
other parts of the system that also need memory.  The "Unable to 
increase stack" probably results from it being unable to grow an ML 
stack if the application recurses very deeply.  I'm guessing that you 
don't have any swap space configured so there's no leeway there.  You 
may have to experiment with the setting.  You don't need --stackspace if 
you set the maximum heap size.


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

[David Matthews]

On 17/02/2016 21:47, Dmitriy Traytel wrote:

ML> Exception- SysErr ("Cannot allocate memory", SOME ENOMEM) raised


This looks like an attempt to allocate memory for something other than 
the heap.  There are quite a few situations where this can happen.


Try adding a --stackspace argument to reserve space for thread stacks 
and anything else. e.g.

ML_OPTIONS="--stackspace 200M"
This option keeps this space back whenever Poly tries to grow the heap 
to avoid the heap using all the available memory.  You may need to 
experiment a bit with how much to reserve depending on why the memory is 
required.  It is possible that you could still get the error if there is 
some sort of loop.


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Proofs

[David Matthews]

On 13/05/2014 17:18, Makarius wrote:

On Tue, 13 May 2014, Tobias Nipkow wrote:


I added a few lemmas to List and now the HOL-Proofs session no longer
terminates. This is what I got to see when I interrupted one run:

^Cpoly(52110,0xb0185000) malloc: *** mach_vm_map(size=8388608) failed
(error code=3)
*** error: can't allocate region
*** set a breakpoint in malloc_error_break to debug
*** Interrupt
HOL-Proofs FAILED

When I load the session interactively, I don't have a problem. Any
hints what I
should be doing?


That is a Poly/ML heap allocation problem specifically on Mac OS X.
David Matthews has occasionally explained the technical side-conditions
imposed by Apple, but I did not really understand them.


On its own this is at most a warning.  If the ML application requires a 
large heap Poly/ML tries to allocate as much memory as it can.  There is 
no way to find out how much free space is left so this sometimes 
involves making allocation requests and testing the result to see if 
they have succeeded.  If a call fails Poly/ML recovers from it.  That is 
perfectly normal.  Other operating systems simply return a failure 
result in these circumstances but for some reason Apple have decided to 
print this message as well.  It typically appears in 32-bit mode when 
the maximum address space has been reached.


That, though is a separate issue from why the session does not 
terminate.  The most likely explanation is that it requires more memory 
than is available and the garbage-collector can't keep up.  I don't know 
why it should be different when you run it interactively.


I would assume that you are running in 32-bit mode.  Have you tried in 
64-bit mode with a larger heap?


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Remaining uses of Proof General?

[David Matthews]

On 08/05/2014 11:25, Makarius wrote:

On Thu, 8 May 2014, Thomas Sewell wrote:


 If I knew a proper way to reduce the priority (or to pre-empt) worker
 threads for that, I would do it.  But it probably needs some work by
 David Matthews on the ML thread infrastructure.


Preempting long-running tasks would change the tradeoffs a lot.
Another possibility would be to introduce a yield-point (cooperative
multitasking) which a task can execute, which will possibly cause its
execution to be delayed in favour of a higher priority task. Adding
that to the tactic combinators would make nearly all Isabelle
workloads much finer-grained.


That sounds rather obvious, but also like even more complication.  David
Matthews has provided a nice simplified version of pthreads in Poly/ML.
He could probably do more, but even on the more complex JVM the
influence on thread scheduling is limited.


I've had a look at providing thread priority in the Poly/ML thread 
package and I may have a go at including something.  Poly/ML leaves 
thread scheduling to the pthreads library which really means to the OS 
and what is available depends on the particular OS.  In general pthreads 
allows control over both priority and "scheduling policy".  I've done 
some tests on what various OSs allow for user (i.e. non-privileged) threads.

Linux. Does not allow either policy or priority to be changed.
Mac OS X.  Allows both policy and priority to be changed.
Cygwin/Windows.  Single scheduling policy.  Allows priority to be changed.
FreeBSD.  Allows priority but not policy to be changed.

What this means is that ML code that wants to set a thread priority is 
going to have to make some enquiries about the priority range allowed.


It looks as though adding a "yield" function would not be hard.  There's 
a question about whether you would really want to use it.  There is a 
cost involved even if there is no other thread that can be scheduled so 
you wouldn't want to call it too often.


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] PolyML crashes

[David Matthews]

Hi,
I'm aware of a number of assertion failures that seem to occur 
intermittently.  This is one of the ones on my list.  I suspect they are 
all symptoms of the same bug but I have never been able to narrow it 
down or reproduce it.  It does seem to occur when the memory management 
is under heavy load.


Thanks for reporting it and if anyone manages to reproduce it more 
consistently I would be very interested.


Regards,
David

On 20/02/2014 14:21, Ondřej Kunčar wrote:

Hi!
In the past couple of months I've gotten a crash of PolyML always with
the same error message. I cannot reproduce the problem reliably but
because it has already happened, let say, six times in the past three
months, I am reporting the problem here:

Unofficial version of Isabelle/HOL (unidentified repository version)
poly: gc_mark_phase.cpp:432: virtual void
MTGCProcessMarkPointers::ScanAddressesInObject(PolyObject*,
POLYUNSIGNED): Assertion `baseAddr > (PolyWord*)obj && baseAddr <
((PolyWord*)obj)+length' failed.


This refers to any changeset in the past three months.

Best,
Ondrej
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Pushing to AFP fails

[David Matthews]

On 18/02/2014 14:45, Andreas Lochbihler wrote:

I am trying to push a changeset to Coinductive to the AFP, but I always
get the following error message:

   remote: abort: could not lock repository /hg/p/afp/code: Permission
denied
   abort: unexpected response: empty string

Until last week, hg push used to work well. Has anything changed?

Andreas


I don't use AFP but I think it's on SourceForge.  I've been having 
similar problems committing to the Poly/ML SVN repository.  Sometimes it 
works and sometimes I get permission errors.  Apparently they are 
experiencing problems with their Allura platform.  See 
http://sourceforge.net/blog/category/sitestatus/


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle_10-Sep-2013

[David Matthews]

On 16/09/2013 11:28, Makarius wrote:

On Fri, 13 Sep 2013, Makarius wrote:


I've made my own tests with the following setup:

 Poly/ML SVN 1848
 IsaFoR a44e26d6605e
 Isabelle a49ce8d72a44
 AFP 4e87a0fc2528

 ML_PLATFORM="x86-darwin"
 ML_HOME="/Volumes/Macintosh_HD/Users/makarius/lib/polyml/polyml-svn/x86-darwin"

 ML_SYSTEM="polyml-5.5.1"
 ML_OPTIONS="--minheap 500 --gcthreads 4 --debug=sharing"



If you say that we can just absorb an exception Fail "Insufficient
memory" in ML, we can do that on the Isabelle/ML side as a workaround.


Trying PolyML.shareCommonData PolyML.rootFunction with some exception
handling, there is another breakdown with PolyML.SaveState.saveState:

   Assertion failed: (space != 0), function ScanAddressAt, file
exporter.cpp, line 187.


It's possible the recovery from insufficient memory is not completely 
correct.  I'm on the point of releasing 5.5.1 so I'd rather not make any 
changes just now which might break something else.  Perhaps just now it 
might be better not to handle the exception.


David

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle_10-Sep-2013

[David Matthews]

On 13/09/2013 11:08, René Thiemann wrote:

I would suggest trying with the --stackspace option e.g.
ML_OPTIONS='--stackspace 500'
The Fail exception with "Insufficient space" arises in a number of places such 
as when trying to fork a thread.  This requires memory outside the ML heap.  The 
stackspace option keeps some space free from the ML heap for these purposes.


I tried it, but the setting was not high enough: then even earlier sessions 
crash with a new
'Run out of store - interrupting threads' error message. This also happens if I 
set stackspace to 1500,
but it succeeded with 5000. However, then still afterwards I get the usual

poly(6820,0xb09a5000) malloc: *** mmap(size=16777216) failed (error code=12)
*** error: can't allocate region

error as before, if I use minheap=1000, or drop the minheap parameter.


I would guess that this is when running the X86/32 version rather than X86/64.


Yes, I use the 32-bit mode. I will later run some tests when using the 64-bit 
mode.

Here is my current setup:

ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86-darwin"
ML_HOME="/Users/rene/.isabelle/contrib/polyml-5.5.0-3/x86-darwin"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="--minheap 1000 --stackspace 5000"



You definitely don't want a value as large as 5000.

I think the exception may be occurring with PolyML.shareCommonData. 
This needs memory outside the heap to hold some tables.  If there is a 
lot of live data in the heap these tables can be large and if the heap 
is taking up most or all of the available virtual memory, a particular 
problem in 32-bit mode, you may get the above message and exception.  Is 
that possible in this case?  It is safe to handle the exception and 
continue; it's just that the sharing process will not be complete so 
that the heap will be bigger than it might otherwise be.


Regards,
David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle_10-Sep-2013

[David Matthews]

On 12/09/2013 19:25, Makarius wrote:

On Thu, 12 Sep 2013, René Thiemann wrote:


I noticed that on my machines I often get an "Insufficient memory" error.

Building Check-DPP ...
poly(59646,0xacc9fa28) malloc: *** mmap(size=134217728) failed (error
code=12)
*** error: can't allocate region
*** set a breakpoint in malloc_error_break to debug
Fail "Insufficient memory":
/Users/rene/.isabelle/Isabelle_10-Sep-2013/heaps/polyml-5.5.0_x86-darwin/Check-DPP

Check-DPP FAILED

To be more precise, when using

ML_OPTIONS="--minheap 1000"

I did not get the error under Isabelle2013, but under
Isabelle_10-Sep-2013, it often fails with setting. Fortunately, using

ML_OPTIONS="--minheap 3000"

mostly works, but it is still annoying, since with this setting, I
cannot start two Isabelle sessions in parallel. Does someone else
notice increased memory consumption / crashes?


There is definitely some continous bloat factor with every new release,
although David Matthews was usually ahead of most big applications in
recent years.  In fact he is about to release Poly/ML 5.5.1 pretty soon,
so a quick test with some repository version of Poly/ML might help (e.g.
SVN 1843).


I would suggest trying with the --stackspace option e.g.
ML_OPTIONS='--stackspace 500'
The Fail exception with "Insufficient space" arises in a number of 
places such as when trying to fork a thread.  This requires memory 
outside the ML heap.  The stackspace option keeps some space free from 
the ML heap for these purposes.


I would guess that this is when running the X86/32 version rather than 
X86/64.  Is that correct?


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Segmentation faults

[David Matthews]

From that crash log it looks as though the crash happened in ML code 
rather than the run-time system itself.  The source of the crash, 
though, could be a bug in the run-time system resulting in some 
addresses being mangled.  It's difficult to say more without being able 
to reproduce it.


David

On 29/05/2013 14:03, Lawrence Paulson wrote:

Following Dave Matthew's instructions, I downloaded a fresh copy of
the sources and executed the following commands. Except the first one
failed, presumably because I had a fresh copy.

make distclean ./configure --disable-shared make make install

I have just taken a look at the crash logs, and it's clear that some
dynamic libraries from a previous installation had got loaded along
with the latest ones. Maybe that was the problem. I wonder how they
got loaded in the first place? I have just deleted them and I hope it
will work now.

Larry

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Segmentation faults

[David Matthews]

On 11/05/2013 12:21, Tjark Weber wrote:

On Thu, 2013-05-02 at 16:18 +0100, Lawrence Paulson wrote:

I am getting a lot of poly/ML segmentation faults, and they are making
it very difficult to do my work, especially as my theories take at
least 15 minutes to load. If it then simply crashes then I'm not
getting anywhere.

Has anybody else had this problem with Poly/ML?


Since nobody else replied: I do get occasional segfaults from Poly/ML
(not only running Isabelle, but also other ML code). David Matthews is
usually quite responsive to bug reports.


That's interesting.  Is there any way to establish a pattern to this? 
Does it happen with particular hardware/operating system?  It's almost 
impossible to debug problems like this unless there's some way I can 
reproduce them.


I notice you said you run "other ML code" since Larry also has both 
Isabelle and the Poly/ML distribution installed.  I had wondered if 
there could be some conflict; in particular the Isabelle version could 
be picking up the shared library from the Poly/ML distribution instead 
of its own.  The reverse is unlikely.


Anyway the more information I have the more likely I can do something.

David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Max threads & Sledgehammer

[David Matthews]

On 07/01/2013 17:49, Stefan Berghofer wrote:

You could certainly hit limits on memory for stacks with a large
number of threads particularly if the default stack size is large.
What does "ulimit -s" say?  You could try setting that smaller.


"ulimit -s" says 102400


This is surprisingly large.  That works out at 100Mbytes per thread, 
assuming that this is "k" as on my Debian machines.  My machines show 
8192 here.  Poly/ML needs only a small space on the C stack so maybe it 
should set the stack size explicitly when the threads are created.


David

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Max threads & Sledgehammer

[David Matthews]

On 07/01/2013 11:24, Makarius wrote:

On Mon, 7 Jan 2013, Stefan Berghofer wrote:


it's a server with 24 CPUs of the type "Intel(R) Xeon(R) CPU E7450 @
2.40GHz" and 132299948 kB RAM.


What could happen here nonetheless is that Poly/ML tries to fork too
many GC threads.


This was indeed the problem.


So how many cores do you have?  I reckon it should work until 32 at
the least.


Well, obviously not :-(


Intel has hyperthreading, so it will report 48 CPUs here, or do you have
12 cores that are reported as 24?  Anyway, we should tell David Matthews
about it as well -- he could restrict his GC threads in a similar manner
as Isabelle/ML does for the worker thread farm.


What does Thread.Thread.numProcessors() report?  That's the number that 
will be used for the GC threads.


I'm not inclined to put an arbitrary limit on the number of threads. 
There are certain parts of the GC process such as the sharing detection 
that can use as much parallelism as there is available.  Other parts 
seem to max out at only a few processors.  I'll bear this in mind.  The 
parallel GC is very new and we need some experience of how it works out 
in practice and whether it needs some tuning.


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Max threads & Sledgehammer

[David Matthews]

On 07/01/2013 10:11, Stefan Berghofer wrote:

On 01/07/2013 10:45 AM, Makarius wrote:

On Fri, 4 Jan 2013, Stefan Berghofer wrote:


I am currently getting an exception Thread "Thread creation failed"
after some time when compiling HOL with PolyML 5.5.0 on a machine
with quite a few CPUs (I am using Isabelle repository version
30bcdd5c8e78). I have the impression that Isabelle just tries to
create as many threads as there are CPUs, which exceeds the maximum
number of threads allowed by the operating system for a single process.



it's a server with 24 CPUs of the type "Intel(R) Xeon(R) CPU E7450 @
2.40GHz" and 132299948 kB RAM.
The operating system is "Linux ts-2 3.2.0-0.bpo.4-amd64 #1 SMP Debian
3.2.35-2~bpo60+1 x86_64 GNU/Linux".



What could happen here nonetheless is that Poly/ML tries to fork too
many GC threads.


This was indeed the problem.


So how many cores do you have?  I reckon it should work until 32 at
the least.


Well, obviously not :-(


You could try ML_OPTIONS="--gcthreads 8" in one of your settings.


I tried it successfully with "--gcthreads 4", which looks like a
reasonable value that is also used in
some of the Admin/isatest/settings files.


Is there a limit on the number of threads per process in Linux?  I 
haven't been able to find anything about it.  You could certainly hit 
limits on memory for stacks with a large number of threads particularly 
if the default stack size is large.  What does "ulimit -s" say?  You 
could try setting that smaller.


By default without the --gcthreads option Poly/ML 5.5 creates one 
garbage collection thread for each processor.  That's probably more than 
are useful if you have 24 processors so -gcthreads 4 or 8 might well be 
a sensible setting.


David

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Library/List_Prefix

[David Matthews]

On 31/08/2012 05:21, Christian Sternagel wrote:

On 08/31/2012 12:44 PM, Gerwin Klein wrote:


On 31/08/2012, at 1:25 PM, Christian Sternagel 
wrote:


Well, it almost worked now ;).

even without -b all my memory was wasted and just as swapping started
in earnest I got an error message, i.e., I have to adapt JinjaThreads
to some previous changes.

Still, I am nowhere close to the 3-4 GB RAM usage that seem to be
possible. Maybe the reason is that I'm on x86_64?


Yes, that'll be it. Memory usage on x86_64 is almost twice that of the
32bit version (which makes sense if you think about it).

Now that you mention it ... ;)

With TypeComp adapted (only minor changes) JinjaThread succeeded while
using 6-8 GB RAM (which magically corresponds to the 3-4 GB on an i386 ;)).


If you're using Poly/ML 5.5 from SVN it could well be worth setting the 
maximum heap size to about 80% of the available memory e.g.

--maxheap 7G
Basically, choose the largest value that will avoid swapping on your 
machine with whatever else you have running.  Commit 1579 has reduced 
the default maximum (without any --maxheap option) from 100% of the 
memory to 80%.


The new heap sizer in 5.5 will detect swapping and reduce the heap 
accordingly but it cannot know exactly how much memory is required by 
the operating system and anything else you are running so it requires 
some swapping activity to know it is at the limit.


The experiments Makarius and I were doing on x86_32 were on machines 
that had at least 4G of real memory so swapping was not an issue.  The 
limit was imposed by the address length and/or the operating system. 
Effectively the OS was setting a value for --maxheap below the memory size.


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle/jEdit: Feature Requests for Ctrl-Click

[David Matthews]

Just to add that I'm very grateful for this support which enables 
Poly/ML to continue and get better with each release since I don't have 
a university or a big company behind me.


If anyone has a feature that requires work on Poly/ML and a bit of money 
I'm happy to discuss it.


David

On 27/08/2012 20:27, Lawrence Paulson wrote:

Various projects of mine, going back many years, have supported
Poly/ML at the rate of £1000 per year. (That's just under €1300.)
This is a much better use of grant money than to give it to already
wealthy publishers for the sake of so-called Gold open access.

Larry

On 27 Aug 2012, at 16:18, Tobias Nipkow  wrote:


Just for the record: I have spent over 20k EUR to this over the
past 1 1/2 years but that will have to be it from the TUM side.


___ isabelle-dev mailing
list isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] isabelle build

[David Matthews]

On 08/08/2012 09:54, David Matthews wrote:

Actually, one has to be careful when interpreting the parallelism
figures.  Much of the time an ML application is memory-bound which means
that using more processors can make an improvement in overall run-time
but the overall CPU usage will grow.  As far as I can tell, the time
that a processor spends waiting for memory counts as its CPU time unlike
when it is waiting for IO.


Just in case that wasn't clear from the context, by "memory-bound" I 
meant limited by the bandwidth between main memory and the processors.


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] isabelle build

[David Matthews]

The garbage collector now includes a pass that looks for cells that have 
the same contents and merges them using the principle that equality in 
ML cannot distinguish between two pointers to the same cell or two cells 
with the same contents.  There has been a PolyML.shareCommonData 
function for a long time that does this but that has always had to be 
called explicitly by the user.  It has also required quite a lot of 
extra memory.  Currently, I understand Isabelle uses it just before it 
saves the state to reduce the sizes of saved state files.


Some time ago Makarius wondered if it was possible to have this invoked 
as part of the GC.  I couldn't see how to do this especially without 
adding any extra memory overhead but gradually I've been improving it. 
The heap sizing code now fires off this pass when memory is particularly 
short since it costs several times the cost of a normal GC.  The latest 
improvement was to find a way to merge deep structures (lists and trees) 
something that PolyML.shareCommonData has always done but at the cost of 
the extra memory.  This made a dramatic difference to JinjaThreads.  It 
appears that it creates many equal data structures and merging these can 
reduce the live data size by some 80%.


Actually, one has to be careful when interpreting the parallelism 
figures.  Much of the time an ML application is memory-bound which means 
that using more processors can make an improvement in overall run-time 
but the overall CPU usage will grow.  As far as I can tell, the time 
that a processor spends waiting for memory counts as its CPU time unlike 
when it is waiting for IO.


David

On 08/08/2012 09:00, Lawrence Paulson wrote:

I understand about the parallelism, but what has cut back on the memory 
consumption?
Larry

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] isabelle build

[David Matthews]

On 06/08/2012 14:01, Makarius wrote:

Just as a teaser, this is what can be done with recent Isabelle + Poly/ML:

   Isabelle/90e5093c3e1c
   AFP/c7ea6a0ad609
   Poly/ML SVN 1569
The best runs of JinjaThreads in isolation are:

Finished JinjaThreads (0:20:31 elapsed time, 2:00:34 cpu time, factor
5.87) # 8/8 threads, 16 GB
Finished JinjaThreads (0:18:57 elapsed time, 1:58:27 cpu time, factor
6.25) # 8/8 threads, 24 GB


Just to add that JinjaThreads runs quite happily in a relatively small 
amount of memory with the latest SVN version of Poly/ML.  6-8 Gbytes are 
fine.  Even in 32-bit mode it takes around 33 minutes.



Special wizardry was performed by David Matthews in the Poly/ML runtime
system in the past 12 months.


I'm looking towards releasing this version of Poly/ML in the next few 
months and I would like to give it as much testing as possible.  I'd 
encourage people to try it out and let me know particularly if there are 
bugs or if things run significantly slower than before.


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Using PolyML's memory consumption profiling on Isabelle

[David Matthews]

On 14/10/2011 10:56, Makarius wrote:

On Fri, 14 Oct 2011, Andreas Schropp wrote:

val dummy_task = Task(NONE, ~1)

Values are not shared?! What the hell?


Datatypes and tuples that contain only constant data are created once 
during compilation.



This looks like an older version. Thomas was referring to this one in
Isabelle/73dde8006820:

fun dummy_task () =
Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing =
new_timing ()};

Since the timing is a mutable variable here, it has to be created afresh
for each use -- in Future.value construction. Normally 1 million extra
allocations are not a big deal, but an experiment from yesterday shows
that there is in fact a measurable impact. See now Isabelle/2afb928c71ca
and the corresponding charts at
http://www4.in.tum.de/~wenzelm/test/stats/at-poly.html

I can only guess that allocation of mutable stuff costs extra.


Allocation of a mutable, at least a fixed-size mutable such as ref, 
doesn't cost any more than allocating an immutable.  However, if a 
mutable survives a GC it has an impact on subsequent GCs.  The worst 
case would be a mutable that survived one GC and then becomes 
unreachable.  It would continue to be scanned in every partial GC until 
it was thrown away by the next full GC.  Does this correspond with what 
you've found?


Regards,
David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Using PolyML's memory consumption profiling on Isabelle

[David Matthews]

On 14/10/2011 09:13, Andreas Schropp wrote:

On 10/13/2011 01:24 PM, Thomas Sewell wrote:

Good day all. Just wanted to let the Isabelle developers know about
the latest feature David Matthews has added to PolyML, and to let you
all know how useful it is.

The feature allows profiling of objects after garbage collection. When
code is compiled with PolyML.compiler.allocationProfiling set to 1,
all objects allocated are also given a pointer to their allocating
function. When the garbage collector runs with
PolyML.compiler.profiling set to 4, a statistical trace is printed of
which objects survived garbage collection.


Cool.

So we have:
profiling = 1 approximates runtime Monte-Carlo style sampling of the
program counter
profiling = 2 records the number of words allocated in each function
(very accurate IIRC)
profiling = 3 ???
profiling = 4 counts GC survivors (very accurately?)


Profiling 3 is the number of cases where the run-time system had to 
emulate an arithmetic operation because the operation required 
long-precision arithmetic.  This is a LOT more expensive than doing the 
arithmetic with short precision ints so it may be worth recoding 
hot-spots that show up with this.


Profiling 4 has just been added so it probably has teething-troubles.

I would really prefer to replace these numbers by a datatype so that 
users don't have to remember numbers.


Regards,
David

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: status (AFP)

[David Matthews]

On 14/10/2011 10:02, Makarius wrote:

On Fri, 14 Oct 2011, Gerwin Klein wrote:


Is anyone else observing intermittent problems like this?

Building Jinja ...
poly: scanaddrs.cpp:107: PolyWord
ScanAddress::ScanStackAddress(PolyWord, StackObject*, bool): Assertion
`val.IsDataPtr()' failed.
/home/kleing/volatile/isadist/Isabelle_13-Oct-2011/lib/scripts/run-polyml:
line 77: 20095 Aborted "$POLY" -q $ML_OPTIONS
Jinja FAILED


Yes, occasionally. Such hard crashes were more frequent in the past, and
we are running much more and bigger jobs now.


I pointed out in an email to Gerwin that this looks very like the bug 
that was fixed in commit 1297 in Poly/ML head and 1318 in the fixes 
branch.  Which version of Poly/ML was this?  It is possible that this 
could be the result of a different bug in which case I will need to look 
more closely.


Regards,
David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Multicore performance preview

[David Matthews]

Makarius wrote:
> On Tue, 21 Oct 2008, Stefan Berghofer wrote:
> 
>> Makarius wrote:
>>> You will need the latest Poly/ML 5.2.1 version to prevent a strange GC 
>>> deadlock problem in 5.1/5.2.
>> Where can I get the latest version? The latest version offered for download
>> on the Sourceforge page
>>
>>   
>> http://sourceforge.net/project/showfiles.php?group_id=148318&package_id=163589
>>
>> is still 5.2
> 
> You are right, 5.2.1 has not been published yet.  The present CVS version 
> is more or less at the same state, see e.g. our /home/polyml/polyml-cvs/.

Makarius was being slightly premature by announcing it yesterday. 
Poly/ML 5.2.1 has now been released and you should find it on 
SourceForge.  It's nice to see the speed-ups, though.

David