Specific error messages for OutOfMemory and other errors

[denis-bogdanas]

At the moment when OOME happens we get:

org.kframework.utils.errorsystem.KEMException: [Error] Critical: Haskell Backend execution failed with code 137 and produced no output.

Front-end should report informative error messages for the following situations:

• kore crashed with out of memory error because it exceeded allocated heap (equivalent to Java OutOfMemoryError)
• kore process was killed by OS, presumably because of low memory (if possible)
• kore process interrupted.
• z3 process interrupted.

This will help debugging memory issues on Jenkins. Also will help distinguishing memory issues from other issues. Cases 1 and 4 can be communicated to front-end via return code.

Front-end should also end with specific error codes in such cases, that can be used by wrapper script to print diagnostics information, like free system memory.

[ttuegel]

The exit code 137 indicates case 2. By default, there is no heap allocation limit, so the user will never see case 1 unless they start setting their own RTS options. Can you explain what cases 3 and 4 are in more detail? I'm not sure what's going on in these cases.

[denis-bogdanas]

Case 3:

kore-exec: [2020-06-25 14:52:17.739179846] Error (ErrorException):
    fd:137: hFlush: resource vanished (Broken pipe)
org.kframework.utils.errorsystem.KEMException: [Error] Critical: Haskell Backend execution failed with code 1 and produced no output.

I suspect this happens when z3 crashes. More specific error code must be reported. Front-end should use it to print a better error message.

[denis-bogdanas]

Case 4 was just to make sure interrupt signal is properly handled. I guess it is already. Front-end prints InterruptedException.

[denis-bogdanas]

@ttuegel In this run we have a case when Haskell process was killed with error 137. Search for Exit status: 137. https://office.runtimeverification.com/jenkins/blue/organizations/jenkins/erc20-verification/detail/PR-162/3/pipeline/

It is unlikely to be OOM, because max memory consumption was only about 4GB. Is there a way to extend our tools to find why this process got killed?

[ttuegel]

Exit code 137 (= 128 + 9) is SIGKILL. I don't think there is anything we can do in the backend to find out why the process was killed because SIGKILL cannot be caught or handled.

[denis-bogdanas]

Then I see only one explanation. The scripts display memory consumption through /usr/bin/time -v. I suspect this command displays the consumption of the top process only, without subprocesses. And some subprocess eats up too much memory. I'll try to run tests failing with 137 again to see what happens.