From 280a510bc740efaa86d23fb11bfef556d53479d6 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 16 Jul 2018 15:34:54 +0200 Subject: [PATCH 1/1] link to Servo's copy of the same code --- ralf/_posts/2018-07-13-arc-synchronization.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/ralf/_posts/2018-07-13-arc-synchronization.md b/ralf/_posts/2018-07-13-arc-synchronization.md index 1ad8a46..2e8f7ea 100644 --- a/ralf/_posts/2018-07-13-arc-synchronization.md +++ b/ralf/_posts/2018-07-13-arc-synchronization.md @@ -188,3 +188,5 @@ In that paper, we did not (yet) have the tools to reason realistically about the 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. 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** -- 2.30.2