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

Topic: this week's meeting


avadacatavra (Sep 26 2018 at 16:33, on Zulip):

I'm at a w3c meeting and won't be able to lead the meeting this week-- @nikomatsakis do you want to lead it or postpone?

nikomatsakis (Sep 26 2018 at 16:33, on Zulip):

either way, but I'm not sure how many write-ups we actually have?

nikomatsakis (Sep 26 2018 at 16:33, on Zulip):

I wanted to check back on who was assigned to what

nikomatsakis (Sep 26 2018 at 16:34, on Zulip):

maybe best to postpone so that we have a bit more time for people to process the writeups anyway? (once we have them, that is)

nikomatsakis (Sep 26 2018 at 16:34, on Zulip):

well, let's do the meeting, but I suspect we won't be able to do much at it

nikomatsakis (Sep 26 2018 at 16:34, on Zulip):

I can lead it

nikomatsakis (Sep 26 2018 at 16:34, on Zulip):

if nothing else it's a time to nag

avadacatavra (Sep 26 2018 at 20:25, on Zulip):

yeah i didn't manage to get to mine, so maybe a postponement + nagging

avadacatavra (Sep 26 2018 at 22:05, on Zulip):

@avadacatavra did you get your writeups done?

avadacatavra (Sep 26 2018 at 22:06, on Zulip):

nooooo.....i will be better

nikomatsakis (Sep 27 2018 at 13:51, on Zulip):

lol

RalfJ (Oct 11 2018 at 14:05, on Zulip):

do we have another mtg today?

nikomatsakis (Oct 11 2018 at 14:07, on Zulip):

I think so, yes, @avadacatavra you around?

Alan Jeffrey (Oct 11 2018 at 15:15, on Zulip):

Hi everyone.

RalfJ (Oct 11 2018 at 15:15, on Zulip):

Hi all!

Alan Jeffrey (Oct 11 2018 at 15:16, on Zulip):

I'll ping @avadacatavra on IRC.

RalfJ (Oct 11 2018 at 15:18, on Zulip):

I'll try slack ;)

RalfJ (Oct 11 2018 at 15:18, on Zulip):

they seem to be offline there though

RalfJ (Oct 11 2018 at 15:19, on Zulip):

(I think that's what that icon means. don't actually know.)

RalfJ (Oct 11 2018 at 15:22, on Zulip):

@nikomatsakis said sth. come up and they're late

Alan Jeffrey (Oct 11 2018 at 15:23, on Zulip):

OK, I can wait. @RalfJ do you have time pressures?

RalfJ (Oct 11 2018 at 15:24, on Zulip):

well I have to leave exactly when the meeting ends (1745)

RalfJ (Oct 11 2018 at 15:24, on Zulip):

to catch a bus

RalfJ (Oct 11 2018 at 15:24, on Zulip):

;)

Alan Jeffrey (Oct 11 2018 at 15:24, on Zulip):

OK, while we're waiting...

Alan Jeffrey (Oct 11 2018 at 15:24, on Zulip):

Have you read "Rust Distilled: An Expressive Tower of Languages"?

RalfJ (Oct 11 2018 at 15:25, on Zulip):

public transport is great but sometimes I wish I had a car so I would have more flexible timing...

RalfJ (Oct 11 2018 at 15:25, on Zulip):

no I do not think I have heard of that

Alan Jeffrey (Oct 11 2018 at 15:25, on Zulip):

There was a talk at the ML workshop co-located with ICFP. https://aaronweiss.us/

RalfJ (Oct 11 2018 at 15:25, on Zulip):

oh yes I have it on my to-read list

RalfJ (Oct 11 2018 at 15:25, on Zulip):

or sth else by the same author?

RalfJ (Oct 11 2018 at 15:25, on Zulip):

what I have is older than ICFP

RalfJ (Oct 11 2018 at 15:26, on Zulip):

same thing though

RalfJ (Oct 11 2018 at 15:26, on Zulip):

was on arXiv way before ICFP

Alan Jeffrey (Oct 11 2018 at 15:26, on Zulip):

I strongly encouraged Amal and Aaron to take part in the unsafe code guidelines discussions.

RalfJ (Oct 11 2018 at 15:27, on Zulip):

and you also strongly encourage me to read their paper? ;)

Alan Jeffrey (Oct 11 2018 at 15:27, on Zulip):

At some point we'll have to start drafting the invariants for &T and &mut T.

Alan Jeffrey (Oct 11 2018 at 15:27, on Zulip):

