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

Topic: Unsafe Policy: does all foreign code count as "an unsafe ...


Lokathor (Feb 28 2020 at 21:25, on Zulip):

Here is some example code:

https://play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=7841ef908f534ef11daca616a16cc0b9

My question is: are the unsafe blocks here actually properly justified? Should we consider it a sound construction?

Suppose you had some other function like this:

#[no_mangle]
pub extern "C" fn foo<'a>(sli: CSharedSlice<'a, u8>) {
  println!("the length is {}", sli.to_slice().len())
}

And a bit of C code calls this function with a totally zeroed struct and UB happens.

If there is UB, it's a bug in the compiler or an unsafe block was used improperly. This is the rule we always live by.

In this case, some C code did the thing which broke the contract of the function and lead to UB. Do we consider the C code to be the improper unsafe block? Because it's still impossible to make foo trigger UB from safe Rust, so it should still be considered sound.

Amanieu (Feb 28 2020 at 22:37, on Zulip):

The original "unsafe block" that is to blame for the UB is the one that invoked the C code that eventually called your function with invalid arguments.

Amanieu (Feb 28 2020 at 22:38, on Zulip):

If your code is a library and the program is in C, then you can just blame the user for the UB since it's his fault he decided to run a C program :mischievous:

Amanieu (Feb 28 2020 at 22:39, on Zulip):

But seriously, I would consider your code perfectly sound as it is.

Lokathor (Feb 28 2020 at 22:48, on Zulip):

Yeah, okay. Might put the full form of this into a crate for easy reference.

ecstatic-morse (Feb 28 2020 at 23:06, on Zulip):

(deleted)

RalfJ (Feb 29 2020 at 08:52, on Zulip):
    // Safety: Safe rust can never construct this type
    // with incorrect fields, so we can trust the fields.

@Lokathor sounds like your type CSharedSlice has some invariant about these fields attached to it.
If you are using "SAFETY:" comments, I think it is a good idea to explicitly write down that invariant in a comment at the type definition. Then "SAFETY" comments elsewhere, like in to_slice can refer to that invariant.
The comment you have there right now is very non-local: this one safety comment suddenly means I need to re-read all the rest of this code to check that what it says is correct. SAFETY comments should be locally checkable.

Lokathor (Feb 29 2020 at 14:02, on Zulip):

Well the safety section is the entire safety section of core::slice::from_raw_parts

Lokathor (Feb 29 2020 at 15:29, on Zulip):

Fundamentally you can't rely on module privacy and then also have local checks

RalfJ (Feb 29 2020 at 18:35, on Zulip):

Lokathor said:

Fundamentally you can't rely on module privacy and then also have local checks

not sure why you'd say that

RalfJ (Feb 29 2020 at 18:36, on Zulip):

but when we formally prove things like RefCell correct, we do everything locally as we'd prefer not to go crazy

RalfJ (Feb 29 2020 at 18:36, on Zulip):

the key point is to put everything global that you might need into the invariant -- because then you can locally check that you always maintain the invariant, and you get to locally assume that everything else follows the invariant, and thus you never need to think about more than one line of code at a time (once the invariant is set)

RalfJ (Feb 29 2020 at 18:37, on Zulip):

when I saw such proofs for the first time my mind was kind of blown :D

RalfJ (Feb 29 2020 at 18:38, on Zulip):

with the current state of the art in formal methods, we can do entirely local proofs (local in "time and space") of the craziest concurrent data structures, and we can do it machine-checked in Coq :)

Lokathor (Mar 01 2020 at 05:28, on Zulip):

Well, assuming that you mean locally to be like, "in the current function", then I don't know how you can possibly locally check an invariant such as "the length value is correct for the allocation associated with this pointer so we can make this slice".

Lokathor (Mar 01 2020 at 05:30, on Zulip):

But, to "zoom out" a bit, there is now a proper draft of this code available on github, <https://github.com/Lokathor/chromium/blob/master/src/c_shared_slice.rs> and I'll add the mutable version tomorrow and put it out as a 0.0.1 if things look good.

RalfJ (Mar 01 2020 at 18:17, on Zulip):

Lokathor said:

Well, assuming that you mean locally to be like, "in the current function", then I don't know how you can possibly locally check an invariant such as "the length value is correct for the allocation associated with this pointer so we can make this slice".

you have to declare the invariant once, globally. and then you, roughly speaking, check locally at each line that it is maintained.

Lokathor (Mar 01 2020 at 18:23, on Zulip):

I agree with that, but I also absolutely wouldn't call it "locally checkable"

RalfJ (Mar 02 2020 at 10:25, on Zulip):

hm. well "local" ("in time and space") is the/a standard term for this in the academic literature, but I am open to alternative suggestions ;)

RalfJ (Mar 02 2020 at 10:26, on Zulip):

there are other proof methods where verifying one thread requires checking something specific to this thread about all the other threads -- that is then not "local" any more

Last update: Jun 05 2020 at 21:20UTC