> 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.
`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.
> `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".
I disagree here (and that's ok).
The unsafe keyword tells Rust "this code is sound", i.e., there exist no program execution for which this code will cause safe Rust to exhibit undefined behavior.
Rust will parse it, type check it, compile it, link it, etc. "as-if" it was sound.
And Rust only makes any guarantees about what your program does if the unsafe code was actually sound.
From the point of view of the compiler, the unsafe block itself is a user-provided proof that whatever that code does is sound.
If you write: unsafe { *ptr } that's a proof that dereferencing the pointer is sound, therefore the pointer is non-null, it points to an aligned allocation able to hold a type, the value at that memory location is a value of that type (i.e. the pointer is dereferenceable), etc.
The Rust compiler accepts your proof and generates code as if your proof is correct. In particular, it will compile code around that code under that assumption, it will eliminate null pointer checks after that code, etc.
If the proof that an unsafe block provides is incorrect, then the behavior is undefined, and Rust makes no guarantees.
I agree with you that given some unsafe code, actually proving it correct is not something that the compiler does, and that creating a tool that does this is hard. If it were easy, the compiler would already do it, and we wouldn't need unsafe at all.
Unsafe exists because there are things that the compiler can't prove correct, and this escape hatch allows the user to provide a proof that the compiler can integrate into how it compiles the program.
There is a whole repository of Iris proofs for unsafe blocks in the Rust standard library, for which we have formal proofs. But these are not integrated in any way with the Rust code one writes. They have been written by humans aiming to get a confirmation that the proof expressed by the unsafe blocks are indeed correct. Some were not, and had to be fixed, and pretty much every fix has generated a paper.
I think you are not using 'proof' in the way that most people would understand it. A proof is usually considered a series of steps someone can take to verify that something is true themselves (i.e. there is no need to trust whoever produced the proof is malicious or mistaken about what they are trying to prove, if you can follow the proof you can see for yourself). Proving something to a compiler therefore is generally understood to mean giving something to the compiler which it actually checks it sound (even if it could not produce the proof on its own). This is effectively how type-checking and borrow checking works (your program is a kind of proof the compiler verifies). 'unsafe' in this case is not a proof, it is more like a promise (not in the async sense) or assertion (not in the debug sense). The compiler trusts that you have not made a mistake, it does not have any way to verify that you haven't. You may have a proof to the person reading the code that there is no mistake (or you may not, either because your proof is incorrect or the person cannot understand the proof), but it is not a proof to the compiler.
(In fact, there was much bikeshedding at one point about renaming the 'unsafe' keyword to make this explicit: suggestioned included 'assumed_safe', 'trustme', 'trusted', as well as less serious ones like 'yolo' and 'hold_my_beer_and_watch_this': https://github.com/rust-lang/rfcs/pull/117)
> I agree [...] actually proving it correct is not something that the compiler does
Yes. Unsafe blocks are bare assertions, no more. Everything you described about what happens in Rustc when you use it is better described as making a bare assertion to the compiler. Everything beyond that is socially constructed. Saying it's a proof sounds even more silly when you recall that Rust programmers treat it as quite the opposite -- radioactive markers of places where the program might cause UB.
You were trying to characterise it as a proof because you're claiming that "Can Rust prove Linux RCU APIs correct?" is an interesting question. But you are actually asking "Will Rust compile RCU code if we assert to it that using the RCU API is safe?", and the answer is unconditionally yes. It is not an interesting question at all. Your misuse of the word proof led you there, so I am suggesting you stop calling the unsafe keyword a proof.
In the broader scheme of things, yes, the way in which Rust encourages you to isolate unsafety is helpful, and so if you wanted something formally verified Rust is a good language for that. That doesn't really translate to RCU, because the hypothetical Rust API would not be an implementation of RCU. All the Iris proofs that have come out of the RustBelt project are bad examples here, because they were actual implementations of things, not APIs around black box implementations that change under your feet when you set kconfigs.
As a final thought, here is a supposedly safe-encapsulated Rust API for RCU, I would invite anyone to suggest how writing down this very simple API or similar + a few calls to extern "C" wrappers for the RCU macros could possibly help "prove Linux RCU APIs correct", whatever that means: https://docs.rs/rcu-clean/0.1.6/rcu_clean/struct.ArcRcu.html
(Little edit: if you're interested in what circumstances will lead Rust wrappers of C code to elucidate safety, look into rlua, a project to create a safe wrapper for Lua (https://github.com/amethyst/rlua). Arguably the main outcome is that we now know that the Lua API cannot be wrapped safely with zero cost, in no small part due to the use of longjmp. Some of RCU's APIs require you do not sleep or block in any way while using it, lest you wake up with the GC train having left the station. For this reason I imagine you won't be able to encode all the usage requirements in the Rust type system, let alone make an actual safe zero-cost API, let alone turn that into a proof of anything.)
I've look at the literature every couple of years, and to the best of my knowledge, there is no paper proving that a subset of the Linux kernel RCU apis are sound.
If you are aware of one, I am intrinsically interested in this topic.
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.