(hopefully) final tweaks

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

diff --git a/personal/_drafts/provenance-matters.md b/personal/_drafts/provenance-matters.md
index 708f9c19686294ec37c20219ce23bb7bc0596d6d..ceb1be513efd06f529258fc2fd1b6b86deb590b8 100644 (file)
--- a/personal/_drafts/provenance-matters.md
+++ b/personal/_drafts/provenance-matters.md
@@ -9,7 +9,7 @@ One key point I was trying to make is that
 > *just because two pointers point to the same address, does not mean they are equal and can be used interchangeably.*
 
 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).
 > *just because two pointers point to the same address, does not mean they are equal and can be used interchangeably.*
 
 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 post is a cautionary tale of what can go wrong when provenance is not considered sufficiently carefully in an optimizing compiler.

 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 -->
 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 -->


@@ -17,71 +17,80 @@ There is also a larger message here about how we could prevent such issues from
 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,
 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 need to take provenance specifically and IR semantics in general more seriously.
+we need to take IR semantics (and specifically provenance) more seriously.
+We use LLVM for the examples because it is particularly easy to study with its single, (comparatively) well-documented IR that a lot of infrastructure evolved around.

 Let's get started!
 
 ## Warm-up: Why IRs need a precise semantics
 
 As a warm-up, I will give a simple example showing that compiler IRs such as LLVM IR need a precise (and precisely documented) semantics.
 Let's get started!
 
 ## Warm-up: Why IRs need a precise semantics
 
 As a warm-up, I will give a simple example showing that compiler IRs such as LLVM IR need a precise (and precisely documented) semantics.

-If you are already familiar with the idea of treating compiler IRs as proper programming languages in their own right, or if you are just here for the pointers, you can skip to the next section.
+If you are already familiar with the idea of treating compiler IRs as proper programming languages in their own right, or if you are just here for the pointers and their provenance, you can skip to the next section.

 
 

-Consider the following simple (and contrived, for the sake of this example) piece of C code:
+Consider the following simple (and contrived, for the sake of this example) piece of C code computing `n * (i+j)`:

 {% highlight c %}
 {% highlight c %}

-int sum_up(int i, int j, int n) {
+int sum_up(int i, int j, unsigned int n) {

   int result = 0;
   while (n > 0) {
     result += i + j;
     n -= 1;
   }
   int result = 0;
   while (n > 0) {
     result += i + j;
     n -= 1;
   }

+  return result;

 }
 {% endhighlight %}
 }
 {% endhighlight %}

-One transformation the compiler might want to do is to move the addition `i+j` out of the loop, to avoid computing the sum each time around the loop:
+One transformation the compiler might want to do is to move the addition `i+j` out of the loop, to avoid computing the sum each time around the loop (this is called "loop-invariant code motion"[^loop]):

 {% highlight c %}
 {% highlight c %}

-int sum_up(int i, int j, int n) { // optimized version
+int sum_up(int i, int j, unsigned int n) { // optimized version

   int result = 0;
   int s = i + j;
   while (n > 0) {
     result += s;
     n -= 1;
   }
   int result = 0;
   int s = i + j;
   while (n > 0) {
     result += s;
     n -= 1;
   }

+  return result;

 }
 {% endhighlight %}
 However, that transformation is actually incorrect.
 If we imagine a caller using this function as `sum_up(INT_MAX, 1, 0)`, then this is a perfectly correct way to call `sum_up`: the loop is never entered, so the overflowing addition `INT_MAX+1` is never performed.
 However, after the desired optimization, the program now causes a signed integer overflow, which is UB (Undefined Behavior) and thus May Never Happen!
 
 }
 {% endhighlight %}
 However, that transformation is actually incorrect.
 If we imagine a caller using this function as `sum_up(INT_MAX, 1, 0)`, then this is a perfectly correct way to call `sum_up`: the loop is never entered, so the overflowing addition `INT_MAX+1` is never performed.
 However, after the desired optimization, the program now causes a signed integer overflow, which is UB (Undefined Behavior) and thus May Never Happen!
 

