-
Notifications
You must be signed in to change notification settings - Fork 17
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
Embrace infinite loops #35
Comments
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:
I think I finally understand. What happens it that the lifetime of the guard gets inferred to be just the call to But still I'd blame the API for being unsafe, not the 'static lifetime for being wrong. |
If we change the analysis, this code does become fine. [And if we add a |
I'm a bit confused. Are you advocating that we should "embrace infinite loops", and hence consider the drop unreachable, or should not? |
@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 B. Don't embrace |
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:
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. |
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 In short, I could to some extent go either way, but it seems better to tread softly here. |
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. |
@nikomatsakis I agree with being conservative----the introduction of NLL is not the time for expanding where
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
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.
Eventually allow taking references to local variables with a
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. |
I proved in our formal model that the following function is safe:
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?
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
Surprising maybe, but it wouldn't actually break anything, would it? The drop code still runs whenever |
Indeed, I do not.
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. |
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.
It assumes that there is a path from any point in the CFG to the exit, that's all.
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.
Perhaps. It would probably require also that we disable unwinding (and recognize that), since otherwise if you do: let x = ...;
use(&x);
loop { } then (Also, can you say a bit more about the connection to rust-embedded/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 |
@nikomatsakis Ah.. I'm doing a bad job of this, mainly because I think the issue is mostly epistemological until " 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 We don't want |
@Ericson2314 in that example (or one very much like it), wouldn't it be possible for the destructor of |
@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! :) |
@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 |
@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 / 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:
But how does
which is pretty ad-hoc :( |
@nikomatsakis One thing I am confident in is that removing the |
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 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 {}
} |
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!();
});
} |
@nikomatsakis And let me not forget your side question from before:
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:
Between DMA and whatever these other use-cases are, I hope we have a compelling use-case. |
I do not think it is a good idea; that was just to demonstrate that something like |
If you do this (today): {
let x = Guard(&mut y); // where Guard has a dtor
...
} you get a guarantee that
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). |
So you quoted @japaric here:
I think that this statement only makes sense if we assume |
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? |
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 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 So I don't expect borrowck to see a guaranteed infinite loop unless the body of the loop is actually empty (that is, |
My current feeling is this: I think the idea of permitting 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., 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 |
(Having written that, though, I am wondering if maybe it would be better to make |
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 I find it somewhat backwards to describe conservative restrictions imposed by the compiler as "guarantees" that people rely on. |
Given that the RFC suggests to add fake unwind edges, this part of the current RFC surprises me:
Doesn't every point of the CFG reach the end? Isn't that the entire point of these fake unwind edges? |
In https://github.com/nikomatsakis/nll-rfc/blob/master/0000-nonlexical-lifetimes.md#layer-2-avoiding-infinite-loops we have
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 theRc
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 amem::forget
call, which I consider unsavory.CC @RalfJung @xfix
The text was updated successfully, but these errors were encountered: