Mace4 malloc issues

Stream: Equational

[Zoltan A. Kocsis (Z.A.K.)]

Jose Brox said:

Here we find a wall I've been hitting a few times with Prover9/Mace4: no matter what memory limit you set up (even unlimited), it seems that it allows an absolute maximum of 1GB, and ignores any quantity above that.

I'll look into this. IIRC Mace4 uses LADR's memory manager to allocate its assignments, and the latter has some default limitations, but setting max_megs explicitly should disable all that. Does mace4 return with a max_megs error, or does it just silently never allocate above 1gig?

First things that occured to me: some env weirdness (ulimit?); or if you're on Windows perhaps your mace4.exe is a 32-bit PE (which would cap your memory severely, but still above 1g). I'll have to see if I can reproduce it, can you send me a test file which should cause mace4 to allocate more than 1g?

[Jose Brox]

Zoltan A. Kocsis (Z.A.K.) ha dicho:

I'll look into this.

Sorry for not giving enough details yesterday (I'm extremely busy with paperwork this month :sweat_smile:). The phenomenon may be subtler: it feels like in Mace4 there may be an "initialization" memory limit (for the initial processing of non-clausal formulas, etc.), which is the one that seems to be fixed, and a "running" memory limit, which can be higher and controlled by the max_megs parameter, both in the GUI under Windows and the command line under Ubuntu (no virtual machine involved, I'm using two separate computers), but with differences. The exit error is always

palloc, Max_megs parameter exceeded

I hadn't looked enough into this, now I've made some checks: In Windows, looking at both the task manager and the performance monitor, the initialization error seems to happen around just 40-50MB of used RAM (although I also saw a 250MB spike in the task manager).
Mace4 max memory.JPG

In contrast, in Ubuntu the error seems to happen at 550MB. I think this is not a ulimit problem:

josebrox:~$ ulimit
unlimited
josebrox:~$ time nice LADR-2009-11A/bin/mace4 -b 20000 -c -f "MACE4 677 anti 255 translation-invariant all f explicited groups order 16" | LADR-2009-11A/bin/interpformat standard > "MACE4 677 anti 255 translation-invariant all f explicited groups order 16.out"

Fatal error:  palloc, Max_megs parameter exceeded

Command exited with non-zero status 1
    0:26.40 real,   26.17 user, 0.14 sys,   0 amem, 566060 mmem

Here in the last line, we see the maximum used memory was 566MB, while in the first line you see I called mace4 with max_megs = 2000MB.

I have other Mace4 runs that, after initialization, have increased to 2GB of physical memory:

    PID USER      PR  NI    VIRT    RES    SHR S  %CPU  %MEM     TIME+ COMMAND
1891056 josebrox  20   0 2136376   2.0g   2076 R  99.0   0.4  41191:08 mace4
1892869 josebrox  20   0 2133600   2.0g   2104 R  99.3   0.4  41105:48 mace4
.
.
.

And the system has 500GB of RAM of which 275GB are free, so there is no problem there.

For Prover9, the problem looks similar but is different: IIRC, it is a
palloc, max_number_vars exceeded error... but this parameter is set to -1 (so unlimited). Tends to happen with first-order formulas involving bijectivity (for finiteness assumptions).

I attach the script that needs more than 556MB at the initialization process:
MACE4 677 anti 255 translation-invariant all f explicited groups order 16

[Notification Bot]

2 messages were moved here from #Equational > FINITE: 677 -> 255 by Zoltan A. Kocsis (Z.A.K.).

[Zoltan A. Kocsis (Z.A.K.)]

@Jose Brox I think I know why this happens. The search phase of Mace4 explicitly turns off the LADR memory allocator's built-in limits, but other passes may simply fail to do this. My first idea is to recompile LADR with the limit set to some high_number, and see if this fixes the issue.