update screen render of thesis

[web.git] / personal / _drafts / provenance-matters.md

diff --git a/personal/_drafts/provenance-matters.md b/personal/_drafts/provenance-matters.md
index 33e843a6d06057c3480c8260fa5acb9a0a64ad58..708f9c19686294ec37c20219ce23bb7bc0596d6d 100644 (file)
--- a/personal/_drafts/provenance-matters.md
+++ b/personal/_drafts/provenance-matters.md
@@ -1,5 +1,5 @@
 ---
 ---

-title: "Pointers Are Complicated II, or: Language first, Optimizations second"
+title: "Pointers Are Complicated II, or: We need better language specs"

 categories: rust
 ---
 
 categories: rust
 ---
 


@@ -10,14 +10,14 @@ One key point I was trying to make is that
 
 This "extra information" that distinguishes different pointers to the same address is typically called [*provenance*](https://rust-lang.github.io/unsafe-code-guidelines/glossary.html#pointer-provenance).
 This post is a cautionary tale of what can happen when provenance is not considered sufficiently carefully in an optimizing compiler.
 
 This "extra information" that distinguishes different pointers to the same address is typically called [*provenance*](https://rust-lang.github.io/unsafe-code-guidelines/glossary.html#pointer-provenance).
 This post is a cautionary tale of what can happen when provenance is not considered sufficiently carefully in an optimizing compiler.

-There is also a larger message here about how we should consider compiler IRs primarily from the perspective of a programming language, and only secondarily from the perspective of "which set of optimizations does this allow".
+There is also a larger message here about how we could prevent such issues from coming up in the future by spending more effort on the specification of compiler IRs.

 
 <!-- MORE -->
 
 
 <!-- MORE -->
 

-I will show a series of three compiler transformation that each seem "intuitively justified" based on wording in the C standard and some common understanding of how pointers work.
+I will show a series of three compiler transformations that each seem "intuitively justified", but when taken together they lead to a clearly incorrect result.

 We will use LLVM for these examples, but the goal is not to pick on LLVM---other compilers suffer from similar issues.
 The goal is to convince you that to build a correct compiler for languages permitting unsafe pointer manipulation such as C, C++, or Rust,
 We will use LLVM for these examples, but the goal is not to pick on LLVM---other compilers suffer from similar issues.
 The goal is to convince you that to build a correct compiler for languages permitting unsafe pointer manipulation such as C, C++, or Rust,

-we need to take provenance specifically and IR semantics more generally seriously.
+we need to take provenance specifically and IR semantics in general more seriously.

 Let's get started!
 
 ## Warm-up: Why IRs need a precise semantics
 Let's get started!
 
 ## Warm-up: Why IRs need a precise semantics


@@ -71,28 +71,27 @@ In a call to `sum_up(INT_MAX, 1, 0)`, the `s` variable introduced by loop hoisti
 Due to this behavior of signed integer overflow, the loop hoisting optimization is *correct* if we consider it as an optimization on programs that are written in LLVM IR.[^cheat]
 In particular, this means we can freely combine this optimization with any other optimization that is *correct* in LLVM IR (such as inlining, replacing definite UB by `unreachable`, and removing unreachable code), and we can be sure that the result obtained after all these optimizations is a correct compilation of our original program.
 
 Due to this behavior of signed integer overflow, the loop hoisting optimization is *correct* if we consider it as an optimization on programs that are written in LLVM IR.[^cheat]
 In particular, this means we can freely combine this optimization with any other optimization that is *correct* in LLVM IR (such as inlining, replacing definite UB by `unreachable`, and removing unreachable code), and we can be sure that the result obtained after all these optimizations is a correct compilation of our original program.
 

-However, to make the argument that an optimization is *correct*, the exact semantics of LLVM IR (what the behavior of all possible programs is and when they have UB) needs to be precisely and unambiguously documented.
+However, to make the argument that an optimization is *correct*, the exact semantics of LLVM IR (what the behavior of all possible programs is and when they have UB) needs to be documented.

 All involved optimizations need to exactly agree on what is and is not UB, to ensure that whatever code they produce will not be considered UB by a later optimization.[^ub-difference]
 This is exactly what we also expect from the specification of a programming language such as C, which is why I think we should consider compiler IRs as proper programming languages in their own right, and specify them with the same diligence as we would specify "normal" languages.
 Sure, no human is going to write many programs in LLVM IR, but clang and rustc produce LLVM IR programs all the time, and as we have seen understanding the exact rules governing these programs is crucial to ensuring that the optimizations LLVM performs do not change program behavior.
 
 [^cheat]: If now you feel like we somehow cheated, since we can always translate the program from C to LLVM IR, optimize there, and translate back, consider this: translating from LLVM IR to C is really hard! In particular, singed integer addition in LLVM IR can *not* be translated into signed integer addition in C, since the former is well-defined with `poison` result in case of overflow, but the latter says overflow is UB. C has, in a sense, strictly more UB than LLVM IR, which makes translation in one direction easy, while the other direction is hard.
 
 All involved optimizations need to exactly agree on what is and is not UB, to ensure that whatever code they produce will not be considered UB by a later optimization.[^ub-difference]
 This is exactly what we also expect from the specification of a programming language such as C, which is why I think we should consider compiler IRs as proper programming languages in their own right, and specify them with the same diligence as we would specify "normal" languages.
 Sure, no human is going to write many programs in LLVM IR, but clang and rustc produce LLVM IR programs all the time, and as we have seen understanding the exact rules governing these programs is crucial to ensuring that the optimizations LLVM performs do not change program behavior.
 
 [^cheat]: If now you feel like we somehow cheated, since we can always translate the program from C to LLVM IR, optimize there, and translate back, consider this: translating from LLVM IR to C is really hard! In particular, singed integer addition in LLVM IR can *not* be translated into signed integer addition in C, since the former is well-defined with `poison` result in case of overflow, but the latter says overflow is UB. C has, in a sense, strictly more UB than LLVM IR, which makes translation in one direction easy, while the other direction is hard.
 

-[^ub-difference]: In fact, I would say that two different variants of the IR with different rules for UB are really *two different programming languages*. A program that is well-defined in one language may have UB in another, so great care needs to be taken when the program is moved from being governed by one set of rules to another.
+[^ub-difference]: In particular, I would say that two different variants of the IR with different rules for UB are really *two different programming languages*. A program that is well-defined in one language may have UB in another, so great care needs to be taken when the program is moved from being governed by one set of rules to another.

 
 *Take-away:* If we want to be able to justify the correctness of a compiler in a modular way, considering only one optimization at a time, we need to perform these optimizations in an IR that has a precise specification of all aspects of program behavior, including UB.
 Then we can, for each optimization separately, consider the question: does the optimization ever change program behavior, and does it ever introduce UB into UB-free programs?
 
 ## How 3 (seemingly) correct optimizations can be incorrect when used together
 
 
 *Take-away:* If we want to be able to justify the correctness of a compiler in a modular way, considering only one optimization at a time, we need to perform these optimizations in an IR that has a precise specification of all aspects of program behavior, including UB.
 Then we can, for each optimization separately, consider the question: does the optimization ever change program behavior, and does it ever introduce UB into UB-free programs?
 
 ## How 3 (seemingly) correct optimizations can be incorrect when used together
 

-With the warm-up done, we are now ready to consider some more tricky optimizations.
+With the warm-up done, we are now ready to consider some more tricky optimizations, which we will use to explore the question of how precise a language specification needs to be.

 We will look at three different optimizations LLVM can perform, and I will show that they *cannot all be correct* since the first and last program we are considering actually have *different behavior*.
 (More precisely: the last program has a possible behavior that was not possible for the first program.)
 This is only possible if at least one optimization changed program behavior in an incorrect way, but it is actually not entirely clear which optimization is the culprit.
 We will look at three different optimizations LLVM can perform, and I will show that they *cannot all be correct* since the first and last program we are considering actually have *different behavior*.
 (More precisely: the last program has a possible behavior that was not possible for the first program.)
 This is only possible if at least one optimization changed program behavior in an incorrect way, but it is actually not entirely clear which optimization is the culprit.

-The reasons this happens, I claim, is that LLVM IR and its optimizations are *not* treated the way our warm-up says they should be treated:
-by precisely defining the behavior and UB of the IR, and arguing why each optimization is *correct* under this definition.
+The reasons this happens, I claim, is that the LLVM IR specification is not precise enough to truly evaluate whether the involved optimizations are *correct*.

 
 

-The sequence of examples is taken from [this talk](https://sf.snu.ac.kr/llvmtwin/files/presentation.pdf#page=32) by Chung-Kil Hur; it was discovered while working on a rigorous specification of LLVM.
+The sequence of examples is taken from [this talk](https://sf.snu.ac.kr/llvmtwin/files/presentation.pdf#page=32) by Chung-Kil Hur; it was discovered while working on a mathematically rigorous specification of LLVM.

 
 Here is the source program:
 {% highlight c %}
 
 Here is the source program:
 {% highlight c %}


@@ -155,8 +154,6 @@ But which one is it?
 In an ideal world, we would have a sufficiently precise semantics for LLVM IR that we would just have to read the docs (or, even better, run some Miri-like tool) to figure out the answer.
 However, describing language semantics at this level of precision is *hard*, and full of trade-offs.
 That's why the LLVM LangRef will not give us a clear answer here, and indeed obtaining a clear answer requires some decisions that have not been explicitly made yet.
 In an ideal world, we would have a sufficiently precise semantics for LLVM IR that we would just have to read the docs (or, even better, run some Miri-like tool) to figure out the answer.
 However, describing language semantics at this level of precision is *hard*, and full of trade-offs.
 That's why the LLVM LangRef will not give us a clear answer here, and indeed obtaining a clear answer requires some decisions that have not been explicitly made yet.

-As a researcher, all I can do is to structure the design space and uncover the trade-offs; it will be up to the LLVM community to decide which option to pick.
-But the key point is that *they will have to make a choice*, because the status quo of doing all three of these optimizations leads to incorrect compilation results.

 
 To proceed, we will use the three optimizations that we considered above as cues: assuming that the optimization is correct for LLVM IR, what does that tell us about the semantics?
 
 
 To proceed, we will use the three optimizations that we considered above as cues: assuming that the optimization is correct for LLVM IR, what does that tell us about the semantics?
 


@@ -179,13 +176,13 @@ Now that we know that provenance exists in pointers, we have to also consider wh
 The second optimization gives us a clue into this aspect of LLVM IR semantics: casting a pointer to an integer and back is optimized away, which means that *integers have provenance*.
 To see why, consider the two expressions `(char*)(int)(p+1)` and `(char*)(int)q`:
 if the optimization of removing pointer-integer-pointer roundtrips is correct, the first operation will output `p+1` and the second will output `q`, which we just established are two different pointers (they differ in their provenance).
 The second optimization gives us a clue into this aspect of LLVM IR semantics: casting a pointer to an integer and back is optimized away, which means that *integers have provenance*.
 To see why, consider the two expressions `(char*)(int)(p+1)` and `(char*)(int)q`:
 if the optimization of removing pointer-integer-pointer roundtrips is correct, the first operation will output `p+1` and the second will output `q`, which we just established are two different pointers (they differ in their provenance).

-The only way to explain this is to say that the input to the `(char*)` cast is different, since the Abstract Machine state is identical in both cases.
+The only way to explain this is to say that the input to the `(char*)` cast is different, since the program state is otherwise identical in both cases.

 But we know that the integer value (i.e., the bit pattern of length 32) that serves as input to the `(char*)` cast is the same, and hence a difference can only arise if integers consist of more than just this bit pattern---just like pointers, integers have provenance.
 
 Finally, let us consider the first optimization.
 Here, a successful equality test `iq == ip` prompts the optimizer to replace one value by the other.
 This optimization demonstrates that *integers do not have provenance*:
 But we know that the integer value (i.e., the bit pattern of length 32) that serves as input to the `(char*)` cast is the same, and hence a difference can only arise if integers consist of more than just this bit pattern---just like pointers, integers have provenance.
 
 Finally, let us consider the first optimization.
 Here, a successful equality test `iq == ip` prompts the optimizer to replace one value by the other.
 This optimization demonstrates that *integers do not have provenance*:

-the optimization is only correct if a successful run-time equality test implies that the two values are equivalent in the Abstract Machine.
+the optimization is only correct if a successful run-time equality test implies that the two values are equivalent in the "Abstract Machine" that is used to describe the language semantics.

 But this means that the Abstract Machine version of this value cannot have any "funny" extra parts that are not represented at run-time.
 Of course, provenance is exactly such a "funny" extra part.
 A different way to phrase the same argument is to say that this optimization is correct only if `iq == ip` implies that both values have the same provenance.
 But this means that the Abstract Machine version of this value cannot have any "funny" extra parts that are not represented at run-time.
 Of course, provenance is exactly such a "funny" extra part.
 A different way to phrase the same argument is to say that this optimization is correct only if `iq == ip` implies that both values have the same provenance.


@@ -215,6 +212,9 @@ This also corresponds to [what has been recently proposed to the C standard comm
 That's why [LLVM bug #34548](https://bugs.llvm.org/show_bug.cgi?id=34548) says that optimizing away pointer-integer-pointer roundtrips is incorrect, and LLVM should stop doing this in the general case.
 There might still be special cases where this can be done, but figuring out the limits of this really needs a more precise description of LLVM IR semantics such as what we proposed [in this paper](https://people.mpi-sws.org/~jung/twinsem/twinsem.pdf).
 
 That's why [LLVM bug #34548](https://bugs.llvm.org/show_bug.cgi?id=34548) says that optimizing away pointer-integer-pointer roundtrips is incorrect, and LLVM should stop doing this in the general case.
 There might still be special cases where this can be done, but figuring out the limits of this really needs a more precise description of LLVM IR semantics such as what we proposed [in this paper](https://people.mpi-sws.org/~jung/twinsem/twinsem.pdf).
 

+But ultimately, it will be up to the LLVM community to make this decision.
+All I can say for sure is that they have to make a choice, because the status quo of doing all three of these optimizations leads to incorrect compilation results.
+

 ## Conclusion
 
 What did we learn?
 ## Conclusion
 
 What did we learn?


@@ -225,32 +225,30 @@ But in a language such as Rust, C or C++ that supports pointer-integer casts, th
 
 We also learned that LLVM has a bug, but that was *not* the point of this blog post.
 The GCC developers [made exactly the same mistake](https://gcc.gnu.org/bugzilla/show_bug.cgi?id=82282), and I got word that MSVC and ICC have the same issue (though I do not know how to verify this).
 
 We also learned that LLVM has a bug, but that was *not* the point of this blog post.
 The GCC developers [made exactly the same mistake](https://gcc.gnu.org/bugzilla/show_bug.cgi?id=82282), and I got word that MSVC and ICC have the same issue (though I do not know how to verify this).

-And I cannot blame them; the way compiler development typically works nowadays, I think bugs like this are inevitable.
+And I cannot blame them; the way compiler development typically works, I think bugs like this are inevitable: when exactly UB arises in an IR is often only loosely specified, so evaluating whether some optimization is *correct* in the sense defined above is basically impossible.

 Pointer provenance is just a particularly good example of where the current approach failed, but it is not the only case.
 For example, [§2.3 of this paper](https://plv.mpi-sws.org/validc/paper.pdf) (see Figure 3 for the code) shows how a sequence of two optimizations can lead to a miscompilation, where the first optimization is correct under the LLVM concurrency model, and the second optimization is correct under the C++11 concurrency model---but there is no concurrency model under which *both* optimizations are correct, so each compiler (or rather, each compiler IR) needs to pick one or the other.
 
 Pointer provenance is just a particularly good example of where the current approach failed, but it is not the only case.
 For example, [§2.3 of this paper](https://plv.mpi-sws.org/validc/paper.pdf) (see Figure 3 for the code) shows how a sequence of two optimizations can lead to a miscompilation, where the first optimization is correct under the LLVM concurrency model, and the second optimization is correct under the C++11 concurrency model---but there is no concurrency model under which *both* optimizations are correct, so each compiler (or rather, each compiler IR) needs to pick one or the other.
 

-Which brings me to my main conclusion for this post: I think the way optimizing compilers for these low-level languages are built is fundamentally flawed.
-The current approach, which one might call "optimizations-first", is to largely think of the semantics of a compiler IR in terms of the set of optimizations that it enables.[^weak-mem]
-However, each additional optimization puts another constraint on the IR semantics---how can we be sure that there even is a way to satisfy all constraints in a single language?
-The only way I know to ensure that the constraint set remains satisfiable, i.e., to ensure that performing all these optimizations in any order does not introduce bugs, is to pick a consistent semantics for the IR and then show each optimization to be *correct* under those semantics, in the sense defined above.
+Which brings me to my main conclusion for this post: to avoid the problem of incompatible optimizations, I think we need to take compiler IRs more serious as programming languages in their own right, and give them a precise specification---including all the UB.
+Now, you may object by saying that LLVM has an extensive LangRef.
+And still, by reading the LLVM specification one could convince oneself that each of the three optimizations above is correct, which as we have seen is contradictory.
+What is missing? Do we need a formal mathematical definition to avoid such ambiguities?
+I do not think so; I think there is something simpler that will already help a lot.
+The source of the contradiction is that some parts of the specification *implicitly* assume that pointers have provenance, which is easy to forget when considering other operations.
+That's why I think it is very important to make such assumptions more explicit: the specification should *explicitly* describe the information that "makes up" a value, which will include things like provenance and whether the value is (wholly or partially) initialized.[^C]
+This information needs to be extensive enough such that a hypothetical interpreter can use it to detect all the UB.
+Doing so makes it obvious that a pointer has provenance, since otherwise it is impossible to correctly check for out-of-bounds pointer arithmetic while also permitting one-past-the-end pointers.

 
 

-[^weak-mem]: We can also clearly see this approach in most discussions around weak memory concurrency effects, which typically are all about which reorderings the compiler is allowed to perform and how barriers can be used to prevent the reorderings. This is the optimizations-first approach in action.
+[^C]: The astute reader will notice that this information is also absent in the C and C++ specifications. That is indeed one my main criticisms of these specifications. It leads to many open questions not only when discussing provenance but also when discussing indeterminate and unspecified values.

 
 

-To avoid the problem of incompatible optimizations, I think we need to take compiler IRs more serious as programming languages in their own right, and properly define the Abstract Machine that describes their semantics---including all the UB!
-I call this "language-first".
-This language definition does not need to be a formal artifact in a proof assistant, but the description needs to be precise enough such that there are no ambiguities, and such that for each desired optimization we can evaluate whether it is *correct* for this IR or not.
-One great way to achieve this is to implement a *reference interpreter* for the IR, an interpreter that not only evaluates IR programs but also says if there was any UB triggered by this execution.
-Writing such an interpreter is a great exercise because it requires explicitly writing out what one could call the "state space" of the Abstract Machine:
-just what *is* a value, which pieces of data are needed to fully describe it, what kind of information is stored in memory, and so on.
-Doing so makes it *immediately obvious* that a pointer has provenance, since otherwise it is impossible to correctly check for out-of-bounds accesses.
+This is my bar for what I consider a sufficiently precise language specification: it needs to contain all the information needed such that writing a UB-checking interpreter is just a matter of "putting in the work", but does not require introducing anything new that is not described in the specification.

 
 

+Ideally, the interpreter is not just hypothetical.

 This is really my main motivation for working on the [Miri interpreter](https://github.com/rust-lang/miri/).
 This is really my main motivation for working on the [Miri interpreter](https://github.com/rust-lang/miri/).

-Of course, practically speaking, its main purpose is to help unsafe code authors avoid UB, but for me personally, I find it equally important that it helps us think about the semantics of Rust and MIR in an *operational* way.
-This helps shift the discussion around MIR from "optimizations-first" more towards "language-first".
-Of course, optimizations are still the key motivating factor for defining the language semantics this way or that way, but ultimately it is the language semantics that serves as "ground truth" and keeps it all together, ensuring everything is mutually compatible.
+Of course, practically speaking, its main purpose is to help unsafe code authors avoid UB, but for me personally, I find it equally important that it helps us think about the semantics of Rust and MIR in a different way.

 
 I hope this was educational, and thanks for reading. :)
 As usual, this post can be discussed in the Rust forums.
 
 I hope this was educational, and thanks for reading. :)
 As usual, this post can be discussed in the Rust forums.

-I am curious what your thoughts are on how we can build compilers that do not suffer from these issues.
+I am curious what your thoughts are on how we can build compilers that do not suffer from the issues I have discussed here.

 
 #### Footnotes
 
 #### Footnotes