Stream: wg-ffi-unwind

Topic: tbd vs ub vs unspecified behavior


nikomatsakis (Oct 16 2019 at 10:05, on Zulip):

I've prepared a pull request that refines the terminology along the lines we discussed yesterday. In particular, it separates

nikomatsakis (Oct 16 2019 at 10:05, on Zulip):

Comments welcome.

nikomatsakis (Oct 16 2019 at 10:06, on Zulip):

@gnzlbg, does that address your confusion?

gnzlbg (Oct 16 2019 at 11:55, on Zulip):

Yes. I think that matches how I worded my thoughts in the other PR, where UB is mostly only used for "there is no reasonable way in which we could define the behavior here or no useful guarantees that we could provide"

Kyle Strand (Oct 16 2019 at 16:38, on Zulip):

Thanks very much for doing this. I have been thinking that introducing some terminology as a standard for the Rust project overall would be worth its own RFC, but in the mean time this WG can adopt it for our own purposes, as long as we're explicit about it

Kyle Strand (Oct 16 2019 at 16:38, on Zulip):

only gave a cursory look to the PR so far but I think it seems good

nikomatsakis (Oct 17 2019 at 16:19, on Zulip):

@gnzlbg regarding our discussion on https://github.com/nikomatsakis/project-ffi-unwind/pull/10, I tried to summarize the situation and all relevant facts in a hackmd document -- I'm curious if you feel there are points missing or points that you disagree with in there.

gnzlbg (Oct 17 2019 at 16:32, on Zulip):

So I think that captures most of it

gnzlbg (Oct 17 2019 at 16:32, on Zulip):

In the section about whether TBD should hit stable, I'd word it a bit differently

gnzlbg (Oct 17 2019 at 16:32, on Zulip):

All unspecified behavior hits stable, that's normal

gnzlbg (Oct 17 2019 at 16:33, on Zulip):

I don't think it is worth it to introduce a definition for TBD in the rust language reference

gnzlbg (Oct 17 2019 at 16:33, on Zulip):

I think it would suffice to say "unspecified behavior" and maybe have a note saying "we are trying to specify this here (link)"

gnzlbg (Oct 17 2019 at 16:34, on Zulip):

When it comes to unspecified behavior, we have all sorts of notes everywhere anyways documenting how certain platforms work

gnzlbg (Oct 17 2019 at 16:35, on Zulip):

For me personally, it would be useful to be able to tell when reading a document that should turn into an RFC at some point, which parts of the document are unspecified because we intend the feature to hit stable in that way, and which parts are unspecified because we haven't looked at it yet

nikomatsakis (Oct 17 2019 at 16:37, on Zulip):

I don't think it is worth it to introduce a definition for TBD in the rust language reference

(I didn't intend to either)

nikomatsakis (Oct 17 2019 at 16:37, on Zulip):

I think it would suffice to say "unspecified behavior" and maybe have a note saying "we are trying to specify this here (link)"

exactly what I had in mind

gnzlbg (Oct 17 2019 at 16:38, on Zulip):

For users on stable Rust that have to use such unspecified behavior, it is obviously useful as well to know which unspecified behavior is intended to be unspecified long term, and which is being worked on, so it would be nice to have a way to hint at this as well

gnzlbg (Oct 17 2019 at 16:38, on Zulip):

exactly what I had in mind

So I think we agree. The document looks fine to me.

nikomatsakis (Oct 17 2019 at 16:40, on Zulip):

great.

nikomatsakis (Oct 17 2019 at 16:40, on Zulip):

I updated it a bit to clarify the points you raised

gnzlbg (Oct 17 2019 at 16:43, on Zulip):

I've added an answer to the question about stable Rust code using this already

gnzlbg (Oct 17 2019 at 16:43, on Zulip):

We have had nightly features to avoid UB for a while, and for different reasons, users have not been able to use them

nikomatsakis (Oct 17 2019 at 17:03, on Zulip):

I've added an answer to the question about stable Rust code using this already

good point!

nikomatsakis (Oct 17 2019 at 17:03, on Zulip):

BTW, @gnzlbg, I can't entirely tell if this concern is still relevant

gnzlbg (Oct 17 2019 at 17:04, on Zulip):

No it isn't, has been resolved

gnzlbg (Oct 17 2019 at 17:04, on Zulip):

For some reason I cannot resolve it :/

gnzlbg (Oct 17 2019 at 17:04, on Zulip):

The button does not show

nikomatsakis (Oct 17 2019 at 17:05, on Zulip):

oh probably because you don't have write access or something to the repo

nikomatsakis (Oct 17 2019 at 17:05, on Zulip):

I should transfer this to rust-lang

gnzlbg (Oct 17 2019 at 17:05, on Zulip):

Ah ok, that makes sense, please resolve it for me

nikomatsakis (Oct 17 2019 at 17:05, on Zulip):

I was kind of waiting but .. that's sort of silly

nikomatsakis (Oct 17 2019 at 17:13, on Zulip):

OK, I revised some of the text and added that hackmd to the repo as our first "resolved concern" and I pushed some other improvements. Going to merg.

Kyle Strand (Oct 17 2019 at 18:04, on Zulip):

Once again I submitted a review post-merge...not sure how inconvenient that is as a form of communication.

Kyle Strand (Oct 25 2019 at 09:51, on Zulip):

How is "unsoundness" defined? Is it potentially a better term than "LLVM-UB" for things that are known to be unsafe?

gnzlbg (Oct 25 2019 at 09:59, on Zulip):

The UCG reference has a definition for that

gnzlbg (Oct 25 2019 at 10:00, on Zulip):

https://github.com/rust-lang/unsafe-code-guidelines/blob/master/reference/src/glossary.md#soundness-of-code--of-a-library

gnzlbg (Oct 25 2019 at 10:01, on Zulip):

"sound == well-typed programs cannot cause Undefined Behavior"

centril (Oct 25 2019 at 10:01, on Zulip):

A safe function is unsound if for some inputs or program states it can lead to a trace that has UB.

gnzlbg (Oct 25 2019 at 10:02, on Zulip):

@Kyle Strand since sound is defined in terms of UB, i don't think you can replace "LLVM-UB" with it (EDIT: unless I'm misunderstanding which use of LLVM-UB you are talking about)

centril (Oct 25 2019 at 10:02, on Zulip):

@Kyle Strand https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/ is a good read

gnzlbg (Oct 25 2019 at 10:04, on Zulip):

Probably not the best introduction if you haven't used the term before

Last update: Nov 15 2019 at 10:50UTC