search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
198 stars 41 forks source link

cvc4 can grow to consume all system memory #419

Open invd opened 5 years ago

invd commented 5 years ago

Even for short programs, cvc4 can spiral out of control and consume all system memory, leading to general system instability, since Ultimate does not enforce (or periodically check) any cvc4 memory usage limits.

This leads to situations where the Ultimate process requires e.g. 4GB, and cvc4 grows to beyond 15GB, exhausting all available system memory. This was confirmed on the newest Ultimate cf7845638a016090978a13501adca3f0b2bbcea4.

Real crashes have been observed with the particular issue #414 for AutomizerMemDerefMemtrack.xml and AutomizerReach.xml, but in my opinion this is a larger issue, as it is independent of individual bugs or performance problems. On a regular Linux, the oom-killer mechanism will usually prevent a complete system breakdown by killing cvc4 and indirectly aborting Ultimate, but this is an emergency measure and other processes are affected as well.

The expected behavior would be that Ultimate makes an effort to abort cvc4 before the system becomes unstable.

danieldietsch commented 5 years ago

As far as I know, cvc4 does not provide any mechanism to limit its memory consumption. Doing it from inside Ultimate is rather tricky. I am not aware of any reasonably platform independent (e.g., a method that works on most Linuxes and a separate method that works on Windows) way of limiting memory consumption of a subprocess from Java (or from the shell, for that matter).