@RalfJ yes, I am doing a lot of strong encouragement :)

RalfJ (Oct 11 2018 at 15:28, on Zulip):

^^

RalfJ (Oct 11 2018 at 15:28, on Zulip):

well I got it printed now, at least

Alan Jeffrey (Oct 11 2018 at 15:28, on Zulip):

most of the battle

RalfJ (Oct 11 2018 at 15:28, on Zulip):

At some point we'll have to start drafting the invariants for &T and &mut T.

right... however, we first need to develop the language/logic in which we want to do that

RalfJ (Oct 11 2018 at 15:28, on Zulip):

like, I have such an invariant in my RustBelt work. but it's not exactly suited for consumption by non-PL-researchers

Alan Jeffrey (Oct 11 2018 at 15:28, on Zulip):

Indeed.

Alan Jeffrey (Oct 11 2018 at 15:29, on Zulip):

Not sure that "first learn CSL" is going to pan out :/

RalfJ (Oct 11 2018 at 15:29, on Zulip):

however, I also don't see anything simpler that actually gets the job done

RalfJ (Oct 11 2018 at 15:29, on Zulip):

but maybe I should read their paper first? ;)

RalfJ (Oct 11 2018 at 15:30, on Zulip):

it also depends on what you mean by "invariants"

RalfJ (Oct 11 2018 at 15:30, on Zulip):

there is Stacked Borrows

RalfJ (Oct 11 2018 at 15:30, on Zulip):

which is answering lots of questions around reference types

Alan Jeffrey (Oct 11 2018 at 15:30, on Zulip):

The ML paper doesn't have the gory details IIRC

RalfJ (Oct 11 2018 at 15:30, on Zulip):

but that's something very different from specifying the semantic invariant of reference types

Alan Jeffrey (Oct 11 2018 at 15:32, on Zulip):

They're using fractional permissions, plus IIRC run-time capabilities kept as shadow state.

RalfJ (Oct 11 2018 at 15:32, on Zulip):

can they handle interior mutability?

RalfJ (Oct 11 2018 at 15:32, on Zulip):

that's what killed it for us

Alan Jeffrey (Oct 11 2018 at 15:33, on Zulip):

Don't know.

Alan Jeffrey (Oct 11 2018 at 15:34, on Zulip):

Is there a short explaination of why interior mutability is an issue? On the surface it seems like it should be a case where there is a capability that is being kept in "real" (i.e. not shadow) state?

Alan Jeffrey (Oct 11 2018 at 15:34, on Zulip):

But devil in the details.

blitzerr (Oct 11 2018 at 15:35, on Zulip):

@RalfJ Could you explain what interior mutability is ?

Alan Jeffrey (Oct 11 2018 at 15:35, on Zulip):

@blitzerr things RefCell.

Alan Jeffrey (Oct 11 2018 at 15:35, on Zulip):

https://doc.rust-lang.org/book/second-edition/ch15-05-interior-mutability.html

blitzerr (Oct 11 2018 at 15:35, on Zulip):

Ahh ! thanks @Alan Jeffrey

RalfJ (Oct 11 2018 at 15:37, on Zulip):

@blitzerr basically, mutating memory where someone holds a shared ref to it

RalfJ (Oct 11 2018 at 15:37, on Zulip):

IOW, violating "shared references point to read-only memory"

blitzerr (Oct 11 2018 at 15:38, on Zulip):

I am very interested in the unsafe-code. But don't know much about it. So I am just following along and would like to contribute. :slight_smile:

RalfJ (Oct 11 2018 at 15:38, on Zulip):

@Alan Jeffrey well, without interior mutability, & is simply modeled as "read-only", done

RalfJ (Oct 11 2018 at 15:38, on Zulip):

fractional permissions can do that (though I'll have to see how they handle lifetimes)

blitzerr (Oct 11 2018 at 15:38, on Zulip):

Hence, the questions :slight_smile:

blitzerr (Oct 11 2018 at 15:38, on Zulip):

thanks @RalfJ

RalfJ (Oct 11 2018 at 15:38, on Zulip):

you're welcome :)

Jake Goulding (Oct 11 2018 at 15:39, on Zulip):

@blitzerr also https://doc.rust-lang.org/std/cell/index.html

Alan Jeffrey (Oct 11 2018 at 15:39, on Zulip):

@RalfJ One thing that interior mutability means is that capabilities sometimes live in real state, not shadow state,

RalfJ (Oct 11 2018 at 15:39, on Zulip):

@Alan Jeffrey but with interior mutability -- really we should call it shared mutability -- the rules for &T are... well, they are whatever T wants them to be

RalfJ (Oct 11 2018 at 15:39, on Zulip):

I dont know what you mean by that

RalfJ (Oct 11 2018 at 15:39, on Zulip):

but capabilities are always shadow as they dont exist on the real machine

RalfJ (Oct 11 2018 at 15:40, on Zulip):

so your proof should reflect that

Alan Jeffrey (Oct 11 2018 at 15:40, on Zulip):

so I can imagine this complicates what is otherwise a nice split between capabilities and the stack/heap.

RalfJ (Oct 11 2018 at 15:40, on Zulip):

or do you mean "Stacked Borrows"-style "shadow state"?

RalfJ (Oct 11 2018 at 15:40, on Zulip):

that would just entirely ignore interior mutability though. you cant statically say in the machine what the rules are as every type defines them for itself.

RalfJ (Oct 11 2018 at 15:41, on Zulip):

for Stacked Borrows, &Cell<T> and *mut T are basically the same thing

Alan Jeffrey (Oct 11 2018 at 15:41, on Zulip):

I'm not sure I have a precise thing here, but...

RalfJ (Oct 11 2018 at 15:41, on Zulip):

no alias reistrictions either way

Alan Jeffrey (Oct 11 2018 at 15:41, on Zulip):

it seems like RefCell is essentially keeping a real-state version of a capability.

RalfJ (Oct 11 2018 at 15:42, on Zulip):

but how do you explain Cell then?

RalfJ (Oct 11 2018 at 15:42, on Zulip):

TBH that looks like a red herring to me

RalfJ (Oct 11 2018 at 15:43, on Zulip):

but I'll first have to figure out which kind of capabilities you mean

RalfJ (Oct 11 2018 at 15:43, on Zulip):

so I may be just misunderstanding entirely

Alan Jeffrey (Oct 11 2018 at 15:43, on Zulip):

@RalfJ good point, I'd mainly been thinking about RefCell not Cell.

RalfJ (Oct 11 2018 at 15:43, on Zulip):

and then there's Rc...

Alan Jeffrey (Oct 11 2018 at 15:44, on Zulip):

@RalfJ does Rc impact anything other than when drop code is run?

Alan Jeffrey (Oct 11 2018 at 15:45, on Zulip):

ie in a model that's ignoring reclaiming memory, does Rc have semantic impact?

RalfJ (Oct 11 2018 at 15:45, on Zulip):

Rc was extremnely hard to prove correct

RalfJ (Oct 11 2018 at 15:45, on Zulip):

in particular, Rc::get_mut

RalfJ (Oct 11 2018 at 15:45, on Zulip):

because the content of an Rc isn't always shared

RalfJ (Oct 11 2018 at 15:45, on Zulip):

and justifying that you can make it not-shared in get_mut was one of the most tricky things in the entire RustBelt paper

Alan Jeffrey (Oct 11 2018 at 15:45, on Zulip):

@RalfJ is Rc difficult for different reasons than RefCell?

RalfJ (Oct 11 2018 at 15:46, on Zulip):

yes

RalfJ (Oct 11 2018 at 15:46, on Zulip):

well, maybe

RalfJ (Oct 11 2018 at 15:46, on Zulip):

not sure what the equivalence relation on "reasons" is^^

Alan Jeffrey (Oct 11 2018 at 15:46, on Zulip):

fair enough, I'm not sure I do either :/

Alan Jeffrey (Oct 11 2018 at 15:47, on Zulip):

from a mile high view, it looks like a model which can cope with RefCell could probably also cope with Rc.

Alan Jeffrey (Oct 11 2018 at 15:47, on Zulip):

(at least, ignoring Rc's impact on memory reclamation)

RalfJ (Oct 11 2018 at 15:48, on Zulip):

from what I recall we had to change the way we do lifetimes to be able to handle Rc::get_mut

RalfJ (Oct 11 2018 at 15:48, on Zulip):

but it might have been RefMut::map instead

RalfJ (Oct 11 2018 at 15:48, on Zulip):

one of the two required fundamental changes that threw us back a couple months

RalfJ (Oct 11 2018 at 15:48, on Zulip):

the other probably benefited from those changes

Alan Jeffrey (Oct 11 2018 at 15:49, on Zulip):

One thing that's slightly annoying is that Rc and RefCell are doing very similar things (keeping a capability in real state rather than shadow state) but in different ways, sigh.

RalfJ (Oct 11 2018 at 15:50, on Zulip):

they are rather fundamentally different in what they do though

RalfJ (Oct 11 2018 at 15:50, on Zulip):

and I wouldnt describe either as keeping a capability in real state^^

RalfJ (Oct 11 2018 at 15:50, on Zulip):

rhater, they have elaborate ways of sharing

Alan Jeffrey (Oct 11 2018 at 15:50, on Zulip):

So each type gets to define its own invariant about the relationship between shadow state and real state.

RalfJ (Oct 11 2018 at 15:50, on Zulip):

and ending sharing

RalfJ (Oct 11 2018 at 15:50, on Zulip):

anyway, got to catch a bus. ttyl!

Alan Jeffrey (Oct 11 2018 at 15:51, on Zulip):

@RalfJ ok, see you later!

Alan Jeffrey (Oct 11 2018 at 15:51, on Zulip):

Hmm, we'll see if @avadacatavra or @nikomatsakis turn up at some point.

Alan Jeffrey (Oct 11 2018 at 15:52, on Zulip):

Otherwise this week's meeting topic was "Ralf and Alan pass the time talking about memory invariants".

blitzerr (Oct 11 2018 at 15:52, on Zulip):

:D

nikomatsakis (Oct 11 2018 at 16:31, on Zulip):

hi all =) I'm sorry, as @RalfJ said, something came up

Alan Jeffrey (Oct 11 2018 at 16:32, on Zulip):

@nikomatsakis hi

nikomatsakis (Oct 11 2018 at 16:32, on Zulip):

(I started a topic with the proper title, for easier finding in the future)

avadacatavra (Oct 11 2018 at 18:15, on Zulip):

i was on a plane

avadacatavra (Oct 11 2018 at 18:15, on Zulip):

sorry about that

avadacatavra (Oct 11 2018 at 18:15, on Zulip):

i'll read backlog and get caught up :)

Nicole Mazzuca (Oct 11 2018 at 18:23, on Zulip):

I'd like to guarantee the following:

- Given a raw lvalue field access of type T on an object x, this should not guarantee that the object x is valid under type T
- it should only guarantee that the field access is inbounds on x
- Given an lvalue-to-raw-pointer conversion of type T, this does not guarantee that the object the lvalue refers to is valid under type T

basically, this means that raw field accesses are equivalent to an offset.

note: code that explains what the above things mean

// raw lvalue field access
given x: *const T;
(*x).y
// lvalue-to-raw-pointer conversion
given x: immutable lvalue U;
&x as *const U
nikomatsakis (Oct 11 2018 at 18:26, on Zulip):

I don't really follow the context here — also, who is guaranteeing what?

e.g., "given a raw lvalue field access of type T on an object x" -- you mean given something like x.f? In that case, though, the object x would not have type T..

...maybe it'd be good to give some Rust example code to get at it more precisely.

Nicole Mazzuca (Oct 11 2018 at 18:28, on Zulip):

See #design in the discord for why I want to guarantee this

Nicole Mazzuca (Oct 11 2018 at 18:28, on Zulip):

also, the language is guaranteeing that this is not UB, basically

nikomatsakis (Oct 11 2018 at 18:31, on Zulip):

(oh, now I see the code, I didn't see it before)

nikomatsakis (Oct 11 2018 at 18:31, on Zulip):

but I feel like the example doesn't make sense in isolation

nikomatsakis (Oct 11 2018 at 18:32, on Zulip):

e.g., it matters a lot what you do with (*x).y -- is that &(*x).y? Is it foo((*x).y)?

Nicole Mazzuca (Oct 11 2018 at 18:33, on Zulip):

the first would be an lvalue-to-reference conversion, in which case all the rules of lvalue-to-reference conversion hold. The second would be an lvalue-to-rvalue conversion, in which case all the rules of lvalue-to-rvalue conversion hold

Aaron Weiss (Oct 11 2018 at 18:49, on Zulip):

@Alan Jeffrey sorry that I couldn't make it this morning (I had one of those GlobalEntry interview things). You're definitely right to say that the ML workshop extended abstract doesn't have tons of details. But it also predates a very useful meeting that I had with @nikomatsakis that has added a lot of clarity. The stuff present in the talk I gave was definitely informed a lot by that meeting and the subsequent changes I've been working on (and am still working on) to our semantics. That being said, I think you've appropriately captured my thinking (and likely Amal's) on RefCell in your talking with @RalfJ. From my perspective right now, it seems like it shouldn't be too hard to add runtime instruments to our operational semantics for Rc and RefCell, but it could certainly surprise me.

Alan Jeffrey (Oct 11 2018 at 19:29, on Zulip):

@Aaron Weiss hi, glad you're here!

Alan Jeffrey (Oct 11 2018 at 19:29, on Zulip):

Ah, that explains the gap between the paper and the talk :)

Alan Jeffrey (Oct 11 2018 at 19:30, on Zulip):

Are the slides online somewhere?

RalfJ (Oct 11 2018 at 20:08, on Zulip):

I am curious to see any other approach to tackling Rc and RefCell :)

RalfJ (Oct 11 2018 at 20:08, on Zulip):

and yes, I'd be interested in the slides as well

Aaron Weiss (Oct 11 2018 at 20:44, on Zulip):

The slides are on my website that you linked, but here's the direct link to the slides: https://aaronweiss.us/pubs/ml18-slides.pdf

RalfJ (Oct 11 2018 at 20:47, on Zulip):

@Aaron Weiss thanks!

RalfJ (Oct 11 2018 at 20:48, on Zulip):

they didnt make a recording, did they?

Aaron Weiss (Oct 11 2018 at 20:50, on Zulip):

Fortunately, they did! Leif was there filming it for the workshop, but she's not responsible for the production. So unfortunately, I have no idea how long until they release the videos.

RalfJ (Oct 11 2018 at 20:51, on Zulip):

ah cool. well if anyone hears something let's post here (and maybe also in the verification-wg thing on gitter, are you on there?)

RalfJ (Oct 11 2018 at 20:52, on Zulip):

ah seems you are. we got three aaron's there^^

RalfJ (Oct 11 2018 at 20:53, on Zulip):

