Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Pre-RFC: Add a built-in support for totality (or non-panicking/aborting) asserting #3625

Open
dead-claudia opened this issue May 6, 2024 · 6 comments

Comments

@dead-claudia
Copy link

dead-claudia commented May 6, 2024

As more and more things get failable or fault-tolerant variants (I'm not even going to try to list them all), and as Rust finds its way into more stability-critical systems where any form of aborting or termination must be avoided at virtually all cost, it'd be incredibly helpful to have something similar to the often-used no_panic userland macro or its inspiration dont_panic built into the compiler.

There's benefits to this that simply cannot be done in userland:

  1. The compiler could infer totality from the absence of any non-returning calls other than the (obviously unsafe) core::intrinsics::unreachable_unchecked(), and then use this to check even debug builds for this. The usual linker approach simply cannot do this.
  2. The compiler could use its awareness of the call chain to pinpoint exactly where the non-returning call could lie, and in some cases recommend to the user possible alternatives.
  3. By marking a function as total, the language server could know to constrain its suggestions to only callers known to panic. Interop with the type checker provides the server with the ability to hide panicking calls from the list of suggestions.
  4. A compiler option could mandate that all functions in a given crate don't panic. This is useful for stability-critical crates as well as #![no_std] crates.

My first thought is maybe a total keyword with the following rules:

  • All intrinsic functions returning ! or a no-variant enum type are considered non-total except for core::intrinsics::unreachable_unchecked()
  • External calls returning ! or a no-variant enum type are considered non-total
  • If validation of convergence of an expression depends on the expression's own totality, it's considered non-total.
    • This handles direct recursion, indirect recursion, and even Y combinators.
    • This check is also sufficient for detecting infinite loops.
  • An expression is considered possibly-non-total if and only if it contains any non-total or possibly-non-total subexpression.
  • A function is considered possibly-non-total if any statement within is possibly-non-total. Calls to it carry this same possible non-totality.
  • The total modifier asserts the function is not possibly-non-total. And total { ... } blocks do the same for their inner statements. Keyword generics/effects/whatever-turns-out-to-be-used will be used to allow parameterization over this similarly to const.

There's admittedly still quite a bit of work to be done here for things like bounded iterators and array index access. Also, the programming style will admittedly start out very different than for typical Rust.

@RustyYato
Copy link

I don't think we can bolt on a termination checker onto Rust. That is use limited to proof assistants.
But the no unwind/abort subset of this proposal does seem useful. How would this interact with traits and generics? It would be a shame if this didn't compose.

@dead-claudia
Copy link
Author

But the no unwind/abort subset of this proposal does seem useful. How would this interact with traits and generics? It would be a shame if this didn't compose.

@RustyYato That was my initial idea before I expanded it to cover other things. But even if those two are all it covers, it's fine by me.

@programmerjake
Copy link
Member

programmerjake commented May 6, 2024

please don't call it converging, that isn't the opposite of diverging as you seem to think, but instead commonly used for GPU code where you want all threads in a workgroup to go back to executing in lock-step at the end of a loop or conditional execution (threads are kinda faked by having one instance of your program per SIMD lane and converging is when all threads that have anything left to run are not masked off by some condition).

you are probably thinking of total, or maybe primitive recursive. LLVM uses willreturn nounwind, which is quite distinct from LLVM convergent.

To be pedantic, converging is the opposite of diverging in the sense of not having the GPU converging property, but that's not the meaning of diverging you mean by enforcing totality.

@dead-claudia dead-claudia changed the title Pre-RFC: Add a built-in support for convergence asserting Pre-RFC: Add a built-in support for totality (or non-panicking/aborting) asserting May 6, 2024
@dead-claudia
Copy link
Author

@RustyYato @programmerjake Updated to use the math term "total" instead of "divergence" (as used to refer to the ! type) to make it clear what I mean. Sorry for the confusion.

Now if maybe software and computer engineering could stop creating ambiguity with math and science terms, that'd be nice... 😅

@kennytm
Copy link
Member

kennytm commented May 6, 2024

... detecting infinite loops.

there are two kinds of "non-totality" (expressions with type !, excluding return/break/continue)

  1. those that kills the execution: panic!(), abort(), exit(), infinite recursion (stack overflow) etc
  2. those that causes the program to loop forever loop {}

practically the first case is much more "dangerous", since once you hit them you'll lose all your states; while for the second case you can still conduct some live debugging and recovery.

however, the proposed "totally" effect will only likely catch code using while loops (since without knowing the condition we must assume they can possibly loop forever), so I'm not very sure about using this new effect to detect "any form of aborting or termination".

@the8472
Copy link
Member

the8472 commented May 23, 2024

I don't think we can bolt on a termination checker onto Rust. That is use limited to proof assistants.

False negatives would be acceptable, just like in the borrow checker. Additionally the user could unsafely assert that a loop will terminate when rust can't determine that.

And while we're wishing for ponies in addition to total there are other desirable properties https://blog.yoshuawuyts.com/extending-rusts-effect-system/#what-are-effects

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

5 participants