Spurious out of memory on SV-COMP Intel TDX tasks

[sim642]

The knightly runs always have some Intel TDX tasks from sv-benchmarks where the result spuriously flips between unknown and OUT OF MEMORY (in either direction). I find this suspicious.

It's important to note that this is unlike spurious TIMEOUT result flips which can happen due to unpredictable CPU behavior (automated frequency adjustment) and overall load on the system. How much memory we allocate should not be affected by such factors.

I don't know why this could be happening but there are some quite extreme cases: OUT OF MEMORY in 42s flipping to unknown in 104s (or vice versa).

[michael-schwarz]

How close is the peak usage to the cap where it terminates? It may be a question of garbage collection running just in time to save us from OOM?

[sim642]

If I remember correctly, something like 4.7GB out of 5GB limit, so relatively close.
But both our allocation and the GC should be deterministic. I think GC should be triggered at the same allocations each time and they should be collecting the same stuff.

It could be that something on Goblint side isn't actually deterministic and causes the allocations to happen differently, but that I don't know why that should be the case either.

[michael-schwarz]

It could be that something on Goblint side isn't actually deterministic and causes the allocations to happen differently, but that I don't know why that should be the case either.

Our interrupt based solverstats are something that comes to mind here.

[michael-schwarz]

Also, something has to be non-deterministic, because otherwise we would also not see tasks wiggling between stack overflow from allocating a frame in OCaml and core dumps if the stack overflow happens in C bindings.

[sim642]

Our interrupt based solverstats are something that comes to mind here.

Indeed, that sounds plausible for making some allocations time-dependent.
That theory could be tested by disabling that.

Also, something has to be non-deterministic, because otherwise we would also not see tasks wiggling between stack overflow from allocating a frame in OCaml and core dumps if the stack overflow happens in C bindings.

That's a good point as well.

It's probably not worth investigating right now because these status flips don't seem to involve trues. I just hope there isn't some other deep C stubbing related issue somewhere...