clarify relation of CTFE correctness and const safety

[web.git] / personal / _posts / 2017-07-14-undefined-behavior.md

diff --git a/personal/_posts/2017-07-14-undefined-behavior.md b/personal/_posts/2017-07-14-undefined-behavior.md
index d664512261876b448b4abc8c287edcff970db549..8176aaf552e60f7f272fd25936e4d5df564fbdd3 100644 (file)
--- a/personal/_posts/2017-07-14-undefined-behavior.md
+++ b/personal/_posts/2017-07-14-undefined-behavior.md
@@ -3,13 +3,12 @@ title: Undefined Behavior and Unsafe Code Guidelines
 categories: internship rust
 ---
 
 categories: internship rust
 ---
 

-Last year, the [Rust unsafe code guidelines strike team](https://internals.rust-lang.org/t/next-steps-for-unsafe-code-guidelines/3864) was founded, and I am on it.
-This is my first official Rust-related position. :-)
-So, finally, with just less than one year of a delay, this is my take at what the purpose of that team is.
+Last year, the [Rust unsafe code guidelines strike team](https://internals.rust-lang.org/t/next-steps-for-unsafe-code-guidelines/3864) was founded, and I am on it. :-)
+So, finally, just one year later, this post is my take at what the purpose of that team is.

 <!-- MORE -->
 Warning:  This post may contain opinions.  You have been warned.
 
 <!-- MORE -->
 Warning:  This post may contain opinions.  You have been warned.
 

-## When are optimizations legal?
+## When are Optimizations Legal?

 
 Currently, we have a pretty good understanding of what the intended behavior of *safe* Rust is.
 That is, there is general agreement (modulo some [bugs](https://github.com/rust-lang/rust/issues/27868)) about the order in which operations are to be performed, and about what each individual operation does.
 
 Currently, we have a pretty good understanding of what the intended behavior of *safe* Rust is.
 That is, there is general agreement (modulo some [bugs](https://github.com/rust-lang/rust/issues/27868)) about the order in which operations are to be performed, and about what each individual operation does.


@@ -38,12 +37,12 @@ After all, if there is any execution for which the assumption does *not* hold, t
 Now, it turns out that it is often really hard to obtain precise aliasing information.
 This could be the end of the game:  No alias information, no way to verify our assumptions, no optimizations.
 
 Now, it turns out that it is often really hard to obtain precise aliasing information.
 This could be the end of the game:  No alias information, no way to verify our assumptions, no optimizations.
 

-## But we want to optimize anyway!
+## Shifting Responsibility

 
 

-However, it turns out that compilers writers want these optimizations *so badly* that they came up with an alternative solution:
-Instead of putting the burden for verifying such assumptions on the compiler, they put it on the programmer.
+However, it turns out that compiler writers consider these optimizations important enough that they came up with an alternative solution:
+Instead of having the compiler verify such assumptions, they declared the programmer responsible.

 
 

-To this end, the C standard says that memory accesses have to happen with the right "effective type":  If data was stored with a `float` pointer, it must not be read with an `int` pointer.
+For example, the C standard says that memory accesses have to happen with the right "effective type":  If data was stored with a `float` pointer, it must not be read with an `int` pointer.

 If you violate this rule, your program has *undefined behavior* (UB) -- which is to say, the program may do *anything* when executed.
 Now, if the compiler wants to make a transformation like reordering the two stores in our example, it can argue as follows:
 In any particular execution of the given function, either `x` and `y` alias or they do not.
 If you violate this rule, your program has *undefined behavior* (UB) -- which is to say, the program may do *anything* when executed.
 Now, if the compiler wants to make a transformation like reordering the two stores in our example, it can argue as follows:
 In any particular execution of the given function, either `x` and `y` alias or they do not.


@@ -53,13 +52,24 @@ However, if they *do* alias, that would violate the effective type restriction,
 As we have seen, in both of the possible cases, the reordering is correct; the compiler is thus free to perform the transformation.
 
 Undefined behavior moves the burden of proving the correctness of this optimization from the compiler to the programmer.
 As we have seen, in both of the possible cases, the reordering is correct; the compiler is thus free to perform the transformation.
 
 Undefined behavior moves the burden of proving the correctness of this optimization from the compiler to the programmer.

-Unfortunately, it is often not easy to say whether a program has undefined behavior or not -- after all, such an analysis being difficult is the entire reason compilers rather rely on UB to perform their optimizations.
+In the example above, what the "effective type" rule really means is that every single memory read of a `float` comes with a *proof obligation*:
+The programmer has to show that that the last write to this memory actually happened through a `float` pointer (baring some exceptions around union and character pointers).
+Similarly, the (in)famous rule that [signed integer overflow is undefined behavior](https://stackoverflow.com/questions/16188263/is-signed-integer-overflow-still-undefined-behavior-in-c) means that every single arithmetic operation on signed integers comes with the proof obligation that this operation will never, ever, overflow.
+The compiler performs its optimization under the assumption that the programmer actually went through the effort and convinced itself that this is the case.
+
+Considering that the compiler can only be so smart, this is a great way to justify optimizations that would otherwise be difficult or impossible to perform.
+Unfortunately, it is often not easy to say whether a program has undefined behavior or not -- after all, such an analysis being difficult is the entire reason compilers have to rely on UB to perform their optimizations.

 Furthermore, while C compilers are happy to exploit the fact that a particular program *has* UB, they do not provide a way to test that executing a program *does not* trigger UB.
 Furthermore, while C compilers are happy to exploit the fact that a particular program *has* UB, they do not provide a way to test that executing a program *does not* trigger UB.

-In fact, it is pretty hard to perform such a test; the standard has not been written with such considerations in mind.
-This has given UB a very bad reputation, and mostly rightly so, I would say.
-[A lengthy blog post](https://blog.regehr.org/archives/1520) summarizes the situation quite well:
-There is progress being made with various sanitizers, but e.g. for the effective type restriction we discussed above, the mitigation (i.e., the way to check or otherwise make sure your programs are not affected) is "turn off optimizations that rely on this".
-That's not very satisfying.
+It also turns out that programmers' intuition often [does not match what the compiler does](https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html), which leads to miscompilations (in the eye of the programmer) and sometimes to security [vulnerabilities](https://lwn.net/Articles/342330/).
+As a consequence, UB has a pretty bad reputation.
+(The fact that most people will not expect an innocent-looking `+` operation to come with subtle proof obligations concerning overflow probably also plays a role in this.
+In other words, this is also an API design problem.)
+
+There are various sanitizers that watch a program while it is being executed and try to detect UB, but they are not able to catch all possible sources of UB.
+Part of the reason this is so hard is that the standard has not been written with such sanitizers in mind.
+This [recent blog post](https://blog.regehr.org/archives/1520) discusses the situation in much more detail.
+For example, for the effective type restriction (also sometimes called "strict aliasing" or "type-based alias analysis") we discussed above, the mitigation -- the way to check or otherwise make sure your programs are not affected -- is to turn off optimizations that rely on this.
+That is not very satisfying.

 
 ## Undefined Behavior in Rust
 
 
 ## Undefined Behavior in Rust
 


@@ -75,12 +85,17 @@ This is what the unsafe code guidelines strike team set out to do.
 We could of course just copy what C does, but I hope I convinced you that this is not a great solution.
 When defining UB for Rust, I hope we can do better than C.
 I think we should strive for programmers' intuition agreeing with the standard and the compiler on what the rules are.
 We could of course just copy what C does, but I hope I convinced you that this is not a great solution.
 When defining UB for Rust, I hope we can do better than C.
 I think we should strive for programmers' intuition agreeing with the standard and the compiler on what the rules are.

-It turns out that is [not the case for C](https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html), which leads to miscompilations and sometimes to security [vulerabilities](https://lwn.net/Articles/342330/).
+If that means we have to be a little more conservative around our optimizations, that seems to be a prize worth paying for more confidence in the compiled program.

 
 

-I also think that tooling to *detect* UB is of paramount importance, and that the specification should be written in a way that such tooling is feasible.
+I also think that tooling to *detect* UB is of paramount importance, and can help shape intuition and maybe even permit us to be less conservative.
+To this end, the specification should be written in a way that such tooling is feasible.

 In fact, specifying a dynamic UB checker is a very good way to specify UB!
 Such a specification would describe the additional state that is needed at run-time to then *check* at every operation whether we are running into UB.
 It is with such considerations in my mind that I have previously written about [miri as an executable specification]({{ site.baseurl }}{% post_url 2017-06-06-MIR-semantics %}).
 
 Coming up next on this channel:  During my [internship]({{ site.baseurl }}{% post_url 2017-05-23-internship-starting %}), I am working on such a specification.
 In fact, specifying a dynamic UB checker is a very good way to specify UB!
 Such a specification would describe the additional state that is needed at run-time to then *check* at every operation whether we are running into UB.
 It is with such considerations in my mind that I have previously written about [miri as an executable specification]({{ site.baseurl }}{% post_url 2017-06-06-MIR-semantics %}).
 
 Coming up next on this channel:  During my [internship]({{ site.baseurl }}{% post_url 2017-05-23-internship-starting %}), I am working on such a specification.

-I have a draft ready now, and I want to share it with the world to see what the world thinks about it.
+My ideas are concrete enough now that I can write down a draft, which I will share with the world to see what the world thinks about it.
+
+**Update:** [Writing down has happened]({{ site.baseurl }}{% post_url 2017-07-17-types-as-contracts %}).
+
+**Update:** Clarified "Shifting Responsibility".