4 ms·

Have you written a lot of concurrent code in rust? Did your experience doing so convince you that it's something you should "fear" doing?

mratsim 6y ago
I've written a multithreading runtime from the ground up in Nim.[1] And yes, writing that taught me that current programming languages are not sufficiently equipped to deal with concurrency bugs, including Rust. The bugs that I had where of the dining philosophers kind (deadlocks or livelocks when trying to put a thread to sleep for example or resolving data dependencies between multiple threads), some were due to a bug in glibc where only formal verification allowed me to ensure that I was doing the correct thing and it was the lower-level layers that was incorrect.[2] Similarly, state machine formal verification to prevent design bugs is something that hardware engineers are deeply aware of but would also be extremely useful to ensure "correct-by-construction" event driven code in software engineering. In comparison, we have many more tools to address memory bugs (Address Sanitizer, Valgrind and fuzzers in particular) but synchronization and communicating state machine bugs are still impractically addressed at the moment. This is something I'd really want Nim to explore and I'm really excited about the Z3 integration[3] to enable new formally verified use-cases[4]. Unfortunately, when I express concerns about those bugs to people from the Rust community, they tend to dismiss those as if the borrow checker was the panacea to all multithreading problems. [1]: https://github.com/mratsim/weave https://github.com/mratsim/weave [2]: https://github.com/mratsim/weave/issues/56 https://github.com/mratsim/weave/issues/56 [3]: https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html [4]: https://github.com/nim-lang/RFCs/issues/222 https://github.com/nim-lang/RFCs/issues/222
- staticassertion 6y ago
  Sorry that I see your post is downvoted, I'm generally in agreement, as an avid rust programmer. Rust can express a lot of safety guarantees, but there's a massive amount of room for improvements, and I'm sorry that the community hasn't been accepting of that in your interactions. > Similarly, state machine formal verification to prevent design bugs are something that hardware engineers are deeply aware of but would also be extremely useful to ensure "correct-by-construction" event driven code. This reminds me a lot of P. Rust has a crate that I wouldn't necessarily recommend, but it might be similar to what you want: https://github.com/fitzgen/state_machine_future https://github.com/fitzgen/state_machine_future Of course, in this case the code is the model, there is no verification here. The Z3 integration with Nim is super cool, would love to see something like that for Rust. I know of some existing research that reminds me of this but I don't have time to dig up the paper - it was implemented in macros, and looked a lot like what you've got there, with pre/post conditions, ensures, etc. If someone has that paper, please link it! I would love to reread. edit: Here's one rust crate leveraging Z3, but not the one I was thinking of https://github.com/Rust-Proof/rustproof https://github.com/Rust-Proof/rustproof
- ibotty 6y ago
  Did you write a bug report to glibc? I'd love to read about how the bug is happening.
  - mratsim 6y ago
    I didn't, however you can read my writeup and investigation attempts here: - https://github.com/mratsim/weave/issues/56 https://github.com/mratsim/weave/issues/56 And the fix was directly using Linux futexes: - https://github.com/mratsim/weave/pull/58/files https://github.com/mratsim/weave/pull/58/files

mratsim 6y ago

I've written a multithreading runtime from the ground up in Nim.[1] And yes, writing that taught me that current programming languages are not sufficiently equipped to deal with concurrency bugs, including Rust. The bugs that I had where of the dining philosophers kind (deadlocks or livelocks when trying to put a thread to sleep for example or resolving data dependencies between multiple threads), some were due to a bug in glibc where only formal verification allowed me to ensure that I was doing the correct thing and it was the lower-level layers that was incorrect.[2] Similarly, state machine formal verification to prevent design bugs is something that hardware engineers are deeply aware of but would also be extremely useful to ensure "correct-by-construction" event driven code in software engineering. In comparison, we have many more tools to address memory bugs (Address Sanitizer, Valgrind and fuzzers in particular) but synchronization and communicating state machine bugs are still impractically addressed at the moment. This is something I'd really want Nim to explore and I'm really excited about the Z3 integration[3] to enable new formally verified use-cases[4]. Unfortunately, when I express concerns about those bugs to people from the Rust community, they tend to dismiss those as if the borrow checker was the panacea to all multithreading problems. [1]: https://github.com/mratsim/weave https://github.com/mratsim/weave [2]: https://github.com/mratsim/weave/issues/56 https://github.com/mratsim/weave/issues/56 [3]: https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html [4]: https://github.com/nim-lang/RFCs/issues/222 https://github.com/nim-lang/RFCs/issues/222

staticassertion 6y ago
Sorry that I see your post is downvoted, I'm generally in agreement, as an avid rust programmer. Rust can express a lot of safety guarantees, but there's a massive amount of room for improvements, and I'm sorry that the community hasn't been accepting of that in your interactions. > Similarly, state machine formal verification to prevent design bugs are something that hardware engineers are deeply aware of but would also be extremely useful to ensure "correct-by-construction" event driven code. This reminds me a lot of P. Rust has a crate that I wouldn't necessarily recommend, but it might be similar to what you want: https://github.com/fitzgen/state_machine_future https://github.com/fitzgen/state_machine_future Of course, in this case the code is the model, there is no verification here. The Z3 integration with Nim is super cool, would love to see something like that for Rust. I know of some existing research that reminds me of this but I don't have time to dig up the paper - it was implemented in macros, and looked a lot like what you've got there, with pre/post conditions, ensures, etc. If someone has that paper, please link it! I would love to reread. edit: Here's one rust crate leveraging Z3, but not the one I was thinking of https://github.com/Rust-Proof/rustproof https://github.com/Rust-Proof/rustproof
ibotty 6y ago
Did you write a bug report to glibc? I'd love to read about how the bug is happening.
- mratsim 6y ago
  I didn't, however you can read my writeup and investigation attempts here: - https://github.com/mratsim/weave/issues/56 https://github.com/mratsim/weave/issues/56 And the fix was directly using Linux futexes: - https://github.com/mratsim/weave/pull/58/files https://github.com/mratsim/weave/pull/58/files