add thesis page stub
[web.git] / ralf / _posts / 2018-07-24-pointers-and-bytes.md
index 35a5c159dbd9d32c4847f6e9af54ad0d63f2e066..68a2cb0cf8483a4a0221b8fa5b841d6354f273e3 100644 (file)
@@ -173,7 +173,7 @@ 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`.
-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 whne a pointer is stored to memory and loaded again.
+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:
@@ -237,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.
 
+**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`.