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

Topic: meeting-2018-12-20


avadacatavra (Dec 20 2018 at 16:10, on Zulip):

Do we want to have a meeting today? I admit I'm feeling some holiday burnout, so I'll leave it up to the group

Alan Jeffrey (Dec 20 2018 at 16:11, on Zulip):

I'm here if we want to meet.

Alan Jeffrey (Dec 20 2018 at 16:12, on Zulip):

@avadacatavra my main agenda item is bugging you to press the green "squash and merge" button on https://github.com/rust-rfcs/unsafe-code-guidelines/pull/51

avadacatavra (Dec 20 2018 at 16:12, on Zulip):

@Alan Jeffrey that's my main goal for today

Alan Jeffrey (Dec 20 2018 at 16:12, on Zulip):

it's good to have goals.

Alan Jeffrey (Dec 20 2018 at 16:13, on Zulip):

Ta.

avadacatavra (Dec 20 2018 at 16:13, on Zulip):

squashed and merged!

avadacatavra (Dec 20 2018 at 16:16, on Zulip):

are there any other prs ready for merge?

RalfJ (Dec 20 2018 at 16:16, on Zulip):

hi all

RalfJ (Dec 20 2018 at 16:16, on Zulip):

what about https://github.com/rust-rfcs/unsafe-code-guidelines/pull/55 ?

avadacatavra (Dec 20 2018 at 16:17, on Zulip):

done

RalfJ (Dec 20 2018 at 16:17, on Zulip):

for https://github.com/rust-rfcs/unsafe-code-guidelines/pull/56 I have one small edit, I'll just quickly do that

RalfJ (Dec 20 2018 at 16:17, on Zulip):

(forgot about rkruppe's other comment)

RalfJ (Dec 20 2018 at 16:18, on Zulip):

are there otherwise comments about these definitions?

nikomatsakis (Dec 20 2018 at 16:18, on Zulip):

:wave:

avadacatavra (Dec 20 2018 at 16:18, on Zulip):

i'd say if there are other comments, we can do a followup

nikomatsakis (Dec 20 2018 at 16:18, on Zulip):

I had a thought about the place terminology

avadacatavra (Dec 20 2018 at 16:19, on Zulip):

/me is in squash and merge mode

nikomatsakis (Dec 20 2018 at 16:19, on Zulip):

I'm not sure if that's relevant to that PR

nikomatsakis (Dec 20 2018 at 16:19, on Zulip):

I remember us discussing it somewhere

RalfJ (Dec 20 2018 at 16:19, on Zulip):

@nikomatsakis that's another PR

nikomatsakis (Dec 20 2018 at 16:19, on Zulip):

ok

nikomatsakis (Dec 20 2018 at 16:19, on Zulip):

I'm ok with merging what's in that PR

RalfJ (Dec 20 2018 at 16:19, on Zulip):

this one defines interior mutability, validity invariant and safety invariant

avadacatavra (Dec 20 2018 at 16:20, on Zulip):

@RalfJ is it ready

RalfJ (Dec 20 2018 at 16:20, on Zulip):

@avadacatavra yes

nikomatsakis (Dec 20 2018 at 16:21, on Zulip):

I think the enum one is clearly not there

nikomatsakis (Dec 20 2018 at 16:21, on Zulip):

but hopefully after a few more iterations will be

RalfJ (Dec 20 2018 at 16:21, on Zulip):

ack

avadacatavra (Dec 20 2018 at 16:22, on Zulip):

what about function pointers

RalfJ (Dec 20 2018 at 16:22, on Zulip):

what about @Nicole Mazzuca 's function pointers?

nikomatsakis (Dec 20 2018 at 16:22, on Zulip):

seems like https://github.com/rust-rfcs/unsafe-code-guidelines/pull/45 has not been updaetd at all

RalfJ (Dec 20 2018 at 16:22, on Zulip):

^^

nikomatsakis (Dec 20 2018 at 16:22, on Zulip):

I think we at least have to address my 'static point

avadacatavra (Dec 20 2018 at 16:22, on Zulip):

jinx @RalfJ

nikomatsakis (Dec 20 2018 at 16:22, on Zulip):

I am not sure if there is anything substantive?

nikomatsakis (Dec 20 2018 at 16:22, on Zulip):

if not, I might be willing to go and push some edits then merge

nikomatsakis (Dec 20 2018 at 16:23, on Zulip):

(presuming @Nicole Mazzuca doesn't mind)

nikomatsakis (Dec 20 2018 at 16:23, on Zulip):

I guess @RalfJ's comments on transmutes looks kind of long :)

nikomatsakis (Dec 20 2018 at 16:23, on Zulip):

I have to read it in depth to understand if it's suggesting some form of deeper edit though

RalfJ (Dec 20 2018 at 16:23, on Zulip):

I don't remember^^

nikomatsakis (Dec 20 2018 at 16:24, on Zulip):

(looks like maybe not?)

RalfJ (Dec 20 2018 at 16:24, on Zulip):

but it needs some incorporating of comments at least

nikomatsakis (Dec 20 2018 at 16:24, on Zulip):

yeah, ok, so not quite ready is tl;dr

RalfJ (Dec 20 2018 at 16:25, on Zulip):

btw, what is the reasin for the squashing?

nikomatsakis (Dec 20 2018 at 16:25, on Zulip):

"squashing"?

RalfJ (Dec 20 2018 at 16:25, on Zulip):

of commits before merging

nikomatsakis (Dec 20 2018 at 16:25, on Zulip):

(is somebody squashing?)

RalfJ (Dec 20 2018 at 16:25, on Zulip):

I usually like preserving history, and also my local branch management is built around the assumption that my branches are merged as-is (I regularly delete all local branches that are now merged into master, to keep only the ones where I still have work to do)

Alan Jeffrey (Dec 20 2018 at 16:26, on Zulip):

@RalfJ it keeps our git history on master clean

avadacatavra (Dec 20 2018 at 16:26, on Zulip):

But it still keeps all of the messages

RalfJ (Dec 20 2018 at 16:26, on Zulip):

if by "clean" you mean "not reflecting the actual edit history" I agree^^

nikomatsakis (Dec 20 2018 at 16:26, on Zulip):

heh

Alan Jeffrey (Dec 20 2018 at 16:26, on Zulip):

there were a million "WIP" commits in the pointers PR for instance.

RalfJ (Dec 20 2018 at 16:26, on Zulip):

fair enough, it might be useful for some PRs, I was just wondering why it is done for all of them

avadacatavra (Dec 20 2018 at 16:27, on Zulip):

Oh because the merge button changed to squash and merge

avadacatavra (Dec 20 2018 at 16:27, on Zulip):

So...

RalfJ (Dec 20 2018 at 16:27, on Zulip):

makes it fairly hard to track which of the gazillion branches in my fork still contains unmerged stuff

avadacatavra (Dec 20 2018 at 16:27, on Zulip):

Sorry lol

RalfJ (Dec 20 2018 at 16:27, on Zulip):

Oh because the merge button changed to squash and merge

it didn't for me? maybe it remembers your last choice or so

nikomatsakis (Dec 20 2018 at 16:27, on Zulip):

I wish git had a hierarchical concept of commits

avadacatavra (Dec 20 2018 at 16:27, on Zulip):

I think so

RalfJ (Dec 20 2018 at 16:27, on Zulip):

anyway

RalfJ (Dec 20 2018 at 16:27, on Zulip):

another topic: can someone please define "representation"?

RalfJ (Dec 20 2018 at 16:27, on Zulip):

I tried, and I think it is the same as "layout"

nikomatsakis (Dec 20 2018 at 16:28, on Zulip):

I consider the two synonyms

RalfJ (Dec 20 2018 at 16:28, on Zulip):

but people are opposed to s/representation/layout/ it seems

nikomatsakis (Dec 20 2018 at 16:28, on Zulip):

hmm, I too am curious what the difference is =)

avadacatavra (Dec 20 2018 at 16:28, on Zulip):

Sounds like a good gh issue to me

Alan Jeffrey (Dec 20 2018 at 16:29, on Zulip):

AFAICT layout == representation == alignment + size is what we landed on.

RalfJ (Dec 20 2018 at 16:29, on Zulip):

alignment + size + field offsets + ABI is what I landed on

RalfJ (Dec 20 2018 at 16:29, on Zulip):

I can just submit a PR along those lines

Alan Jeffrey (Dec 20 2018 at 16:29, on Zulip):

oh yes, I always forget about ABI.

Alan Jeffrey (Dec 20 2018 at 16:30, on Zulip):

"field offsets" is an odd one, because it sounds like it should only apply to structs,

Alan Jeffrey (Dec 20 2018 at 16:30, on Zulip):

though really it applies to anything that can be transmuted to a struct.

RalfJ (Dec 20 2018 at 16:30, on Zulip):

unions have fields as well

RalfJ (Dec 20 2018 at 16:30, on Zulip):

as do enums

RalfJ (Dec 20 2018 at 16:31, on Zulip):

but yeah it applays to arrays etc as well

RalfJ (Dec 20 2018 at 16:31, on Zulip):

not sure what a better term would be?

RalfJ (Dec 20 2018 at 16:31, on Zulip):

"offsets of interior data"? sounds really odd to me

Alan Jeffrey (Dec 20 2018 at 16:31, on Zulip):

just "offsets"?

RalfJ (Dec 20 2018 at 16:31, on Zulip):

I feel there should be an "offset of what"

Alan Jeffrey (Dec 20 2018 at 16:32, on Zulip):

"subterm"?

RalfJ (Dec 20 2018 at 16:32, on Zulip):

"field/element offsets"

RalfJ (Dec 20 2018 at 16:32, on Zulip):

I don't see any terms here

RalfJ (Dec 20 2018 at 16:32, on Zulip):

"subobjects", but I bet @Nicole Mazzuca won't like that^^

Alan Jeffrey (Dec 20 2018 at 16:32, on Zulip):

indeed, you can spot my PL background peeking through there.

RalfJ (Dec 20 2018 at 16:32, on Zulip):

isn't there a good synonym for "component"

RalfJ (Dec 20 2018 at 16:33, on Zulip):

"constituent" or so

RalfJ (Dec 20 2018 at 16:33, on Zulip):

well we can bikeshed that on the PR

avadacatavra (Dec 20 2018 at 16:33, on Zulip):

If we aren’t reaching a consensus on this quickly I’d prefer the discussion to happen in gh

avadacatavra (Dec 20 2018 at 16:33, on Zulip):

Thanks @RalfJ

Alan Jeffrey (Dec 20 2018 at 16:33, on Zulip):

"contiguous substring" is the name for it viewed as a bitstring, not sure that helps though.

RalfJ (Dec 20 2018 at 16:33, on Zulip):

@avadacatavra I'm learning :D

RalfJ (Dec 20 2018 at 16:34, on Zulip):

@nikomatsakis you wanted to say something about places?

nikomatsakis (Dec 20 2018 at 16:34, on Zulip):

I can leave a comment in the PR

nikomatsakis (Dec 20 2018 at 16:34, on Zulip):

I saw there was some other comments towards the end I should read

nikomatsakis (Dec 20 2018 at 16:35, on Zulip):

the tl;dr is that I am not convinced that "place" is a good term to apply to an expression

nikomatsakis (Dec 20 2018 at 16:35, on Zulip):

(I've generally found it more awkward than I would like)

RalfJ (Dec 20 2018 at 16:35, on Zulip):

hm

nikomatsakis (Dec 20 2018 at 16:36, on Zulip):

(but this is a broader bikeshed that would want to involve the compiler team, at least)

RalfJ (Dec 20 2018 at 16:36, on Zulip):

so you don't agree with my 2x2 grid of decomposing things

avadacatavra (Dec 20 2018 at 16:36, on Zulip):

Anything else for the meeting? Seems like a good time to just wrap previous discussions up right now

RalfJ (Dec 20 2018 at 16:36, on Zulip):

yay, even more colors :D

nikomatsakis (Dec 20 2018 at 16:37, on Zulip):

so you don't agree with my 2x2 grid of decomposing things

possibly not :) I'm not sure yet, I want to refresh my memory

RalfJ (Dec 20 2018 at 16:37, on Zulip):

there are some untagged issues at https://github.com/rust-rfcs/unsafe-code-guidelines/issues

RalfJ (Dec 20 2018 at 16:37, on Zulip):

most of them seem "proposed discussion topic" or so

RalfJ (Dec 20 2018 at 16:38, on Zulip):

we also have two writeup-needed

nikomatsakis (Dec 20 2018 at 16:39, on Zulip):

writeup-needed:

nikomatsakis (Dec 20 2018 at 16:39, on Zulip):

I do feel like it would be good to get a handle on the "ZST" aspect, which I feel like has come up a few places

nikomatsakis (Dec 20 2018 at 16:39, on Zulip):

but I'm not sure it's a blocking concern per se

nikomatsakis (Dec 20 2018 at 16:39, on Zulip):

we can move to another "area of discussion" without resolving it, I think?

RalfJ (Dec 20 2018 at 16:40, on Zulip):

sure, though if someone involved in the discussion could at least be assigned that'd also be nice

RalfJ (Dec 20 2018 at 16:40, on Zulip):

(will be back in 2min)

nikomatsakis (Dec 20 2018 at 16:41, on Zulip):

I guess I can tackle those, but I'm just not wanting to overcommit. Want to finish up the enum stuff first.

Nicole Mazzuca (Dec 20 2018 at 16:42, on Zulip):

@RalfJ afaict that is the correct way to use the term subobject

Nicole Mazzuca (Dec 20 2018 at 16:43, on Zulip):

@nikomatsakis the difference between representation and layout, it seems to me, is the difference between "struct { 0: i32, 1: i32} is laid out with the 32-bit 0 first, and the 32-bit 1 next"

Nicole Mazzuca (Dec 20 2018 at 16:44, on Zulip):

i.e., it's a property of subobjects

RalfJ (Dec 20 2018 at 16:44, on Zulip):

(re)

Nicole Mazzuca (Dec 20 2018 at 16:44, on Zulip):

like, that's what that immediately says to me

RalfJ (Dec 20 2018 at 16:44, on Zulip):

@nikomatsakis the difference between representation and layout, it seems to me, is the difference between "struct { 0: i32, 1: i32} is laid out with the 32-bit 0 first, and the 32-bit 1 next"

you only have one thing after the between

RalfJ (Dec 20 2018 at 16:44, on Zulip):

so it is the difference between that and... what?

Nicole Mazzuca (Dec 20 2018 at 16:45, on Zulip):

patience!

Nicole Mazzuca (Dec 20 2018 at 16:45, on Zulip):

I'm on my phone

RalfJ (Dec 20 2018 at 16:45, on Zulip):

okay :) I thought I just missed the 2nd part

avadacatavra (Dec 20 2018 at 16:47, on Zulip):

I think we should move on to the next topic with our next meeting

avadacatavra (Dec 20 2018 at 16:47, on Zulip):

Sound acceptable?

nikomatsakis (Dec 20 2018 at 16:47, on Zulip):

I feel like we are ready

nikomatsakis (Dec 20 2018 at 16:48, on Zulip):

e.g., the enum PR is basically in the "small refinement" stage it seems

Nicole Mazzuca (Dec 20 2018 at 16:48, on Zulip):

as opposed to representation, which is like, "struct { 0: i32, 1: i32 } has the value representation Int[-2^31, 2^31 - 1] × Int[-2 ^ 31, 2^31 - 1] and the object representation {0 = x; 1 = y} |-> object_repr(x) ++ object_repr(y)"

RalfJ (Dec 20 2018 at 16:48, on Zulip):

@Nicole Mazzuca none of our disucssion about representation has been about mapping rust types to mathematical sets

Nicole Mazzuca (Dec 20 2018 at 16:48, on Zulip):

i.e., representation, to me, is the actual bytes to values

RalfJ (Dec 20 2018 at 16:49, on Zulip):

(and in fact I think such a mapping, for the most part, has no place in a language's operational semantics)

avadacatavra (Dec 20 2018 at 16:49, on Zulip):

Ok when things are ready for merge just ping me in the pr

RalfJ (Dec 20 2018 at 16:49, on Zulip):

"values" are bitstrings

Nicole Mazzuca (Dec 20 2018 at 16:49, on Zulip):

that is the basis for my discussion

RalfJ (Dec 20 2018 at 16:49, on Zulip):

but I know you disagree :)

avadacatavra (Dec 20 2018 at 16:49, on Zulip):

And I’ll make sure to look over all of the issues and label them appropriately

RalfJ (Dec 20 2018 at 16:49, on Zulip):

the thing is, we've not been talking about mathematical values in this "area of discussion"

RalfJ (Dec 20 2018 at 16:49, on Zulip):

so that's clearly not how we used the term representation.

nikomatsakis (Dec 20 2018 at 16:50, on Zulip):

seems like all the more reason to centralize on layout

Nicole Mazzuca (Dec 20 2018 at 16:50, on Zulip):

well, there are two different things here

avadacatavra (Dec 20 2018 at 16:50, on Zulip):

@RalfJ @Nicole Mazzuca perhaps we should move this to a new topic/gh for further discussion

RalfJ (Dec 20 2018 at 16:50, on Zulip):

I agree "representation" makes sense as a term for what you are describing though, and I also agree that concept is a useful one in many circumstances, just not when defining an operational semantics.

RalfJ (Dec 20 2018 at 16:51, on Zulip):

in fact that's one reason why I want to just say "layout" instead for what we discussed, to free the term "representation" for how you want to use it

Nicole Mazzuca (Dec 20 2018 at 16:51, on Zulip):

ah, hmm

avadacatavra (Dec 20 2018 at 16:51, on Zulip):

No meeting next week! Everyone have a lovely holiday :champagne:

Nicole Mazzuca (Dec 20 2018 at 16:51, on Zulip):

okay, that makes sense

Nicole Mazzuca (Dec 20 2018 at 16:51, on Zulip):

then I'm okay with standardizing on layout

RalfJ (Dec 20 2018 at 16:52, on Zulip):

I agree "representation" makes sense as a term for what you are describing though, and I also agree that concept is a useful one in many circumstances, just not when defining an operational semantics.

to follow-up on that: "representation" is commonly used in static analysis or so, along the lines you are using it, but I dont think there has to be THE normative "mathematical representation" of any Rust type. different analysis may need different reps. so we shouldnt fix one here, but give a precise enough spec of the behavior of the underlying bit and bytes so that people can define their own (sound) reps on top.

Alan Jeffrey (Dec 20 2018 at 17:01, on Zulip):

Happy holidays everyone!

Nicole Mazzuca (Dec 20 2018 at 17:08, on Zulip):

@RalfJ well, for stuff like, I dunno, +, you have to define a mapping from bytes to values, no?

RalfJ (Dec 20 2018 at 17:08, on Zulip):

@Nicole Mazzuca we need it for a few primitive types, where we have primitive operations, yes

RalfJ (Dec 20 2018 at 17:09, on Zulip):

and there's usually not much choice there

RalfJ (Dec 20 2018 at 17:09, on Zulip):

(not anymore, anyway^^ with two's complement everywhere)

RalfJ (Dec 20 2018 at 17:09, on Zulip):

and I dont even think of this as a property of the type. it's a property of the operation

RalfJ (Dec 20 2018 at 17:09, on Zulip):

(webassembly gets this right IMO, with signed and unsigned int ops but only one kind of int type)

RalfJ (Dec 20 2018 at 17:10, on Zulip):

of course in a higher-level language it makes sense to distinguish signed and unsigned int types

RalfJ (Dec 20 2018 at 17:10, on Zulip):

but they most serve to automatically infer whether you mean signed or unsigned < (etc.)

Nicole Mazzuca (Dec 20 2018 at 17:19, on Zulip):

well, that's true for almost every lower level IR

RalfJ (Dec 20 2018 at 17:29, on Zulip):

true

RalfJ (Dec 20 2018 at 17:30, on Zulip):

I just wanted to be sure we agree^^ if representation is more a property of operations than types, that gives it quite a different nature from the validity invariant

Nicole Mazzuca (Dec 20 2018 at 17:36, on Zulip):

I prefer to think of it as a property of the type

Nicole Mazzuca (Dec 20 2018 at 17:36, on Zulip):

non-abstract data types are their representations

Nicole Mazzuca (Dec 20 2018 at 17:37, on Zulip):

and you write operations on those representations

Nicole Mazzuca (Dec 20 2018 at 17:37, on Zulip):

(in my view)

Nicole Mazzuca (Dec 20 2018 at 17:37, on Zulip):

(I know plenty of people have a different one)

RalfJ (Dec 20 2018 at 17:37, on Zulip):

my issue with that view is that IMO memory is untyped -- so the represetnation doesnt really have any effect between operations

RalfJ (Dec 20 2018 at 17:37, on Zulip):

and it also doesnt matter for all operations

RalfJ (Dec 20 2018 at 17:38, on Zulip):

but of course i32 will always use the same rep no matter whether we are talking multiplication or <, so it is also somewhat attached to the type

Nicole Mazzuca (Dec 20 2018 at 17:38, on Zulip):

sure, memory is untyped, but Rust is a value based language at the cute

Nicole Mazzuca (Dec 20 2018 at 17:38, on Zulip):

*core

RalfJ (Dec 20 2018 at 17:38, on Zulip):

well that's where we definitely disagree :)

Nicole Mazzuca (Dec 20 2018 at 17:39, on Zulip):

let x : i32 = 0; is not memory, for example

RalfJ (Dec 20 2018 at 17:39, on Zulip):

it is

Nicole Mazzuca (Dec 20 2018 at 17:39, on Zulip):

(or, x is not memory)

RalfJ (Dec 20 2018 at 17:39, on Zulip):

every place/lvalue is just a spot in memory

RalfJ (Dec 20 2018 at 17:39, on Zulip):

but from what I have seen that disagreement is purely philosophical and doesn't actually lead to different semantics

Nicole Mazzuca (Dec 20 2018 at 17:39, on Zulip):

this is true

RalfJ (Dec 20 2018 at 17:40, on Zulip):

and these are the kind of disagreements I can live with very well. I prefer them with two formal definitions and a proof of equivalence. ;)

Last update: Dec 12 2019 at 01:50UTC