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

Topic: Meeting-2019-03-14


avadacatavra (Mar 14 2019 at 15:16, on Zulip):

Happy Thursday!

Alan Jeffrey (Mar 14 2019 at 15:16, on Zulip):

:wave:

Nicole Mazzuca (Mar 14 2019 at 15:16, on Zulip):

(* waves *)

nikomatsakis (Mar 14 2019 at 15:17, on Zulip):

cc @WG-unsafe-code-guidelines

gnzlbg (Mar 14 2019 at 15:17, on Zulip):

hi

avadacatavra (Mar 14 2019 at 15:17, on Zulip):

Everyone ready for a meeting?

gnzlbg (Mar 14 2019 at 15:17, on Zulip):

in one hour or now ?

nikomatsakis (Mar 14 2019 at 15:18, on Zulip):

(In calendar, the meeting is pegged to US time, so now.)

avadacatavra (Mar 14 2019 at 15:18, on Zulip):

@gnzlbg in portland

gnzlbg (Mar 14 2019 at 15:19, on Zulip):

so i'm ready I think I was notified that the meeting changed time but didn't register it mentally :D

nikomatsakis (Mar 14 2019 at 15:20, on Zulip):

Reminder: I just wanted to mention the lang team sync meeting which takes place in 3.5 hours. The write-up of current status is here, if you have any comments, changes, or additions they would be welcome (or thoughts on specific questions you'd like to add).

avadacatavra (Mar 14 2019 at 15:24, on Zulip):

Ok so, how is validity going?

avadacatavra (Mar 14 2019 at 15:24, on Zulip):

have we had enough discussions to do some writeups

nikomatsakis (Mar 14 2019 at 15:24, on Zulip):

From the meeting notes:

[np]: http://smallcultfollowing.com/babysteps/blog/2018/08/13/never-patterns-exhaustive-matching-and-uninhabited-types-oh-my/

nikomatsakis (Mar 14 2019 at 15:24, on Zulip):

but that's all I know ;)

nikomatsakis (Mar 14 2019 at 15:25, on Zulip):

we had talked about trying to do some sort of summary

nikomatsakis (Mar 14 2019 at 15:25, on Zulip):

to help "collect" the discussions on ints/references

nikomatsakis (Mar 14 2019 at 15:26, on Zulip):

as described here

nikomatsakis (Mar 14 2019 at 15:26, on Zulip):

but we don't really have a plan for who will do that afaik

avadacatavra (Mar 14 2019 at 15:27, on Zulip):

hmm...i want to volunteer but i've been pretty swamped. i could create a db paper and share the link so that if i start and then get swamped, it doesn't get lost?

gnzlbg (Mar 14 2019 at 15:27, on Zulip):

one point about validity that i always mention is teachability, how easy / hard will it be to explain to somebody what must always hold, validity wise.

avadacatavra (Mar 14 2019 at 15:28, on Zulip):

ok...so it does seem like we're ready to do writeups for validity

nikomatsakis (Mar 14 2019 at 15:28, on Zulip):

hmm...i want to volunteer but i've been pretty swamped. i could create a db paper and share the link so that if i start and then get swamped, it doesn't get lost?

seems like a good start =)

avadacatavra (Mar 14 2019 at 15:29, on Zulip):

which is good to hear

nikomatsakis (Mar 14 2019 at 15:29, on Zulip):

one point about validity that i always mention is teachability, how easy / hard will it be to explain to somebody what must always hold, validity wise.

one question I have

RalfJ (Mar 14 2019 at 15:29, on Zulip):

hi all! sorry, I missed that mtg is 1h earlier today

nikomatsakis (Mar 14 2019 at 15:29, on Zulip):

@RalfJ's original wrote-up talked some about what it means for something to "always" hold

nikomatsakis (Mar 14 2019 at 15:29, on Zulip):

have we discussed that very much?

avadacatavra (Mar 14 2019 at 15:29, on Zulip):

i don't think we have

avadacatavra (Mar 14 2019 at 15:30, on Zulip):

do we mean that for any execution of a program it will hold?

nikomatsakis (Mar 14 2019 at 15:30, on Zulip):

