memory limit option ignored

[easychair]

I ran vampire with a memory limit of 4M, it happily went over 16M. It is a very serious issue, as it prevents experiments with several Vampires running on the same computer

[mezpusz]

I see that there is a lower limit 20971520 which is 20MB. @MichaelRawson is there a reason we don't go below that?

[quickbeam123]

I think the idea with 20MB was to allow Vampire start up properly, before it potentially starts getting restrained by a limit.
(For instance, I am getting "% Peak memory usage: 9 MB" for the empty input.)
So I guess the constant's value = 20MB is reasonable.

But:

• Instead of ignoring, we could still use 20MB if the limit is lower.
• We could have an explicit constraint on the option, so that the user get's informed.

@easychair, are you interested in such really low limits or was this just a test case?

Because, modulo the above-mentioned, the limiting seems to work:

./vampire_rel_master_10430 Problems/PUZ/PUZ039-1.p -m 20
% Running in auto input_syntax mode. Trying TPTP
% Memory limit exceeded!
% ------------------------------
% Version: Vampire 5.0.0 (commit e7971972d on 2025-11-03 15:09:54 +0000)
% Termination reason: Memory limit
% Termination phase: Saturation
% Time elapsed: 0.170 s
% Peak memory usage: 18 MB
% Instructions burned: 519 (million)
% ------------------------------

at least on Linux. The function call used to implement this is known to be ignored by MacOs.

[MichaelRawson]

You need around 15MB to get to the memory limiting function on some platforms IIRC. So 20MB seemed like reasonable headroom.

[easychair]

Sorry, I made an error yesterday - I meant I set it to 4G and it went over 16G (not megabytes)

[easychair]

BTW, I propose to do the same as MariaDB - to allow to specify memory limits like this:

-m 4G

in addition to the current

-m 4000

It is much easier for human users

[MichaelRawson]

Oh. That is a straight-up bug then, will investigate.

[MichaelRawson]

What system are you using, @easychair ? And the precise invocation if possible. This should work on Linux.

#594

[easychair]

I ran it on MacOS. I have not tested Linux yet

[easychair]

Consistent across all tests - memory limit ignored

[MichaelRawson]

Doesn't work at all on MacOS (although it should), apparently. If we care enough we could try to patch around it some other way, but setrlimit with RLIMIT_DATA is what you want to do, really.

[MichaelRawson]

The previous solution involved hooking into the global operator new and doing some accounting. This was all well and good but didn't actually track memory use very precisely. It's much easier (and more performant) to ask the system nicely to do it.

[quickbeam123]

From a related community:

The corresponding information is hard to find, but Mac OS seems to intentionally provide these APIs (ulimit on the shell, resource.setrlimit in Python) but ignore them.

(https://ai-fast-downward.dmi.unibas.ch/issue825)

[easychair]

You refer to a 7-years old discussion, yes, more recent ones say the same. This means one cannot use MacOS for anything, as Vampire can bring any Mac to a standstill.
However, I have a reservation against "to ask the system nicely to do it". In the old past Vampire would deallocate some memory if the memory limit is reached and keep running, sometimes for hours after. With the current solution this is no longer possible.
This feature was discontinued when Krystof and me had to re-implement Vampire nearly from scratch in less than a year but there was an intention to bring it back. It is not very nice that we cannot do it now at all. We had (and probably still have) examples when Vampire terminated early in CASC by memory limit when only a small percentage of memory was occupied by anything useful.
As an example, I wanted to run Vampire for 24 hours on a problem two days ago. This is simply impossible since it fills out 100G memory in an hour. I guess over 99G was rubbish that would not be used in 24 hours

[easychair]

Given the circumstances and the previous discussion, here is my proposal.

1. We can either leave it as it is or add conditional code for MacOS for overloading the global "new". My preference is the latter because we can hurt MacOS users making experiments. It is not very hard to do, right?
2. Should we ever decide we would like to restore "continue solving when the memory limit is reached", it will be easy to restore it by overloading the global new
3. I saw that the default value of -m has changed to 128G with a reference to StarExec (???). This can hurt all users. I have a very expensive monstrous Mac with 96G and I managed to go over it with Vampire. I propose to set to something that is consistent with a typical modern computer (laptop). For Macs the minimum memory now seems to be 16G, so I would set it to 8G. I am not familiar with typical Windows computers. I asked ChatGPT - it says 8G budget laptops, 16G mid-range laptops, so I'd say for our typical user it is at least 16G. So shall we make it 8G?