Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" me...


view this post on Zulip Email Gateway (Jan 05 2021 at 23:29):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I am running Isabelle2021-RC1 under Ubuntu 20.04. Is there any way to limit the memory use
of the "veriT" prover? It seems not to be a very good citizen in this respect: when it is
run from the "try" command it seems willing to grow its address space even to significantly
exceed the total amount of system RAM. For example, I just observed a virtual address space
of 37.8GB on a system with 32GB total RAM and of course Java, poly, and various other things
were also running, so this is unsupportable. When this occurs, the system is sent into a
thrashing mode, from which it is difficult even to get back control of the desktop so that
the offending process can be identified and killed. So some ability to impose a limit is
needed here.

view this post on Zulip Email Gateway (Jan 06 2021 at 08:30):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Eugene,

I never use "try", so I need some more information:

If the trashing is not too hard to reproduce:

at the top of the file?

at the top of the file?

Thanks,

Mathias

view this post on Zulip Email Gateway (Jan 06 2021 at 11:03):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
On 1/6/21 3:29 AM, Mathias Fleury wrote:

Hi Eugene,

I never use "try", so I need some more information:

I am not sure that I understand this question. Threads share a single address space, so the amount of memory used
is not a property of a single thread, but of a process. If you are asking about processes, then it was one veriT
process. I did not check how many threads were part of that process.

It is not easy for me to supply any kind of simple theory with straightforward instructions for reproducing,
but the next time it happens I will see if I can reproduce by using the same "try" in the same context.

Again, I don't know what you mean by "real memory usage". Unless a program uses some tricks such as sparse
address spaces (which can be useful in some kind of in-memory database situations), the virtual memory will be the
sum of the code, data, heap and stack sizes. Code and read-only data can be shared between processes, but this is
not an issue here because there is only one veriT process, and I don't think any shared libraries used would be
contributing to the issue. The usage in question is almost certainly dynamic memory usage; i.e. heap.

Linux utilities such as "top" and "ps" do report "virtual size" and "resident-set size". The resident-set size
would be the amount of actual RAM currently in use by the process. This number is obviously limited by the
amount of installed RAM and once it reaches a certain level there can essentially not be any further increases,
though the size of the virtual address space can continue to increase if there is available swap.
In the case of the example I cited, the RSS reached about 26GB, which took up enough of the system RAM so that
there was severe thrashing.

If the trashing is not too hard to reproduce:

at the top of the file?

at the top of the file?

I can try this, but do not know if/when I will be able to report on results, since the situation is not
deterministically reproducible at this time.

Thanks,

Mathias

On 06/01/2021 00:28, Eugene W. Stark wrote:

I am running Isabelle2021-RC1 under Ubuntu 20.04. Is there any way to limit the memory use
of the "veriT" prover? It seems not to be a very good citizen in this respect: when it is
run from the "try" command it seems willing to grow its address space even to significantly
exceed the total amount of system RAM. For example, I just observed a virtual address space
of 37.8GB on a system with 32GB total RAM and of course Java, poly, and various other things
were also running, so this is unsupportable. When this occurs, the system is sent into a
thrashing mode, from which it is difficult even to get back control of the desktop so that
the offending process can be identified and killed. So some ability to impose a limit is
needed here.

view this post on Zulip Email Gateway (Jan 10 2021 at 20:56):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
One additional data point: The excessive memory consumption issue is not limited to sledgehammer --
it can occur even when there is simply a use in an Isar proof of smt that specifies "verit".
The problem does not occur with proofs that already succeed in a short period of time; it happens when
you invalidate some portion of the proof by editing, so that the particular smt proof doesn't work
any more. This means that you can spam your whole session (if not your whole computer) if you happen
to make some changes that trigger uncontrolled memory use by veriT in subsequent proofs that
used to work before you made the changes.

This is very much making me want a way to limit the memory use, otherwise I have to figure out how to
disable veriT completely.

view this post on Zulip Email Gateway (Jan 11 2021 at 07:28):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Eugene,