(is there controversy?)

gnzlbg (Mar 14 2019 at 15:30, on Zulip):

i think we kind of just accepted it, as in, if some invariant does not always need to hold, then it is not a validity invariant

nikomatsakis (Mar 14 2019 at 15:30, on Zulip):

I find it kind of unclear in my head, somehow. but I guess it means, roughly, "on every access"

RalfJ (Mar 14 2019 at 15:30, on Zulip):

wdym "any execution"?

gnzlbg (Mar 14 2019 at 15:31, on Zulip):

i understood that they must hold even if there is no access

RalfJ (Mar 14 2019 at 15:31, on Zulip):

if the program is non-deterministic, validity is like OOB or other kinds of UB... if there is a a way to make it happen, then it happens

RalfJ (Mar 14 2019 at 15:31, on Zulip):

i understood that they hold even if there is no access

the problem is defining what that means

RalfJ (Mar 14 2019 at 15:31, on Zulip):

memory is not typed

RalfJ (Mar 14 2019 at 15:32, on Zulip):

so only at an access do we have a type and a location and can verify that the memory at that location matches the type

gnzlbg (Mar 14 2019 at 15:32, on Zulip):

let b: bool = transmute(3); // === unreachable

RalfJ (Mar 14 2019 at 15:32, on Zulip):

we have an issue about that...

RalfJ (Mar 14 2019 at 15:32, on Zulip):

here: https://github.com/rust-lang/unsafe-code-guidelines/issues/84

RalfJ (Mar 14 2019 at 15:32, on Zulip):

@gnzlbg there is a bad access there: when the 3 gets written to b as type bool

RalfJ (Mar 14 2019 at 15:32, on Zulip):

so that one is UB even with an "only at accesses" model

avadacatavra (Mar 14 2019 at 15:33, on Zulip):

so are there different models of 'always'?

RalfJ (Mar 14 2019 at 15:33, on Zulip):

(= is a typed operation, and it acts at type bool here)

RalfJ (Mar 14 2019 at 15:33, on Zulip):

@avadacatavra well look at https://github.com/rust-lang/unsafe-code-guidelines/issues/84

nikomatsakis (Mar 14 2019 at 15:33, on Zulip):

I guess a "tricky" case might be if you had a *mut T pointing at some memory and you modified it (via some alias) to not be a valid T, but you never use the reference again, right?

RalfJ (Mar 14 2019 at 15:33, on Zulip):

there are examples there of things that are not UB according to Miri or any model I have designed or seen so far

nikomatsakis (Mar 14 2019 at 15:33, on Zulip):

anyway, I'll read ucg#84

RalfJ (Mar 14 2019 at 15:33, on Zulip):

but would be UB under some informal idea of "always"

RalfJ (Mar 14 2019 at 15:34, on Zulip):

I guess a "tricky" case might be if you had a *mut T pointing at some memory and you modified it (via some alias) to not be a valid T, but you never use the reference again, right?

yeah that's exactly what the issue is about

gnzlbg (Mar 14 2019 at 15:34, on Zulip):

ah I remember #84

avadacatavra (Mar 14 2019 at 15:34, on Zulip):

/me feels an existential crisis coming on

RalfJ (Mar 14 2019 at 15:34, on Zulip):

why that?^^

nikomatsakis (Mar 14 2019 at 15:34, on Zulip):

ps ucg#84 should work now as a shorthand

gnzlbg (Mar 14 2019 at 15:35, on Zulip):

so this is tricky

nikomatsakis (Mar 14 2019 at 15:35, on Zulip):

anyway we don't have to work out the details, I mostly wanted to ensure this question was not overlooked:)

nikomatsakis (Mar 14 2019 at 15:35, on Zulip):

