Embrace infinite loops

[Ericson2314]

In https://github.com/nikomatsakis/nll-rfc/blob/master/0000-nonlexical-lifetimes.md#layer-2-avoiding-infinite-loops we have

let scope = Scope::new();
let mut foo = 22;

unsafe {
  // dtor joins the thread
  let _guard = scope.spawn(&mut foo);
  loop {
    foo += 1;
  }
  // drop of `_guard` joins the thread
}

in which, without "unwind" edges, _guard is not considered live because its destructor isn't run, so the code type checks. I think this methodology overly embraces the "destructors may not be run approach" we adopted after the Rc issue.

At least in unsafe code, it would be friendlier to have the rule "lvalues with Drop types are live from initialization until the destructor is run". Then _guard is considered live for all outgoing control flow, in which case the code doesn't type check. [As an optimization, we could reclaim the stack slot, but it's important not to adjust the duration of the borrow.]

Philosophically I don't like distinguishing between the lifetime of a value and the lifetime of a reference. I say all things are live until they are dropped, but if dropping is unobservable we are free to move the drop around in the CFG to get more code to type check. Shortening the like _guard, since it's drop is observable, is therefore only possible with a conceptually by adding a mem::forget call, which I consider unsavory.

CC @RalfJung @xfix

[RalfJung]

As you already mentioned, that API is unsafe anyway. So I wouldn't blame the infinite loop borrow checking here.

So @arielby brought up this code:

let mut foo = 22;

unsafe {
  // dtor joins the thread
  let _guard = thread::spawn(|foo| {
    loop {
      // in other thread: continuously read from `foo`
      println!("{}", foo);
    }
  );
  // we assume `_guard` is not live here, because why not?
  loop {
    foo += 1;
  }
  // unreachable drop of `_guard` joins the thread
}

I think I finally understand. What happens it that the lifetime of the guard gets inferred to be just the call to spawn because the destructor isn't reachable and hence does not extend the lifetime. That's a surprising interaction indeed.

But still I'd blame the API for being unsafe, not the 'static lifetime for being wrong.

[Ericson2314]

If we change the analysis, this code does become fine. [And if we add a Leakble trait for Rc and mem::forget's sake, we can make the interface safe too, but that's another matter.]

[nikomatsakis]

@Ericson2314

I think this methodology overly embraces the "destructors may not be run approach" we adopted after the Rc issue.

I'm a bit confused. Are you advocating that we should "embrace infinite loops", and hence consider the drop unreachable, or should not?

[Ericson2314]

@nikomatsakis Sorry for the confusion. I am both embracing and not embracing stuff here, which was definitely harder to follow than I intended.

A. Do embrace the infinite loop and thus deduce the drop won't be run. (We can and should still take into account genuine panic edges, but there wouldn't be one there since the += doesn't desugar into a method call.)

B. Don't embrace Drop not being guaranteed: Unless mem::forget is involved, if a Drop type isn't dropped, it must be assumed to be alive. I consider doing the normal liveness analysis here tantamount to inserting a mem::forget, which I think is hostile to unsafe code just the same way exploiting UB for optimization can be. OTOH I consider the liveness analysis for non-Drop types to be communiting the "identity drop" (a la non lexical drop), which is fine since it has no behavior.

[Ericson2314]

BTW that reminds me of a philosophical difference. In the opener you distinguish between the lifetime of the a value vs reference. I, however, something think of it as:

1. There is only the lifetime of values,
2. all lifetimes constrained by a scope-based destructor placement,
3. but the borrow checker can commute those identity drops to allow more code to type-check.

Pretty sure these are just two ways of looking at the same thing, but it might give some context to my views in this thread.

[nikomatsakis]

So I think this is sort of a "not entirely obvious" question. However, what pushed me in favor of my current proposal was a few things:

Introducing false unwind edges to infinite loops is the conservative position. We can always change it later.

Most of the time, code can indeed panic, so I find it a bit... discontinuous that in certain very extreme cases (e.g., loops that don't invoke other functions), the borrowck suddenly behaves very differently. This seems like it might be quite surprising, and I don't really see a compelling advantage to that just now. i.e., code is improved by this discontinuity?

Finally, although I agree with @RalfJung that the "scope-enforced-by-dtor" API is unsound in general, it is also a useful pattern to do in one's own code. If you have a local variable that you don't move, it is perfectly safe to rely on its destructor executing, and in fact that is often the most convenient way to write code that handles unwinding intelligently (this is especially important in unsafe code). I feel like having a let statement like let _x = ...; with a destructor is a kind of fixed pattern, and having it sometimes infer very short borrows around an infinite loop just feels surprising. Perhaps this is the same argument as the previous paragraph. =)

In short, I could to some extent go either way, but it seems better to tread softly here.

[nikomatsakis]

Ah, one other thing: if we don't have a universal exit from the control-flow graph, then it is also true that we need to do some work to make liveness analyses work. The standard dataflow analysis is a reverse data-flow that begins at the exit from the CFG.

This doesn't quite make sense the way I wrote it. I have to do a bit more investigation, but I know that some results around liveness assume an exit, at minimum.

[Ericson2314]

@nikomatsakis I agree with being conservative----the introduction of NLL is not the time for expanding where 'static is valid, for example. But I'd use that same reasoning to argue against the current plan:

Introducing false unwind edges to infinite loops is the conservative position. We can always change it later.

Adding fake edges to enforce an invariant of always having is not conservative. We can't stop adding those edges if we rely on that invariant. The conservative thing would be something like adding non-deterministic fake edges---infinite loops might or might not exit, so we can't rely on either. That would close off the extra 'statics, and keep the variable alive because of the potential destructor call. [I suppose the fake panic edges are also optional, but I get the sense your planned assumes that control would be assumed to eventually exit.]

the "scope-enforced-by-dtor" API is unsound in general, it is also a useful pattern to do in one's own code.

Oh I absolutely agree. Furthermore, I still want an opt-out leak trait, to control in a type-directed manner whether the destructor is optional, so this can be made actually safe.

I don't really see a compelling advantage to that just now.

Eventually allow taking references to local variables with a 'static would probably be useful for some embedded things. In https://github.com/japaric/embedded-hal/issues/14 for example, this came up utterly coincidentally. [I say probably because I haven't worked all the way through a specific use case yet---it was not something I had realized might be possible.] Furthermore, with aborting on panic, function calls in loops are no problem either. Again, I don't want to do this right off the bat, but I don't want to close it off either.

