add GhostCell paper

[web.git] / personal / _posts / 2020-12-14-provenance.md

diff --git a/personal/_posts/2020-12-14-provenance.md b/personal/_posts/2020-12-14-provenance.md
index bb2faed3c8678b38615cff4660c5e7e6dbc41525..4e95665df3daa7bc67ad5806493469143e2c6ee2 100644 (file)
--- a/personal/_posts/2020-12-14-provenance.md
+++ b/personal/_posts/2020-12-14-provenance.md
@@ -1,7 +1,9 @@
 ---
 title: "Pointers Are Complicated II, or: We need better language specs"
 ---
 title: "Pointers Are Complicated II, or: We need better language specs"

-categories: rust
+categories: rust research

 forum: https://internals.rust-lang.org/t/pointers-are-complicated-ii-or-we-need-better-language-specs/13562
 forum: https://internals.rust-lang.org/t/pointers-are-complicated-ii-or-we-need-better-language-specs/13562

+license: CC BY-SA 4.0
+license-url: https://creativecommons.org/licenses/by-sa/4.0/

 ---
 
 Some time ago, I wrote a blog post about how [there's more to a pointer than meets the eye]({% post_url 2018-07-24-pointers-and-bytes %}).
 ---
 
 Some time ago, I wrote a blog post about how [there's more to a pointer than meets the eye]({% post_url 2018-07-24-pointers-and-bytes %}).


@@ -262,7 +264,7 @@ Nowadays, its main purpose is to help unsafe code authors avoid UB, but for me p
 It also feeds back into the design of the UB rules by discovering patterns that people want or need to use but that are not currently accepted by Miri.
 
 On the LLVM side, the main development in this area is [Alive](https://blog.regehr.org/archives/1722), a tool that can automatically validate[^validate] optimizations performed by LLVM.
 It also feeds back into the design of the UB rules by discovering patterns that people want or need to use but that are not currently accepted by Miri.
 
 On the LLVM side, the main development in this area is [Alive](https://blog.regehr.org/archives/1722), a tool that can automatically validate[^validate] optimizations performed by LLVM.

-Alive has found [many bugs in LLVM optimizations](https://github.com/AliveToolkit/alive2/blob/master/BugList.md), and indeed much of the recent dialog with the LLVM community aimed at a more precise IR semantics is pushed by the people building Alive, lead by Nuno P. Lopes and John Regehr.
+Alive has found [many bugs in LLVM optimizations](https://github.com/AliveToolkit/alive2/blob/master/BugList.md), and indeed much of the recent dialog with the LLVM community aimed at a more precise IR semantics is pushed by the people building Alive, led by Nuno P. Lopes and John Regehr.

 
 [^validate]: A note on terminology: "validating" an optimization means that given the program text before and after the optimization, the tool will try to prove that this particular transformation is correct. This is in contrast to "verifying" an optimization where a once-and-forall proof is carried out showing that the optimization will always perform a correct transformation. Verification gives a much stronger result, but is also extremely difficult to carry out, so validation is a great middle-ground that is still able to find plenty of bugs.
 
 
 [^validate]: A note on terminology: "validating" an optimization means that given the program text before and after the optimization, the tool will try to prove that this particular transformation is correct. This is in contrast to "verifying" an optimization where a once-and-forall proof is carried out showing that the optimization will always perform a correct transformation. Verification gives a much stronger result, but is also extremely difficult to carry out, so validation is a great middle-ground that is still able to find plenty of bugs.
 


@@ -270,7 +272,7 @@ Progress on these specification efforts is slow, though, in particular when it t
 I hope this post can raise awareness for the subtle problems optimizing compilers are facing, and convince some people that figuring out the specification of compiler IRs is an important and interesting problem to work on. :)
 
 That's all I have for today, thanks for sticking with me!
 I hope this post can raise awareness for the subtle problems optimizing compilers are facing, and convince some people that figuring out the specification of compiler IRs is an important and interesting problem to work on. :)
 
 That's all I have for today, thanks for sticking with me!

-As usual, this post can be [discussed in the Rust forums](https://internals.rust-lang.org/t/pointers-are-complicated-ii-or-we-need-better-language-specs/13562).
+As usual, this post can be [discussed in the Rust forums](https://internals.rust-lang.org/t/pointers-are-complicated-ii-or-we-need-better-language-specs/13562) and [on Reddit](https://www.reddit.com/r/rust/comments/kd157i/pointers_are_complicated_ii_or_we_need_better/).

 I am curious what your thoughts are on how we can build compilers that do not suffer from the issues I have discussed here.
 
 #### Footnotes
 I am curious what your thoughts are on how we can build compilers that do not suffer from the issues I have discussed here.
 
 #### Footnotes