RFC: Resource limits for proof harnesses

[tedinski]

This issue is a task to write/propose an RFC for resource limits.

Resource limits include:

1. Timeouts on proof harnesses. Including a default, and annotations to change them, or flags to manipulate them.
2. Possibly memory limits. Also including a default plus annotations/etc.

The need for these is two-fold:

1. Without resource limits, we get poor customer experiences. For instance, unwinding problems manifest as non-termination without a timeout. CI time can be unbounded when certain failures occur.
2. Resource limits are necessary to get a good experience from parallel harness runners. (If nothing else, we need to know which harnesses need a lot of memory, and limit concurrency so they have enough available. But we can also ensure best performance by starting with longest-timeout harnesses, to keep concurrency high.)

There are questions to resolve:

1. What is the default timeout? (I will initially propose an aggressive one. Maybe 15s)
2. Should memory limits be hard or soft or a combination? (e.g. use OS features to hard-limit to 2GB? Or just track usage and warn if it's over? Or both: hard limit X GB, warn when close to X?)
3. Should memory limits be numeric or "order of magnitude" (low, medium, high, extreme. Perhaps corresponding to 1 GB, 2 GB, 8GB, whole machine.) Or perhaps both.
4. How would memory limits interact with "library back-ends"? Perhaps we must always do solving in a separate process?
5. Should we have command line flags to manipulate them? Which flags? (e.g. we have strange flags around unwind bounds right now, because we start off thinking about only one proof harness at a time.)

and probably more.

Early comments about things I should think about welcome, but details can wait for the RFC.

[tedinski]

• Related #885

[tedinski]

We should ensure we're able to detect (at least) "timeout due to unwinding" versus "timeout due to problem size" and clarify then that an "adding #[kani::unwind(x)]" is the next step.

[karkhaz]

One thing that occurs to me is that I wouldn't really want to specify particular memory sizes. What I'm really concerned about is that the usage doesn't exhaust the available RAM on my machine; I'd like to specify that kani terminate itself when available RAM is less than 5%, say. It feels cumbersome to me to have to specify that I want the mem limit is 24 GiB if I have to manually check that I actually have that much RAM available, it would be nice if the tool could check for me.

On the other hand, if I purposely want to constrain RAM to a very specific value for testing, it's probably good to be able to specify an absolute value too.

This also seems like something like I would want set all the time, rather than having to pass it in using a flag. Do we have a global configuration file for kani? Or maybe read an environment variable, like

export KANI_TERMINATE_ON_AVAILABLE_MEM_PERC=5
# or
export KANI_TERMINATE_ON_AVAILABLE_MEM_GiB=16