I know that some results around liveness assume an exit, at minimum.

What I did with stateful mir is tantamount to the status of a variable/location following the dual of CFG---variables' types were assigned per edge (pre- and post- conditions), and transitioned on the node. [The difference between my non-fixed type vs your status bits I think is irrelevant to this restriction.] A liveness-inference traversal would stop recurring on encountering an already-visited node, and simply need to ensure that the status bits on all incoming edges matched.

[RalfJung]

If we change the analysis, this code does become fine.

I proved in our formal model that the following function is safe:

use std::mem::transmute;

fn diverging_static_loop<F, T: 'static>(x: &T, f: F)
    where F: FnOnce(&'static T)
{
    f(unsafe { transmute(x) });
    loop {}
}

Notice that our formal model does not have panic, so this may still be unsound in the presence of panic -- but anyway, panics would be taken care of in the CFG by the unwind edges. This of course is all irrelevant when panics abort, but do we really want borrowck behavior to depend on panic=abort vs. unwind?

For this reason, I think it is perfectly reasonable to accept this code. Of course, as you pointed out, this does rule out some other code -- but IMHO the interesting question to ask is which guarantee for safe code do we lose by permitting this, and how useful is that guarantee?

---

BTW that reminds me of a philosophical difference. In the opener you distinguish between the lifetime of the a value vs reference. I, however, something think of it as:

1. There is only the lifetime of values,

This is funny. ;) I think Rust's lifetimes only apply to references, not values. Values may have a "lifetime" in a broader sense of the word, but the thing Rust calls 'a is strictly something that applies only to references. This is also the strategy I followed in the RustBelt model.

---

I feel like having a let statement like let _x = ...; with a destructor is a kind of fixed pattern, and having it sometimes infer very short borrows around an infinite loop just feels surprising. Perhaps this is the same argument as the previous paragraph. =)

Surprising maybe, but it wouldn't actually break anything, would it? The drop code still runs whenever _x goes out of scope. It just happens to be the case that that never happens.

[nikomatsakis]

@RalfJung

This of course is all irrelevant when panics abort, but do we really want borrowck behavior to depend on panic=abort vs. unwind?

Indeed, I do not.

Surprising maybe, but it wouldn't actually break anything, would it?

Not directly. It might allow code to type-check that the user might not have expected to, and hence they would not be getting the guarantees they expect. It would also just generally make the behavior of the compiler more surprising and brittle -- small changes to an infinite loop (like, almost anything) would introduce potential unwind edges.

