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

Topic: meeting-2019-03-07


nikomatsakis (Mar 07 2019 at 16:10, on Zulip):

Meeting today in a few minutes @WG-unsafe-code-guidelines

## Agenda Nominations

nikomatsakis (Mar 07 2019 at 16:10, on Zulip):
nikomatsakis (Mar 07 2019 at 16:10, on Zulip):

(Feel free to add your own :)

nikomatsakis (Mar 07 2019 at 16:10, on Zulip):
gnzlbg (Mar 07 2019 at 16:10, on Zulip):
nikomatsakis (Mar 07 2019 at 16:11, on Zulip):
RalfJ (Mar 07 2019 at 16:19, on Zulip):

hi there! sorry I'm late (and then Zulip had connection issues)

RalfJ (Mar 07 2019 at 16:19, on Zulip):
RalfJ (Mar 07 2019 at 16:22, on Zulip):

hello?

nikomatsakis (Mar 07 2019 at 16:22, on Zulip):

Hi =)

nikomatsakis (Mar 07 2019 at 16:22, on Zulip):

OK, ;let's do it -- @avadacatavra you around?

nikomatsakis (Mar 07 2019 at 16:23, on Zulip):

ok, to start here, I am still trying to organize this idea of a "lang team sync meeting" -- and in general to broadcast more to the outside world what we've been up to

nikomatsakis (Mar 07 2019 at 16:23, on Zulip):

I posted a draft write-up summarizing where we are, what's happened so far

nikomatsakis (Mar 07 2019 at 16:23, on Zulip):

I'd love feedback

nikomatsakis (Mar 07 2019 at 16:24, on Zulip):

It's missing in particular some concept of the current discussion area because -- frankly -- I've not been able to follow along =(

RalfJ (Mar 07 2019 at 16:24, on Zulip):

I'm afraid I didn't yet have time to read it, sorry

nikomatsakis (Mar 07 2019 at 16:24, on Zulip):

Yeah, that's fine, do you think you will have time?

nikomatsakis (Mar 07 2019 at 16:24, on Zulip):

It's not super long :)

nikomatsakis (Mar 07 2019 at 16:24, on Zulip):

If not, that's ok too, but good to know :)

RalfJ (Mar 07 2019 at 16:25, on Zulip):

after I finish writing my thesis proposal, I guess

RalfJ (Mar 07 2019 at 16:25, on Zulip):

or maybe on the weekend when I dont feel like working^^

nikomatsakis (Mar 07 2019 at 16:25, on Zulip):

When do you anticipate finishing up your thesis proposal, if you have an estimate?

nikomatsakis (Mar 07 2019 at 16:25, on Zulip):

I'm not thining now so much of that document as about the idea of a sync in general

nikomatsakis (Mar 07 2019 at 16:26, on Zulip):

(i.e., should I just expect you're too busy to participate, which would probably be fine)

RalfJ (Mar 07 2019 at 16:26, on Zulip):

I hope to get it done next week, I've been pushing it ahead way too long

nikomatsakis (Mar 07 2019 at 16:26, on Zulip):

ok, I agree you should prioritize that :)

nikomatsakis (Mar 07 2019 at 16:26, on Zulip):

ok, that's all I had to say on that topic I guess

RalfJ (Mar 07 2019 at 16:26, on Zulip):

but it's not like I'll be less busy afterwards^^ I'll likely have a paper and a talk to write until the end of the month...

nikomatsakis (Mar 07 2019 at 16:26, on Zulip):

Maybe a few quick notes on this? It would help me in finishing up the write-up, if nothing else

RalfJ (Mar 07 2019 at 16:28, on Zulip):

hm yeah. basically the boring stuff is boring as expected -- the composed types, like enums structs, arrays and so on (@gnzlbg volunteered to do a writeup for them)

RalfJ (Mar 07 2019 at 16:28, on Zulip):

and then for integers and references we basically have pretty much every possible opinion represented

nikomatsakis (Mar 07 2019 at 16:28, on Zulip):

lol ok

RalfJ (Mar 07 2019 at 16:28, on Zulip):

oh and then unions^^

nikomatsakis (Mar 07 2019 at 16:28, on Zulip):

I guess the question is whether we can get away from the opinions to maybe principles or tests we can use to discriminate between them

RalfJ (Mar 07 2019 at 16:28, on Zulip):

these are the three big open questions

RalfJ (Mar 07 2019 at 16:29, on Zulip):

"tests"?

nikomatsakis (Mar 07 2019 at 16:29, on Zulip):

but ok so -- integers, references, and unions are the big "open questions"

nikomatsakis (Mar 07 2019 at 16:29, on Zulip):

"tests"?

I mean .. not like "test cases" .. but like "decision criteria"

nikomatsakis (Mar 07 2019 at 16:29, on Zulip):

I'm imagining things like "doing X is a common pattern in C FFI and we want to preserve those" etc

nikomatsakis (Mar 07 2019 at 16:30, on Zulip):

it might be interesting to try and tease out the values people are using to back their positions

nikomatsakis (Mar 07 2019 at 16:30, on Zulip):

so we can try to judge based on those

nikomatsakis (Mar 07 2019 at 16:30, on Zulip):

partly just thinking out loud

RalfJ (Mar 07 2019 at 16:30, on Zulip):

there are some I guess, though not at all like that

nikomatsakis (Mar 07 2019 at 16:30, on Zulip):

I guess an obvious next step, put another way, is try to summarize current thread thus far

nikomatsakis (Mar 07 2019 at 16:30, on Zulip):

points of agreement / disagreement etc

RalfJ (Mar 07 2019 at 16:30, on Zulip):

@Taylor Cramer wants all the layout optimizations, @centril wants the strongest possible invariant, and I want an implementation in Miri.

nikomatsakis (Mar 07 2019 at 16:30, on Zulip):

I might be game to do some of that, just to help me catch up

nikomatsakis (Mar 07 2019 at 16:30, on Zulip):

Taylor Cramer wants all the layout optimizations, centril wants the strongest possible invariant, and I want an implementation in Miri.

perfect :)

