rename Iris workshop talk file to be more consistent

[web.git] / personal / _posts / 2018-07-24-pointers-and-bytes.md

diff --git a/personal/_posts/2018-07-24-pointers-and-bytes.md b/personal/_posts/2018-07-24-pointers-and-bytes.md
index dfd6bd1cfc1186d61cd74074ac9f84e6a5f47e08..68a2cb0cf8483a4a0221b8fa5b841d6354f273e3 100644 (file)
--- a/personal/_posts/2018-07-24-pointers-and-bytes.md
+++ b/personal/_posts/2018-07-24-pointers-and-bytes.md
@@ -19,7 +19,7 @@ I hope that by the end of this post, you will agree with me on both of these sta
 ## Pointers Are Complicated
 
 What is the problem with "pointers are just integers"?  Let us consider the following example:<br>
 ## Pointers Are Complicated
 
 What is the problem with "pointers are just integers"?  Let us consider the following example:<br>

-(I am using C++ code here mostly because writing unsafe code is easier in C++, and unsafe code is where these problems really show up. C has all the same issues, as does unsafe Rust.)
+(I am using C++ code here mostly because writing unsafe code is easier in C++ than in Rust, and unsafe code is where these problems really show up. C has all the same issues, as does unsafe Rust.)

 {% highlight c++ %}
 int test() {
     auto x = new int[8];
 {% highlight c++ %}
 int test() {
     auto x = new int[8];


@@ -56,7 +56,7 @@ int test() {
     auto x = new int[8];
     auto y = new int[8];
     y[0] = 42;
     auto x = new int[8];
     auto y = new int[8];
     y[0] = 42;

-    auto x_ptr = &x[8]; // one past the end
+    auto x_ptr = x+8; // one past the end

     if (x_ptr == &y[0])
       *x_ptr = 23;
     return y[0];
     if (x_ptr == &y[0])
       *x_ptr = 23;
     return y[0];


@@ -119,8 +119,15 @@ C++ and Rust employ a more "high-level" view of memory and pointers, restricting
 When formally describing what the programmer may and may not do in these languages, as we have seen, the model of pointers as integers falls apart, so we have to look for something else.
 This is another example of using a "virtual machine" that's different from the real machine for specification purposes, which is an idea [I have blogged about before]({% post_url 2017-06-06-MIR-semantics %}).
 
 When formally describing what the programmer may and may not do in these languages, as we have seen, the model of pointers as integers falls apart, so we have to look for something else.
 This is another example of using a "virtual machine" that's different from the real machine for specification purposes, which is an idea [I have blogged about before]({% post_url 2017-06-06-MIR-semantics %}).
 

-Here's a simple proposal (in fact, this is the model of pointers used in [CompCert](https://hal.inria.fr/hal-00703441/document) and my [RustBelt work]({% post_url 2017-07-08-rustbelt %}), and it is also how [miri](https://github.com/solson/miri/) implements pointers):
+Here's a simple proposal (in fact, this is the model of pointers used in [CompCert](https://hal.inria.fr/hal-00703441/document) and my [RustBelt work]({% post_url 2017-07-08-rustbelt %}), and it is also how [miri](https://github.com/solson/miri/) implements [pointers](https://github.com/rust-lang/rust/blob/fefe81605d6111faa8dbb3635ab2c51d59de740a/src/librustc/mir/interpret/mod.rs#L121-L124)):

 A pointer is a pair of some kind of ID uniquely identifying the *allocation*, and an *offset* into the allocation.
 A pointer is a pair of some kind of ID uniquely identifying the *allocation*, and an *offset* into the allocation.

+If we defined this in Rust, we might write
+{% highlight rust %}
+struct Pointer {
+    alloc_id: usize,
+    offset: isize,
+}
+{% endhighlight %}

 Adding/subtracting an integer to/from a pointer just acts on the offset, and can thus never leave the allocation.
 Subtracting a pointer from another is only allowed when both point to the same allocation (matching [C++](https://timsong-cpp.github.io/cppwp/n4140/expr.add#6)).[^2]
 
 Adding/subtracting an integer to/from a pointer just acts on the offset, and can thus never leave the allocation.
 Subtracting a pointer from another is only allowed when both point to the same allocation (matching [C++](https://timsong-cpp.github.io/cppwp/n4140/expr.add#6)).[^2]
 


@@ -137,8 +144,10 @@ However, this simple model starts to fall apart once you consider pointer-intege
 In miri, casting a pointer to an integer does not actually do anything, we now just have an integer variable (i.e., its *type* says it is an integer) whose *value* is a pointer (i.e., an allocation-offset pair).
 However, multiplying that "integer" by 2 leads to an error, because it is entirely unclear what it means to multiply such an abstract pointer by 2.
 
 In miri, casting a pointer to an integer does not actually do anything, we now just have an integer variable (i.e., its *type* says it is an integer) whose *value* is a pointer (i.e., an allocation-offset pair).
 However, multiplying that "integer" by 2 leads to an error, because it is entirely unclear what it means to multiply such an abstract pointer by 2.
 

-This is the most lazy thing to do, and we do it because it is not clear what else to do (other than not supporting these casts at all -- but this way, miri can run more programs).
-In our abstract machine, there is no single coherent "address space" that all allocations live in, that we could use to map every pointer to a distinct integer.
+I should clarify that this is *not* a good solution when defining language semantics.
+It works fine for an interpreter though.
+It is the most lazy thing to do, and we do it because it is not clear what else to do (other than not supporting these casts at all -- but this way, miri can run more programs):
+In our abstract machine, there just is no single coherent "address space" that all allocations live in, that we could use to map every pointer to a distinct integer.

 Every allocation is just identified by an (unobservable) ID.
 We could now start to enrich this model with extra data like a base address for each allocation, and somehow use that when casting an integer back to a pointer... but that's where it gets really complicated, and anyway discussing such a model is not the point of this post.
 The point it to discuss the *need* for such a model.
 Every allocation is just identified by an (unobservable) ID.
 We could now start to enrich this model with extra data like a base address for each allocation, and somehow use that when casting an integer back to a pointer... but that's where it gets really complicated, and anyway discussing such a model is not the point of this post.
 The point it to discuss the *need* for such a model.


@@ -150,6 +159,8 @@ We mostly just ignore the problem in miri and opportunistically do as much as we
 A full definition of a language like C++ or Rust of course cannot take this shortcut, it has to explain what really happens here.
 To my knowledge, no satisfying solution exists, but academic research is [getting closer](http://sf.snu.ac.kr/publications/llvmtwin.pdf).
 
 A full definition of a language like C++ or Rust of course cannot take this shortcut, it has to explain what really happens here.
 To my knowledge, no satisfying solution exists, but academic research is [getting closer](http://sf.snu.ac.kr/publications/llvmtwin.pdf).
 

+**Update:** This was by no means meant to be an exhaustive list of academic research on C in general. I do not know of other work that focuses directly on the interplay of integer-pointer casts and optimizations, but other noteworthy work on formalizing C includes [KCC](https://github.com/kframework/c-semantics), [Robbert Krebber's PhD thesis](https://robbertkrebbers.nl/thesis.html) and [Cerberus](https://www.cl.cam.ac.uk/~pes20/cerberus/). **/Update**
+

 This is why pointers are not simple, either.
 
 ## From Pointers to Bytes
 This is why pointers are not simple, either.
 
 ## From Pointers to Bytes


@@ -162,7 +173,8 @@ We have to say what the value of `v` is, so we have to find some way to answer t
 (And this is an entirely separate issue from the problem with multiplication that came up in the last section. We just assume some abstract type `Pointer`.)
 
 We cannot represent a byte of a pointer as an element of `0..256`.
 (And this is an entirely separate issue from the problem with multiplication that came up in the last section. We just assume some abstract type `Pointer`.)
 
 We cannot represent a byte of a pointer as an element of `0..256`.

-Instead, we will remember both the pointer, and which byte of the pointer we got.
+Essentially, if we use a naive model of memory, the extra "hidden" part of a pointer (the one that makes it more than just an integer) would be lost when a pointer is stored to memory and loaded again.
+We have to fix this, so we have to extend our notion of a "byte" to accomodate that extra state.

 So, a byte is now *either* an element of `0..256` ("raw bits"), *or* the n-th byte of some abstract pointer.
 If we were to implement our memory model in Rust, this might look as follows:
 {% highlight rust %}
 So, a byte is now *either* an element of `0..256` ("raw bits"), *or* the n-th byte of some abstract pointer.
 If we were to implement our memory model in Rust, this might look as follows:
 {% highlight rust %}


@@ -225,6 +237,8 @@ Finally, `Uninit` is also a better choice for interpreters like miri.
 Such interpreters have a hard time dealing with operations of the form "just choose any of these values" (i.e., non-deterministic operations), because if they want to fully explore all possible program executions, that means they have to try every possible value.
 Using `Uninit` instead of an arbitrary bit pattern means miri can, in a single execution, reliably tell you if your programs uses uninitialized values incorrectly.
 
 Such interpreters have a hard time dealing with operations of the form "just choose any of these values" (i.e., non-deterministic operations), because if they want to fully explore all possible program executions, that means they have to try every possible value.
 Using `Uninit` instead of an arbitrary bit pattern means miri can, in a single execution, reliably tell you if your programs uses uninitialized values incorrectly.
 

+**Update:** Since writing this section, I have written an entire [post dedicated to uninitialized memory and "real hardware"]({% post_url 2019-07-14-uninit %}) with more details, examples and references. **/Update**
+

 ## Conclusion
 
 We have seen that in languages like C++ and Rust (unlike on real hardware), pointers can be different even when they point to the same address, and that a byte is more than just a number in `0..256`.
 ## Conclusion
 
 We have seen that in languages like C++ and Rust (unlike on real hardware), pointers can be different even when they point to the same address, and that a byte is more than just a number in `0..256`.