(though we can also discuss, if there aren't other things)

avadacatavra (Mar 14 2019 at 15:36, on Zulip):

i would say the other thing would be (since we seem to be ready for writeups) WHAT'S NEXT

gnzlbg (Mar 14 2019 at 15:36, on Zulip):

PRs ?

RalfJ (Mar 14 2019 at 15:36, on Zulip):

also this reminds me I still have to set up a sandbox for Zoom... or is there an opensource client?

gnzlbg (Mar 14 2019 at 15:37, on Zulip):

@nikomatsakis and @Nicole Mazzuca wanted to read the layout of array and we wanted to merge it afterwards if there weren't any issues

RalfJ (Mar 14 2019 at 15:37, on Zulip):

i would say the other thing would be (since we seem to be ready for writeups) WHAT'S NEXT

you mean after validity?

avadacatavra (Mar 14 2019 at 15:37, on Zulip):

yeah

RalfJ (Mar 14 2019 at 15:37, on Zulip):

there's a lot of writeup still needing to be done, not sure if I am ready to look that far ahead^^

Nicole Mazzuca (Mar 14 2019 at 15:37, on Zulip):

ah, sorry, I did that and it read well

avadacatavra (Mar 14 2019 at 15:38, on Zulip):

@RalfJ to be clear i'm not saying we're moving on yet, but we should start thinking about what the next topic should be

avadacatavra (Mar 14 2019 at 15:38, on Zulip):

also--who will be at rustconf?

gnzlbg (Mar 14 2019 at 15:38, on Zulip):

@avadacatavra once validity and layout are ironed out, we should probably have a sprint to polish the book, ideally in such a form that can be RFC'ed

gnzlbg (Mar 14 2019 at 15:38, on Zulip):

but I don't think we are there yet

RalfJ (Mar 14 2019 at 15:38, on Zulip):

yeah

RalfJ (Mar 14 2019 at 15:39, on Zulip):

/me checks when RustConf is

nikomatsakis (Mar 14 2019 at 15:39, on Zulip):

One thing that comes to mind is that

nikomatsakis (Mar 14 2019 at 15:40, on Zulip):

there may be value in pursuing stacked borrows more, not 100% sure what that means

avadacatavra (Mar 14 2019 at 15:40, on Zulip):

so, i won't be at rustconf (my best friend is getting married). but if there's enough interest, i'll facilitate some wg face to face meetings

RalfJ (Mar 14 2019 at 15:40, on Zulip):

uh, RustConf overlaps witrh ICFP

nikomatsakis (Mar 14 2019 at 15:40, on Zulip):

e.g., I was thinking about the controversy around NLL and two-phase borrows, which relates to stacked borrows

RalfJ (Mar 14 2019 at 15:40, on Zulip):

and with ICFP being in Berlin, I should really go there

RalfJ (Mar 14 2019 at 15:40, on Zulip):

so I won't be at RustConf, I'm afraid

RalfJ (Mar 14 2019 at 15:41, on Zulip):

does it make sense to tackle stacked borrows when we dont even have a memory model or a MIR model?

gnzlbg (Mar 14 2019 at 15:41, on Zulip):

@nikomatsakis pursuing stacked borrows more before the first RFC?

RalfJ (Mar 14 2019 at 15:42, on Zulip):

also we have a couple open questions in the ucg repo

RalfJ (Mar 14 2019 at 15:42, on Zulip):

and some more in the old repo (that we should migrate)

gnzlbg (Mar 14 2019 at 15:44, on Zulip):

i think it definetely makes sense to continue to pursue stacked borrows in miri, but I recall I had some questions about it that weren't easy to answer without a MIR model

nikomatsakis (Mar 14 2019 at 15:44, on Zulip):

nikomatsakis pursuing stacked borrows more before the first RFC?

not as a blocker for first RFC

nikomatsakis (Mar 14 2019 at 15:44, on Zulip):

more as a "next area to focus on" after RFC

nikomatsakis (Mar 14 2019 at 15:44, on Zulip):

I'm not sure if that is the right thing though

RalfJ (Mar 14 2019 at 15:46, on Zulip):

re: ref/int; if we can disentangle them then maybe doing it the usual GH style is not actually so bad. but it might anyway be worth experimenting with dropbox paper

gnzlbg (Mar 14 2019 at 15:46, on Zulip):

I think that's the long term goal, so it makes sense to work out the steps required to get there

RalfJ (Mar 14 2019 at 15:46, on Zulip):

like, if @gnzlbg did the struct/enum stuff there, that'd make it much easier for me to to drive-by fixes

RalfJ (Mar 14 2019 at 15:46, on Zulip):

and paper has a "comment" thing, right?

RalfJ (Mar 14 2019 at 15:47, on Zulip):

we should just try not to have technical discussions there

RalfJ (Mar 14 2019 at 15:47, on Zulip):

they should be moved back to the existing or a new GH issue

avadacatavra (Mar 14 2019 at 15:47, on Zulip):

ok, so:
- meeting with lang team later today
- gnzlbg doing some writeups (enum, struct, array)
- i'll start the other one (int, refs, etc) and share a link
- stacked borrows next?
- work on RFC (what will this cover--draft in paper?)

RalfJ (Mar 14 2019 at 15:47, on Zulip):

and we often end up discussing technical stuff in the GH PR... hm

gnzlbg (Mar 14 2019 at 15:49, on Zulip):

that feels unavoidable, when there is a prototype of the spec new issues always show up

RalfJ (Mar 14 2019 at 15:49, on Zulip):

i'll start the other one (int, refs, etc) and share a link

cool! I figured I'd have to do that.^^

RalfJ (Mar 14 2019 at 15:50, on Zulip):

that feels unavoidable, when there is a prototype of the spec new issues always show up

yeah. and paper isn't very good for that.

gnzlbg (Mar 14 2019 at 15:50, on Zulip):

so anything else ?

avadacatavra (Mar 14 2019 at 15:51, on Zulip):

/me needs more tea now

gnzlbg (Mar 14 2019 at 15:51, on Zulip):

I just checked and travis-ci is disabled for the repo in the rust-lang/ org

nikomatsakis (Mar 14 2019 at 15:51, on Zulip):

I can fix that, probably

nikomatsakis (Mar 14 2019 at 15:51, on Zulip):

and paper has a "comment" thing, right?

I'm a big fan of paper's comment thing

nikomatsakis (Mar 14 2019 at 15:51, on Zulip):

we should just try not to have technical discussions there

but yes this

avadacatavra (Mar 14 2019 at 15:51, on Zulip):

i do all of my blog post drafting in paper now

nikomatsakis (Mar 14 2019 at 15:54, on Zulip):

I just checked and travis-ci is disabled for the repo in the rust-lang/ org

fixed

gnzlbg (Mar 14 2019 at 15:54, on Zulip):

thanks

nikomatsakis (Mar 14 2019 at 15:54, on Zulip):

although I probably have to edit the travis config

nikomatsakis (Mar 14 2019 at 15:54, on Zulip):

to add back the encrypted token thing

gnzlbg (Mar 14 2019 at 15:54, on Zulip):

yes :/

gnzlbg (Mar 14 2019 at 15:55, on Zulip):

i'd like to propose something for the next meeting: triaging all still open repr-issues. It seems to me that some of them are already fixed, some need fixing before an RFC, and some would require RFCs of their own.

RalfJ (Mar 14 2019 at 15:57, on Zulip):

I dont understand the distinction between the last two

nikomatsakis (Mar 14 2019 at 15:58, on Zulip):

i'd like to propose something for the next meeting: triaging all still open repr-issues. It seems to me that some of them are already fixed, some need fixing before an RFC, and some would require RFCs of their own.

I like the idea of going over them, regardless.

gnzlbg (Mar 14 2019 at 15:59, on Zulip):

@RalfJ for example we might want to guarantee further enum optimizations, but those don't need to be part of the first UCG RFC

gnzlbg (Mar 14 2019 at 15:59, on Zulip):

as in the first UCG RFC documents what we already guarantee, but proposing new guaranteed enum layout optimizations might be better done on its own RFC

RalfJ (Mar 14 2019 at 16:01, on Zulip):

I see. so those would be issue we'd leave open for now, not blocking The RFC.

gnzlbg (Mar 14 2019 at 16:02, on Zulip):

yes

gnzlbg (Mar 14 2019 at 16:20, on Zulip):

@nikomatsakis so travis works again, is the GITHUB_TOKEN set up?

Last update: Nov 19 2019 at 17:45UTC