Writing correct lock-free and distributed stateful systems in Rust, with TLA+
1–10 of 96 posts
Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+
#2I like this a lot
Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+
#3I like this a lot
Same here!
Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+
#4There's a lot of interest in formally verifying things about the unsafe subset of Rust, for example the Rust Belt project: http://plv.mpi-sws.org/rustbelt/. One thing I've not well understood is how these efforts may be affected by some of the conversations around the unsafe code guidelines effort:
https://github.com/rust-lang/rfcs/pull/1643 https://github.com/nikomatsakis/rust-memory-model
Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+
#5There's a lot of interest in formally verifying things about the unsafe subset of Rust, for example the Rust Belt project: http://plv.mpi-sws.org/rustbelt/ . One thing I've not well understood is how these efforts may be affected by some of the conversations around the unsafe code guidelines effort: https://github.com/rust-lang/rfcs/pull/1643 https://github.com/nikomatsakis/rust-memory-model
Just curious: Are there also attempts in the reverse direction?
That is, are there attempts to improve the Rust language and/or optimizer such that more and more "unsafe" sections can be replaced by safe code that has the same performance? (maybe even compiles down to the same machine code)
Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+
#6There's a lot of interest in formally verifying things about the unsafe subset of Rust, for example the Rust Belt project: http://plv.mpi-sws.org/rustbelt/ . One thing I've not well understood is how these efforts may be affected by some of the conversations around the unsafe code guidelines effort: https://github.com/rust-lang/rfcs/pull/1643 https://github.com/nikomatsakis/rust-memory-model
Just curious: Are there also attempts in the reverse direction? That is, are there attempts to improve the Rust language and/or optimizer such that more and more "unsafe" sections can be replaced by safe code that has the same performance? (maybe even compiles down to the same machine code)
There are already a lot of cases where LLVM can successfully optimize away things like safe Rust's bounds checks in loops.
There are also efforts to include "const generics" which will let you use e.g. array lengths as generics that may be able to teach LLVM new optimizations. Maybe someday in the far future that will grow into some kind of dependent typing extension for Rust? That could potentially allow for safe, bounds-check free array access that would currently require unsafe. But I don't know if that would allow for proving the kinds of things this article discusses.
Ultimately though, the unsafe subset is pretty small and is generally in my experience only interesting when building heavily reused abstractions (the kinds of lock-free algorithms OP discusses for example). It'll be really cool if these efforts expose some ways to shrink reliance on unsafe code, but I'm personally not sweating it.
Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+
#7There's a lot of interest in formally verifying things about the unsafe subset of Rust, for example the Rust Belt project: http://plv.mpi-sws.org/rustbelt/ . One thing I've not well understood is how these efforts may be affected by some of the conversations around the unsafe code guidelines effort: https://github.com/rust-lang/rfcs/pull/1643 https://github.com/nikomatsakis/rust-memory-model
Just curious: Are there also attempts in the reverse direction? That is, are there attempts to improve the Rust language and/or optimizer such that more and more "unsafe" sections can be replaced by safe code that has the same performance? (maybe even compiles down to the same machine code)
There is interest in enabling safe interface, that is, improving Rust the language so that you can provide safe interface with better performance. A good example is so-called "streaming iterator".
There is less interest in changing Rust so that currently unsafe implementation (not interface) of safe interface can be made safe, that is, verified by compiler. As grandparent stated, and I agree, as long as interface is safe I don't think it is important that implementation is verified by compiler (hence safe) or some external tool or hand proof.
Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+
#8There's a lot of interest in formally verifying things about the unsafe subset of Rust, for example the Rust Belt project: http://plv.mpi-sws.org/rustbelt/ . One thing I've not well understood is how these efforts may be affected by some of the conversations around the unsafe code guidelines effort: https://github.com/rust-lang/rfcs/pull/1643 https://github.com/nikomatsakis/rust-memory-model
Just curious: Are there also attempts in the reverse direction? That is, are there attempts to improve the Rust language and/or optimizer such that more and more "unsafe" sections can be replaced by safe code that has the same performance? (maybe even compiles down to the same machine code)
> That is, are there attempts to improve the Rust language and/or optimizer such that more and more "unsafe" sections can be replaced by safe code that has the same performance?
I write a fair bit of production and hobby Rust, some of it very performance-intensive. And at this point, 'unsafe' is already very rare in the code I see. The most common uses:
1. For implementing certain core data structures based on pointers. This is pretty rare—there are good implementations of just about everything I need, either from the 'std::collections' library (which uses a moderate amount of 'unsafe') or from third parties (who tend to use much less 'unsafe').
2. For the FFI. Again, this is increasingly rare: More and more key libraries are now available as pure Rust, and the "big" C libraries typically have well-maintained bindings.
3. Theoretically, for performance. But I've written tons of high-performance, benchmarked Rust without ever touching 'unsafe'.
And I do feed a fair bit of my code through fuzzers, and they've never found an exploitable weakness.
So my gut feeling? There really isn't much 'unsafe' out there. And the small amount of 'unsafe' code that exists is probably—based on my experience fuzzing it—"safer" than all but the very best C/C++ code. I can live with that for now, on a strictly practical level.
Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+
#9Earlier quoted context omitted.
Just curious: Are there also attempts in the reverse direction? That is, are there attempts to improve the Rust language and/or optimizer such that more and more "unsafe" sections can be replaced by safe code that has the same performance? (maybe even compiles down to the same machine code)
There is interest in enabling safe interface, that is, improving Rust the language so that you can provide safe interface with better performance. A good example is so-called "streaming iterator". There is less interest in changing Rust so that currently unsafe implementation (not interface) of safe interface can be made safe, that is, verified by compiler. As grandparent stated, and I agree, as long as interface is…
Maybe I'm missing something, but I could write an interface labelled sage on top of any unsafe code I want. Why doesn't it matter that my unsafe implementation is proven correct?
Re: Writing correct lock-free and distributed stateful systems in Rust, with TLA+
#10Lets say you model-checked some distributed algorithm with TLA+. You then implement it in Rust. How are you going to check that your implementation implements exactly the algorithm you have checked and not some other algorithm which looks very similar?
I think the phrase 'reliable systems' is more appropriate to what you are up to, as opposed to the phrase 'correct systems' which usually corresponds to formal verification.