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

Topic: ucg#203

gnzlbg (Sep 19 2019 at 07:44, on Zulip):

@RalfJ I was wondering if we need to use the term "Undefined Behavior" in the spec at all

gnzlbg (Sep 19 2019 at 07:45, on Zulip):

One thing that is becoming clearer to me is that it is a bad name, it means different things to different people, and the name is not really that self-describing. What does undefined mean? Not defined? A lot of things are not defined, out of scope, unspecified, etc.

gnzlbg (Sep 19 2019 at 07:46, on Zulip):

One thing I'm tending to wish more and more is that we would, instead, define what "guaranteed behavior" is

gnzlbg (Sep 19 2019 at 07:47, on Zulip):

Or something like that, that talks about: if you stick to the contract of the rust abstract machine, the compiler / impl guarantees that your program runs on real hardware according to the abstract machine rules.

gnzlbg (Sep 19 2019 at 07:48, on Zulip):

And then talking about implementation-defined/unspecified might become: the implementation must guarantee what the behavior is, and for implementation-defined it must say what those guarantees are

gnzlbg (Sep 19 2019 at 07:49, on Zulip):

The guarantee then cannot be "there are no guarantees", since the abstract machines requires the implementation to have to guarantee some concrete behavior

gnzlbg (Sep 19 2019 at 07:49, on Zulip):

After going through all that, then we come to "behavior for which there are no guarantees, not by the abstract machine, implementation, etc."

gnzlbg (Sep 19 2019 at 07:51, on Zulip):

The implementation might provide some, the hardware might provide some, but that doesn't matter for the abstract machine

gnzlbg (Sep 19 2019 at 07:51, on Zulip):

The abstract machine can do anything, like optimizing away code that reaches there.

gnzlbg (Sep 19 2019 at 07:51, on Zulip):

Users cannot do negative reasoning about this type of behavior.

gnzlbg (Sep 19 2019 at 07:52, on Zulip):

To allow users to assume that something cannot happen, we would need to provide them with an explicit guarantee that justifies that, e.g., references are guaranteed to never be null

gnzlbg (Sep 19 2019 at 07:53, on Zulip):

I think doing it this way might make the document much easier to understand

gnzlbg (Sep 19 2019 at 07:54, on Zulip):

instead of writing "if you do this, the behavior is undefined", "exhibits undefined behavior", "is undefined behavior" - we'd just more plainly write "The abstract machine does not guarantee anything about programs that do X".

gnzlbg (Sep 19 2019 at 07:56, on Zulip):

Or just like you propose, "Doing X is an error in the abstract machine"

gnzlbg (Sep 19 2019 at 07:56, on Zulip):

That would also link nicely with miri, where the goal is for UB to just be raised as an error.

Lokathor (Sep 20 2019 at 02:25, on Zulip):

Absolutely, we should focus more on saying what's guaranteed. That's both what people writing unsafe code want to know for sure, and also the kind of thing an eventual spec will have to specify.

RalfJ (Oct 09 2019 at 12:52, on Zulip):

Or just like you propose, "Doing X is an error in the abstract machine"

agreed, I think positive statements are better. that said, we likely do still need to relate to C-style terminology, just because many people use it and think they know what it means (many of those are wrong, but well).

RalfJ (Oct 09 2019 at 12:53, on Zulip):

but the roead for that could be to explain UB in terms of this: "UB is an error condition in the abstract machine; the Rust compiler assumes that such errors are never reached by the program it compiles"

RalfJ (Oct 09 2019 at 12:54, on Zulip):

and this is also in line with me saying "it is a spec bug to leave out a case": when the spec does a case distinction, it should explicitly list all cases that are abstract machine errors; there is no "implicit" fall-back to that -- there is no "implicit UB".

gnzlbg (Oct 10 2019 at 05:28, on Zulip):

Makes sense

Last update: Jul 03 2020 at 17:15UTC