nikomatsakis (Mar 07 2019 at 16:31, on Zulip):

I guess an obvious next step, put another way, is try to summarize current thread thus far

this is something where, if we were going to have a public sync, we could put this as a "please help, we need this"

gnzlbg (Mar 07 2019 at 16:31, on Zulip):

I’m still not convinced about what to do with integers validity wise (in either direction)

RalfJ (Mar 07 2019 at 16:31, on Zulip):

some of the integer and reference decisions are intertwined

gnzlbg (Mar 07 2019 at 16:31, on Zulip):

Both paths seem to require large trade offs

nikomatsakis (Mar 07 2019 at 16:32, on Zulip):

(I'm adding the :point_up: emoji to my own comment, not to make it look like the world agrees with me, but to help me find it later when preparing a summary of the meeting :)

RalfJ (Mar 07 2019 at 16:32, on Zulip):

yeah I was about to say, most people (I think) agree we want to keep &mut [u8] to uninitialized data non-UB (which can be achieved in several ways), but @gnzlbg doesn't agree

nikomatsakis (Mar 07 2019 at 16:33, on Zulip):

are we able to write-up partial summaries, and to isolate areas of disagreemnt into new issues?

nikomatsakis (Mar 07 2019 at 16:33, on Zulip):

or are the questions too...atomic to permit that

RalfJ (Mar 07 2019 at 16:33, on Zulip):

not sure how new issues would help

RalfJ (Mar 07 2019 at 16:33, on Zulip):

we kind of already have one issue for all of these 3 open questions

RalfJ (Mar 07 2019 at 16:33, on Zulip):

and the integer and reference thing is somewhat connected, I dont think splitting more will help

nikomatsakis (Mar 07 2019 at 16:33, on Zulip):

ok, it's not that I think "new issues" will help, it's that I'm trying to understand if there are like N details and people agree on most of them, but for 1 or 2 that it would be helpful to isolate

nikomatsakis (Mar 07 2019 at 16:34, on Zulip):

sounds like no

RalfJ (Mar 07 2019 at 16:34, on Zulip):

(namely, we could allow &mut [u8] to uninitialized data either by allowing uninitialized integers, or by making references non-recursive wrt. validity)

RalfJ (Mar 07 2019 at 16:34, on Zulip):

ok, it's not that I think "new issues" will help, it's that I'm trying to understand if there are like N details and people agree on most of them, but for 1 or 2 that it would be helpful to isolate

yeah I don't think so. this is all one big connected mess.

gnzlbg (Mar 07 2019 at 16:35, on Zulip):

FWIW it's not that i disagree with that, but that I think that this trade-offs convenience with teachability, and i'm not convinced that's the right tradeoff

RalfJ (Mar 07 2019 at 16:35, on Zulip):

and it has spider arms that connect to things like ptr::freeze

gnzlbg (Mar 07 2019 at 16:35, on Zulip):

Arguments for both sides have been given by pretty much everyone that commented, and I have the feeling a lot of people changed their minds after the all hands

gnzlbg (Mar 07 2019 at 16:35, on Zulip):

but i failed to understand what made them change their minds

gnzlbg (Mar 07 2019 at 16:36, on Zulip):

so maybe a summary comment explaining that would help

RalfJ (Mar 07 2019 at 16:36, on Zulip):

FWIW it's not that i disagree with that, but that I think that this trade-offs convenience with teachability, and i'm not convinced that's the right tradeoff

what I meant to say is that you don't agree with allowing it.

nikomatsakis (Mar 07 2019 at 16:36, on Zulip):

it sounds to me like there has been a lot of conversation and the participants have a good understanding of the "map"

RalfJ (Mar 07 2019 at 16:36, on Zulip):

Arguments for both sides have been given by pretty much everyone that commented, and I have the feeling a lot of people changed their minds after the all hands

really?

nikomatsakis (Mar 07 2019 at 16:36, on Zulip):

and so it would be good to try and write it out

gnzlbg (Mar 07 2019 at 16:37, on Zulip):

Arguments for both sides have been given by pretty much everyone that commented, and I have the feeling a lot of people changed their minds after the all hands

really?

IIRC you were arguing in favor of invalid only within unions before

RalfJ (Mar 07 2019 at 16:37, on Zulip):

FWIW, unions are probably closest to an agreement, but that's also the most isolated discussion

RalfJ (Mar 07 2019 at 16:37, on Zulip):

you were arguing in favor of invalid only within unions before

ah right

nikomatsakis (Mar 07 2019 at 16:37, on Zulip):

Sounds like we could have one summary of the union position, and one summary of ints/references?

RalfJ (Mar 07 2019 at 16:37, on Zulip):

yeah I think I've just seen too much code in the wild that has invalid integers

RalfJ (Mar 07 2019 at 16:38, on Zulip):

(all the Read::read stuff, and then the tricks that AtomicCell is playing)

nikomatsakis (Mar 07 2019 at 16:38, on Zulip):

let's move on from this maybe? I think meeting will end soon

gnzlbg (Mar 07 2019 at 16:38, on Zulip):

Like @RalfJ I think the issue with validity is that the issues are intertwined, and also might interact with layout optimizations, so maybe a holistic summary about what issues are there and how they interact might be better than summarizing each of the things, except for unions, structs, etc. where things are clearer

nikomatsakis (Mar 07 2019 at 16:39, on Zulip):

I can try to follow up with this @gnzlbg =)

RalfJ (Mar 07 2019 at 16:39, on Zulip):

the union stuff interacts with layout

RalfJ (Mar 07 2019 at 16:39, on Zulip):

but int/ref doesn't

nikomatsakis (Mar 07 2019 at 16:39, on Zulip):

Like RalfJ I think the issue with validity is that the issues are intertwined, and also might interact with layout optimizations, so maybe a holistic summary about what issues are there and how they interact might be better than summarizing each of the things, except for unions, structs, etc. where things are clearer

ok this is one of the questions I wanted to get at

nikomatsakis (Mar 07 2019 at 16:39, on Zulip):

whether we can separate or not

RalfJ (Mar 07 2019 at 16:39, on Zulip):

must be like the only thing it doesnt interact with :P

nikomatsakis (Mar 07 2019 at 16:39, on Zulip):

I would then like to reframe the discussion from

nikomatsakis (Mar 07 2019 at 16:39, on Zulip):

arguing for alternatives

nikomatsakis (Mar 07 2019 at 16:39, on Zulip):

to producing a well-structued summary of the intertwined considerations

nikomatsakis (Mar 07 2019 at 16:39, on Zulip):

and then we can get back to arguing :)

RalfJ (Mar 07 2019 at 16:40, on Zulip):

that's hard though

gnzlbg (Mar 07 2019 at 16:40, on Zulip):

might be a good idea to add it as a PR, and incrementally grow it, and then post it in the active discussion

nikomatsakis (Mar 07 2019 at 16:40, on Zulip):

exactly...

gnzlbg (Mar 07 2019 at 16:40, on Zulip):

let's try to collect each argument only once

nikomatsakis (Mar 07 2019 at 16:40, on Zulip):

right, I'm imagining taking an initial stab in a PR or Dropbox paper, and then having some collaboration on elaborating it

RalfJ (Mar 07 2019 at 16:41, on Zulip):

paper might even be better here, that's easier to edit collaboratively

RalfJ (Mar 07 2019 at 16:41, on Zulip):

I think it's less about arguments and more about "here are all sorts of things that depend on this decision"

nikomatsakis (Mar 07 2019 at 16:42, on Zulip):

yes I know

nikomatsakis (Mar 07 2019 at 16:42, on Zulip):

I was actually going to say that

nikomatsakis (Mar 07 2019 at 16:42, on Zulip):

i'm bringing in a bit of framing from other lang-team debates, where it can be more argumentative, but I don't think that's the problem here

nikomatsakis (Mar 07 2019 at 16:42, on Zulip):

but I still think that times like these are a great point to step back

RalfJ (Mar 07 2019 at 16:42, on Zulip):

for ref/int, I imagine sections like "optimizing away functions that take &!", "initializing a buffer with Read::read", "AtomicCell", ...

nikomatsakis (Mar 07 2019 at 16:42, on Zulip):

and collaborate on trying to figure out how to express the "solution space" so that others can understand it

nikomatsakis (Mar 07 2019 at 16:43, on Zulip):

if nothing else, it will help us tremendously when we revisit these questions years from now, after having made a decision, and want to udnerstand why :)

nikomatsakis (Mar 07 2019 at 16:43, on Zulip):

it helps that I haven't been participating so I can see how much shared context you + @gnzlbg have right now :)

RalfJ (Mar 07 2019 at 16:43, on Zulip):

you are very optimistic assuming we'll have made a decision a year from now :P

nikomatsakis (Mar 07 2019 at 16:43, on Zulip):

i.e., I have no idea what the heck you are talking about ;)

gnzlbg (Mar 07 2019 at 16:43, on Zulip):

we should narrow the litmust test into "definetely want to support", and "decision X would allow supporting Y"
many of the arguments are of the later form, but discussion diverges because it is not clear whether Y is worth supporting

RalfJ (Mar 07 2019 at 16:44, on Zulip):

I think there's too many implications. I'd rather structure it by listing a bunch of pattern and then describing what allowing this pattern implies for int/refs.

gnzlbg (Mar 07 2019 at 16:45, on Zulip):

is the idea to just focus on int/refs first ?

RalfJ (Mar 07 2019 at 16:45, on Zulip):

well they are one area

gnzlbg (Mar 07 2019 at 16:45, on Zulip):

that would be fine by me

RalfJ (Mar 07 2019 at 16:45, on Zulip):

I think for unions we can write our normal summary + documenting the disagreement or whatever we called it

RalfJ (Mar 07 2019 at 16:45, on Zulip):

and the rest isnt controversial

gnzlbg (Mar 07 2019 at 16:45, on Zulip):

so are there other items in the list for the meeting ?

nikomatsakis (Mar 07 2019 at 16:45, on Zulip):

we had a few other things

nikomatsakis (Mar 07 2019 at 16:46, on Zulip):

I will pursue this

and

not sure what @RalfJ had in mind here

RalfJ (Mar 07 2019 at 16:46, on Zulip):

well we have a PR, I think it's ready for merging

gnzlbg (Mar 07 2019 at 16:47, on Zulip):

i think it might be a good idea if ubsan and niko also at least give it a read

RalfJ (Mar 07 2019 at 16:48, on Zulip):

sure, whatever

RalfJ (Mar 07 2019 at 16:48, on Zulip):

anyway I got to go, ttyl!

nikomatsakis (Mar 07 2019 at 16:48, on Zulip):

i think it might be a good idea if ubsan and niko also at least give it a read

happy to do so -- if there anything controversial? (cc @Nicole Mazzuca)

gnzlbg (Mar 07 2019 at 16:55, on Zulip):

there shouldn't be, but more eyes never hurt

Nicole Mazzuca (Mar 07 2019 at 16:57, on Zulip):

I can read it later today

gnzlbg (Mar 07 2019 at 16:58, on Zulip):

awesome, thank you both

nikomatsakis (Mar 12 2019 at 15:46, on Zulip):

Minutes posted -- I realize we've not been doing this so well. =)

Last update: Nov 19 2019 at 18:40UTC