I believe that there are two different problems here:

  1. tactics running forever and using a lot of memory. This already
    happens with metis or blast. However, this behavior might be new for
    smt, because the smt_timeout was disabled
    (http://isabelle.in.tum.de/repos/isabelle/rev/478b7599a1a0) and smt
    solver are a lot more powerful than metis/blast. This is not
    specific to veriT and can happen with Z3 too.

    *  Solution: Set the smt_timeout to some reasonable value.

  2. the Sledgehammer problem that I cannot reproduce. It is hard to know
    what is really happening here, because I would not be surprised that
    the problem is actually the opposite: Isabelle uses tons of memory
    and is not able to kill veriT within the timeout and, therefore,
    veriT has a lot more time to use memory.

The motivation for 1 is avoiding timeouts that are hardware dependent
(e.g., if you run things on a raspberry pi).

For 2, can you give me the ouput of the sledgehammer_params command?

Mathias

view this post on Zulip Email Gateway (Jan 11 2021 at 13:53):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Metis and blast run in ML, so are limited by the size of the ML heap. Poly accepts a parameter that allows
you to limit the size of the ML heap. Similarly, Java accepts a parameter that allows you to limit the size
of its heap. The problem here is that now there are additional processes getting fired off that can consume
memory voraciously, and there is no way to limit it. There is only a certain amount of RAM on the system,
and if each process uses as much as it wants with no limitation, then the RAM will become overcommitted and
the system unstable. It would be best if there were a single limit to the total amount of memory used by
all Isabelle-related processes, but that is a more complex thing to implement and a fallback is to make it
possible to place limits on the less-essential tools (e.g. smt solvers) that can cause trouble.

view this post on Zulip Email Gateway (Jan 14 2021 at 06:24):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Eugene,

On 11/01/2021 14:52, Eugene W. Stark wrote:

Default parameters for Sledgehammer:
...
provers = cvc4 vampire z3 e

This indicates that veriT is not called by Sledgehammer as a prover
backend. So problem 2 does not exist for you.

Metis and blast run in ML, so are limited by the size of the ML heap. Poly accepts a parameter that allows
you to limit the size of the ML heap. Similarly, Java accepts a parameter that allows you to limit the size
of its heap. The problem here is that now there are additional processes getting fired off that can consume
memory voraciously, and there is no way to limit it. There is only a certain amount of RAM on the system,
and if each process uses as much as it wants with no limitation, then the RAM will become overcommitted and
the system unstable. It would be best if there were a single limit to the total amount of memory used by
all Isabelle-related processes, but that is a more complex thing to implement and a fallback is to make it
possible to place limits on the less-essential tools (e.g. smt solvers) that can cause trouble.

You never have to use smt in your development (that might cripple
Sledgehammer however).

Anyway, unless you find a way to replicate the issue, I believe that
setting the smt_timeout solves the problem and that no change is
required in Isabelle.

Thanks for the report,

Mathias

On 1/11/21 2:28 AM, Mathias Fleury wrote:

Hi Eugene,

I believe that there are two different problems here:

1. tactics running forever and using a lot of memory. This already happens with metis or blast. However, this behavior
might be new for smt, because the smt_timeout was disabled
(http://isabelle.in.tum.de/repos/isabelle/rev/478b7599a1a0) and smt solver are a lot more powerful than metis/blast.
This is not specific to veriT and can happen with Z3 too.
*  Solution: Set the smt_timeout to some reasonable value.

2. the Sledgehammer problem that I cannot reproduce. It is hard to know what is really happening here, because I would
not be surprised that the problem is actually the opposite: Isabelle uses tons of memory and is not able to kill
veriT within the timeout and, therefore, veriT has a lot more time to use memory.

The motivation for 1 is avoiding timeouts that are hardware dependent (e.g., if you run things on a raspberry pi).

For 2, can you give me the ouput of the sledgehammer_params command?

Mathias

On 10/01/2021 21:56, Eugene W. Stark wrote:

One additional data point: The excessive memory consumption issue is not limited to sledgehammer --
it can occur even when there is simply a use in an Isar proof of smt that specifies "verit".
The problem does not occur with proofs that already succeed in a short period of time; it happens when
you invalidate some portion of the proof by editing, so that the particular smt proof doesn't work
any more. This means that you can spam your whole session (if not your whole computer) if you happen
to make some changes that trigger uncontrolled memory use by veriT in subsequent proofs that
used to work before you made the changes.

This is very much making me want a way to limit the memory use, otherwise I have to figure out how to
disable veriT completely.

On 1/6/21 6:03 AM, Eugene W. Stark wrote:

On 1/6/21 3:29 AM, Mathias Fleury wrote:

Hi Eugene,

I never use "try", so I need some more information:

  • Are you talking about one veriT thread  that used so much memory or more than one veriT thread?
    I am not sure that I understand this question. Threads share a single address space, so the amount of memory used
    is not a property of a single thread, but of a process. If you are asking about processes, then it was one veriT
    process. I did not check how many threads were part of that process.
  • on what theory was this? I would like to reproduce that.
    It is not easy for me to supply any kind of simple theory with straightforward instructions for reproducing,
    but the next time it happens I will see if I can reproduce by using the same "try" in the same context.
  • What was the real memory usage? Virtual memory is pretty meaningless: I have a program that has a virtual memory usage
    of 256G but uses only 9M...

Again, I don't know what you mean by "real memory usage". Unless a program uses some tricks such as sparse
address spaces (which can be useful in some kind of in-memory database situations), the virtual memory will be the
sum of the code, data, heap and stack sizes. Code and read-only data can be shared between processes, but this is
not an issue here because there is only one veriT process, and I don't think any shared libraries used would be
contributing to the issue. The usage in question is almost certainly dynamic memory usage; i.e. heap.

Linux utilities such as "top" and "ps" do report "virtual size" and "resident-set size". The resident-set size
would be the amount of actual RAM currently in use by the process. This number is obviously limited by the
amount of installed RAM and once it reaches a certain level there can essentially not be any further increases,
though the size of the virtual address space can continue to increase if there is available swap.
In the case of the example I cited, the RSS reached about 26GB, which took up enough of the system RAM so that
there was severe thrashing.

If the trashing is not too hard to reproduce:

  • Does it still happen if you deactivate veriT in sledgehammer by adding:

    ML ‹
    fun verit_rm_stgy f stgy thy =
      let
        val ctxt' = f (Proof_Context.init_global thy);
        val thy' = Proof_Context.theory_of ctxt';
      in Context.theory_map (Verit_Proof.verit_rm_stgy stgy) thy' end;

    setup ‹fold (verit_rm_stgy (fn x=> x)) ["del_insts", "ccfv_SIG", "ccfv_threshold", "default", "best"]›

    ML ‹Verit_Proof.all_veriT_stgies (Context.Proof @{context})›
    (should print: val it = []: string list)

at the top of the file?

  • If the previous point works, does it still happen if you deactivate all but one veriT strategy in sledgehammer, by adding:

    ML ‹
    fun verit_rm_stgy f stgy thy =
      let
        val ctxt' = f (Proof_Context.init_global thy);
        val thy' = Proof_Context.theory_of ctxt';
      in Context.theory_map (Verit_Proof.verit_rm_stgy stgy) thy' end;

    setup ‹fold (verit_rm_stgy (fn x=> x)) ["del_insts", "ccfv_SIG", "ccfv_threshold", "default"]›

    ML ‹Verit_Proof.all_veriT_stgies (Context.Proof @{context})›
    (should print: val it = ["best"]: string list)

at the top of the file?
I can try this, but do not know if/when I will be able to report on results, since the situation is not
deterministically reproducible at this time.

Thanks,

Mathias

On 06/01/2021 00:28, Eugene W. Stark wrote:

I am running Isabelle2021-RC1 under Ubuntu 20.04. Is there any way to limit the memory use
of the "veriT" prover? It seems not to be a very good citizen in this respect: when it is
run from the "try" command it seems willing to grow its address space even to significantly
exceed the total amount of system RAM. For example, I just observed a virtual address space
of 37.8GB on a system with 32GB total RAM and of course Java, poly, and various other things
were also running, so this is unsupportable. When this occurs, the system is sent into a
thrashing mode, from which it is difficult even to get back control of the desktop so that
the offending process can be identified and killed. So some ability to impose a limit is
needed here.

view this post on Zulip Email Gateway (Jan 14 2021 at 16:28):

From: Thomas Sewell <tals4@cam.ac.uk>
I think it might be worth mentioning that there are good ways to set
resource limits on processes in any given OS. I've got consistent
results
from ulimit on linux in the past (in a non-Isabelle project that run
thousands of SMT queries). It might be possible to add such limits to
the veriT tasks as they're created, if necessary by wrapping the veriT
binary in a script.

Best regards,
Thomas.

view this post on Zulip Email Gateway (Jan 27 2021 at 20:55):

From: Makarius <makarius@sketis.net>
This does not sound very portable: Would this work on Windows (with or without
Cygwin)?

Makarius

view this post on Zulip Email Gateway (Jan 27 2021 at 20:59):

From: Makarius <makarius@sketis.net>
On 11/01/2021 08:28, Mathias Fleury wrote:

I believe that there are two different problems here:

  1. tactics running forever and using a lot of memory. This already happens
    with metis or blast. However, this behavior might be new for smt, because
    the smt_timeout was disabled
    (http://isabelle.in.tum.de/repos/isabelle/rev/478b7599a1a0) and smt solver
    are a lot more powerful than metis/blast. This is not specific to veriT
    and can happen with Z3 too.
    *  Solution: Set the smt_timeout to some reasonable value.

The quoted changeset says:

changeset: 72347:478b7599a1a0
parent: 72342:4195e75a92ef
user: desharna

view this post on Zulip Email Gateway (Jan 27 2021 at 21:24):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I don't have anything further to add. I reported what I observed and what my opinion was about it.

view this post on Zulip Email Gateway (Jan 28 2021 at 12:31):

From: Thomas Sewell <tals4@cam.ac.uk>
It's likely there's a Windows feature similar to ulimit, but I
have no idea what it might be. I quickly checked whether python's
setrlimit was considered "portable", and it doesn't appear to be
the case.

Even if a portable version exists, I can't think of a sensible
default value. A sufficiently advanced user could already apply
this on a compatible platform by fiddling with the contents of
Isabelle's contrib directory, I think, so maybe there's no need
for any action.

Cheers,
Thomas.

view this post on Zulip Email Gateway (Feb 04 2021 at 08:09):

From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
The idea came from me. Having a tactic operate with a timeout seems quite fragile. This adds a layer of randomness to Isabelle. In each AFP entry's ROOT file, there's a timeout for the entire session, which is a good practical compromise, but if we start having timeouts in every individual tactic, we might get all sorts of random failures. Other tactics like "auto" or "metis" don't have timeout.

If this is the only or best way to reduce veriT's memory usage, we could consider reverting 478b7599a1a0, but this seems dubious to me.

Jasmin

view this post on Zulip Email Gateway (Feb 05 2021 at 10:27):

From: Dominique Unruh <unruh@ut.ee>
Hi,

If this is the only or best way to reduce veriT's memory usage, we could consider reverting 478b7599a1a0, but this seems dubious to me.

Perhaps a compromise would be to activate timeouts only for the
interactive session? I find that the most annoying thing about timeouts
is that they can make a build of large heaps fail because the computer
goes into swapping. While in the interactive session, timeouts could be
nice so that the computer does not go into expensive infinite loops when
something changes during editing. And since the interactive session is
usually edited by the same person who inserts the timeout, it's then up
to each person whether they want to use a timeout or not. (And
unpredictability is less of a problem during the interactive editing.)

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Feb 05 2021 at 13:36):

From: Makarius <makarius@sketis.net>
For my part, it is formally OK to do nothing for the release.

It is up to the SMT + veriT experts to say if there is something severely
wrong that needs to be changed for the Isabelle2021 release. RC5 is planned
for 08-Feb-2021. The final release approx. 1 week later.

Makarius


Last updated: Mar 28 2024 at 12:29 UTC