3 ms·
So many thoughts. * Rust threads run on CPU cores, but also GPU cores, FPGA cores, and a wider range of nastier hardware than Linux kernel threads run on. * T
by volta83 5y ago
So many thoughts.
* Rust threads run on CPU cores, but also GPU cores, FPGA cores, and a wider range of nastier hardware than Linux kernel threads run on.
* The author implies throughout the text that safe Rust operations might not be allowed in unsafe Rust. This hints at a deep misunderstanding of how Rust works.
* C, C++, and similar languages, do not have as a goal to be "sound". Soundness is, however, core to Rust's value proposition.
* C, C++, and similar languages, do not have the goal that undefined behavior must always trap in their abstract machines. But Rust does.
* C++ and similar languages do not have the goal of forever-backwards-compatibility (e.g. C++ breaks backwardward compatibility on almost every new standard release). Rust, however, guarantees that all programs written for Rust 1.0 in 2015 that have no undefined behavior will build and run correctly _forever_.
* Rust has many compiler backends, e.g., LLVM-IR, GCC, Cranelift, SPIR-V, etc. Rust code is translated to the IR of those toolchains. That is, those IRs would need to be extended with the new semantics as well to be useful.
> But again, this decision rests not with me, but with the Rust communty.
The Rust community needs people working on formalizing the memory model further. So if they are interested, they should jump right in.
They should probably start by understanding Rust as is today, learning about unsafe code, and well the blog post cites https://plv.mpi-sws.org/rustbelt/rbrlx/ https://plv.mpi-sws.org/rustbelt/rbrlx/ , but it is clear from the exposition that the author has not deeply understood that paper, so maybe they should also take a deeper look at that. All the proofs are open-source. So if they think they can extend the soundness proofs with new features that are also sound, that could be a place to start.
- littlestymaar 5y ago> * C, C++, and similar languages, do not have the goal that undefined behavior must always trap in their abstract machines. But Rust does. What do you mean ?
- volta83 5y agoThe implementation of the Rust abstract machine - miri - stops execution of Rust programs when they exhibit undefined behavior. C, C++, etc. don't even have implementations of their abstract machines. They don't have one existing as a goal. And they are happy to make certain operations exhibit undefined behavior even if that implies that it would make an implementation of the abstract machine that traps impossible. This is why even if you were to combine valgrind with address sanitizer, memory sanitizer, thread sanitizer, undefined-behavior-sanitizer, and other existing C and C++ tools, there is still a lot of classes of undefined behavior that these tools can't detect. That's fine in C and C++, but not fine in Rust. In Rust, if we add a new type of undefined behavior, the constraint is that it should be (demonstrably) possible to extend miri to detect it, such that if a user doesn't know whether some program exhibits undefined behavior for some inputs, they can just run it under miri, and miri will precisely pinpoint which part of their code exhibited undefined behavior and why, and how their program execution got there.
- littlestymaar 5y agoThanks! > This is why even if you were to combine valgrind with address sanitizer, memory sanitizer, thread sanitizer, undefined-behavior-sanitizer, and other existing C and C++ tools, there is still a lot of classes of undefined behavior that these tools can't detect. Do you have specific examples of such UB?
- volta83 5y agoSure: TBAA, access to invalid union field (in C++), etc. Many of them are impossible in theory to check, and many are impossible to efficiently check in practice.
- pjmlp 5y agoTo keep Rust's safety model, anything that is UB should only be allowed in unsafe code blocks. However to be 100% sure of what can be considered safe, it needs to be the same regardless of what hardware is being targeted. That is how C got its UB in first place, WG14 didn't want to rule out any kind of hardware that was possible to target so UB it was. Other memory safe systems programming languages have gone through other path and were willing to add abstractions to their runtimes instead, ensuring that the memory model remains consistent to the developers. Naturally in languages that want to be zero cost abstraction, that solution is not welcomed.
- Lhiw 5y agoGuessing safety guarantee's? https://doc.rust-lang.org/reference/behavior-considered-undefined.html https://doc.rust-lang.org/reference/behavior-considered-unde...