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

[Lars Hupel]

> 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.

No, I initially planned to, but Makarius usually advises against it. I'm
not sure how to proceed here.

Cheers
Lars
___
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

[Lars Hupel]

> 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:
)

Cheers
Lars

___
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

[Lars Hupel]

>> 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.
>
> 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.


Cheers
Lars
___
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

[Lars Hupel]

> 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.

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

Cheers
Lars
___
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] Formula_Derivatives FAILED: Cannot allocate memory

[Lars Hupel]

> yes, I also saw this on testboard and was confused.

I'm at a loss, too. Maybe Makarius can give some hints on what the cause
could possibly be. I could increase the heap space even more, but not
sure if that is a good idea.

Cheers
Lars
___
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

[Lars Hupel]

> The obvious explanation is a failing proof which keeps using up more and more 
> memory.

Wouldn't that be deterministic, then? It only fails spuriously.
___
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

[Dmitriy Traytel]

Hi Lars,

yes, I also saw this on testboard and was confused.

On my (low-end 2 core) machine (isabelle/e4e09a6e3922, afp/123d7cbae549):

~/repos/nonprim-corec/paper$ isabelle build -vd '$AFP' Formula_Derivatives
ISABELLE_BUILD_OPTIONS="threads=4 parallel_proofs=2"

ISABELLE_BUILD_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss4m"

ML_PLATFORM="x86-darwin"
ML_HOME="/Users/traytel/.isabelle/contrib/polyml-5.6-1/x86-darwin"
ML_SYSTEM="polyml-5.6"
ML_OPTIONS="-H 500”

[...]

Running Formula_Derivatives …

[...]

Timing Formula_Derivatives (4 threads, 269.115s elapsed time, 708.123s cpu 
time, 222.858s GC time, factor 2.63)
Finished Formula_Derivatives (0:04:34 elapsed time, 0:11:53 cpu time, factor 
2.60)

Dmitriy

> On 17 Feb 2016, at 22:22, Lars Hupel  wrote:
> 
> Despite increasing the ML heap size with "-H 2000", the session
> "Formula_Derivatives" is failing. The build VMs have 32 GB of RAM, so
> that shouldn't be a problem. Here are the relevant environment variables:
> 
> ML_PLATFORM="x86-linux"
> ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86-linux"
> ML_SYSTEM="polyml-5.6"
> ML_OPTIONS="-H 2000"
> 
> What strikes me as odd is that it's always the same session.
> 
> 
> 
> Formula_Derivatives FAILED
> (see also
> /media/data/jenkins/.isabelle/heaps/polyml-5.6_x86-linux/log/Formula_Derivatives)
> 
>  sig
>val check_eqv:
>   WS1S.idx ->
> WS1S.nat ->
>   ((WS1S.nat, WS1S.nat) WS1S.atomic, WS1S.orderb) WS1S.aformula ->
> (Presb.presb, unit) WS1S.aformula -> bool
>type 'a set
>  end
> ### theory "WS1S_Presburger_Equivalence"
> ### 11.322s elapsed time, 30.652s cpu time, 4.624s GC time
> ### Ignoring duplicate rewrite rule:
> ### find0 SO ?vr (Eq_Const ?v ?va ?vb) \ False
> ### Ignoring duplicate rewrite rule:
> ### find0 SO ?vr (Less ?v ?va ?vb) \ False
> ### Ignoring duplicate rewrite rule:
> ### find0 SO ?vr (Plus_FO ?v ?va ?vb ?vc) \ False
> ### Ignoring duplicate rewrite rule:
> ### find0 SO ?vr (Eq_FO ?v ?va ?vb) \ False
> val it = (): unit
> ML> Exception- SysErr ("Cannot allocate memory", SOME ENOMEM) raised
> ___
> 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

[isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

[Lars Hupel]

Despite increasing the ML heap size with "-H 2000", the session
"Formula_Derivatives" is failing. The build VMs have 32 GB of RAM, so
that shouldn't be a problem. Here are the relevant environment variables:

ML_PLATFORM="x86-linux"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86-linux"
ML_SYSTEM="polyml-5.6"
ML_OPTIONS="-H 2000"

What strikes me as odd is that it's always the same session.



Formula_Derivatives FAILED
(see also
/media/data/jenkins/.isabelle/heaps/polyml-5.6_x86-linux/log/Formula_Derivatives)

  sig
val check_eqv:
   WS1S.idx ->
 WS1S.nat ->
   ((WS1S.nat, WS1S.nat) WS1S.atomic, WS1S.orderb) WS1S.aformula ->
 (Presb.presb, unit) WS1S.aformula -> bool
type 'a set
  end
### theory "WS1S_Presburger_Equivalence"
### 11.322s elapsed time, 30.652s cpu time, 4.624s GC time
### Ignoring duplicate rewrite rule:
### find0 SO ?vr (Eq_Const ?v ?va ?vb) \ False
### Ignoring duplicate rewrite rule:
### find0 SO ?vr (Less ?v ?va ?vb) \ False
### Ignoring duplicate rewrite rule:
### find0 SO ?vr (Plus_FO ?v ?va ?vb ?vc) \ False
### Ignoring duplicate rewrite rule:
### find0 SO ?vr (Eq_FO ?v ?va ?vb) \ False
val it = (): unit
ML> Exception- SysErr ("Cannot allocate memory", SOME ENOMEM) raised
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev