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

Topic: Slides for talk on unsafe rust


Alan Jeffrey (May 09 2019 at 14:53, on Zulip):

I wrote some slides, all comments welcome

Alan Jeffrey (May 09 2019 at 14:53, on Zulip):

https://docs.google.com/presentation/d/1m_HxkTXWsUpX0mYGpP07eHRAzbbl-o6WQgUkb7gF-oA

Alan Jeffrey (May 09 2019 at 14:54, on Zulip):

@RalfJ in particular, is the diagram on slide 13 horribly inaccurate?

Alan Jeffrey (May 09 2019 at 14:54, on Zulip):

(I'm trying to summarize stacked borrows in one slide, which is tricky.)

Alan Jeffrey (May 09 2019 at 14:57, on Zulip):

Also, are there other topics I should add to the laundry list on slide 15?

RalfJ (May 09 2019 at 15:07, on Zulip):

oh dear, the contextual definition of unsafety^^ fun stuff

RalfJ (May 09 2019 at 15:08, on Zulip):

(there might have been other ways to break josephine with an otherwise-safe abstraction pre-1.20, but that doesnt change the point you are making so whatever)

RalfJ (May 09 2019 at 15:09, on Zulip):

re: Stacked Borrows, the "shared"/"unique" labels are not really on the edges from the ptr to the stack... those would be just IDs. the stack then does 2 things, it orders the ID and it says which of them are Unique, SharedReadOnly, SharedReadWrite

RalfJ (May 09 2019 at 15:11, on Zulip):

Also, are there other topics I should add to the laundry list on slide 15?

not sure how specific you want to get. "developing a language spec"? "figuring out how our semantics relate to LLVM's"?

Alan Jeffrey (May 09 2019 at 15:18, on Zulip):

There's an argument that Josephine got broken by may_dangle, but you have to spec-lawyer the may_dangle requirements, but this sort of complicates the presentation, which is making the point "yes, this can happen in the wild".

Alan Jeffrey (May 09 2019 at 15:18, on Zulip):

I was pleasantly surprised to discover that the contextual defn is no longer in the rustonomicon / lang spec, the wording now is vaguer.

RalfJ (May 09 2019 at 15:18, on Zulip):

I was thinking of a lib that implements ManuallyDrop by transmuting stuff to byte arrays. IIRC someone pointed to a lib that actually does this for FFI or so...

Alan Jeffrey (May 09 2019 at 15:19, on Zulip):

True, but that's not in std.

RalfJ (May 09 2019 at 15:19, on Zulip):

ManuallyDrop is the better-to-understand example anyway

Alan Jeffrey (May 09 2019 at 15:19, on Zulip):

indeed

RalfJ (May 09 2019 at 15:19, on Zulip):

well, having this conflict between 2 user libs makes it even more "fun" in some way

Alan Jeffrey (May 09 2019 at 15:20, on Zulip):

OK, I'm interested in your comment re the diagram trying to explain stacked borrows...

RalfJ (May 09 2019 at 15:20, on Zulip):

if the conflict is with libstd, then I guess per default libstd "wins" -- at least if the change was vetted by the lang team. but when it's two user libs, uh, we can roll a dice to decide?^^

Alan Jeffrey (May 09 2019 at 15:21, on Zulip):

I originally had the tags in the pointer nodes rather than on the edges

Alan Jeffrey (May 09 2019 at 15:21, on Zulip):

which is how it's explained in the blog post,

Alan Jeffrey (May 09 2019 at 15:21, on Zulip):

but isn't it equivalent to have the tags on the edges?

RalfJ (May 09 2019 at 15:23, on Zulip):

which blog post? things changed a bit with https://www.ralfj.de/blog/2019/04/30/stacked-borrows-2.html

Alan Jeffrey (May 09 2019 at 15:24, on Zulip):

I was thinking of stacked-borrows-2.

RalfJ (May 09 2019 at 15:25, on Zulip):

the "tags" there are just IDs

RalfJ (May 09 2019 at 15:25, on Zulip):

no Unique/Shared

RalfJ (May 09 2019 at 15:26, on Zulip):

this unique/shared/raw looks a lot like stacked borrows 1

Alan Jeffrey (May 09 2019 at 15:26, on Zulip):

oh I guess I had v1 and v2 mixed up in my head.

Alan Jeffrey (May 09 2019 at 15:26, on Zulip):

does miri implement v1 or v2?

RalfJ (May 09 2019 at 15:27, on Zulip):

nowadays? v2

RalfJ (May 09 2019 at 15:27, on Zulip):

the error msg you copied is from v2

Alan Jeffrey (May 09 2019 at 15:27, on Zulip):

OK, so I should line up with v2 then.

Alan Jeffrey (May 09 2019 at 15:28, on Zulip):

In v2 there's no longer metadata in the pointers, just the memory locations, yes?

RalfJ (May 09 2019 at 15:30, on Zulip):

well, the metadata is the ID

RalfJ (May 09 2019 at 15:31, on Zulip):

so there's still pointer provenance

RalfJ (May 09 2019 at 15:31, on Zulip):

but the per-ptr-metadata no longer says "unique" or "shared" or so. it just says "18" or "25" or "<untagged>".

Alan Jeffrey (May 09 2019 at 15:32, on Zulip):

Is SharedRW just used for interior mutability?

RalfJ (May 09 2019 at 15:33, on Zulip):

no, also for *mut

Alan Jeffrey (May 09 2019 at 15:34, on Zulip):

*const and *mut are treated differently?

RalfJ (May 09 2019 at 15:36, on Zulip):

yes :/

RalfJ (May 09 2019 at 15:36, on Zulip):

they are treated differently by the borrow checker

RalfJ (May 09 2019 at 15:37, on Zulip):

so as long as that is the case, I feel it also makes sense for Stacked Borrows, which is like a "dynamic extension" of the borrow checker

Alan Jeffrey (May 09 2019 at 15:37, on Zulip):

TIL

Alan Jeffrey (May 09 2019 at 15:37, on Zulip):

/me reads https://github.com/rust-lang/rust/issues/56604#issuecomment-477954315

RalfJ (May 09 2019 at 15:37, on Zulip):

to be clear, the difference is only in what happens when you create the raw ptr (from a ref)

RalfJ (May 09 2019 at 15:37, on Zulip):

after that, they behave the same

RalfJ (May 09 2019 at 15:47, on Zulip):

lol I can watch you edit :P

Alan Jeffrey (May 09 2019 at 16:01, on Zulip):

OK, is the current version more in line with stacked borrows v2?

RalfJ (May 09 2019 at 16:06, on Zulip):

the diagram looks great! the comment below is not entirely correct though ("UB: creating a unique reference to a shared location")

RalfJ (May 09 2019 at 16:06, on Zulip):

if the unique ref was created from x, all would be fine

RalfJ (May 09 2019 at 16:06, on Zulip):

the issue is creating a unique ref from an RO pointer

RalfJ (May 09 2019 at 16:07, on Zulip):

(aka a ptr with an ID that just has RO permission in the stack)

Alan Jeffrey (May 09 2019 at 16:14, on Zulip):

@RalfJ OK, I am now confused...

Alan Jeffrey (May 09 2019 at 16:15, on Zulip):

the granting item for creating r is SharedRW isn't it?

RalfJ (May 09 2019 at 16:17, on Zulip):

no. your SharedRW is wrong. (I had missed that.)

RalfJ (May 09 2019 at 16:17, on Zulip):

raw-to-raw-casts do nothing

RalfJ (May 09 2019 at 16:17, on Zulip):

the interesting action is your &T-to-*const T when q gets created.

RalfJ (May 09 2019 at 16:17, on Zulip):

that adds a SharedRO(<untagged>)

Alan Jeffrey (May 09 2019 at 16:20, on Zulip):

Ah, in (p as *const T as *mut T) it's only the SharedRO that gets pushed on the stack, not the sharedRW?

RalfJ (May 09 2019 at 16:20, on Zulip):

Showing the untagged item as just SharedRW is a bit misleading since this tag does not apply to all pointers -- it only applies to untagged ptrs

RalfJ (May 09 2019 at 16:20, on Zulip):

Ah, in (p as *const T as *mut T) it's only the SharedRO that gets pushed on the stack, not the sharedRW?

correct. no SharedRW ever gets pushed in your example.

Alan Jeffrey (May 09 2019 at 16:24, on Zulip):

OK, I replaced that by _: SharedRO

Alan Jeffrey (May 09 2019 at 16:25, on Zulip):

since the slide no longer has any SharedRW on it, I'm tempted to s/sharedRO/shared/

RalfJ (May 09 2019 at 16:26, on Zulip):

I'd still also fix the sentence at the bottom

RalfJ (May 09 2019 at 16:27, on Zulip):

the issue with r is not the location, its the pointer it comes from

Alan Jeffrey (May 09 2019 at 16:31, on Zulip):

Oh I see, so when doing q.as_mut() we are looking for a granting item with tag _: Unique or _: SharedRW and there is none.

RalfJ (May 09 2019 at 16:36, on Zulip):

yes. (and it's _ because that's q's tag)

RalfJ (May 09 2019 at 16:37, on Zulip):

that's not "requires a _: unique" though

RalfJ (May 09 2019 at 16:37, on Zulip):

if you dont want to mention SharedRW, maybe state the negative? "UB: Creating a unique reference from a SharedRO-pointer"

Alan Jeffrey (May 09 2019 at 16:38, on Zulip):

hmm, I guess I elided too much by getting rid of sharedRW.

Alan Jeffrey (May 09 2019 at 17:00, on Zulip):

BTW, while I was writing the slides, I was wondering if there's a model where we consider pointers to have Drop code that has no effect on the state, but updates the shadow state? Then all the "removing entries from the stack" would be done by drop, not by accesses.

Alan Jeffrey (May 09 2019 at 17:01, on Zulip):

This model would have more UB, as it would depend on when the compiler inserts drops for pointers, which it can only do using static information .

Alan Jeffrey (May 09 2019 at 17:17, on Zulip):

Oops should have tagged @RalfJ re ^

Alan Jeffrey (May 09 2019 at 17:17, on Zulip):

The venue for the talk is https://www.meetup.com/Chicago-Rust-Meetup/events/260918979/

RalfJ (May 09 2019 at 17:52, on Zulip):

BTW, while I was writing the slides, I was wondering if there's a model where we consider pointers to have Drop code that has no effect on the state, but updates the shadow state? Then all the "removing entries from the stack" would be done by drop, not by accesses.

I haven't thought about this. It wouldn't really be implementable in Miri because there's no actual code saying when that "virtual drop" happens. I mean, &T are even Copy, that kind of contradicts the idea of them being Drop as well. And then there is the question of what happens when someone mem::forget's?

RalfJ (May 09 2019 at 17:52, on Zulip):

also with NLL we do have ptrs that get invalidated before they would get dropped. so it dosn't seem to me like it'd be a good fit.

RalfJ (May 09 2019 at 17:52, on Zulip):

The venue for the talk is https://www.meetup.com/Chicago-Rust-Meetup/events/260918979/

cool!

RalfJ (May 09 2019 at 17:52, on Zulip):

@Alan Jeffrey ^

Alan Jeffrey (May 09 2019 at 18:04, on Zulip):

@RalfJ yes, you'd have to introduce a type &immut T which is like &T but doesn't implement Copy, and have all &mut T to &T coercions go via &immut T.

Alan Jeffrey (May 09 2019 at 18:05, on Zulip):

That way &immut T could have drop code.

Alan Jeffrey (May 09 2019 at 18:05, on Zulip):

And grr, mem::forget, grr.

RalfJ (May 09 2019 at 18:08, on Zulip):

RalfJ yes, you'd have to introduce a type &immut T which is like &T but doesn't implement Copy, and have all &mut T to &T coercions go via &immut T.

I dont think that'd be enough; we still also have to do retagging for regulat &T to be sure we really have a pointer with the right permissions

Alan Jeffrey (May 09 2019 at 19:43, on Zulip):

I wrote a very rough first draft implementation at https://play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=79c808e6d9d84a4176083b517d1680db

Alan Jeffrey (May 09 2019 at 19:46, on Zulip):

@RalfJ no interior mutability, checks for use-after-free etc. But it does have the idea of using drop code to update shadow state on &immut T. The shadow state is very simple, just one bit!

RalfJ (May 09 2019 at 19:47, on Zulip):

My first attempt in 2017, "Types as Contracts", relied on EndLifetime -- knowing in the code when a lifetime ended. I kind of abandoned that idea after my experience there. But this is somehow different, it per-reference, not per-lifetime.

Alan Jeffrey (May 09 2019 at 19:52, on Zulip):

@RalfJ yes, this is sort of like using explicit markers for lifetimes, but using them to explicitly freeze / thaw a mutable reference.

Alan Jeffrey (May 09 2019 at 19:53, on Zulip):

Of course really you'd want each byte to have its own shadow state, not just each object.

RalfJ (May 10 2019 at 07:11, on Zulip):

still, to support NLL this pretty much requires the borrow checker to mark in the code where lifetimes end. And with pollonius, not even the borrow checker knows.

Alan Jeffrey (May 10 2019 at 15:38, on Zulip):

@RalfJ Since the lifetime ends are just used to update the shadow state, can the spec just give the compiler the freedom to add them wherever it likes? This doesn't help miri though :/

RalfJ (May 10 2019 at 16:35, on Zulip):

that also sounds rather inconvenient when you try to argue that your unsafe code is correct -- which crucially depends on the shadow state

RalfJ (May 10 2019 at 16:36, on Zulip):

I dont think the compiler should have the freedom to insert code whereever it likes if that code can cause UB^^

Alan Jeffrey (May 13 2019 at 00:09, on Zulip):

@RalfJ True, but it's the same annoyance as reasoning about any program with drop code.

Alan Jeffrey (May 13 2019 at 00:09, on Zulip):

I wrote a cleaner version of this at https://play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=90773fba2b71073841015190bc8c1fdb

RalfJ (May 13 2019 at 11:07, on Zulip):

RalfJ True, but it's the same annoyance as reasoning about any program with drop code.

@Alan Jeffrey not really... the other drop code is real, and when we are working on the MIR it is explicit. that is one reason why I like to work on the MIR level.

RalfJ (May 13 2019 at 11:09, on Zulip):

Also, I think there is not enough information here to handle interior mutability -- in particular, code like this where & and &mut alias and both can be reborrowed:

fn aliasing_mut_and_shr() {
    fn inner(rc: &RefCell<i32>, aliasing: &mut i32) {
        *aliasing += 4;
        let _escape_to_raw = rc as *const _;
        *aliasing += 4;
        let _shr = &*rc;
        *aliasing += 4;
        // also turning this into a frozen ref now must work
        let aliasing = &*aliasing;
        let _val = *aliasing;
        let _escape_to_raw = rc as *const _; // this must NOT unfreeze
        let _val = *aliasing;
        let _shr = &*rc; // this must NOT unfreeze
        let _val = *aliasing;
    }

    let rc = RefCell::new(23);
    let mut bmut = rc.borrow_mut();
    inner(&rc, &mut *bmut);
    drop(bmut);
    assert_eq!(*rc.borrow(), 23+12);
}
Alan Jeffrey (May 13 2019 at 14:58, on Zulip):

I think we should move this to a new topic...

Alan Jeffrey (May 30 2019 at 14:25, on Zulip):

I gave the talk, it seemed to go well.

RalfJ (May 30 2019 at 14:35, on Zulip):

awesome :)

Alan Jeffrey (May 30 2019 at 14:39, on Zulip):

The talk was recorded, though there may have been issues with the audio, so we shall see if its usable. I hope I didn't say anything too controversial!

Alan Jeffrey (May 30 2019 at 14:40, on Zulip):

I did get a comment afterwards of "boy you don't like C APIs", which is probably true.

Last update: Nov 19 2019 at 18:00UTC