show how to fix the Arc problem

diff --git a/personal/_posts/2017-08-11-types-as-contracts-evaluation.md b/personal/_posts/2017-08-11-types-as-contracts-evaluation.md
index 226d48f9464fe2649280154921e571d69128587b..a95de96e45cb20c90507edb785b18b5e12750df9 100644 (file)
--- a/personal/_posts/2017-08-11-types-as-contracts-evaluation.md
+++ b/personal/_posts/2017-08-11-types-as-contracts-evaluation.md
@@ -111,6 +111,27 @@ Nevertheless, the type of `inner` says that there is a valid shared reference to
 
 Notice that even if `inner` did not care about the types, validation would still fail when `drop_slow` goes on calling the safe function `Layout::for_value` and passes it the invalid `&ArcInner<T>`.
 
 
 Notice that even if `inner` did not care about the types, validation would still fail when `drop_slow` goes on calling the safe function `Layout::for_value` and passes it the invalid `&ArcInner<T>`.
 

+To fix this, we have to make sure that the type `&ArcInner` is not used after `data` is dropped.
+The following would work, for example:
+{% highlight rust %}
+unsafe fn drop_slow(&mut self) {
+    let ptr = self.ptr.as_ptr();
+
+    let layout = Layout::for_value(&*ptr);
+
+    // Destroy the data at this time, even though we may not free the box
+    // allocation itself (there may still be weak pointers lying around).
+    ptr::drop_in_place(&mut (*ptr).data);
+    // We must not use the type &(mut) ArcInner from now on, because that
+    // type is actually no longer valid.
+
+    if (*ptr).weak.fetch_sub(1, Release) == 1 {
+        atomic::fence(Acquire);
+        Heap.dealloc(ptr as *mut u8, layout)
+    }
+}
+{% endhighlight %}
+

 ## 2 Changes to the Model
 
 There were a whole bunch of other test failures, but they all turned out to be bugs in the implementations or even the model, rather than legit violations of the "Types as Contracts" idea.
 ## 2 Changes to the Model
 
 There were a whole bunch of other test failures, but they all turned out to be bugs in the implementations or even the model, rather than legit violations of the "Types as Contracts" idea.


@@ -231,7 +252,7 @@ Speaking of the implementation, the problem around write locks described in [§2
 
 While [§1.1](#11-ownership-passing-via-raw-pointers) is "fixed" by exempting unsafe code from the full range of checks, and the trouble with uninitialized memory ([§1.2](#12-uninitialized-memory)) will hopefully be solved as a side-effect of [changing the way uninitialized memory is handled](https://internals.rust-lang.org/t/mem-uninitialized-and-trap-representations/4167/18?u=ralfjung), this still leaves `Arc::drop` ([§1.3](13-arcdrop)) as an open problem.
 This comes down to a judgment call: We could relax validation sufficiently (e.g., relaxing validation in entire modules when they do certain unsafe things, and not validating private fields of structs that we cannot access) to make this code legal, or we could declare that code to actually be UB.
 
 While [§1.1](#11-ownership-passing-via-raw-pointers) is "fixed" by exempting unsafe code from the full range of checks, and the trouble with uninitialized memory ([§1.2](#12-uninitialized-memory)) will hopefully be solved as a side-effect of [changing the way uninitialized memory is handled](https://internals.rust-lang.org/t/mem-uninitialized-and-trap-representations/4167/18?u=ralfjung), this still leaves `Arc::drop` ([§1.3](13-arcdrop)) as an open problem.
 This comes down to a judgment call: We could relax validation sufficiently (e.g., relaxing validation in entire modules when they do certain unsafe things, and not validating private fields of structs that we cannot access) to make this code legal, or we could declare that code to actually be UB.

-The concrete problem in `Arc` can be fixed fairly easily by acquiring a reference to the `weak` field *before* dropping the user data in the `Arc`; the question is whether this kind of code is something that programmers actually expect to be legal -- and if they do, whether we can do anything about that (by providing documentation, or tools, or whatever else is necessary).
+The concrete problem in `Arc` can be fixed fairly easily as I have shown; the question is whether this kind of code is something that programmers actually expect to be legal -- and if they do, whether we can do anything about that (by providing documentation, or tools, or whatever else is necessary).

 Of course, it may also turn out that this shows that the entire approach is not actually feasible.
 
 Interestingly, the [discussion](https://internals.rust-lang.org/t/types-as-contracts/5562) of my previous post introducing Types as Contracts was to a large extend not even about this model, but about the underlying model of what memory and pointers are, and how to write a checker that actually faithfully models what LLVM does.
 Of course, it may also turn out that this shows that the entire approach is not actually feasible.
 
 Interestingly, the [discussion](https://internals.rust-lang.org/t/types-as-contracts/5562) of my previous post introducing Types as Contracts was to a large extend not even about this model, but about the underlying model of what memory and pointers are, and how to write a checker that actually faithfully models what LLVM does.


@@ -245,3 +266,5 @@ Still, I certainly intend to stay involved. This problem is way too interesting
 
 As always, please comment with your thoughts on the topic.
 I am particularly curious about what kind of test cases you are throwing at miri, and how it is doing!
 
 As always, please comment with your thoughts on the topic.
 I am particularly curious about what kind of test cases you are throwing at miri, and how it is doing!

+
+**Update**: I added a proposal for how to fix the `Arc` problem.