I am actually quite surprised I am still the only Ralf in Rustland (that I know of)... it's a pretty common name around here. There are actually two people sharing my first and last name at my university (well, if you count past members, one of them left before the other joined)^^

Aaron Weiss (Oct 11 2018 at 20:54, on Zulip):

Yeah, I'm keeping my eyes peeled for the video since I intend on tweeting about it and sharing it with some friends who weren't there to see it. So, if I find them first, I'll definitely post them here and on the verification-wg.

Aaron Weiss (Oct 11 2018 at 20:55, on Zulip):

The work is obviously in a much rougher state than RustBelt (otherwise, it'd already be published :wink:), but I think has been going a lot better since the aforementioned meeting with Niko.

RalfJ (Oct 11 2018 at 21:09, on Zulip):

I'm certainly curious what you'll end up with :) I sure hope there's something simpler than our proofs^^

avadacatavra (Nov 15 2018 at 12:08, on Zulip):

I am finally off the three planes it took to get home. I’m happy to lead a meeting today to make up for the last one :)

gnzlbg (Nov 15 2018 at 13:40, on Zulip):

When is the meeting? I thought it was going to start 40 minutes ago :/

gnzlbg (Nov 15 2018 at 13:40, on Zulip):

Isn't it 13:00 UTC ?

RalfJ (Nov 15 2018 at 13:48, on Zulip):

since it moved by 1h with US DST, I'd expect it to be 16:15 UTC

RalfJ (Nov 15 2018 at 13:48, on Zulip):

or maybe 16:00, not sure if we did that move by 15min

avadacatavra (Nov 15 2018 at 16:01, on Zulip):

Meeting in 15 :)

Alan Jeffrey (Nov 15 2018 at 16:03, on Zulip):

Captain, sensors are picking up an unexpected meeting.

nikomatsakis (Nov 15 2018 at 16:06, on Zulip):

so I made a Zulip topic but apparently I did my math wrong :)

nikomatsakis (Nov 15 2018 at 16:07, on Zulip):

in that topic, however, there are a few thoughts about agenda etc

nikomatsakis (Nov 15 2018 at 16:07, on Zulip):

also, @gnzlbg, do you want to be added to the calendar invite?

nikomatsakis (Nov 15 2018 at 16:07, on Zulip):

(if you're not already)

gnzlbg (Nov 15 2018 at 16:07, on Zulip):

@nikomatsakis yes please

RalfJ (Nov 15 2018 at 16:07, on Zulip):

Captain, sensors are picking up an unexpected meeting.

we said last week we'd move to this week because noone was there

nikomatsakis (Nov 15 2018 at 16:11, on Zulip):

I suppose I did not make a new calendar invite :P

nikomatsakis (Nov 15 2018 at 16:11, on Zulip):

for this day

Last update: Nov 20 2019 at 11:25UTC