guarantees around panics and crashes

[tjhance]

Panics in Rust

To provide a guarantee, it's important to distinguish the various types of panics that can occur in a Rust program. Let's start with the facts about Rust:

• Process Aborts
  • OOM is one; I'm not really sure of the others. RFC 2116 has some information about Rust's out-of-memory handling. It sounds like in some cases, the OS might "lie" to the program about how much memory it has, in which case the program might exceed its memory usage and get killed on memory access rather than during alloc. Furthermore, if the allocator itself fails, it also aborts.
• Unwinding panics
  • Includes stuff like:
    • Arithmetic overflow (debug mode)
    • Index out-of-bounds
    • Invalid use of RefCell
  • An unwinding panic can be caught by catch_unwind.
  • An unwinding panic will, at most, kill a single thread, but other threads can keep going.
  • Because of this, unsafe Rust code needs to take care to be unwind-safe.
    • I believe this is why Rust sets OOM to be an abort; too much code implicitly relies on this for unwind-safety.
  • Users may want to panic in some cases, although idiomatically, they should use Result<...> for errors if they intend to handle them.
  • EDIT: jay points out that one can set panic=abort to force all panics to be aborts, which means unwinding is impossible. He also points out that unwinding is completely impossible on some architectures.

Implications for Verus

Now, when verification comes into the picture:

• Obviously, there's nothing to do about the OS killing a process, which should be considered outside the scope of Rust's program semantics, and if users want to account for such things, they need to use some kind of crash-safety methodology.
• Even if we assume the process has accurate knowledge of the amount of memory, verifying that every malloc succeeds would require complex resource management. Our previous projects didn't attempt to verify this sort of thing (although some of them used statically allocated memory, which would have made this trivial). E.g., VeriBetrKV's specification implicitly allowed for crashes on out-of-memory, and didn't make any kind of guarantee like, "will definitely succeed if given XX memory".
  • Luckily, since OOM causes an abort, we don't need to verify a lack-of-OOM in order to achieve unwind-safety.
• For Verus, 'unwind safety' is important for invariant blocks; that is, we need to show that an invariant block doesn't panic and exit without restoring the invariant.
• Many types of unwinding panics (index out-of-bounds, arithmetic overflow, etc.) are clearly in-scope for verification, especially given the consensus over at Integer overflow panics in debug mode but is allowed by the verifier #45.
• I'm not really sure about stuff like RefCell. A user might use our replacements (like PCell) which does not panic, and whose used are verified; but a different user might be willing to accept the possibility of panics.

Verus's guarantees?

Although this was a lot of information, I think it all points towards a fairly simple takeaway for Verus's guarantees.

• Verus's guarantees, like Rust, should distinguish between unwinding-panic and abort-panic.
  • The default would be that we guarantee no unwind-panics, but make no guarantee about abort-panics.
  • This leaves open the possibility for fn specification attributes like #[verifier(may_unwind)] for more flexibility.

[jaybosamiya]

A few notes (slightly ramble-y, sorry):

1. catch_unwind is not as ubiquitous as say try-catch in other languages. In fact, from the catch_unwind docs (emphasis theirs):

   It is not recommended to use this function for a general try/catch mechanism. The Result type is more appropriate to use for functions that can fail on a regular basis.

2. catch_unwind doesn't catch all panics, only unwinding panics (mentioned by Travis above, but just linking to relevant part of the docs (emphasis theirs):

   Note that this function might not catch all panics in Rust. A panic in Rust is not always implemented via unwinding, but can be implemented by aborting the process as well. This function only catches unwinding panics, not those that abort the process.

3. Whether certain panics are unwinding or not depends on compile-time options (docs for the compiler flag for panic handling, emphasis mine):

   This option lets you control what happens when the code panics.

   abort: terminate the process upon panic
   unwind: unwind the stack upon panic

   If not specified, the default depends on the target.

4. Some targets don't just have their defaults as abort but worse, just cannot support unwind (docs for cargo profiles, emphasis mine):

   When set to "unwind", the actual value depends on the default of the target platform. For example, the NVPTX platform does not support unwinding, so it always uses "abort".

---

At a high-level, all of this tells us that catch_unwind can't really be relied upon; additionally, its usage in user-written Rust code is relatively rare anyways. Certain situations such as mutex-lock-poisoning in the standard library may depend upon it, but in platforms where it is an abort, there isn't really a way for the lock to get poisoned in the first place (the whole process dies(?)).

---

Let us now (hypothetically) consider a world where we force panic=abort. In such a situation, catch_unwind is no longer useful, so we eliminate it from the standard library.

How bad do things get? Given that we can verify the absence of many kinds of panics, I would argue, not too terrible. Arith overflows, out-of-bounds indexing, etc. are some of the most common causes for panics, and those are all verified to not exist, so we are already in a less-panicky world.

For situations where a RefCell ends up panicking due to a reborrow, well that's an actual bug that should be fixed by fixing the source code, since there is no "unpredictable" reason for it to actually occur (even if debugging and fixing this might be non-trivial). Specifically, handling such panics via catch_unwind is just asking for trouble for the sake of trouble.

For custom hand-made panic!()s and todo!()s and such, handling via a catch_unwind is also a weird thing to do, when Result<_, _> is right there.

OOM-errors and such are uncatchable panics anyways, so don't play a role in this discussion.

---

All of this evidence seemingly points us towards: simply disallow both catch_unwind and unwind-panics entirely.

Are there situations where we necessarily need to use unwind-panics and catch_unwind? In regular Rust, sure; but I'd argue that due to being able to verify away most of the common causes for panics, we don't really need unwind-panics.

Side note: there is a compiled-binary-size and also (small but non-trivial) runtime speed advantage to panic=abort

---

On the Rust side of things, there is a useful crate no-panic to prove the absence of panics. (Also see panic-never and dont_panic). With no-panic, the crate abuses the linker to prove the absence of panics. What if we did something similar? Complete absence of panics entirely would be great. I don't think the same approach works out of the box though (the no-panic crate is actually quite restrictive, while we should be able to prove a lot more things as being panic-free)

---

Non-panic aborts (stuff we should probably rule out of scope): of course, there is the OOM-based process killing as Travis mentioned; also uncatchable signals like SIGKILL. Also sudden power loss or brownout. Basically all of these are situations that don't include any "panic" from within the process, but an externally-caused abort. Stopping stuff due to the outside world requires a lot more crash-safety methodologies, and prob best left out of scope, rather than having the burden of that forced on all Verus code.

[tjhance]

panic=abort is good to know about (I hadn't known about it). Certainly, it would be the easiest way to accomplish the first sub-bullet of my proposal above, that is, to guarantee no unwind-panics. We would still want to document which sorts of (aborting) panics Verus does & does not protect against, and we could still allow "user" panics as aborting panics.

That said, I think there is a use-case for being able to reason about code that might unwind, which is when Verus interfaces with trusted code. Ideally, people would be able to write verified libraries in Verus, which might then be included by users writing ordinary rust code who may want to use their own configuration. For example, if a verified library accepts a closure from the client library, the verified code may need to wrap a call in catch_unwind if it's necessary to ensure unwind-safety. So I think we should leave our options open to maybe reason about possibly-unwinding functions in the future.