link to 'two kinds of invariants'
[web.git] / personal / _posts / 2018-07-13-arc-synchronization.md
index 2e8f7eab1d2510c2cb57d68a308552dccfdc920f..7579dcf46a17b802966eeea4d2ce6836c805cb77 100644 (file)
@@ -4,11 +4,11 @@ categories: rust research
 reddit: /rust/comments/8ykuhv/the_tale_of_a_bug_in_arc_synchronization_and_data/
 ---
 
 reddit: /rust/comments/8ykuhv/the_tale_of_a_bug_in_arc_synchronization_and_data/
 ---
 
-While I was busy doing Rust-unrelated research, [RustBelt](https://plv.mpi-sws.org/rustbelt/) continues to move and recently found another bug (after [a missing `impl !Sync` that we found previously]({{ site.baseurl }}{% post_url 2017-06-09-mutexguard-sync %})): It turns out that `Arc::get_mut` did [not perform sufficient synchronization](https://github.com/rust-lang/rust/issues/51780), leading to a data race.
+While I was busy doing Rust-unrelated research, [RustBelt](https://plv.mpi-sws.org/rustbelt/) continues to move and recently found another bug (after [a missing `impl !Sync` that we found previously]({% post_url 2017-06-09-mutexguard-sync %})): It turns out that `Arc::get_mut` did [not perform sufficient synchronization](https://github.com/rust-lang/rust/issues/51780), leading to a data race.
 
 Notice that I am just the messenger here, the bug was actually found by [Hai](https://people.mpi-sws.org/~haidang/) and [Jacques-Henri](https://jhjourdan.mketjh.fr/).
 Still, I'd like to use this opportunity to talk a bit about weak memory, synchronization and data races.
 
 Notice that I am just the messenger here, the bug was actually found by [Hai](https://people.mpi-sws.org/~haidang/) and [Jacques-Henri](https://jhjourdan.mketjh.fr/).
 Still, I'd like to use this opportunity to talk a bit about weak memory, synchronization and data races.
-This is just a primer, there are tons of resources on the web that go into more detail (for example [here](http://preshing.com/20120913/acquire-and-release-semantics/)).
+This is just a primer, there are tons of resources on the web that go into more detail (for example [here](https://preshing.com/20120913/acquire-and-release-semantics/)).
 
 <!-- MORE -->
 
 
 <!-- MORE -->
 
@@ -173,7 +173,7 @@ I said that `Mutex`/`RwLock` are good enough *most of the time*.
 However, `Arc` is one of those cases where the overhead induced by an exclusive lock is just way too big, so it is worth using a more optimized, unsafe implementation.
 As such, you are going to find plenty of atomic accesses in [the source code of `Arc`](https://github.com/rust-lang/rust/blob/c0955a34bcb17f0b31d7b86522a520ebe7fa93ac/src/liballoc/sync.rs#L201).
 
 However, `Arc` is one of those cases where the overhead induced by an exclusive lock is just way too big, so it is worth using a more optimized, unsafe implementation.
 As such, you are going to find plenty of atomic accesses in [the source code of `Arc`](https://github.com/rust-lang/rust/blob/c0955a34bcb17f0b31d7b86522a520ebe7fa93ac/src/liballoc/sync.rs#L201).
 
-And it turns out, as Hai and Jacques-Henri noticed when attempting to prove correctness of [`Arc::get_mut`](https://doc.rust-lang.org/beta/std/sync/struct.Arc.html#method.get_mut), that there is one place where `Relaxed` as used as an ordering, [but it really should have been `Acquire`](https://github.com/rust-lang/rust/pull/52031).
+And it turns out, as Hai and Jacques-Henri noticed when attempting to prove correctness of [`Arc::get_mut`](https://doc.rust-lang.org/stable/std/sync/struct.Arc.html#method.get_mut), that there is one place where `Relaxed` was used as an ordering, [but it really should have been `Acquire`](https://github.com/rust-lang/rust/pull/52031).
 Discussing the exact details of the bug would probably fill another blog post (`Arc` is *really* subtle), but the high-level story is exactly like in our example above: Thanks to `Acquire`, an ordering is induced between the code that follows the `get_mut` and the code in another thread that dropped the last other `Arc`, decrementing the reference count to 1.
 The PR that fixed the problem contains [some more details in the comments](https://github.com/rust-lang/rust/pull/52031/files).
 With `Relaxed`, no such ordering is induced, so we have a data race.
 Discussing the exact details of the bug would probably fill another blog post (`Arc` is *really* subtle), but the high-level story is exactly like in our example above: Thanks to `Acquire`, an ordering is induced between the code that follows the `get_mut` and the code in another thread that dropped the last other `Arc`, decrementing the reference count to 1.
 The PR that fixed the problem contains [some more details in the comments](https://github.com/rust-lang/rust/pull/52031/files).
 With `Relaxed`, no such ordering is induced, so we have a data race.
@@ -182,11 +182,13 @@ To be fair, it is very unlikely that this race could lead to real misbehavior, b
 [^1]: "Mostly", you may wonder?  Unfortunately it turns out that there is [one `Relaxed` access in `make_mut`](https://github.com/rust-lang/rust/blob/c0955a34bcb17f0b31d7b86522a520ebe7fa93ac/src/liballoc/sync.rs#L793) that Hai and Jacques-Henri have not yet been able to prove correct.  However, this is likely fixable by making the entire proof more complicated.  The version where that `Relaxed` is also replaced by `Acquire` *has* been proven correct, albeit still against a model of relaxed memory accesses that is not quite as weak as C11.
 
 One last thing:
 [^1]: "Mostly", you may wonder?  Unfortunately it turns out that there is [one `Relaxed` access in `make_mut`](https://github.com/rust-lang/rust/blob/c0955a34bcb17f0b31d7b86522a520ebe7fa93ac/src/liballoc/sync.rs#L793) that Hai and Jacques-Henri have not yet been able to prove correct.  However, this is likely fixable by making the entire proof more complicated.  The version where that `Relaxed` is also replaced by `Acquire` *has* been proven correct, albeit still against a model of relaxed memory accesses that is not quite as weak as C11.
 
 One last thing:
-I have previously claimed that our [first RustBelt paper]({{ site.baseurl }}{% post_url 2017-07-08-rustbelt %}) already verified correctness of `Arc`, how can there still be bugs?
+I have previously claimed that our [first RustBelt paper]({% post_url 2017-07-08-rustbelt %}) already verified correctness of `Arc`, how can there still be bugs?
 In that paper, we did not (yet) have the tools to reason realistically about these ordering issues we have been discussing here, so instead we worked with a "sequentially consistent" logic which essentially assumes the strongest possible mode, `SeqCst`, for all atomic accesses.
 (We did not discuss `SeqCst` above, and in fact there are not many cases where it is really needed. [`Release` and `Acquire` are enough most of the time](https://internals.rust-lang.org/t/sync-once-per-instance/7918/8?u=ralfjung).)
 This is one of the simplifications we made compared to real Rust to make the verification feasible.
 In that paper, we did not (yet) have the tools to reason realistically about these ordering issues we have been discussing here, so instead we worked with a "sequentially consistent" logic which essentially assumes the strongest possible mode, `SeqCst`, for all atomic accesses.
 (We did not discuss `SeqCst` above, and in fact there are not many cases where it is really needed. [`Release` and `Acquire` are enough most of the time](https://internals.rust-lang.org/t/sync-once-per-instance/7918/8?u=ralfjung).)
 This is one of the simplifications we made compared to real Rust to make the verification feasible.
-We were realistic enough to find [another bug]({{ site.baseurl }}{% post_url 2017-06-09-mutexguard-sync %}), but not realistic enough for this one.
+We were realistic enough to find [another bug]({% post_url 2017-06-09-mutexguard-sync %}), but not realistic enough for this one.
 Hai and Jacques-Henri are currently working on remedying this particular simplification by extending the first RustBelt paper to also cover weak memory, and that's when they ran into this problem.
 
 **Update:** Turns out Servo has a [copy of `Arc`](https://doc.servo.org/servo_arc/index.html) that [has the same problem](https://github.com/servo/servo/issues/21186). So we got two bugs for the price of one. :)  **/Update**
 Hai and Jacques-Henri are currently working on remedying this particular simplification by extending the first RustBelt paper to also cover weak memory, and that's when they ran into this problem.
 
 **Update:** Turns out Servo has a [copy of `Arc`](https://doc.servo.org/servo_arc/index.html) that [has the same problem](https://github.com/servo/servo/issues/21186). So we got two bugs for the price of one. :)  **/Update**
+
+#### Footnotes