8 ms·

> Given that DEC Alpha famously had difficulty with RCU, it is only reasonable to ask how Rust will do with it. > Including some wild speculation about how Ru

> Given that DEC Alpha famously had difficulty with RCU, it is only reasonable to ask how Rust will do with it. > Including some wild speculation about how Rust's ownership model might be generalized I recommend starting with the latests post in the series and the conclusions(https://paulmck.livejournal.com/64209.html https://paulmck.livejournal.com/64209.html and https://paulmck.livejournal.com/65056.html https://paulmck.livejournal.com/65056.html). From the snippets at the beginning, it looks like the author documented how they started learning about how to solve these problems in Rust, and it does not take too long until the comment section starts pointing the author at crossbeam-rs, GhostCell, etc. which only start appearing in the series in the last couple of sections. Learning Rust by implementing a linked-list is pretty hard, but "Learning Rust by implementing RCU" has to be, by far, the hardest way to learn Rust that I know of. Kudos to the author for pushing through this so quickly and thoroguly. The posts are all excellent. I wish the author would go a little bit more into crossbeam-rs. One thing the author does not consider, is that a safe Rust interface to RCU is essentially a "proof of correctness" for RCU, i.e., it proves that using RCU via that interface cannot introduce undefined behavior. (Or maybe more technically, the contracts on the correctness of unsafe code within the safe wrapper provide a potentially incorrect "proof" of this). AFAIK no such correctness proof for the C APIs exists (there are a couple of linters that catch some issues, but there is no proof that say that if you stick by those warnings your code is UB free). The author seems to be assuming that the C APIs to RCU have been proved correct, which AFAIK is incorrect, and by ignoring the safe Rust APIs to RCU, the author is missing out on potentially finding issues on the correctness of the C APIs that Rust would discover. Basically, the question: "Can we expose Linux RCU apis to Rust?" is definetly worth asking, but the question "Can Rust prove Linux RCU APIs correct?" is much more interesting. If it can't, then why not? The fact that we have such proofs for other RCU and hazard pointers APIs in Rust shows that this is at least possible in general. And if Linux RCU can't be exposed in safe Rust, precisely understanding why would definitely be illuminating (Can Linux RCU be proven correct outside Rust, but not in Rust? Or maybe does Linux RCU APIs can actually be proven incorrect by Rust?).

dbrgn 5y ago
Note: If someone wants to learn Rust by implementing linked lists, then https://rust-unofficial.github.io/too-many-lists/ https://rust-unofficial.github.io/too-many-lists/ is a must-read :)
- volta83 5y ago
  Arguably, that's just too hardcore. You can implement doubly-linked lists in safe Rust by using Rc and Weak, Option, and RefCell (or Arc and Mutex for a safe concurrent doubly-linked list). Learning about safe Rust is gentler and more useful for a beginner, than starting to learn Rust by learning about "unsafe code". You have to know what safe Rust allows so that you can appropriately know to which contract unsafe Rust must adhere to.
  - quotemstr 5y ago
    > You can implement doubly-linked lists in safe Rust by using Rc and Weak, Option, and RefCell (or Arc and Mutex for a safe concurrent doubly-linked list). You can, but not without introducing runtime overhead relative to C and C++, e.g., by forcing reference-counting where none would be necessary in C. Rust's safety checks do in fact block some safe and zero-overhead abstractions familiar to people working in C and C++, and denying that isn't helpful. Stating that these techniques can be implemented in Rust with overhead is missing the point. Arguing that the added overhead is "minimal" (which is a meaningless word, since the word "minimal" just means "I don't care about your scenario") is still missing the point: it's overhead that's not present in unsafe languages. The reason people use languages like C++ and Rust is to get zero cost abstractions and explicit control over the machine. If you want good performance but don't care about precise control over the machine, write Java or C# or something high level like that. You'll be just as safe as you would be in Rust and more productive. I'm really tired of this motte and bailey stuff. Rust proponents say Rust gives you fine grained machine control and safety with no performance compromises, and then when you point out that the language doesn't quite live up to that promise, Rust proponents start telling you that you didn't really need that performance anyway. This argumentative tic is annoying.
    - 5y ago
gpderetta 5y ago
I can't access the article at $JOB, but if I understand correctly, Rust would guarantee that usage of the RCU API si correct, but it would be silent on the API implementation itself as it would be written with unsafe (but crossbeam-rs). On the other hand the author is probably saying that the kernel RCU C API itself has been proven correct, either manually or by machine checking (directly the C code or a translation of it in a proof assistant); usages of the API might not be proven correct though. Also note that the author of the article is the actual inventor of RCU.
- volta83 5y ago
  > Also note that the author of the article is the actual inventor of RCU. I know, so? > On the other hand the author is probably saying that the kernel RCU C API itself has been proven correct, But this is not true right? There is no formal proof, e.g., in Coq, that proves a useful subset of the RCU C API correct (as in, if you stick to this useful subset, you can't introduce UB). OTOH, a safe Rust API could be proved correct to use at least, and an implementation of it that uses unsafe, like the one in crossbeam-rs, is typically very amenable to theorem provers (much more than C). So what I am saying is that the author is ignoring the value of providing a safe Rust API for RCU, like crossbeam-rs. If the Linux RCU APIs can't be mapped to it, then maybe they are incorrect to use, and this is why we can't prove them correct. Doing the work of mapping them, and understanding any issues, could lead to changes to those APIs that might allow us to prove them correct.
  - gpderetta 5y ago
    A quick search shows a bunch of papers about RCU possibly containing proofs. I don't know if there is a coq proof, but there are other dedicated tools to model lock-free algorithms, or possibly the proofs were done by hand. Of course that's still not proving the actual C code, the translation probably still need to checked by hand.
  - pca006132 5y ago
    > an implementation of it that uses unsafe, like the one in crossbeam-rs, is typically very amenable to theorem provers (much more than C) Just wondering, how many unsafe code in commonly used libraries (standard library, tokio etc.) are proved using theorem provers?
mftb 5y ago
RCU - Read, Copy, Update - A strategy for readers and writers, where the readers do not exclude writers (best as I can tell).
- ncmncm 5y ago
  ... without any sort of locking.
GoblinSlayer 5y ago
>AFAIK no such correctness proof for the C APIs exists There's a whole proven correct kernel: http://sel4.systems/ http://sel4.systems/
- volta83 5y ago
  SeL4 is not the Linux kernel and it doesn't use RCU. So yes, there is a correctness proof for a completely different operating system that does not use the one thing we are talking about here.
cormacrelf 5y ago
> that a safe Rust interface to RCU is essentially a "proof of correctness" for RCU, i.e., it proves that using RCU via that interface cannot introduce undefined behavior. (Or maybe more technically, the contracts on the correctness of unsafe code within the safe wrapper provide a potentially incorrect "proof" of this). Adding an unsafe block around a call to C code doesn't prove anything. Rust does not provide proofs of the code you write in it, except if you do not use unsafe at all. RCU is an API and a general technique. It can be implemented a ton of different ways (including, as the author noted, as a single instruction if Linux is built with pre-emption disabled). You must not conflate the the soundness of an API with the soundness of its implementation. 'Can Rust prove Linux RCU APIs correct?' is nearly completely without meaning. A similarly meaningless project would be to prove that the idea of malloc/free is correct. There's nothing that could even be incorrect or correct about it, and you don't need Rust wrappers to tell you that. Now prove glibc's malloc is correct; very different question.
- volta83 5y ago
  > Adding an unsafe block around a call to C code doesn't prove anything. I didn't say otherwise. What I said is that writing unsafe code is writing a proof that the code is correct. If the proof is incorrect, the behavior is undefined, and Rust makes no guarantees. unsafe literally means "I've proven this code correct". As mentioned, most uses of unsafe in the standard library are accompanied by a comment that documents the proof.
  - cormacrelf 5y ago
    `unsafe { ... }` means "I hope you are convinced by my arguments in the surrounding comments, or better still in my POPL21 paper, that this is correct". Other than that, not much. The keyword itself has essentially zero relationship with the existence of a formal proof. You are talking about proof in a very loose sense. The narrower point I think you're making is that hopefully attempting to create a safe API around the RCU pattern makes someone think about RCU's correctness even harder. I'm not sure it will produce much, given how much attention RCU has already received in the past 20 years. Any innovation you get from that process will probably be concentrated in describing/encoding the ownership pattern in Rust terms, since that's non-obvious. But the epoch GC implemented in Crossbeam is pretty similar overall to RCU, so it has much to build on in that regard.
jaytaylor 5y ago
RCU, for the uninitiated: https://en.m.wikipedia.org/wiki/Read-copy-update https://en.m.wikipedia.org/wiki/Read-copy-update

dbrgn 5y ago

Note: If someone wants to learn Rust by implementing linked lists, then https://rust-unofficial.github.io/too-many-lists/ https://rust-unofficial.github.io/too-many-lists/ is a must-read :)

volta83 5y ago
Arguably, that's just too hardcore. You can implement doubly-linked lists in safe Rust by using Rc and Weak, Option, and RefCell (or Arc and Mutex for a safe concurrent doubly-linked list). Learning about safe Rust is gentler and more useful for a beginner, than starting to learn Rust by learning about "unsafe code". You have to know what safe Rust allows so that you can appropriately know to which contract unsafe Rust must adhere to.
- quotemstr 5y ago
  > You can implement doubly-linked lists in safe Rust by using Rc and Weak, Option, and RefCell (or Arc and Mutex for a safe concurrent doubly-linked list). You can, but not without introducing runtime overhead relative to C and C++, e.g., by forcing reference-counting where none would be necessary in C. Rust's safety checks do in fact block some safe and zero-overhead abstractions familiar to people working in C and C++, and denying that isn't helpful. Stating that these techniques can be implemented in Rust with overhead is missing the point. Arguing that the added overhead is "minimal" (which is a meaningless word, since the word "minimal" just means "I don't care about your scenario") is still missing the point: it's overhead that's not present in unsafe languages. The reason people use languages like C++ and Rust is to get zero cost abstractions and explicit control over the machine. If you want good performance but don't care about precise control over the machine, write Java or C# or something high level like that. You'll be just as safe as you would be in Rust and more productive. I'm really tired of this motte and bailey stuff. Rust proponents say Rust gives you fine grained machine control and safety with no performance compromises, and then when you point out that the language doesn't quite live up to that promise, Rust proponents start telling you that you didn't really need that performance anyway. This argumentative tic is annoying.
  - 5y ago

gpderetta 5y ago

I can't access the article at $JOB, but if I understand correctly, Rust would guarantee that usage of the RCU API si correct, but it would be silent on the API implementation itself as it would be written with unsafe (but crossbeam-rs). On the other hand the author is probably saying that the kernel RCU C API itself has been proven correct, either manually or by machine checking (directly the C code or a translation of it in a proof assistant); usages of the API might not be proven correct though. Also note that the author of the article is the actual inventor of RCU.

volta83 5y ago
> Also note that the author of the article is the actual inventor of RCU. I know, so? > On the other hand the author is probably saying that the kernel RCU C API itself has been proven correct, But this is not true right? There is no formal proof, e.g., in Coq, that proves a useful subset of the RCU C API correct (as in, if you stick to this useful subset, you can't introduce UB). OTOH, a safe Rust API could be proved correct to use at least, and an implementation of it that uses unsafe, like the one in crossbeam-rs, is typically very amenable to theorem provers (much more than C). So what I am saying is that the author is ignoring the value of providing a safe Rust API for RCU, like crossbeam-rs. If the Linux RCU APIs can't be mapped to it, then maybe they are incorrect to use, and this is why we can't prove them correct. Doing the work of mapping them, and understanding any issues, could lead to changes to those APIs that might allow us to prove them correct.
- gpderetta 5y ago
  A quick search shows a bunch of papers about RCU possibly containing proofs. I don't know if there is a coq proof, but there are other dedicated tools to model lock-free algorithms, or possibly the proofs were done by hand. Of course that's still not proving the actual C code, the translation probably still need to checked by hand.
- pca006132 5y ago
  > an implementation of it that uses unsafe, like the one in crossbeam-rs, is typically very amenable to theorem provers (much more than C) Just wondering, how many unsafe code in commonly used libraries (standard library, tokio etc.) are proved using theorem provers?

mftb 5y ago

RCU - Read, Copy, Update - A strategy for readers and writers, where the readers do not exclude writers (best as I can tell).

ncmncm 5y ago
... without any sort of locking.

GoblinSlayer 5y ago

>AFAIK no such correctness proof for the C APIs exists There's a whole proven correct kernel: http://sel4.systems/ http://sel4.systems/

volta83 5y ago
SeL4 is not the Linux kernel and it doesn't use RCU. So yes, there is a correctness proof for a completely different operating system that does not use the one thing we are talking about here.

cormacrelf 5y ago

> that a safe Rust interface to RCU is essentially a "proof of correctness" for RCU, i.e., it proves that using RCU via that interface cannot introduce undefined behavior. (Or maybe more technically, the contracts on the correctness of unsafe code within the safe wrapper provide a potentially incorrect "proof" of this). Adding an unsafe block around a call to C code doesn't prove anything. Rust does not provide proofs of the code you write in it, except if you do not use unsafe at all. RCU is an API and a general technique. It can be implemented a ton of different ways (including, as the author noted, as a single instruction if Linux is built with pre-emption disabled). You must not conflate the the soundness of an API with the soundness of its implementation. 'Can Rust prove Linux RCU APIs correct?' is nearly completely without meaning. A similarly meaningless project would be to prove that the idea of malloc/free is correct. There's nothing that could even be incorrect or correct about it, and you don't need Rust wrappers to tell you that. Now prove glibc's malloc is correct; very different question.

volta83 5y ago
> Adding an unsafe block around a call to C code doesn't prove anything. I didn't say otherwise. What I said is that writing unsafe code is writing a proof that the code is correct. If the proof is incorrect, the behavior is undefined, and Rust makes no guarantees. unsafe literally means "I've proven this code correct". As mentioned, most uses of unsafe in the standard library are accompanied by a comment that documents the proof.
- cormacrelf 5y ago
  `unsafe { ... }` means "I hope you are convinced by my arguments in the surrounding comments, or better still in my POPL21 paper, that this is correct". Other than that, not much. The keyword itself has essentially zero relationship with the existence of a formal proof. You are talking about proof in a very loose sense. The narrower point I think you're making is that hopefully attempting to create a safe API around the RCU pattern makes someone think about RCU's correctness even harder. I'm not sure it will produce much, given how much attention RCU has already received in the past 20 years. Any innovation you get from that process will probably be concentrated in describing/encoding the ownership pattern in Rust terms, since that's non-obvious. But the epoch GC implemented in Crossbeam is pretty similar overall to RCU, so it has much to build on in that regard.

jaytaylor 5y ago

RCU, for the uninitiated: https://en.m.wikipedia.org/wiki/Read-copy-update https://en.m.wikipedia.org/wiki/Read-copy-update