+[^loop]: If you are a regular reader of my blog, you will recognize this as the same optimization that already played a crucial role in [a previous post of mine]({% post_url 2020-07-15-unused-data %}). Loop-invariant code motion is a great optimization to look at when considering corner cases of IR semantics.
+

 One might be tempted to ignore this problem because the UB on integer overflow is a compiler-only concept; every target supported by the compiler will do the obvious thing and just produce an overflowing result.
 However, there might be other compiler passes running after the optimization we are considering.
 One might be tempted to ignore this problem because the UB on integer overflow is a compiler-only concept; every target supported by the compiler will do the obvious thing and just produce an overflowing result.
 However, there might be other compiler passes running after the optimization we are considering.

-One such pass might inline `sum_up`, and another pass might notice the `INT_MAX+1` and replace it by `unreachable`, and another pass might then just remove all our code since it is unreachable.
-Each of these passes has a good reason to exist (it can help real code become a lot faster or help prune dead code), but if we combine them all with our loop hoisting optimization, the result is a disaster.
+One such pass might inline `sum_up`, and another pass might notice the `INT_MAX+1` and replace it by `unreachable` since UB code is "by definition" unreachable, and another pass might then just remove all our code since it is unreachable.
+Each of these passes has a good reason to exist (it can help real code become a lot faster or help prune dead code), but if we combine them all with loop-invariant code motion, the result is a disaster.

 
 

-I am convinced that the only way to avoid such problems is to find a way to justify the correctness of each optimization *in isolation*.
+One way (and the only systematic way I know) to avoid such problems is to make sure that we can justify the correctness of each optimization *in isolation*.

 Each optimization must be *correct* for any possible program, where *correct* means that the optimized program must only "do things" that the original program could have done as well.
 (This is basically the "as-if" rule in the C standard, and is typically called "refinement" in the academic literature.)
 In particular, no optimization must ever introduce UB into a UB-free program.
 
 Each optimization must be *correct* for any possible program, where *correct* means that the optimized program must only "do things" that the original program could have done as well.
 (This is basically the "as-if" rule in the C standard, and is typically called "refinement" in the academic literature.)
 In particular, no optimization must ever introduce UB into a UB-free program.
 

-It may seem now that under this premise, it is impossible to perform the loop hoisting optimization we are considering.
+It may seem now that under this premise, it is impossible to perform the loop-invariant code motion we are considering.

 But that is not the case!
 But that is not the case!

-We can perform the optimization, *we just cannot perform it in C*.
-Instead, we have to perform it in LLVM IR (or any other IR with a suitable semantics).
-Specifically, signed integer overflow in LLVM yields a `poison` result.
-It is not UB to produce `poison`, it is just UB to use `poison` in certain ways (the details do not matter here).
-In a call to `sum_up(INT_MAX, 1, 0)`, the `s` variable introduced by loop hoisting is unused, so the fact that its value is `poison` does not matter!
+So far, what we have seen is that the optimization is not *correct* when being performed on a C program.
+But when LLVM performs these optimizations, it does not consider the program to be written in C---it considers the program to be written in LLVM IR, which has a different semantics than C.
+Specifically, signed integer overflow in LLVM IR yields a `poison` result.
+It is not UB to produce `poison`, it is just UB to use `poison` in certain ways (the details of this do not matter here).
+In a call to the optimized `sum_up(INT_MAX, 1, 0)`, the `s` variable introduced by loop-invariant code motion is unused, so the fact that its value is `poison` does not matter!
+
+Due to this behavior of signed integer overflow, this case of loop-invariant code motion is *correct* if we consider it as an optimization on programs that are written in LLVM IR.[^cheat]
+The "price" we pay for this is that replacing `INT_MAX+1` by `unreachable` is not *correct* in LLVM IR, since it is not UB.

 
 

