From 6b193cf5f19077de20c195bc0be6cf0b4e7719e0 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Fri, 13 Jul 2018 18:25:42 +0200 Subject: [PATCH] extend footnote --- personal/_posts/2018-07-13-arc-synchronization.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/personal/_posts/2018-07-13-arc-synchronization.md b/personal/_posts/2018-07-13-arc-synchronization.md index 7c78cd0..37f3a31 100644 --- a/personal/_posts/2018-07-13-arc-synchronization.md +++ b/personal/_posts/2018-07-13-arc-synchronization.md @@ -178,7 +178,7 @@ Discussing the exact details of the bug would probably fill another blog post (` With `Relaxed`, no such ordering is induced, so we have a data race. To be fair, it is very unlikely that this race could lead to real misbehavior, but I am still happy to know that we now have a proof that `Arc` is mostly[^1] correctly synchronized. -[^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. +[^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? -- 2.30.2