mention abstract machine earlier

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

diff --git a/ralf/_posts/2017-06-09-mutexguard-sync.md b/ralf/_posts/2017-06-09-mutexguard-sync.md
index 62ac7def999ecaf7ca877dc1a371d0e4040b85b3..2fe628a5e9e2a07bfc01c9a9cfb6b3c908fd5aa8 100644 (file)
--- a/ralf/_posts/2017-06-09-mutexguard-sync.md
+++ b/ralf/_posts/2017-06-09-mutexguard-sync.md
@@ -1,10 +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/
 ---
 
 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 -->
 


@@ -105,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.


@@ -117,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]


@@ -129,3 +129,4 @@ However, I hope I convinced you that if we don't act, errors like the one descri
 That said, such decisions are of course going to go through the usual RFC process.
 It's certainly possible that someone comes up with a compromise that preserves some of the usefulness of auto traits, without putting safety at risk.
 
 That said, such decisions are of course going to go through the usual RFC process.
 It's certainly possible that someone comes up with a compromise that preserves some of the usefulness of auto traits, without putting safety at risk.
 

+#### Footnotes