safe intrusive collections with pinning: first draft

[web.git] / personal / _posts / 2017-07-17-types-as-contracts.md

diff --git a/personal/_posts/2017-07-17-types-as-contracts.md b/personal/_posts/2017-07-17-types-as-contracts.md
index 6bcaea00e2aaa8a212ff32801d0d4cc4a592dbde..d7b1b71a54c6dfbdc236bb1a5bf7fe2978f002ce 100644 (file)
--- a/personal/_posts/2017-07-17-types-as-contracts.md
+++ b/personal/_posts/2017-07-17-types-as-contracts.md
@@ -283,11 +283,11 @@ For compound types like tuples, `struct` or `enum`, validation proceeds recursiv
 In particular, the enum discriminant is checked to be in-range (in particular, nothing can pass validation at an empty enum type).
 However, because the recursive validation will only lock memory that's actually covered by a field, we also have to acquire the appropriate lock for padding bytes and the enum discriminant here.
 
-Finally, at a reference type, two things happen.
-First, the reference itself is stored in memory somewhere; this memory has to be locked just like the validation of `i32` locks the memory used to store the integer.
-The reference is also checked to be non-NULL and properly aligned for the type it points to.
-Furthermore, validation proceeds recursively after *dereferencing* the reference.
-Crucially, the `mutbl` and `lft` for this recursive call are taking the reference type into account:
+Finally, when encountering a box or reference type, two things happen.
+First, the pointer itself is stored in memory somewhere; this memory has to be locked just like the validation of `i32` locks the memory used to store the integer.
+The pointer is also checked to be non-NULL and properly aligned for the type it points to.
+Furthermore, validation proceeds recursively after *dereferencing* the pointer.
+Crucially, for the case of validating a reference, the `mutbl` and `lft` for this recursive call are taking the type into account:
 If `lft` was `None` and this reference's lifetime ends within the function (i.e., there is a corresponding `EndRegion` somewhere), it is now set to the reference's lifetime.
 If `mutbl` was mutable, it becomes immutable when following a shared reference.
 
@@ -305,7 +305,7 @@ This grants the functions write access to memory that we are explicitly passing
 Suspend validation occurs before taking a reference, using the lifetime of the new reference.
 This encodes the fact that when the lifetime ends (and hence the lock is being reacquired), we are the exclusive owner of this memory again.
 
-**Update**: It has been pointed out to me that another way for values to flow back into a function is through mutable references. Good catch! I will need to extend the validation machinery to also perform acquire validation when a write lock is reacquired. **/Update**
+**Update:** It has been pointed out to me that another way for values to flow back into a function is through mutable references. Good catch! I will need to extend the validation machinery to also perform acquire validation when a write lock is reacquired. **/Update**
 
 To summarize, validation statements are emitted during MIR construction in the following places:
 - At the beginning of the function, we perform acquire validation of the arguments.