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

Area proposal: validity invariants #54

Merged
merged 4 commits into from Dec 13, 2018

Conversation

@RalfJung
Copy link
Member

RalfJung commented Dec 10, 2018

Which invariants derived from types are there that the compiler expects to be always maintained, and (equivalently) that unsafe code must always uphold (or else cause undefined behavior)? This is what is called "validity invariant" in my blog post.

Goals

  • For every primitive type, determine which assumptions (if any) the compiler makes about values not occurring at that type (serving as a lower bound for what to declare invalid), and determine which popular patterns in unsafe code might create "interesting" values of this type that safe code cannot create on its own (serving as an upper bound for how much we want to declare invalid). Both of these bounds are soft, but informative.
  • Based on that, map out a design space of invariants that seem reasonable.
  • Determine when exactly the validity invariant is assumed to hold.
RalfJung added 3 commits Dec 10, 2018
* Structs, tuples, arrays and all other aggregates (closures, ...)
* Is there anything to say besides: All fields must be valid at their
respective types?
* The padding between fields can be anything, including uninitialized. It was

This comment has been minimized.

Copy link
@rkruppe

rkruppe Dec 10, 2018

Member

Are generator fields (and more generally generator contents) exposed to user code at all? If not, this doesn't seem like something UCG have to say anything about, just pure rustc implementation details.

This comment has been minimized.

Copy link
@RalfJung

RalfJung Dec 10, 2018

Author Member

Are generator fields (and more generally generator contents) exposed to user code at all?

They are not, AFAIK.

But I think when we are in the business of type invariants, we should not forget about types like closures or generators. Just because the user cannot write them directly, doesn't mean their invariants are not important to know -- and compiler devs also need guidance for how to approach validity invariants.

And, of course, unsafe code could start to play games with these fields.

This comment has been minimized.

Copy link
@rkruppe

rkruppe Dec 11, 2018

Member

It's certainly a related issue, but one that interacts with generator implementation details much more than with user-facing guarantees or semantics of Rust-the-language, so I'm not sure the group of people here is the best to discuss it. So I think it would be reasonable to punt on it to reduce the scope of the validity invariant discussion and get it done more quickly. But we could also open the issue for generators and maybe end up wrapping up the discussion without any decisions being made about generators.

And, of course, unsafe code could start to play games with these fields.

Regardless of how generators end up being organized internally, I am quite certain they should be opaque, i.e., user code should not be allowed to poke at their contents in such a way.

This comment has been minimized.

Copy link
@gnzlbg

gnzlbg Dec 11, 2018

Collaborator

I always reasoned about closures as being equivalent to a struct that one could write by hand (and with feature(fn_traits) one actually can). The rules for building that struct are part of the language, but the layout, validity, etc. of this struct would follow from the layout and validity invariants that we specify here for primitive types, structs, etc.

I would find it extremely weird if the same wouldn't be true for generators. That is, the exact type of the Generator would be unspecified, but this type would be a normal Rust type, e.g., a struct or an union, with normal Rust fields (struct, unions, primitive types, etc.).

Otherwise, Generator would need to be a new kind of thing that isn't a struct, union, etc. and that would probably block people from writing user-defined Generators just like we can build "user-defined" closures.

This comment has been minimized.

Copy link
@RalfJung

RalfJung Dec 12, 2018

Author Member

we could also open the issue for generators and maybe end up wrapping up the discussion without any decisions being made about generators.

That seems reasonable. And I agree unsafe code shouldn't mess with implementation details of closures or generators, but that doesn't follow from them being in any way different than other struct -- it entirely follows from the fact that unsafe code must not make any assumption about that the struct (its fields etc) looks like.

"user code should not be allowed to poke at their contents in such a way" also applies to many, many other data types -- to pick an example, HashMap (or else we couldn't replace it by hashbrown as is being pursued right now).

@avadacatavra

This comment has been minimized.

Copy link
Collaborator

avadacatavra commented Dec 13, 2018

@RalfJung when you're happy with this, let's merge it

This discussion is meant to focus on the question: Which invariants derived from
types are there that the compiler expects to be *always* maintained, and
(equivalently) that unsafe code must *always* uphold (or else cause undefined
behavior)? This is what is called "validity invariant" in

This comment has been minimized.

Copy link
@nikomatsakis

nikomatsakis Dec 13, 2018

Collaborator

I'm curious whether there exist properties that unsafe code must always uphold but which it cannot rely upon. The idea would be: for now, we require that this is true, but we expect we may not require it forever. Technically, from the compiler's POV, we can tweak these predicates because that just makes less code UB -- but unsafe code could be relying on the fact that doing otherwise would be UB, and that could be a problem.

This seems like a more general thing -- it also e.g. arises in the reprsentation discussion -- but once we start getting into invariants, I expect we should think carefully about this distinction.

I would sort of like this to be noted somewhere as a kind of "cross-cutting concern" -- i.e., for each area, we are aiming to define these two predicates (what unsafe code must uphold, and what it can rely on) somewhat separately.

This comment has been minimized.

Copy link
@RalfJung

RalfJung Dec 13, 2018

Author Member

I agree in general. We want some "wiggle room" in our definition of what unsafe code can do, certainly when it comes to the safety invariant. I am less sure for the validity invariant.

My main problem with this is that I don't have a good understanding yet of how this works formally. That's mostly because I did not spend enough time to think about this.

@RalfJung RalfJung merged commit b34616c into rust-lang:master Dec 13, 2018
@RalfJung

This comment has been minimized.

Copy link
Member Author

RalfJung commented Dec 13, 2018

when you're happy with this, let's merge it

done

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
5 participants
You can’t perform that action at this time.