-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.
+The great thing about *correct* optimizations is that we can combine any number of them in any order (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.
+(In the academic lingo, we would say that "refinement is transitive".)

 
 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.
 
 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.
+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.
+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.[^ub-difference]

 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.
 
 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.
+[^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 strictly more UB than LLVM IR (for integer arithmetic), which makes translation in one direction easy, while the other direction is hard.

 
 

-[^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.
+[^ub-difference]: In particular, 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?
 
 *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?

+For a *correct* optimization, the answer to these questions is "no".

 
 ## How 3 (seemingly) correct optimizations can be incorrect when used together
 
 
 ## How 3 (seemingly) correct optimizations can be incorrect when used together
 


@@ -103,13 +112,14 @@ if (iq == ip) {
   print(q[0]);
 }
 {% endhighlight %}
   print(q[0]);
 }
 {% endhighlight %}

-We are using C syntax here, but remember that we just use C syntax as a convenient way to write programs in LLVM IR.
+We are using C syntax here just as a convenient way to write programs in LLVM IR.

 For simplicity, we assume that `int` has the right size to hold a pointer value; just imagine we used `uintptr_t` if you want to be more general.
 
 This program has two possible behaviors: either `ip` (the address one-past-the-end of `p`) and `iq` (the address of `q`) are different, and nothing is printed.
 Or the two are equal, in which case the program will print "10" (`iq` is the result of casting `q` to an integer, so casting it back will yield the original pointer, or at least a pointer pointing to the same object / location in memory).
 
 For simplicity, we assume that `int` has the right size to hold a pointer value; just imagine we used `uintptr_t` if you want to be more general.
 
 This program has two possible behaviors: either `ip` (the address one-past-the-end of `p`) and `iq` (the address of `q`) are different, and nothing is printed.
 Or the two are equal, in which case the program will print "10" (`iq` is the result of casting `q` to an integer, so casting it back will yield the original pointer, or at least a pointer pointing to the same object / location in memory).
 

-The first "optimization" we will perform is to exploit that `iq == ip`, so we can replace all `iq` by `ip`, and subsequently inline the definition of `ip`:
+The first "optimization" we will perform is to exploit that if we enter the `if` body, we have `iq == ip`, so we can replace all `iq` by `ip`.
+Subsequently the definition of `ip` is inlined:

 {% highlight c %}
 char p[1], q[1] = {0};
 int ip = (int)(p+1);
 {% highlight c %}
 char p[1], q[1] = {0};
 int ip = (int)(p+1);


@@ -168,7 +178,7 @@ Looking more closely, however, reveals that things are not quite so simple!
 However, LLVM IR (just like C) does not permit memory accesses through one-past-the-end pointers.
 It makes a difference whether we use `p+1` or `q` inside the `if`, even though we know (in that branch) that both pointers point to the same memory location.
 This demonstrates that in LLVM IR, there is more to a pointer than just the address it points to---it also matters how this address was computed.
 However, LLVM IR (just like C) does not permit memory accesses through one-past-the-end pointers.
 It makes a difference whether we use `p+1` or `q` inside the `if`, even though we know (in that branch) that both pointers point to the same memory location.
 This demonstrates that in LLVM IR, there is more to a pointer than just the address it points to---it also matters how this address was computed.

-This something extra is what we typically call *provenance*.
+This extra information is typically called *provenance*.

 It is impossible to argue for the *correct*ness of the third optimization without acknowledging that provenance is a real part of the semantics of an LLVM IR program.
 In a flat memory model where pointers are just integers (such as most assembly languages), this optimization is simply wrong.
 
 It is impossible to argue for the *correct*ness of the third optimization without acknowledging that provenance is a real part of the semantics of an LLVM IR program.
 In a flat memory model where pointers are just integers (such as most assembly languages), this optimization is simply wrong.
 


@@ -177,7 +187,7 @@ The second optimization gives us a clue into this aspect of LLVM IR semantics: c
 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 program state is otherwise identical in both cases.
 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 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.
+But we know that the integer values computed by `(int)(p+1)` and `(int)q` (i.e., the bit pattern of length 32 that serve as input to the `(char*)` casts) are the same, and hence a difference can only arise if these 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.
 
 Finally, let us consider the first optimization.
 Here, a successful equality test `iq == ip` prompts the optimizer to replace one value by the other.


@@ -185,7 +195,7 @@ 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" 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.
 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.
+A different way to phrase the same argument is to say that this optimization is correct only if `iq == ip` evaluating to `true` implies that both values have the same "Abstract Machine" representation, so if that representation involves provenance, both values must have the same provenance.

 This would be a possible definition of `==` in LLVM IR, but only in principle---in practice this means the LLVM backends have to compile `==` in a way that pointer provenance is taken into account, which of course is impossible.
 
 *Take-away:*
 This would be a possible definition of `==` in LLVM IR, but only in principle---in practice this means the LLVM backends have to compile `==` in a way that pointer provenance is taken into account, which of course is impossible.
 
 *Take-away:*


@@ -205,12 +215,12 @@ Removing provenance altogether kills all but the most simple alias analyses.[^al
 On the other hand, declaring that integers have provenance does not just disable the first optimization in the chain shown above, it also disables common arithmetic optimizations such as `x - x` being equivalent to `0`.
 Even achieving commutativity and associativity of `+` becomes non-trivial once integers have provenance.
 
 On the other hand, declaring that integers have provenance does not just disable the first optimization in the chain shown above, it also disables common arithmetic optimizations such as `x - x` being equivalent to `0`.
 Even achieving commutativity and associativity of `+` becomes non-trivial once integers have provenance.
 

-[^alias]: Sadly, I do not know of a systematic study of the performance impact of this decision. It is my understanding that many compiler developers "obviously" consider this way too costly of a fix to the problem, but it would still be great to underpin this with some proper data.
+[^alias]: Sadly, I do not know of a systematic study of the performance impact of going with the third option: which part of the alias analysis is still correct, and how much slower is a compiler that only performs such a restricted form of alias analysis? It is my understanding that many compiler developers "obviously" consider this way too costly of a fix to the problem, but it would still be great to underpin this with some proper data. In any case, the third option would entail a complete re-design of LLVM's `noalias`, which would be bad news both for Rust (which uses `noalias` to encode alias information embedded in Rust's reference types) and clang (which uses `noalias` to encode C's `restrict`).

 
 So, I think that the issue should be resolved by saying that pointers have provenance but integers do not, which means that it is the second optimization that is wrong.
 This also corresponds to [what has been recently proposed to the C standard committee](http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2577.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.
 
 So, I think that the issue should be resolved by saying that pointers have provenance but integers do not, which means that it is the second optimization that is wrong.
 This also corresponds to [what has been recently proposed to the C standard committee](http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2577.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).
+There might still be special cases where this can be done, but figuring out the limits of this requires 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.
 
 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.


@@ -221,25 +231,25 @@ What did we learn?
 First of all, pointers are complicated.
 Precisely describing their semantics in a way that is consistent with common alias analyses requires adding a notion of "provenance".
 In a language such as Java or ML where pointers are opaque types whose representation cannot be observed, this is actually fairly easy to do.
 First of all, pointers are complicated.
 Precisely describing their semantics in a way that is consistent with common alias analyses requires adding a notion of "provenance".
 In a language such as Java or ML where pointers are opaque types whose representation cannot be observed, this is actually fairly easy to do.

-But in a language such as Rust, C or C++ that supports pointer-integer casts, the introduction of provenance poses some really tricky questions, and at least one of the commonly performed optimizations in this space has to give.
+But in a language such as Rust, C, or C++ that supports pointer-integer casts, the introduction of provenance poses some really tricky questions, and at least one of the commonly performed optimizations in this space has to give.

 
 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, 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.
 
 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, 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.
+For another example, see [§2.3 of this paper](https://plv.mpi-sws.org/validc/paper.pdf) (Figure 3 contains the code) which 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.
+The warm-up example is another trivial case of this: loop-invariant code motion of arithmetic operations and UB on arithmetic overflow can both be *correct*, but not in the same IR.

 
 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.
 
 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.
+Now, you may object by saying that LLVM has an [extensive LangRef](https://llvm.org/docs/LangRef.html), 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.
 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]
+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]({% post_url 2018-07-24-pointers-and-bytes %}).[^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.
 
 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.
 

-[^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.
+[^C]: The astute reader will notice that this information is also absent in the C and C++ specifications. That is indeed one of my main criticisms of these specifications. It leads to many open questions not only when discussing provenance (including `restrict`, which I did not even go into here) but also when discussing indeterminate and unspecified values or the rules around effective types.

 
 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.
 
 
 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.