add Coq typeclass index problem draft

[web.git] / personal / _posts / 2017-06-09-mutexguard-sync.md

diff --git a/personal/_posts/2017-06-09-mutexguard-sync.md b/personal/_posts/2017-06-09-mutexguard-sync.md
index a01980f5f964a11fea3c811ba1f080027b6fbaaa..456d289e7e9d2dda31397d975c71f9c7f2975474 100644 (file)
--- a/personal/_posts/2017-06-09-mutexguard-sync.md
+++ b/personal/_posts/2017-06-09-mutexguard-sync.md
@@ -1,9 +1,10 @@
 ---
 title: How MutexGuard was Sync When It Should Not Have Been
 ---
 title: How MutexGuard was Sync When It Should Not Have Been

-categories: rust
+categories: rust research
+reddit: /rust/comments/6gavfe/how_mutexguard_was_sync_when_it_should_not_have/

 ---
 
 ---
 

-A couple of weeks ago, our ongoing effort to [formalize Rust's type system]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}) lead to us actually discovering a bug in the Rust standard library:
+A couple of weeks ago, our ongoing effort to [formalize Rust's type system]({% post_url 2015-10-12-formalizing-rust %}) lead to us actually discovering a bug in the Rust standard library:

 `MutexGuard` implemented `Sync` in cases where it should not. This could lead to data races in safe programs. Ouch.
 <!-- MORE -->
 
 `MutexGuard` implemented `Sync` in cases where it should not. This could lead to data races in safe programs. Ouch.
 <!-- MORE -->
 


@@ -104,7 +105,7 @@ I don't think it is very surprising that this was overlooked.
 Ideally, types like `MutexGuard<T>` would *not* get these automatic implementations of `Send` and `Sync`.
 That would make sure that, if some type incorrectly implements these traits, at least it comes from some piece of incorrect `unsafe` somewhere.
 This is exactly the point of `unsafe`: Marking clearly the points in the code that have to be audited extra-carefully.
 Ideally, types like `MutexGuard<T>` would *not* get these automatic implementations of `Send` and `Sync`.
 That would make sure that, if some type incorrectly implements these traits, at least it comes from some piece of incorrect `unsafe` somewhere.
 This is exactly the point of `unsafe`: Marking clearly the points in the code that have to be audited extra-carefully.

-The reality is [somewhat more subtle than this]({{ site.baseurl }}{% post_url 2016-01-09-the-scope-of-unsafe %}), but nevertheless, `unsafe` does its job pretty well -- except for when it comes to auto traits.
+The reality is [somewhat more subtle than this]({% post_url 2016-01-09-the-scope-of-unsafe %}), but nevertheless, `unsafe` does its job pretty well -- except for when it comes to auto traits.

 
 To make things worse, imagine what happens when auto traits are stabilized, so that crates can introduce their own auto traits.
 Some of them may want to express additional guarantees that the compiler cannot check, so some of these auto traits may be unsafe.
 
 To make things worse, imagine what happens when auto traits are stabilized, so that crates can introduce their own auto traits.
 Some of them may want to express additional guarantees that the compiler cannot check, so some of these auto traits may be unsafe.


@@ -116,7 +117,7 @@ However, as we have seen, with user-defined auto traits, we actually care a lot!
 Again, I think the solution here is that types like `MutexGuard<T>` should not automatically implement unsafe auto traits.
 What do I mean by "types like `MutexGuard<T>`"?
 The point that makes `MutexGuard<T>` special here is that there is an invariant attached with this type that all instances of `MutexGuard<T>` satisfy.
 Again, I think the solution here is that types like `MutexGuard<T>` should not automatically implement unsafe auto traits.
 What do I mean by "types like `MutexGuard<T>`"?
 The point that makes `MutexGuard<T>` special here is that there is an invariant attached with this type that all instances of `MutexGuard<T>` satisfy.

-(I describe this concept of types with additional invariants in more detail [in one of my previous blog posts]({{ site.baseurl }}{% post_url 2016-01-09-the-scope-of-unsafe %})).
+(I describe this concept of types with additional invariants in more detail [in one of my previous blog posts]({% post_url 2016-01-09-the-scope-of-unsafe %})).

 My proposal is to *tell the compiler* that this is the case.
 If the compiler understands that a type is "more than what it seems to be", we could know during compilation that we have to be more cautious when handling this type -- and in particular, we could have such types *not* automatically implement unsafe auto traits.
 In fact, I [proposed such an annotation](https://internals.rust-lang.org/t/pre-rfc-unsafe-types/3073) previously for different reasons, [and so did others](https://github.com/rust-lang/rfcs/issues/381).[^1]
 My proposal is to *tell the compiler* that this is the case.
 If the compiler understands that a type is "more than what it seems to be", we could know during compilation that we have to be more cautious when handling this type -- and in particular, we could have such types *not* automatically implement unsafe auto traits.
 In fact, I [proposed such an annotation](https://internals.rust-lang.org/t/pre-rfc-unsafe-types/3073) previously for different reasons, [and so did others](https://github.com/rust-lang/rfcs/issues/381).[^1]