clarify abstract nature of pointers

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

diff --git a/ralf/_posts/2018-07-24-pointers-and-bytes.md b/ralf/_posts/2018-07-24-pointers-and-bytes.md
index a51fb48652b79c9adbebe92fe018407ecca1249e..b3a74c480016c1d2c85b501e34b36cd0857f4bb1 100644 (file)
--- a/ralf/_posts/2018-07-24-pointers-and-bytes.md
+++ b/ralf/_posts/2018-07-24-pointers-and-bytes.md
@@ -111,7 +111,15 @@ So, what *is* a pointer?
 I don't know the full answer to this.
 In fact, this is an open area of research.
 
-Here's a simple proposal (in fact, this is the model used in my [RustBelt work]({{ site.baseurl }}{% post_url 2017-07-08-rustbelt %}), and it is also how [miri](https://github.com/solson/miri/) implements pointers):
+One important point to stress here is that we are just looking for an *abstract model* of the pointer.
+Of course, on the actual machine, pointers are integers.
+But the actual machine also does not do the kind of optimizations that modern C++ compilers do, so it can get away with that.
+If we wrote the above programs in assembly, there would be no UB, and no optimizations.
+C++ and Rust employ a more "high-level" view of memory and pointers, restricting the programmer for the benefit of optimizations.
+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]({{ site.baseurl }}{% 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]({{ site.baseurl }}{% post_url 2017-07-08-rustbelt %}), and it is also how [miri](https://github.com/solson/miri/) implements pointers):
 A pointer is a pair of some kind of ID uniquely identifying the *allocation*, and an *offset* into the allocation.
 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]
@@ -200,11 +208,10 @@ Using `Uninit` instead of an arbitrary bit pattern means miri can, in a single e
 
 ## Conclusion
 
-We have seen that 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`.[^4]
+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`.
 With this, I think we are ready to look at a first draft of my "2018 memory model" (working title ;) -- in the next post. :)
 
+Thanks to @rkruppe and @nagisa for help in finding arguments for why `Uninit` is needed.
 If you have any questions, feel free to [ask in the forums](https://internals.rust-lang.org/t/pointers-are-complicated-or-whats-in-a-byte/8045)!
 
-[^4]: And just to be clear, I am talking about a pointer or byte in the model of an optimized *programming language* here.  When modeling hardware, everything is different.
-
 #### Footnotes