26 ms·

Rust concurrency: the archetype of a message-passing bug

187 points by polyglotfacto 6y ago

ivanbakel 6y ago
This is a cool technical exploration of some concurrency ideas: but event loops combined with Rust's borrow checker actually make for a re-invention of the actor model from first principles. Languages like Pony, and the actor model more generally, were designed to prevent a whole class of concurrency bugs (same as Rust) - what's interesting is that, like this post shows, they also have unexpected problems with message causality. It makes me wonder if there's an even better abstraction out there which will solve this kind of concurrency bug, and what will arise after these are solved.
- zzzcpan 6y ago
  I'm pretty sure the exact problems the article describes can be solved with proper implementation of actor model, i.e. Erlang-style implementation, where actors can be killed, dying actors can cause messages to be send and messages can be received in specified order. Basically lack of proper richer actor primitives is what pushed them into the mess they are in.
  - fzzzy 6y ago
    I agree with this. Supervision is an essential part of the erlang model.
  - toast0 6y ago
    The problem described in the article could also exist if you followed the same messaging flow. Erlang and OTP may make it easier to have a better flow, but it's not a magic bullet. Plenty of ways to write race conditions and get unexpected message orderings (especially on a multinode system)
    - dnautics 6y ago
      Yeah this happens a lot, and in practice it's not a big deal. I noticed that when I redeploy, there's a nondeterministic flurry of errors in my system on the node that restarts. Finally I came to understand that this was race conditions. But it's honestly not a big deal. The system restarts anything in a funny state and moves on with its life. I feel like if you have something exquisitely race-condition sensitive that you aren't aware that it should be so, then you're not using OTP correctly.
- mcintyre1994 6y ago
  I haven't gotten to use it yet, but I think Pony would at least claim to prevent this problem. On https://tutorial.ponylang.io/types/at-a-glance.html https://tutorial.ponylang.io/types/at-a-glance.html it says: > All message passing is causal. (Not casual!) The word 'causal' is hyperlinked to https://courses.cs.vt.edu/~cs5204/fall00/causal.html https://courses.cs.vt.edu/~cs5204/fall00/causal.html which contains: > The purpose of causal ordering of messages is to insure that the same causal relationship for the "message send" events correspond with "message receive" events. (i.e. All the messages are processed in order that they were created.)
  - ivanbakel 6y ago
    Not at all - in fact, the problem described in the article is a typical pitfall of the causal ordering system. In a simplified version: A -1-> B B -2-> C A ---3------> C The human expectation is that 2 happens "before" 3, because that's how it looks. The reality is that 1 happens before 3, and 1 happens before 2, but 2 and 3 have no causal relation - and the runtime is free to rearrange them in any order. That's why the solution is essentially A -1-> B B -2-> C B -3-> C Because then 2 really happens before 3.
    - mratsim 6y ago
      Everyone dealing with actors, multithreading, distributed systems should read about Vector Clocks: - https://en.wikipedia.org/wiki/Vector_clock https://en.wikipedia.org/wiki/Vector_clock - Detecting Causal Relationships in Distributed Computations:In Search of the Holy Grail, Schwarz et al - http://www.vs.inf.ethz.ch/publ/papers/holygrail.pdf http://www.vs.inf.ethz.ch/publ/papers/holygrail.pdf
      - hugey010 6y ago
        Now that's some CS I wasn't even aware of! Although, I'm confused why those process clocking topics are considered specific to distributed systems and not computation in general.
    - 6y ago
- SAI_Peregrinus 6y ago
  > and what will arise after these are solved. Look at unintuitive situations in special relativity. The unituitiveness is essentially a concurrency bug in our mental model of how the universe works, as opposed to how it actually works. Almost all of the issues are due to mistaken ideas about what it means for two events to happen "at the same time" or in a given order. I suspect programming concurrency will continue to create bugs because humans ideas of time don't actually match up to reality. Obviously not usually due to relativity, but there are all sorts of complexities in the underlying systems we program for that intuition doesn't capture well.
- oconnor663 6y ago
  I think the fundamentally tricky part is that sometimes you want your concurrent code to have this sort of nondeterministic behavior. I think the Rayon FAQ does a good job of summarizing the problem: https://github.com/rayon-rs/rayon/blob/master/FAQ.md#but-wait-isnt-rust-supposed-to-free-me-from-this-kind-of-thinking https://github.com/rayon-rs/rayon/blob/master/FAQ.md#but-wai... > Consider for example when you are conducting a search in parallel, say to find the shortest route. To avoid fruitless search, you might want to keep a cell with the shortest route you've found thus far. This way, when you are searching down some path that's already longer than this shortest route, you can just stop and avoid wasted effort...Now in this case, we really WANT to see results from other threads interjected into our execution!
  - ivanbakel 6y ago
    Oh, certainly. You don't want programmers to go around insisting there's a global ordering to their message systems. But the problem I think could be solved is where programmers have a causal dependency, but they don't encode it in the program. The next generation of concurrent languages could have the killer correctness features for solving causality problems.
  - polyglotfacto 6y ago
    Yes, I would say the tricky part is accurately modelling what you want. Also, instead of actual nondeterministic behavior, I think that you rather want different things to be deterministic. The article is an example of "task parallelism", where you have different threads doing different things on different (local) data. Having those threads communicate via message-passing is a nice way to model workflows crossing thread boundaries, and in that setup you usually want some sort of deterministic behavior related to the ordering of operations(for a given workflow). On the other hand, I think the Rayon example is a good case of "data parallelism", where you have workers doing "the same thing" on "the same (shared-)data". In such a case, perhaps locks and shared-data are a better fit than message-passing, and indeed what you're after is not necessarily some sort of sequential ordering of worker operations. However you still probably want the ability to make other deterministic assertions about the behavior of the workers. I wrote another article highlighting some of these "different determinism" at https://medium.com/@polyglot_factotum/rust-concurrency-five-easy-pieces-871f1c62906a?source=friends_link&sk=fa043036d86e078fd7a50c7f109c1163 https://medium.com/@polyglot_factotum/rust-concurrency-five-...
- dnautics 6y ago
  >It makes me wonder if there's an even better abstraction out there which will solve this kind of concurrency bug, and what will arise after these are solved. You could go the erlang way, which is to give up. Unexpected concurrency bug? Crash, then restart from a sane state. It's highly effective. Your VM is carved up into failure domains that reduce the blast radius of such a crash to the minimum reasonable collection of processes. This is what frameworks like pony don't get. The reason why erlang actors (aka microservices) are so effective is that they declare, define, and decouple failure domains, and assign responsibility over these failure domains to specific bits of code and ultimately specific teams.
  - staticassertion 6y ago
    I agree with all of your post except for the premise - concurrency bugs won't necessarily lead to a crash, but often just a bad result.
    - dnautics 6y ago
      that's not the premise. Maybe I should reframe it this way: you should detect inconsistent results and use "crash" as a strategy to restore consistency. Also of importance is to log these events and work towards fixing the concurrency bug by addressing the root cause in the long run with application monitoring.
      - staticassertion 6y ago
        Ah, ok sure.
      - senderista 6y ago
        That’s one thing about Erlang that took me too long to grok: “let it crash” applies to bugs, not expected errors.
        dnautics 6y ago
        Haha also i guess you might also decide that correctness is unimportant. How often does this bug happen? Is it a once-a-week thing with no user-facing effect? Just let it ride until you're scaling hard. Your labor as a programmer is expensive, no need to chase down every possible bug.
