10 ms·
Unsoundness in Pin
- est31 7y agoFor the uninitiated: Rust differentiates between safe and unsafe code (safe being the default and unsafe needing the unsafe keyword). The unsafe code is like C/C++: it's more powerful than safe code, allowing you to do more things, including allowing you to trigger undefined behavour. Any mistake can possibly mean UB with all the consequences of crashes, wrong behaviour and nasal demons. Safe Rust on the other hand, is not supposed to be allowed to trigger such UB, no matter what you write. If you are able to trigger UB in 100% safe code, it's considered a bug in the language, an unsoundness bug. Note that it was known that Pin/Generators had soundness problems when you turned on noalias optimization flags [1]. They have however decided to stabilize it without fixing those problems as they could be fixed afterwards as well. I'm not entirely sure yet about the impact of this one, will have to read the thread I guess. [1]: https://github.com/rust-lang/rust/issues/62149#issuecomment-521149328 https://github.com/rust-lang/rust/issues/62149#issuecomment-...
- deleted 7y ago[deleted]
- mauricioc 7y agoSimon Peyton Jones initial intuition [0] was that Rust would be full of soundness holes due to not starting with a full formalization. Derek Dryer, Ralf Jung and others in the RustBelt project [1] did amazing work in formalizing Rust's safety guarantees, showing that Peyton Jones' guess was not accurate. There is nothing wrong about having bugs, of course, but the reaction to the bug in this thread shows that mathematical correctness is not as universally valued as I thought it would be. I agree with the sentiment that this is a bigger issue that shouldn't be discussed in a technical thread about a specific bug. However, after reading this, it is unclear to me whether mathematical correctness is regarded in the Rust project as an explicit goal, an explicit non-goal or an unessential nice-to-have. (I do not mean to insinuate anything with the word "unclear", as I believe all three options are valid and appeal to different use cases. Almost all of the popular languages don't care about this, for instance.) [0] https://youtu.be/t0mhvd3-60Y?t=130 https://youtu.be/t0mhvd3-60Y?t=130 [1] https://plv.mpi-sws.org/rustbelt/ https://plv.mpi-sws.org/rustbelt/
- steveklabnik 7y ago> However, after reading this, it is unclear to me whether mathematical correctness is regarded in the Rust project as an explicit goal, an explicit non-goal or an unessential nice-to-have. (I do not mean to insinuate anything with the word "unclear", as I believe all three options are valid and appeal to different use cases.) It's a balance. We cannot drop everything, nor stop all development, in order to get proofs. However, we are actively working toward formalizing the language itself, because we do see value in it.
- mauricioc 7y agoTotally reasonable stance, in my opinion, since Rust moves quickly and formalizing things takes time. But what is the stance on soundness bugs? Are they sometimes acceptable as permanent parts of the language, or is it a goal to eventually fix any soundness bugs that show up?
- steveklabnik 7y agoSoundness bugs are the only thing we make an exception in our stability policy for. In general, unsoundness is treated as a serious issue. However, "unsoundness" can mean a few different things; in the "semantics of the language" sense, they're taken very seriously. In the "there's a compiler bug" sense, they're taken seriously, but in accordance with how likely they are to affect end users, and how much work they are to fix. For example, an incorrect type signature in the standard library was fixed one day after release by changing it to the correct one and re-releasing; an issue where casting between floating points and integers causes some problems has still not been fixed, because it partially has to do with LLVM's semantics combined with our semantics, and it's not clear how to do the right thing while not seriously regressing performance. (That being said that particular issue has had a flurry of activity in the past week...) The GitHub label for these bugs is A-Unsound, which has the description "A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/Soundness" https://en.wikipedia.org/wiki/Soundness".
- 7y ago
- kibwen 7y agoFor those who haven't heard of `Pin` before (which is reasonable even for Rust users, for whom this is a rather obscure corner of the standard library): it's essentially a trait that indicates that a value cannot be moved from its current location in memory. Here's an analogy: Rust already differs from most languages in that the behavior that you get "by default" when defining a new type is very limited. For example, if I define a type `struct Foo`, then by default this type can't be copied around: `let x = Foo; let y = x;` is a simple operation that in most languages would involve copying memory, but in Rust involves a move instead. You can think of a move as a copy where the original value is no longer accessible (whether or not any bytes in memory actually get copied as a result of a move is an implementation detail, and is (hopefully) often optimized away). In order to make our type copyable, we would add an implementation of the `Copy` trait. The observation is that moving is a more fundamental operation than copying, therefore, it is easier for types to opt in to copying than to opt out. When Rust was released in 2015 this was a relatively radical concept for a language targeting a mainstream audience (we're essentially describing Rust's entire concept of ownership here, after all). But it turns out that it's possible that Rust may not have been radical enough! Consider: what if you want a type that not only can't be copied, but can't be moved as well? Before Rust 1.0 it wasn't clear that such a concept of "unmoveability" would be generally useful. There were certainly cases, such as self-referential structs, that could have benefited from such a concept, however making moveability opt-in rather than opt-out would have required all types that do want to be moveable to explicitly announce that fact (via something like `#[derive(Move)]`), which is an annotation burden on all other code that must be considered. It wasn't until the async/await work that another, more critical need for unmoveability was found: if the generators interally produced by `async` are capable of moving, then that means that generators are incapable of containing references, which means that async/await would become drastically less useful; there would be an entire fundamental part of the language that simply couldn't be used with it. Thus `Pin` was born in order to denote things that cannot be moved (and whose design is itself a very, very long discussion). For this reason I'm somewhat amused by one of the comments in the OP asking something like "if `Pin` had remained unstable for an additional year, would this particular instance of unsoundness have been caught?" Because, conversely, we could ask whether Rust itself could have remained unstable for another five years and found a design that would have obviated `Pin` entirely by making moveability opt-in. However, of course, such things are easy to ask in hindsight, and stability is a prerequisite for having a broad base of adoption. Finding a balance between immediate stability and eventual perfection is the holy grail of industrial language design. (Regarding the bug in the OP itself, I think it's unfortunate but I'm not especially worried by it at this juncture. The fact that Ralf Jung's team is looking into it gives me confidence that formal methods will eventually be applied here to more thoroughly explore the soundness of `Pin` in general (Ralf being one of the people who shaped `Pin` originally), and in the meantime I wouldn't be opposed to a band-aid fix, given that working extensively with `Pin` in the way shown in the OP is rare for normal users.)
- fortran77 7y ago[Comment removed because of content critical to Rust]
- kibwen 7y agoRather, Rust pushes soundness concerns into specific abstractions which have a hope of ever being formally verified (there are at least three teams working on this), and whose essential soundness invariants can be documented. Coupled with a philosophy that soundness bugs must be fixed even if it means breaking language backwards-compatibility and a community that takes soundness very seriously, I'd contend that this is a dramatic step forward for language security (especially if it can continue to light a fire under C++ to inspire it to evolve towards a more statically-verifiable design).
- rcxdude 7y agoThe evidence so for does not really support your conclusion. Even with some worse soundness bugs than this (a few were actually triggered commonly enough the fix only emitted a warning to give enough time for users to fix their code), bug density in safe rust code seems to be way down compared to C and C++.
- saagarjha 7y agoCan you stop editing your comments to mean something entirely different after people respond to you? Here’s what I have from a couple of minutes ago: > Basically, Rust just pushes the subtle bugs down a few layers, making them more subtle and likely to bite you at the worst possible time. > And false confidence in the borrow checker and the type checker will make it harder to find these problems. I'll pass. Here is what you have now: > Rust is different from any other language, considering the care and deftness that its creators go to bring advanced computer science and language concepts to the masses. This isn’t the first time you’ve done this and it makes it very difficult to interact with you in good faith.
- jeltz 7y agoPersonally I am not convinced Pin is a good idea as it works now. Not because of this soundness bug but because it is too hard to understand. Just look at how much explanation is required in the manual and how large the code examples are. https://doc.rust-lang.org/beta/std/pin/index.html https://doc.rust-lang.org/beta/std/pin/index.html
- kibwen 7y agoAgreed that `Pin` is imposing by dint of trying to provide "more fundamental" guarantees than Rust was originally designed for (see my sibling comment on this topic). Though ideally in the long run I'd hope that no regular user would ever have to encounter it (right now I think it may show up in some contexts related to futures, but as Rust's async story matures I would hope to see that need diminish).
- jeltz 7y agoIdeally the basic building blocks of Rust should be so easy to understand that any experienced Rust developer could use them too and not just the core team. The cases where I personally wanted Pin were cases that I think will be solved in the future as async improves, but there are probably other more fringe cases which wont.
- kibwen 7y agoAbsolutely, I don't think there should be arbitrary barriers to entry for people who wish to dive into the deepest parts of Rust's type system. Finding a suitable replacement for `Pin` would be such a big task that I'd say it's not worth considering for anything short of a hypothetical "Rust 2", but hopefully in the meantime we'll soldier on and get a better idea of the problem space in the meantime.
- fluffything 7y agoPretty much anybody writing `async` code, using `Futures`, etc. needs to deeply understand `Pin`, pinning, etc. Otherwise it is impossible to become productive with that part of the language.
- svnpenn 7y agoI am new to Rust, but this: for<'a, T: ?Sized> &'a T !: DerefMut Seems like a hunk of unreadable code. Is this valid Rust? https://internals.rust-lang.org/t/unsoundness-in-pin/11311/33 https://internals.rust-lang.org/t/unsoundness-in-pin/11311/3...
- kibwen 7y agoI think the `!` part might be a typo, and that pseudocode needs more context to be valid, but the individual elements are themselves valid even if you'd never see them composed in this way, and I wouldn't expect any regular user to have to ever read or write anything like this. The leading `for<>` indicates a higher-ranked lifetime (which I've never once needed in eight years of writing Rust (though to be fair, I think it's only existed for like six of those years...), the `!` is the "Never" type indicating a statically-impossible state (honestly it really should just be called `Never` rather than `!`, this is a leftover artifact of prehistoric versions of Rust that predate even me. Maybe I'll write an RFC to propose that), the `?Sized` is a one-of-a-kind trait bound that users might need rarely (but I don't bother with, generally), and the `'a` is a lifetime type parameter (which is common for anyone working with references, although it's such an important part of the language that you don't bat an eye at it after a while).
- dethinking 7y agoYes, it’s a type signature. It looks typical of Rust internals, but it would be very verbose for user code. You’re not wrong to find it illegible; apart from the syntax, that phrase invokes the concepts of lifetimes, mutability, borrowing, and traits, none of which have straightforward semantic analogues in other common languages. But FWIW they’re primitive concepts in Rust. A typical Rust user wouldn’t read or write code that looks like that very much, but they would know what it means, if that makes any sense. Edit: Seeing sibling comments about whether this snippet actually parses, I guess I should amend this to say that a typical Rust user has an idea of what it’s supposed to mean :)
- hollerith 7y agoSignature for the type of which identifier? "for"?
- eximius 7y agoI didn't follow all of it, but it sounds not so bad. 1 & 2 both involve unsafe code that, while possibly reasonable in a complex application, is obviously wrong in the simple case. Of course turning a reference into a mutable reference will cause trouble. Was Pin SUPPOSED to be resilient to unsafe code? In any case, seems like a bug in DerefMut and Clone, not Pin. The others are a bit more esoteric and do seem potentially concerning, but I'm not sure. But still, I'm left with my earlier question: just how resilient is Pin supposed to be?
- kibwen 7y ago> Was Pin SUPPOSED to be resilient to unsafe code? Regardless, for a user to be able to trigger undefined behavior without using the `unsafe` keyword indicates a bug here that must be fixed at the level of the language or standard library.
- eximius 7y agoBut it does require unsafe? The implementation of DerefMut and Clone for the type being pinned require unsafe.
- steveklabnik 7y ago> Was Pin SUPPOSED to be resilient to unsafe code? Remember, unsafe does not mean "I can do whatever I want," it means "I am promising to uphold some guarantee on my own." That is, let's assume we have a function: /// Makes a new Foo. /// /// # Safety /// /// x must never be greater than 5 unsafe fn new(x: i32) -> Foo { and you write let x = 6; unsafe { new(x); } You have a bug, even though new is marked unsafe. In my understanding of the unsafe examples above, the unsafe code was upholding the invariants that it was required to uphold, and so would be more like having written `let x = 2;` in the above example, if that caused an issue, clearly there's a bug.
- eximius 7y agoI think this is a little too dumbed down for me to see the relevance to the actual problem. Also, I believ 1&2 both require unsafe code to implement the trait that allows the unsoundness. For what &T can I safely implement DerefMut? Is it the fault of Pin that a type has DerefMut implemented that the unsafe block of that implementation doesn't uphold safety?
- staticassertion 7y agoUnsoundness in Pin aside, I think the conversation between Boats and Ralph is more interesting - are soundness issues going to be so strange and edgecasey that they can be addressed as one-offs, or does rust need a more formal model to ensure edge cases are covered? I have no answer, it's just the only interesting part of that discussion imo. Everything else is just details of an issue that's too weird to really fully understand for me, and not novel or interesting enough to invest into understanding, anyway.
- withoutboats 7y ago(I was the primary designer of the Pin API.) Since (to a first approximation) every individual who has the expertise and contextual knowledge to really evaluate this issue is a poster on internals.rust-lang.org, its pretty surprising to find this thread on the front page of Hacker News. I imagine some Hacker News users who upvoted this link did so out of technical interest, but I suspect a large portion of the attention comes from some combination of these misconceptions: - The misconception that this could have a practical impact on users (the code being discussed on the thread is all obviously pathological & contrived). - The misconception that Rust's type system and standard library never contain soundness issues and that this is an exceptional event (in fact we have a number of longstanding soundness issues). We have a policy of fixing all soundness issues, so this issue will be fixed. In the meantime, while we decide the best solution, it will have no practical impact on Rust users. And none of the solutions we are considering would involve significant breakage to users, or invalidate any real code. At a high level: the soundness issue occurs because the Pin API was designed based on certain reasoning about the behavior of pointers. This reasoning would be sound but for the fact that we have allowed certain exceptions in relationship to pointers to what are called the "orphan rules" (which usually enable local reasoning like this). These exceptions allow users to introduce code which, while contrived, allows them to violate the guarantees of the Pin API. Such is life.
- tyingq 7y agoThe comments seem mostly about "technical interest".
- davesque 7y agoI think this is really the bottom line here. This "Pin soundness" matter really seems analogous to the process that any compiler project would go through to identify and fix obscure compiler bugs. I don't think it's quite so deserving of the amount of attention it's getting.
- temac 7y ago> The misconception that this could have a practical impact on users (the code being discussed on the thread is all obviously pathological & contrived). Famous last words? I mean I'm not an expert in Rust and even less in Pin, but I've seen my share of theoretical bugs thought of not possibly having any impact in the real world because of too theoretical. In other areas, when you debug a triple segfault and you understand the crazy conditions that lead to it, or when you render a piece of C++ code conforming instead of technically UB and it then starts to crash when in its UB form it worked perfectly, you start to consider that everything is possible :)