[nikomatsakis]

@Ericson2314

Adding fake edges to enforce an invariant of always having is not conservative. We can't stop adding those edges if we rely on that invariant.

Hmm, maybe we're miscommunicating. When I say "fake edges" I mean "edges that are not taken at runtime" -- but are treated (by the analysis) as potential control-flow. This sounds kind of exactly like what you describe later on, so I think we are proposing the same thing.

I suppose the fake panic edges are also optional, but I get the sense your planned assumes that control would be assumed to eventually exit.

It assumes that there is a path from any point in the CFG to the exit, that's all.

Furthermore, I still want an opt-out leak trait, to control in a type-directed manner whether the destructor is optional, so this can be made actually safe.

I don't understand what this "leak" trait would do... oh, you mean something to assert that a value doesn't leak? In that case, seems orthogonal-ish to this particular discussion.

Eventually allow taking references to local variables with a 'static would probably be useful for some embedded thing.

Perhaps. It would probably require also that we disable unwinding (and recognize that), since otherwise if you do:

let x = ...;
use(&x); 
loop { }

then use() can always unwind. In other words, I think the only time that a local variable that can be borrowed for a static lifetime is when we are not doing anything of interest with it, basically.

(Also, can you say a bit more about the connection to https://github.com/japaric/embedded-hal/issues/14? It's not obvious yet to me how this would be better than using static buffers and things -- I guess maybe you can get a &'static mut T that is actually safe, which is neat.)

[Ericson2314]

@nikomatsakis Ah.. I'm doing a bad job of this, mainly because I think the issue is mostly epistemological until "'static-from-locals", as I'll call it, is permitted.

N.B. I edited this a bunch, sorry.

I shouldn't have brought up invisible panic edges. They are just a means to an end. I am fine for now with the end of giving references to locals something other than there most general type---that's conservative. I don't like the implementation relying on there always been a non-accessible edge----that maybe be an implementation detail, but it's still a non-conservative one as some future Rust with true infinite loops violates it.

I guess was trying say the fake-edge trick is fine as long as we only embrace it's conservative ramifications, and not it's hand-tying ones, but that's a silly point to make. It's better to first establish what we're trying to avoid first.

Anyways, here's an attempt to get beyond the epistemological: Without relying on panic=abort in any way, we can say

unsafe { 
    let x = ...;
    let y: Foo<'static> = use(&'static mut x);
    loop { possibly_panic!(); }
}

is effectively safe as long as Foo<'_> is exception-safe. It can only be exception safe if some destructor (either x's or y's, depending on the extract strategy) is always run on the panicking edge. If we agree unsafe code ought to be able to achieve and take advantage of that guarantee, then we can side-step talking about a Leak trait, which is only needed to allow safe code to do that too.

We don't want use to need to just transmute the lifetime without constraint---that's too big a sledge hammer. But I think a) the explicit &'static mut + b) being in an unsafe context, is perhaps enough opt-in to tell the borrow checker to avoid worrying about the panic edges. Maybe an even more verbose &unsafe 'static mut would be better.

[nikomatsakis]

@Ericson2314 in that example (or one very much like it), wouldn't it be possible for the destructor of Foo to store the &'static reference in some global somewhere?

[Ericson2314]

@nikomatsakis Yes! as long as the destructors somehow prevented that reference from being accessible if the thread panicked.

Also, great job. You responded just as I finished editing! :)

[nikomatsakis]

@Ericson2314 so -- in that case -- how is this code safe?

unsafe { 
    let x = ...;
    let y: Foo<'static> = use(&'static x);
    loop { }
}

I feel like I'm missing something. It seems like the dtor of Foo could store the pointer into the stack frame, and then some caller could (during its dtor, or with catch_unwind) access that pointer.

[Ericson2314]

@nikomatsakis I'm not quite sure what you are asking? But I didn't like my responses either.

Here's a revised example, which for clarity doesn't need concurrency / Send / Sync, or 'static.

unsafe 'a: {
    let like_a_global: Bar<'a, T> = Bar::Inaccessable;
    catch_unwind(|| {
        let x: T = ...;
        // initialize like_a_global, despite `x` not living long enough
        // in the presence of panics.
        'b: {
            let y: Foo<'b, T> = use(&'a x, &mut 'a like_a_global);
            loop { possibly_panic!(); }
            // on panic, `y`'s destructor makes `like_a_global` `Inaccessible` again.
        }
    });
}

I think before I made these mistakes before:

1. It's Bar that needs to be exception-safe, but I didn't have an explicit Bar.
2. Foo should not have argument 'a, because with 'a it's not guaranteed by the types to have its panic handler run early enough. With 'b it is.

But how does Foo get constrained by that lifetime? I'm worried we'd need a

&{ 'a /* without panics */, 'b /* with panics */} x

which is pretty ad-hoc :(

[Ericson2314]

@nikomatsakis One thing I am confident in is that removing the possibly_panic!() should have no effect if we do have fake edges (it's a stand-in for those), and only reduce the obligations of the code to be sound if don't have fake edges---exception safety becomes contingency planning for an impossibility.

[RalfJung]

Not directly. It might allow code to type-check that the user might not have expected to, and hence they would not be getting the guarantees they expect. It would also just generally make the behavior of the compiler more surprising and brittle -- small changes to an infinite loop (like, almost anything) would introduce potential unwind edges.

Which guarantee is it that they would no longer be getting? Certainly none of the guarantees that I have written down in my formal model. I think that my example code (if we add take_mut's abort-on-panic type) should be considered safely encapsulating the unsafe block. That doesn't mean that it has to be accepted by the typechecker; it just goes to show that we already do not have a guarantee that local variables cannot be 'static.

I can see the argument that having the type-checker accept these programs will never actually be useful, and introduces a somewhat surprising non-continuity. That's purely an ergonomic point though not a technical one.

EDIT: To be clear, I mean this code

use std::mem::transmute;
use std::panic;

fn diverging_static_loop<F, T: 'static>(x: &T, f: F)
    where F: FnOnce(&'static T)
{
    panic::catch_unwind(panic::AssertUnwindSafe(|| f(unsafe { transmute(x) })))
        .unwrap_or_else(|_| ::std::process::abort());
    loop {}
}

[KamilaBorowska]

diverging_static_loop provided before in this issue is unsafe when unwind is allowed. I don't think it is when unwind is not allowed, but is it a good idea to allow code that compiles only when panic=abort?

use std::mem::transmute;

fn diverging_static_loop<F, T: 'static>(x: &T, f: F)
where
    F: FnOnce(&'static T),
{
    f(unsafe { transmute(x) });
    loop {}
}

struct DropDetector;

impl DropDetector {
    fn method_call(&self) {
        println!("Calling a method...");
    }
}

impl Drop for DropDetector {
    fn drop(&mut self) {
        println!("Dropping...");
    }
}

struct RefCaller(Option<&'static DropDetector>);

impl Drop for RefCaller {
    fn drop(&mut self) {
        self.0.unwrap().method_call();
    }
}

fn main() {
    let mut ref_caller = RefCaller(None);
    let drop_detector = DropDetector;
    diverging_static_loop(&drop_detector, |detector| {
        ref_caller.0 = Some(detector);
        panic!();
    });
}

[Ericson2314]

@nikomatsakis And let me not forget your side question from before:

(Also, can you say a bit more about the connection to japaric/embedded-hal#14? It's not obvious yet to me how this would be better than using static buffers and things -- I guess maybe you can get a &'static mut T that is actually safe, which is neat.)

Yeah, I basically mean that, so DMA can be done with stack arrays without blocking. @japaric, whose thought much more about embedded Rust than me, also wrote:

I have mentioned before that stuff allocated in never-ending functions (fn() -> !) should have a different lifetime to indicate that they can't be deallocated. That would be useful here but that feature doesn't exist.

Between DMA and whatever these other use-cases are, I hope we have a compelling use-case.

[RalfJung]

diverging_static_loop provided before in this issue is unsafe when unwind is allowed. I don't think it is when unwind is not allowed, but is it a good idea to allow code that compiles only when panic=abort?

I do not think it is a good idea; that was just to demonstrate that something like diverging_static_loop can be a "safe" function, if panic=abort is enforced. The second version of diverging_static_loop should be safe even in the presenve of panics.

[nikomatsakis]

@RalfJung

Which guarantee is it that they would no longer be getting?

If you do this (today):

{ 
  let x = Guard(&mut y); // where Guard has a dtor
  ...
}

you get a guarantee that y is unavailable for the rest of the block (i.e., cannot be modified except through x without a compilation error). As we saw in the motivating example, this guarantee does not hold under some very particular cases around infinite loops. I think these cases have to be very narrow indeed, though, since anything that might unwind will extend lifetime of the borrow to at least after the unwinding point.

I can see the argument that having the type-checker accept these programs will never actually be useful, and introduces a somewhat surprising non-continuity. That's purely an ergonomic point though not a technical one.

This is to my mind primarily a question of making the system behave in a predictable fashion (while still being expressive enough for whatever it is we want).

[nikomatsakis]

@Ericson2314

So you quoted @japaric here:

I have mentioned before that stuff allocated in never-ending functions (fn() -> !) should have a different lifetime to indicate that they can't be deallocated. That would be useful here but that feature doesn't exist.

I think that this statement only makes sense if we assume panic=abort (and take that into account for the type system), no? Otherwise, fn() -> ! functions can be thought of as "guaranteed to panic" =) (at least, that's how I always thought of them).

[nikomatsakis]

@Ericson2314

Here's a revised example

Sorry, maybe I'm just too distracted, but can you now add a few notes with just what you were attempting to demonstrate with this example?

[notriddle]

About this example:

let mut foo = 22;

unsafe {
  // dtor joins the thread
  let _guard = thread::spawn(|foo| {
    loop {
      // in other thread: continuously read from `foo`
      println!("{}", foo);
    }
  );
  // we assume `_guard` is not live here, because why not?
  loop {
    foo += 1;
  }
  // unreachable drop of `_guard` joins the thread
}

If you compile in debug mode, won't foo += 1 eventually panic? And shouldn't typecheck always assume that foo += 1 can panic, even though it technically can't in release mode, because nobody wants type checking to depend on debug-mode-vs-release-mode?

---

To make a slightly more relevant point, the compiler has to assume that arithmetic might panic, either because it involves overflow checks, or because it involves the Wrapping<T> type which the compiler has to assume might panic because it's a library type.

So I don't expect borrowck to see a guaranteed infinite loop unless the body of the loop is actually empty (that is, loop {}). And if somebody is writing loop {}, they probably want this kind of special behavior, because they are legitimately doing weird stuff.

[nikomatsakis]

My current feeling is this:

I think the idea of permitting 'static lifetime when we know that a function will not terminate is interesting. However, unless we decide to let the borrow checker reason about whether panic=abort or not, it is not of much practical use (as e.g. @notriddle just commented), because there is really very little you can do of interest that doesn't potentially panic.

Personally, I would prefer that, for the time being, we keep the rules behaving more "regular", without surprising special cases of no practical value (e.g., loop { } causes let x = Foo(&mut y) to release its lock far earlier than it otherwise would). [That said, I agree with @RalfJung that there is no "guarantee" necessarily being preserved here -- i.e., there is no "safe API' that one could build because of this behavior that would not otherwise be possible.]

Then, as a future extension in a later RFC, I think it would be interesting to explore integrating knowledge of panic=abort into the borrow checker. This would mean that any -> ! function would be considered to never return (rather than "only returns by unwinding"), and naturally we could eliminate all panic paths and so forth (hence a += 1 cannot unwind either). In this context, I can see that enabling (e.g.) &'static borrows of local variables could be very useful!

[nikomatsakis]

(Having written that, though, I am wondering if maybe it would be better to make loop { } at least behave the same in either model; so that the two are more unified. Meh, ok, I'm on the fence now. Though I think that later RFC I alluded to could also alter the behavior of loop { } in any mode, and it would be backwards compatible, precisely because of the fact that no "new guarantees" are being introduced here.)

[RalfJung]

You get a guarantee that y is unavailable for the rest of the block

I see. I am not sure if this translate to any invariant that you can guarantee on a semantic level though, so this looks mostly like a linting-level guarantee to me. I also have to say this us (a) subtle, and (b) if we start going here, we can just as well reject the entire concept of NLL -- as NLL destroys the guarantee that a borrow, once in scope, will make sure that stuff is locked until the end of the current block. (Just remove the assumption that Guard implements drop from your example, and then we have an example of the exact same guarantee that is currently provided but will be "lost" with NLL.)

I find it somewhat backwards to describe conservative restrictions imposed by the compiler as "guarantees" that people rely on.

[RalfJung]

Given that the RFC suggests to add fake unwind edges, this part of the current RFC surprises me:

The reason that we require the end point of the CFG to be reachable is because otherwise the data never escapes the current function,

Doesn't every point of the CFG reach the end? Isn't that the entire point of these fake unwind edges?