Stream: t-lang/wg-unsafe-code-guidelines

Topic: how-to-cope


nikomatsakis (Aug 24 2018 at 12:03, on Zulip):

So I was thinking about how to structure conversations and so forth. I wrote down some thoughts in this gist:

https://gist.github.com/nikomatsakis/13d7232609e6f6f86e0e1d4cc0afec99

I'm curious for feedback!

nikomatsakis (Aug 24 2018 at 12:03, on Zulip):

cc @RalfJ @avadacatavra

nikomatsakis (Aug 24 2018 at 12:04, on Zulip):

my goal was "lightweight process to allow us to actually make some progress" but my main concern is "overkill?"

nikomatsakis (Aug 24 2018 at 12:15, on Zulip):

updated gist with an actual example a discussion proposal

nikomatsakis (Aug 24 2018 at 12:35, on Zulip):

updated again

RalfJ (Aug 24 2018 at 12:36, on Zulip):

ah, process...^^

RalfJ (Aug 24 2018 at 12:36, on Zulip):

so would "validity of &mut T" be a separate discussion from "validity of i32"?

nikomatsakis (Aug 24 2018 at 12:37, on Zulip):

I envisioned that as a separate thread, but I'm open to suggestion

nikomatsakis (Aug 24 2018 at 12:37, on Zulip):

it might be that we want fewer, coarser threads

nikomatsakis (Aug 24 2018 at 12:37, on Zulip):

since a lot of times there is "cross-talk"

RalfJ (Aug 24 2018 at 12:37, on Zulip):

thread = discussion?

nikomatsakis (Aug 24 2018 at 12:37, on Zulip):

but one of the things I hoped with that process document was to allow us to customize this "per conversation", too

nikomatsakis (Aug 24 2018 at 12:37, on Zulip):

hmm no I imagined "discussion" as a bundle of related threads :)

nikomatsakis (Aug 24 2018 at 12:38, on Zulip):

I should probably make that clearer

avadacatavra (Aug 24 2018 at 12:38, on Zulip):

@RalfJ do you have a repo for the valgrind stuff? i think we should also have pointers to related projects

nikomatsakis (Aug 24 2018 at 12:38, on Zulip):

"discussion area", perhaps

nikomatsakis (Aug 24 2018 at 12:38, on Zulip):

@RalfJ did you look at my example proposal?

avadacatavra (Aug 24 2018 at 12:40, on Zulip):

@nikomatsakis re "Relationship to Rust reference" it's not clear to me that the unsafe code guidelines document is the mdbook in the repo (which i'm assuming it is?)

avadacatavra (Aug 24 2018 at 12:42, on Zulip):

also--are we thinking next week for the official reboot launch discussion?

nikomatsakis (Aug 24 2018 at 12:45, on Zulip):

yeah I should probably change the rpeo a bit to match

nikomatsakis (Aug 24 2018 at 12:45, on Zulip):

but I meant the mdbook in the repo

nikomatsakis (Aug 24 2018 at 12:45, on Zulip):

and probably the "active discussions" should not be part of the mdbook

RalfJ (Aug 24 2018 at 12:46, on Zulip):

@nikomatsakis oO that's a HUGE amount of things discussed together

RalfJ (Aug 24 2018 at 12:46, on Zulip):

TBH I would separate out safety invariants entierly

nikomatsakis (Aug 24 2018 at 12:46, on Zulip):

I was wondering about that

RalfJ (Aug 24 2018 at 12:46, on Zulip):

they need so much machinery to talk about precisely

nikomatsakis (Aug 24 2018 at 12:47, on Zulip):

yeah

nikomatsakis (Aug 24 2018 at 12:47, on Zulip):

seems good to me

nikomatsakis (Aug 24 2018 at 12:47, on Zulip):

one thing I was thinking as I biked home is

RalfJ (Aug 24 2018 at 12:47, on Zulip):

and we have a lock-in problem, where we cannot ever strneghten or weaken then -- and I still wonder if there is a mechanism to achiebve that

nikomatsakis (Aug 24 2018 at 12:47, on Zulip):

it's also fine for there to be open issues accumulating thoughts (or threads, etc)

nikomatsakis (Aug 24 2018 at 12:47, on Zulip):

but I'd prefer that I at least don't have to pay as much attention to those

nikomatsakis (Aug 24 2018 at 12:47, on Zulip):

that is, the "this is the active area of discussion" idea is meant to help both steer but also ensure we make progress on something at any moment

RalfJ (Aug 24 2018 at 12:48, on Zulip):

hehe

nikomatsakis (Aug 24 2018 at 12:48, on Zulip):

(point being: if we accumualte thoughts about safety invariants as we go, we can note those down elsewhere)

nikomatsakis (Aug 24 2018 at 12:48, on Zulip):

and we have a lock-in problem, where we cannot ever strneghten or weaken then -- and I still wonder if there is a mechanism to achiebve that

it seems to me that all invariants have some measure of this problem

RalfJ (Aug 24 2018 at 12:48, on Zulip):

