3 ms·
> 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
by 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 agoA 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?
- volta83 5y agoMost of the unsafe code in libcore is proved in Iris. Some of the unsafe code in the standard library also. Some parts of crossbeam have pencil&paper proofs documented.
- steveklabnik 5y agoDon't have comprehensive enough data to know, but part of the standard library was proven via the Rustbelt project, and it found some places where there were bugs, as well as some places where things could safely be loosened up.