jojobas 6y ago
Rust docs never claimed to prevent race conditions (which he doesn't call by name). https://doc.rust-lang.org/nomicon/races.html https://doc.rust-lang.org/nomicon/races.html
- pjmlp 6y ago
  True, but that is something that many miss a lot when discussing Rust virtues. Yes the type system is a great help when dealing with thread based concurrency/paralellism, but not so much for the scenarios where we are already using type safe managed languages in distributed computing across multiple processes, most likely not even written in the same language. Which by the way, given the recent security exploits, is much preferable to go back to, instead of relying on threads for parallelism.
  - mratsim 6y ago
    That's my main grip with Rust "Fearless Concurrency", fearing concurrency and dipping into it with your toes is a good thing. Claiming "Fearless Concurrency" but ignoring synchronization bugs, at a low-level in concurrent data structures or at a high-level in concurrent systems is misleading. People will be fearlessly introducing livelocks.
    - jstrong 6y ago
      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
mratsim 6y ago
And that's where model checking / formal verification is a tremendous help (or would be if it was easier to use). There are many properties of multithreaded/distributed systems that are emergent and that current static compilers don't address. In distributed systems it's becoming more common to use TLA+[1] to model the system and ensure that we don't have bugs at the design level (rather than just the system level). In particular for message-passing, I'm quite curious about the state of the research on Communicating Finite State Machines[1] and Petri Nets[2] and if there are actual products that could be integrated in regular languages and are not just of academic interest only. I expect that Ada/Sparks[1] has some support for this pattern though Ada multithreading story is not there yet (?). I'm quite excited about the future Z3 prover integration in Nim[5] and the potential to write concurrent programs free of design bugs[6] to address both ends of the concurrency bugs: - bugs in the low-level concurrent data structure via formal verification (which is something I used int he past to prove that my design was bug-free and that the deadlock I experienced was a condition variable bugs in Glibc[7] and I had to directly use futexes instead. - bugs in the high-level design, implemented as event-loop / finite state-machine reacting to events as received by channels Are there people working on model checkers or formal verification in Rust? Like the author, i think addressing memory bugs.the borrow checker is only a part of the "fearless concurrency" story and preventing design bugs would be extremely valuable. [1]: https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html [2]: https://en.wikipedia.org/wiki/Communicating_finite-state_machine https://en.wikipedia.org/wiki/Communicating_finite-state_mac... [3]: https://en.wikipedia.org/wiki/Petri_net https://en.wikipedia.org/wiki/Petri_net [4]: https://www.adacore.com/sparkpro https://www.adacore.com/sparkpro [5]: https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html [6]: https://github.com/nim-lang/RFCs/issues/222 https://github.com/nim-lang/RFCs/issues/222 [7]: https://github.com/mratsim/weave/issues/56 https://github.com/mratsim/weave/issues/56 And shameless plug, my talk at the NimConf on debugging multithreading programs (data structure and design): https://www.youtube.com/watch?v=NOAI2wH9Cf0&list=PLxLdEZg8DRwTIEzUpfaIcBqhsj09mLWHx&index=11 https://www.youtube.com/watch?v=NOAI2wH9Cf0&list=PLxLdEZg8DR... Slides: https://docs.google.com/presentation/d/e/2PACX-1vRq2wvd4q_mohbu2a_bYnhJwO487XY1s3cTYs52_p5_PmF0Uc3AcNnBg45Y9AtJ0WMnanip9UewRZd3/pub?start=false&loop=false&delayms=3000 https://docs.google.com/presentation/d/e/2PACX-1vRq2wvd4q_mo...
- 6y ago
Vanit 6y ago
Heh, reading this is reminiscent of the shortcomings of Typescript when external data is mistyped. Ps I love Typescript.
crazypython 6y ago
A good theoretical understanding will never replace a compiler that yells at you for making a mistake in that theoretical understanding. Learn teh theory instead.
devit 6y ago
Seems like the solution is to wait for the requests to complete, at least up to the point where a "slot" is reserved in the sequence order of a single actor.
Animats 6y ago
It should be noted that combining shared-state with event-loops is usually a recipe for subtle disaster. Go has that problem, too. The claim for Go was that concurrency would be done via message passing. But, in the examples in the original manual, and often in practice, what's being passed on the channel is some kind of reference to shared data. In a garbage collected language, this is OK as long as the sender only sends new objects and never touches them after sending. Still, it's easy to screw up, and the language does not help. In both Go and Python, there's not much thread-local data that the language will not let you export to another thread. That's a lack. Shared state that isn't obviously shared state is a recipe for trouble caused by later maintenance programming. This is one of Rust's strengths. Sharing has to be explicit. Shutdown is always hard in an event queue environment. Go makes it harder by making a write to a closed channel kill the whole program. So if a receiver decides it needs to shut down, it can't just close the receive end of the channel and let the sender hit a send error. Negotiations are required to get the sender shut down.
- linuxftw 6y ago
  > Go makes it harder by making a write to a closed channel kill the whole program. So if a receiver decides it needs to shut down, it can't just close the receive end of the channel and let the sender hit a send error. Negotiations are required to get the sender shut down. And thus Borg was born. Too hard to write processes that handle situations gracefully, so let's just let the process die and spin up a new one immediately. Literally was looking at a patch set that was proposed recently that involved several channels in Go and one of the codepaths was os.Exit(1) for lack of any meaningful mechanism to sanely clean everything up. Sadly, this was in library code, so would be totally unexpected by the caller and probably not desirable whatsoever.
  - Animats 6y ago
    And thus Borg was born. Yes. Basic Dijkstra producer-consumer one-way queues are simple and elegant. But the error cases are hell. OK, so if the consumer wants to make the producer stop, it sets an abort flag. That's a shared variable. (Does it need a lock? Does it need a lock or fencing on ARM, which has weaker memory concurrency guarantees than x86?) So, producer sees the abort flag set and closes its end of the channel, right? Maybe not. Maybe the channel is full, and the producer is blocked on a send. OK, so, when the consumer aborts, it has to enter a drain loop, doing receives and discarding the result until it gets an EOF/channel close. That will unblock the producer, and then the consumer can exit. But what if the producer doesn't have anything to send right now? Now the consumer is stuck waiting for the producer to send more data, and the consumer can't exit. Should the consumer close the producer's end of the channel after setting the abort flag? Now there's a race condition between checking the abort flag and sending. Add a critical section that covers both actions? Now the producer can be blocked while in a critical section. This creates a potential deadlock if the consumer wants to set the abort flag while the producer is inside the critical section. Now both ends are blocked and there's a deadlock. But it all looked so simple in theory!

187 points by polyglotfacto 6y ago

This is a cool technical exploration of some concurrency ideas: but event loops combined with Rust's borrow checker actually make for a re-invention of the actor model from first principles. Languages like Pony, and the actor model more generally, were designed to prevent a whole class of concurrency bugs (same as Rust) - what's interesting is that, like this post shows, they also have unexpected problems with message causality. It makes me wonder if there's an even better abstraction out there which will solve this kind of concurrency bug, and what will arise after these are solved.

zzzcpan 6y ago
I'm pretty sure the exact problems the article describes can be solved with proper implementation of actor model, i.e. Erlang-style implementation, where actors can be killed, dying actors can cause messages to be send and messages can be received in specified order. Basically lack of proper richer actor primitives is what pushed them into the mess they are in.
- fzzzy 6y ago
  I agree with this. Supervision is an essential part of the erlang model.
- toast0 6y ago
  The problem described in the article could also exist if you followed the same messaging flow. Erlang and OTP may make it easier to have a better flow, but it's not a magic bullet. Plenty of ways to write race conditions and get unexpected message orderings (especially on a multinode system)
  - dnautics 6y ago
    Yeah this happens a lot, and in practice it's not a big deal. I noticed that when I redeploy, there's a nondeterministic flurry of errors in my system on the node that restarts. Finally I came to understand that this was race conditions. But it's honestly not a big deal. The system restarts anything in a funny state and moves on with its life. I feel like if you have something exquisitely race-condition sensitive that you aren't aware that it should be so, then you're not using OTP correctly.
mcintyre1994 6y ago
I haven't gotten to use it yet, but I think Pony would at least claim to prevent this problem. On https://tutorial.ponylang.io/types/at-a-glance.html https://tutorial.ponylang.io/types/at-a-glance.html it says: > All message passing is causal. (Not casual!) The word 'causal' is hyperlinked to https://courses.cs.vt.edu/~cs5204/fall00/causal.html https://courses.cs.vt.edu/~cs5204/fall00/causal.html which contains: > The purpose of causal ordering of messages is to insure that the same causal relationship for the "message send" events correspond with "message receive" events. (i.e. All the messages are processed in order that they were created.)
- ivanbakel 6y ago
  Not at all - in fact, the problem described in the article is a typical pitfall of the causal ordering system. In a simplified version: A -1-> B B -2-> C A ---3------> C The human expectation is that 2 happens "before" 3, because that's how it looks. The reality is that 1 happens before 3, and 1 happens before 2, but 2 and 3 have no causal relation - and the runtime is free to rearrange them in any order. That's why the solution is essentially A -1-> B B -2-> C B -3-> C Because then 2 really happens before 3.
  - mratsim 6y ago
    Everyone dealing with actors, multithreading, distributed systems should read about Vector Clocks: - https://en.wikipedia.org/wiki/Vector_clock https://en.wikipedia.org/wiki/Vector_clock - Detecting Causal Relationships in Distributed Computations:In Search of the Holy Grail, Schwarz et al - http://www.vs.inf.ethz.ch/publ/papers/holygrail.pdf http://www.vs.inf.ethz.ch/publ/papers/holygrail.pdf
    - hugey010 6y ago
      Now that's some CS I wasn't even aware of! Although, I'm confused why those process clocking topics are considered specific to distributed systems and not computation in general.
  - 6y ago
SAI_Peregrinus 6y ago
> and what will arise after these are solved. Look at unintuitive situations in special relativity. The unituitiveness is essentially a concurrency bug in our mental model of how the universe works, as opposed to how it actually works. Almost all of the issues are due to mistaken ideas about what it means for two events to happen "at the same time" or in a given order. I suspect programming concurrency will continue to create bugs because humans ideas of time don't actually match up to reality. Obviously not usually due to relativity, but there are all sorts of complexities in the underlying systems we program for that intuition doesn't capture well.
oconnor663 6y ago
I think the fundamentally tricky part is that sometimes you want your concurrent code to have this sort of nondeterministic behavior. I think the Rayon FAQ does a good job of summarizing the problem: https://github.com/rayon-rs/rayon/blob/master/FAQ.md#but-wait-isnt-rust-supposed-to-free-me-from-this-kind-of-thinking https://github.com/rayon-rs/rayon/blob/master/FAQ.md#but-wai... > Consider for example when you are conducting a search in parallel, say to find the shortest route. To avoid fruitless search, you might want to keep a cell with the shortest route you've found thus far. This way, when you are searching down some path that's already longer than this shortest route, you can just stop and avoid wasted effort...Now in this case, we really WANT to see results from other threads interjected into our execution!
- ivanbakel 6y ago
  Oh, certainly. You don't want programmers to go around insisting there's a global ordering to their message systems. But the problem I think could be solved is where programmers have a causal dependency, but they don't encode it in the program. The next generation of concurrent languages could have the killer correctness features for solving causality problems.
- polyglotfacto 6y ago
  Yes, I would say the tricky part is accurately modelling what you want. Also, instead of actual nondeterministic behavior, I think that you rather want different things to be deterministic. The article is an example of "task parallelism", where you have different threads doing different things on different (local) data. Having those threads communicate via message-passing is a nice way to model workflows crossing thread boundaries, and in that setup you usually want some sort of deterministic behavior related to the ordering of operations(for a given workflow). On the other hand, I think the Rayon example is a good case of "data parallelism", where you have workers doing "the same thing" on "the same (shared-)data". In such a case, perhaps locks and shared-data are a better fit than message-passing, and indeed what you're after is not necessarily some sort of sequential ordering of worker operations. However you still probably want the ability to make other deterministic assertions about the behavior of the workers. I wrote another article highlighting some of these "different determinism" at https://medium.com/@polyglot_factotum/rust-concurrency-five-easy-pieces-871f1c62906a?source=friends_link&sk=fa043036d86e078fd7a50c7f109c1163 https://medium.com/@polyglot_factotum/rust-concurrency-five-...
dnautics 6y ago
>It makes me wonder if there's an even better abstraction out there which will solve this kind of concurrency bug, and what will arise after these are solved. You could go the erlang way, which is to give up. Unexpected concurrency bug? Crash, then restart from a sane state. It's highly effective. Your VM is carved up into failure domains that reduce the blast radius of such a crash to the minimum reasonable collection of processes. This is what frameworks like pony don't get. The reason why erlang actors (aka microservices) are so effective is that they declare, define, and decouple failure domains, and assign responsibility over these failure domains to specific bits of code and ultimately specific teams.
- staticassertion 6y ago
  I agree with all of your post except for the premise - concurrency bugs won't necessarily lead to a crash, but often just a bad result.
  - dnautics 6y ago
    that's not the premise. Maybe I should reframe it this way: you should detect inconsistent results and use "crash" as a strategy to restore consistency. Also of importance is to log these events and work towards fixing the concurrency bug by addressing the root cause in the long run with application monitoring.
    - staticassertion 6y ago
      Ah, ok sure.
    - senderista 6y ago
      That’s one thing about Erlang that took me too long to grok: “let it crash” applies to bugs, not expected errors.
      - dnautics 6y ago
        Haha also i guess you might also decide that correctness is unimportant. How often does this bug happen? Is it a once-a-week thing with no user-facing effect? Just let it ride until you're scaling hard. Your labor as a programmer is expensive, no need to chase down every possible bug.

jojobas 6y ago

Rust docs never claimed to prevent race conditions (which he doesn't call by name). https://doc.rust-lang.org/nomicon/races.html https://doc.rust-lang.org/nomicon/races.html

pjmlp 6y ago
True, but that is something that many miss a lot when discussing Rust virtues. Yes the type system is a great help when dealing with thread based concurrency/paralellism, but not so much for the scenarios where we are already using type safe managed languages in distributed computing across multiple processes, most likely not even written in the same language. Which by the way, given the recent security exploits, is much preferable to go back to, instead of relying on threads for parallelism.
- mratsim 6y ago
  That's my main grip with Rust "Fearless Concurrency", fearing concurrency and dipping into it with your toes is a good thing. Claiming "Fearless Concurrency" but ignoring synchronization bugs, at a low-level in concurrent data structures or at a high-level in concurrent systems is misleading. People will be fearlessly introducing livelocks.
  - jstrong 6y ago
    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

mratsim 6y ago

And that's where model checking / formal verification is a tremendous help (or would be if it was easier to use). There are many properties of multithreaded/distributed systems that are emergent and that current static compilers don't address. In distributed systems it's becoming more common to use TLA+[1] to model the system and ensure that we don't have bugs at the design level (rather than just the system level). In particular for message-passing, I'm quite curious about the state of the research on Communicating Finite State Machines[1] and Petri Nets[2] and if there are actual products that could be integrated in regular languages and are not just of academic interest only. I expect that Ada/Sparks[1] has some support for this pattern though Ada multithreading story is not there yet (?). I'm quite excited about the future Z3 prover integration in Nim[5] and the potential to write concurrent programs free of design bugs[6] to address both ends of the concurrency bugs: - bugs in the low-level concurrent data structure via formal verification (which is something I used int he past to prove that my design was bug-free and that the deadlock I experienced was a condition variable bugs in Glibc[7] and I had to directly use futexes instead. - bugs in the high-level design, implemented as event-loop / finite state-machine reacting to events as received by channels Are there people working on model checkers or formal verification in Rust? Like the author, i think addressing memory bugs.the borrow checker is only a part of the "fearless concurrency" story and preventing design bugs would be extremely valuable. [1]: https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html [2]: https://en.wikipedia.org/wiki/Communicating_finite-state_machine https://en.wikipedia.org/wiki/Communicating_finite-state_mac... [3]: https://en.wikipedia.org/wiki/Petri_net https://en.wikipedia.org/wiki/Petri_net [4]: https://www.adacore.com/sparkpro https://www.adacore.com/sparkpro [5]: https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html [6]: https://github.com/nim-lang/RFCs/issues/222 https://github.com/nim-lang/RFCs/issues/222 [7]: https://github.com/mratsim/weave/issues/56 https://github.com/mratsim/weave/issues/56 And shameless plug, my talk at the NimConf on debugging multithreading programs (data structure and design): https://www.youtube.com/watch?v=NOAI2wH9Cf0&list=PLxLdEZg8DRwTIEzUpfaIcBqhsj09mLWHx&index=11 https://www.youtube.com/watch?v=NOAI2wH9Cf0&list=PLxLdEZg8DR... Slides: https://docs.google.com/presentation/d/e/2PACX-1vRq2wvd4q_mohbu2a_bYnhJwO487XY1s3cTYs52_p5_PmF0Uc3AcNnBg45Y9AtJ0WMnanip9UewRZd3/pub?start=false&loop=false&delayms=3000 https://docs.google.com/presentation/d/e/2PACX-1vRq2wvd4q_mo...

6y ago

Vanit 6y ago

Heh, reading this is reminiscent of the shortcomings of Typescript when external data is mistyped. Ps I love Typescript.

crazypython 6y ago

A good theoretical understanding will never replace a compiler that yells at you for making a mistake in that theoretical understanding. Learn teh theory instead.

devit 6y ago

Seems like the solution is to wait for the requests to complete, at least up to the point where a "slot" is reserved in the sequence order of a single actor.

Animats 6y ago

It should be noted that combining shared-state with event-loops is usually a recipe for subtle disaster. Go has that problem, too. The claim for Go was that concurrency would be done via message passing. But, in the examples in the original manual, and often in practice, what's being passed on the channel is some kind of reference to shared data. In a garbage collected language, this is OK as long as the sender only sends new objects and never touches them after sending. Still, it's easy to screw up, and the language does not help. In both Go and Python, there's not much thread-local data that the language will not let you export to another thread. That's a lack. Shared state that isn't obviously shared state is a recipe for trouble caused by later maintenance programming. This is one of Rust's strengths. Sharing has to be explicit. Shutdown is always hard in an event queue environment. Go makes it harder by making a write to a closed channel kill the whole program. So if a receiver decides it needs to shut down, it can't just close the receive end of the channel and let the sender hit a send error. Negotiations are required to get the sender shut down.

linuxftw 6y ago
> Go makes it harder by making a write to a closed channel kill the whole program. So if a receiver decides it needs to shut down, it can't just close the receive end of the channel and let the sender hit a send error. Negotiations are required to get the sender shut down. And thus Borg was born. Too hard to write processes that handle situations gracefully, so let's just let the process die and spin up a new one immediately. Literally was looking at a patch set that was proposed recently that involved several channels in Go and one of the codepaths was os.Exit(1) for lack of any meaningful mechanism to sanely clean everything up. Sadly, this was in library code, so would be totally unexpected by the caller and probably not desirable whatsoever.
- Animats 6y ago
  And thus Borg was born. Yes. Basic Dijkstra producer-consumer one-way queues are simple and elegant. But the error cases are hell. OK, so if the consumer wants to make the producer stop, it sets an abort flag. That's a shared variable. (Does it need a lock? Does it need a lock or fencing on ARM, which has weaker memory concurrency guarantees than x86?) So, producer sees the abort flag set and closes its end of the channel, right? Maybe not. Maybe the channel is full, and the producer is blocked on a send. OK, so, when the consumer aborts, it has to enter a drain loop, doing receives and discarding the result until it gets an EOF/channel close. That will unblock the producer, and then the consumer can exit. But what if the producer doesn't have anything to send right now? Now the consumer is stuck waiting for the producer to send more data, and the consumer can't exit. Should the consumer close the producer's end of the channel after setting the abort flag? Now there's a race condition between checking the abort flag and sending. Add a critical section that covers both actions? Now the producer can be blocked while in a critical section. This creates a potential deadlock if the consumer wants to set the abort flag while the producer is inside the critical section. Now both ends are blocked and there's a deadlock. But it all looked so simple in theory!