yeah seems okay to have a place

nikomatsakis (Aug 24 2018 at 12:48, on Zulip):

that is, if we say that the validity invariant is X, then there will be safe code that maintains X; we can weaken X (which I guess is your point?)

nikomatsakis (Aug 24 2018 at 12:49, on Zulip):

but we certainly can't strengthen X?

RalfJ (Aug 24 2018 at 12:49, on Zulip):

but given how often people confuse these invariants, it should be somewhat separate

nikomatsakis (Aug 24 2018 at 12:49, on Zulip):

I'm not convinced we can even weaken X really

nikomatsakis (Aug 24 2018 at 12:49, on Zulip):

i.e., unsafe code might be doing things that are only correct if X is true

RalfJ (Aug 24 2018 at 12:49, on Zulip):

yeah we can make more stuff valid is what I mean

RalfJ (Aug 24 2018 at 12:49, on Zulip):

not the other way around of course

RalfJ (Aug 24 2018 at 12:49, on Zulip):

but for safety we do not even have that

nikomatsakis (Aug 24 2018 at 12:49, on Zulip):

I see, the reason being:

nikomatsakis (Aug 24 2018 at 12:49, on Zulip):

unsafe code assumes (at boundaries) the the full safety invariant holds

RalfJ (Aug 24 2018 at 12:49, on Zulip):

unsafe code has a manually written precondition

nikomatsakis (Aug 24 2018 at 12:50, on Zulip):

and else that

RalfJ (Aug 24 2018 at 12:50, on Zulip):

and if we make more things valid, previously calling that unsafe code with invalid things was UB

nikomatsakis (Aug 24 2018 at 12:50, on Zulip):

right, ok I see

RalfJ (Aug 24 2018 at 12:50, on Zulip):

and so we can do whatever

nikomatsakis (Aug 24 2018 at 12:50, on Zulip):

in other words:

RalfJ (Aug 24 2018 at 12:50, on Zulip):

basically wekaning validity only can affect programs that previously violated validity

RalfJ (Aug 24 2018 at 12:50, on Zulip):

and those were UB

nikomatsakis (Aug 24 2018 at 12:50, on Zulip):

if unsafe code is relying on the validity invariant holding

nikomatsakis (Aug 24 2018 at 12:50, on Zulip):

that is (in principle, at least) something that would be stated by "copying" the current validity invariant as a precondition

RalfJ (Aug 24 2018 at 12:50, on Zulip):

all code is relying on the validity invariant holding. this is not even a question

nikomatsakis (Aug 24 2018 at 12:51, on Zulip):

well, if we weakened it...

nikomatsakis (Aug 24 2018 at 12:51, on Zulip):

that is, if we made more things valid

RalfJ (Aug 24 2018 at 12:51, on Zulip):

ah I think I see what you mean

RalfJ (Aug 24 2018 at 12:51, on Zulip):

yes. if unsafe code says "call me on any valid data", that cannot be weakened together with the actual validity the compiler relies on

RalfJ (Aug 24 2018 at 12:52, on Zulip):

regarding the confusion of the two invariants, I am amazed people seemed to have picked up my terminology so I hope that helps a bit^^

nikomatsakis (Aug 24 2018 at 12:53, on Zulip):

concrete example:

nikomatsakis (Aug 24 2018 at 12:53, on Zulip):

if we said "from now on, &T may be unaligned"

nikomatsakis (Aug 24 2018 at 12:53, on Zulip):

we could adjust our codegen

nikomatsakis (Aug 24 2018 at 12:53, on Zulip):

but others might still be using the old one

nikomatsakis (Aug 24 2018 at 12:54, on Zulip):

(or packing things in the low bits)

nikomatsakis (Aug 24 2018 at 12:55, on Zulip):

PS I think what we ought to do is to define not just one validity invariant

nikomatsakis (Aug 24 2018 at 12:56, on Zulip):

well, it depends of course

nikomatsakis (Aug 24 2018 at 12:56, on Zulip):

but we may find places where we say "you must guarantee this is true, but you can't rely on it being true"

nikomatsakis (Aug 24 2018 at 12:56, on Zulip):

I think i'll bring this up on internals, a bit off topic here :)

nikomatsakis (Aug 24 2018 at 12:59, on Zulip):

posted

RalfJ (Aug 24 2018 at 13:10, on Zulip):

I have a hard time with those "must guarantee but cannot rely"

RalfJ (Aug 24 2018 at 13:11, on Zulip):

how would a def.n of UB for that look like?

RalfJ (Aug 24 2018 at 13:19, on Zulip):

^^

avadacatavra (Aug 24 2018 at 13:20, on Zulip):

FYI: we can stick this poll into the announcement: https://doodle.com/poll/ruur88tf99stspzu#calendar

nikomatsakis (Aug 24 2018 at 15:47, on Zulip):

posted: https://internals.rust-lang.org/t/proposal-for-unsafe-code-guidelines-process/8294/2

Last update: Nov 20 2019 at 11:50UTC