6 ms·

How concurrency works: A visual guide

170 points by simplegeek 2y ago

kolektiv 2y ago
Is there a deadlocked thread that should have rendered the 'n'?
tansan 2y ago
Better title: > How concurrecy works: A text guide
- suprfsat 2y ago
  > concurrecy
tapland 2y ago
Is text written an in an image field more visual than other text?
- deleted 2y ago
  [deleted]
- jazzyjackson 2y ago
  I don't know, are arrows textual?
  - tapland 2y ago
    Yes <- No
neonsunset 2y ago
space state The really visual of explosion is demonstration nice!
7bit 2y ago
This is a text book, not a visual guide. Visual does not mean text in images, which this is.
cess11 2y ago
OK, great, formal verification gives some guarantees, that sounds nice and all. It's just that all the academic math nerds that are fluent in the checking tools are busy getting payed much more than average software developers, and I have a suspicion that they'll get less done per year in terms of features and refactorings of the code that immediately makes the monies flow. I find the BEAM/OTP process model relatively simple to use, and it moves some of the friction from logic bugs to a throughput problem.
- neonsunset 2y ago
  Such model has usability shortcomings for tightly interleaving concurrent code often encountered in high-performance applications or even in business code which does not want to maintain its worker pool or spool up a new BEAM process every time it needs to send two HTTP requests at the same time.
  - spinningslate 2y ago
    > even in business code which does not want to maintain its worker pool or spool up a new BEAM process every time it needs to send two HTTP requests at the same time. Just... no. First off, I'll bet a vanishingly small number of application developers on BEAM languages do anything to manage their own worker pools. The BEAM does it for them: it's one of its core strengths. You also imply that "spinning up a new BEAM process" has significant overhead, either computationally or cognitively. That, again, is false. Spinning up processes is intrinsic to Erlang/Elixir/Gleam and other BEAM languages. It's encouraged, and the BEAM has been refined over the years to make it fast and reliable. There are mature, robust facilities for doing so - as well as communicating among concurrent processes during their execution and/or retrieving results at termination. You've made clear before that you believe async/await is a superior concurrency model to the BEAM process-based approach. Or, more specifically, async/await as implemented in .Net [1]. Concurrent programming is still in its infancy, and it's not yet clear which model(s) will win out. Your posts describing .Net's async approach are helpful contributions to the discussion. Statements such as that quoted above are not. [1]: https://news.ycombinator.com/item?id=40427935 https://news.ycombinator.com/item?id=40427935 -- EDIT: fixed typo.
lincpa 2y ago
[dead]
charlieflowers 2y ago
The initial comments here surprise me. I’ve never seen such poor quality comments on such a good article on Hacker News. The article is top notch, highly recommend. It explains from first principles very clearly what the (a?) mechanism is behind model checking. So is the ability to compute the entire state space and prove that liveness and/or safety properties hold the single main basis of model checker’s effectiveness? Or are there other fundamental capabilities as well?
- spinningslate 2y ago
  Agree. The remaining comments boil down to: 1. "It's not visual, it's text". Yeah, but: how many "visual" representations have no text? And there _are_ visuals in there: the depictions of state space. They include text (hard to see how they'd be useful without) but aren't solely so. 2. "Meh, verification is for well paid academics, it's not for the real world". First off, I doubt those "academics" are earning more than median sw devs, never mind those in the SV bubble. More importantly: there are well-publicised examples of formal verification being used for real-world code, see e.g. [1]. It's certainly true that verification isn't widespread. It has various barriers, from use of formal maths theory and presentation to the compute load arising from combinatorial explosion of the state space. Even if you don't formally verify, understanding the state space size and non-deterministic path execution of concurrent code is fundamentally important. As Dijkstra said [2]: > our intellectual powers are rather geared to master static relations and that our powers to visualise processes evolving in time are relatively poorly developed. For that reason we should do (as wise programmers aware of our limitations) our utmost to shorten the conceptual gap between the static process and the dynamic program, to make the correspondence between the program (spread out in space) and the process (spread out in time) as trivial as possible. He was talking about sequential programming: specifically, motivating the use of structured programming. It's equally applicable to concurrent programming though. [1]: https://github.com/awslabs/aws-lc-verification https://github.com/awslabs/aws-lc-verification [2]: https://homepages.cwi.nl/~storm/teaching/reader/Dijkstra68.pdf https://homepages.cwi.nl/~storm/teaching/reader/Dijkstra68.p...
  - CyberDildonics 2y ago
cjfd 2y ago
These kinds of analyses are all nice and funny and so on but the issue here is that on real computers it does not quite work like this. One thing is that an optimizer may change the order in which statements are executed and then all guarantees go out of the window. Another is when writing to main memory the hardware may also reorder writes. So the whole process is filled with gotchas on every level. What one should remember is that if multiple threads do things with the same memory location where one of the 'things' that are done is writing, it is always wrong. The way to fix it then is to use the appropriate protection. E.g., use a mutex or use an atomic variable.
- vishnugupta 2y ago
  Heh this reminds me of a really good book, The Art of Multiprocessor Programming [1]. It has two parts, the first one goes quite a hit into the theory. And the second part begins with a real example where the theory doesn’t hold and it’s aptly titled “Welcome to The Real World”. [1] https://github.com/amilajack/reading/blob/master/Computer_Science/The%20Art%20of%20Multiprocessor%20Programming.pdf https://github.com/amilajack/reading/blob/master/Computer_Sc...
  - ignoramous 2y ago
    I find Andrew McFadden's Symmetric Multi-Processor Primer for Android (https://developer.android.com/training/articles/smp https://developer.android.com/training/articles/smp) a good warm-up to the book.
dragontamer 2y ago
Therein lies SIMDs advantage. The instruction pointer is all synchronized, providing you with fewer states to reason about. Then GPUs mess that up by letting us run blocks/thread groups independently, but now GPUs have highly efficient barrier instructions that line everyone back up. It turns out that SIMDs innate assurances of instruction synchronization at the SIMD lane level is why warp based coding / wavefront coding is so efficient though, as none of those barriers are necessary anymore.
- titzer 2y ago
  SIMD and thread-level parallelism solve completely different problems.
  - dragontamer 2y ago
    Ish. We use threads to solve all kinds of things, including 'More Compute'. SIMD is limited to 'More Compute' (unable to process I/O like sockets concurrently, or other such thread patterns). But as it turns out, more compute is a problem that many programmers are still interested in. Similarly, you can use Async patterns for the I/O problem (which seems to be more efficient anyway than threads). -------- So when we think about a 2024 style program, you'd have SIMD for compute limited problems (Neural Nets, Matricies, Raytracing). Then Async for Sockets, I/O, etc. etc. Which puts traditional threads in this weird jack of trades position: not as good as SIMD methods for raw compute. Not as good as Async for I/O. But threads do both. Fortunately, there seem to be problems with both a lot of I/O and a lot of compute involved simultaneously.
    - titzer 2y ago
      It's not just I/O, it's data pipelining. Threads can be used to do a lot of different kinds of compute in parallel. For example, one could pipeline a multi-step computation, like a compiler: make one thread for parsing, one for typechecking, one for optimizing, and one for codegening, and then have function move as work packages between threads. Or, one could have many threads doing each stage in serial for different functions in parallel. Threads give programmers the flexibility to do a wide variety of parallel processing (and sometimes even get it right). IMHO the jury is still out on whether async I/O is worth it, either in terms of performance or the potential complexity that applications might incur in trying to do it via callback hell. Many programmers find synchronous I/O to be a really, really intuitive programming model, and the lowest levels of the software stack (i.e. syscalls) are almost always synchronous.
rubee64 2y ago
*concurrency
titzer 2y ago
The problem with this article, though it presents model checking and state space exploration well, is that it doesn't present weak memory models[1], which are the reality on all multiprocessor/multicore systems these days. Thus is perpetuates misconceptions about concurrent programming. This is a poor example of model checking because it assumes sequential consistency and actually confuses people by reinforcing incorrect assumptions. [1] With weak memory hardware, it is effectively impossible to write correct programs without using at least one of atomic read-modify-write or barriers, because both compilers and hardware can reorder both reads and writes, to a maddening degree. (I previously posted this comment as a reply to a comment that got flagged.)
- lala_lala 2y ago
  As I read it, it felt more like an exploration from state space stand point (and not an example of model checking) which to me sounded quite reasonable. Unusual and intuitive I'd say.
  - fn-mote 2y ago
    The author does start talking about model checking in the third paragraph and go on using "SPIN", so there's a significant part that is interested in model checking, anyway. I can see where the parent is coming from. I think you can both be right - it can be valuable in any case.
- rramadass 2y ago
  > Thus is perpetuates misconceptions about concurrent programming ... it assumes sequential consistency and actually confuses people by reinforcing incorrect assumptions. That's not quite true. The article explicitly mentions problems with interleaving of instructions between two processes (aka threads) which is the fundamental problem of concurrency. If you consider only a single thread in isolation its program order is always maintained even though compiler optimizations and hardware OOO execution actually execute the instructions in data order. Consistency Model - https://en.wikipedia.org/wiki/Consistency_model https://en.wikipedia.org/wiki/Consistency_model
rramadass 2y ago
Coincidentally, i am currently going through Distributed Algorithms: An Intuitive Approach (second edition) by Wan Fokkink. It seems really good and is a catalog of classic algorithms for both Shared-Memory and Message-Passing architectures. It is a rather slim book with explanations and precise mathematical notation. Pseudo-code for a subset of these algorithms are given in the appendix. The 1st edition divides the algorithms under two broad sections viz; "Message Passing" (eg. chapter Mutual Exclusion) and "Shared Memory" (eg. chapter Mutual Exclusion II) while the 2nd edition removes these section headings and simply groups under functional categories (eg. both the above under one chapter Mutual Exclusion). Book website - https://mitpress.mit.edu/9780262037662/distributed-algorithms/ https://mitpress.mit.edu/9780262037662/distributed-algorithm...
- selimthegrim 2y ago
  Thank you for the book recommendations.
pphysch 2y ago
> If you’re implementing without formally verifying your solution through model checking, you only think you’re implementing it correctly. This is a comforting idea, but enumerating every possible state of a real-world (integrated/distributed) software system is a fool's task. Spend less time on formal verification (fancy word for perfectionism) and more time on risk analysis and cybernetics. Instead of praying that nothing ever goes wrong, plan for faults and design systems that integrate human and machine to respond rapidly and effectively. "Correctable" is a much more practical target than "always correct".
divan 2y ago
A bit more visual guide: Visualizing Concurrency in Go (2016) https://divan.dev/posts/go_concurrency_visualize/ https://divan.dev/posts/go_concurrency_visualize/
drewcoo 2y ago
This again? Didn't expect that.

170 points by simplegeek 2y ago

kolektiv 2y ago

Is there a deadlocked thread that should have rendered the 'n'?

tansan 2y ago

Better title: > How concurrecy works: A text guide

suprfsat 2y ago
> concurrecy

tapland 2y ago

Is text written an in an image field more visual than other text?

deleted 2y ago
[deleted]
jazzyjackson 2y ago
I don't know, are arrows textual?
- tapland 2y ago
  Yes <- No

neonsunset 2y ago

space state The really visual of explosion is demonstration nice!

7bit 2y ago

This is a text book, not a visual guide. Visual does not mean text in images, which this is.

cess11 2y ago

OK, great, formal verification gives some guarantees, that sounds nice and all. It's just that all the academic math nerds that are fluent in the checking tools are busy getting payed much more than average software developers, and I have a suspicion that they'll get less done per year in terms of features and refactorings of the code that immediately makes the monies flow. I find the BEAM/OTP process model relatively simple to use, and it moves some of the friction from logic bugs to a throughput problem.

neonsunset 2y ago
Such model has usability shortcomings for tightly interleaving concurrent code often encountered in high-performance applications or even in business code which does not want to maintain its worker pool or spool up a new BEAM process every time it needs to send two HTTP requests at the same time.
- spinningslate 2y ago
  > even in business code which does not want to maintain its worker pool or spool up a new BEAM process every time it needs to send two HTTP requests at the same time. Just... no. First off, I'll bet a vanishingly small number of application developers on BEAM languages do anything to manage their own worker pools. The BEAM does it for them: it's one of its core strengths. You also imply that "spinning up a new BEAM process" has significant overhead, either computationally or cognitively. That, again, is false. Spinning up processes is intrinsic to Erlang/Elixir/Gleam and other BEAM languages. It's encouraged, and the BEAM has been refined over the years to make it fast and reliable. There are mature, robust facilities for doing so - as well as communicating among concurrent processes during their execution and/or retrieving results at termination. You've made clear before that you believe async/await is a superior concurrency model to the BEAM process-based approach. Or, more specifically, async/await as implemented in .Net [1]. Concurrent programming is still in its infancy, and it's not yet clear which model(s) will win out. Your posts describing .Net's async approach are helpful contributions to the discussion. Statements such as that quoted above are not. [1]: https://news.ycombinator.com/item?id=40427935 https://news.ycombinator.com/item?id=40427935 -- EDIT: fixed typo.

lincpa 2y ago

[dead]

charlieflowers 2y ago

The initial comments here surprise me. I’ve never seen such poor quality comments on such a good article on Hacker News. The article is top notch, highly recommend. It explains from first principles very clearly what the (a?) mechanism is behind model checking. So is the ability to compute the entire state space and prove that liveness and/or safety properties hold the single main basis of model checker’s effectiveness? Or are there other fundamental capabilities as well?

spinningslate 2y ago
Agree. The remaining comments boil down to: 1. "It's not visual, it's text". Yeah, but: how many "visual" representations have no text? And there _are_ visuals in there: the depictions of state space. They include text (hard to see how they'd be useful without) but aren't solely so. 2. "Meh, verification is for well paid academics, it's not for the real world". First off, I doubt those "academics" are earning more than median sw devs, never mind those in the SV bubble. More importantly: there are well-publicised examples of formal verification being used for real-world code, see e.g. [1]. It's certainly true that verification isn't widespread. It has various barriers, from use of formal maths theory and presentation to the compute load arising from combinatorial explosion of the state space. Even if you don't formally verify, understanding the state space size and non-deterministic path execution of concurrent code is fundamentally important. As Dijkstra said [2]: > our intellectual powers are rather geared to master static relations and that our powers to visualise processes evolving in time are relatively poorly developed. For that reason we should do (as wise programmers aware of our limitations) our utmost to shorten the conceptual gap between the static process and the dynamic program, to make the correspondence between the program (spread out in space) and the process (spread out in time) as trivial as possible. He was talking about sequential programming: specifically, motivating the use of structured programming. It's equally applicable to concurrent programming though. [1]: https://github.com/awslabs/aws-lc-verification https://github.com/awslabs/aws-lc-verification [2]: https://homepages.cwi.nl/~storm/teaching/reader/Dijkstra68.pdf https://homepages.cwi.nl/~storm/teaching/reader/Dijkstra68.p...
- CyberDildonics 2y ago

cjfd 2y ago

These kinds of analyses are all nice and funny and so on but the issue here is that on real computers it does not quite work like this. One thing is that an optimizer may change the order in which statements are executed and then all guarantees go out of the window. Another is when writing to main memory the hardware may also reorder writes. So the whole process is filled with gotchas on every level. What one should remember is that if multiple threads do things with the same memory location where one of the 'things' that are done is writing, it is always wrong. The way to fix it then is to use the appropriate protection. E.g., use a mutex or use an atomic variable.

vishnugupta 2y ago
Heh this reminds me of a really good book, The Art of Multiprocessor Programming [1]. It has two parts, the first one goes quite a hit into the theory. And the second part begins with a real example where the theory doesn’t hold and it’s aptly titled “Welcome to The Real World”. [1] https://github.com/amilajack/reading/blob/master/Computer_Science/The%20Art%20of%20Multiprocessor%20Programming.pdf https://github.com/amilajack/reading/blob/master/Computer_Sc...
- ignoramous 2y ago
  I find Andrew McFadden's Symmetric Multi-Processor Primer for Android (https://developer.android.com/training/articles/smp https://developer.android.com/training/articles/smp) a good warm-up to the book.

dragontamer 2y ago

Therein lies SIMDs advantage. The instruction pointer is all synchronized, providing you with fewer states to reason about. Then GPUs mess that up by letting us run blocks/thread groups independently, but now GPUs have highly efficient barrier instructions that line everyone back up. It turns out that SIMDs innate assurances of instruction synchronization at the SIMD lane level is why warp based coding / wavefront coding is so efficient though, as none of those barriers are necessary anymore.

titzer 2y ago
SIMD and thread-level parallelism solve completely different problems.
- dragontamer 2y ago
  Ish. We use threads to solve all kinds of things, including 'More Compute'. SIMD is limited to 'More Compute' (unable to process I/O like sockets concurrently, or other such thread patterns). But as it turns out, more compute is a problem that many programmers are still interested in. Similarly, you can use Async patterns for the I/O problem (which seems to be more efficient anyway than threads). -------- So when we think about a 2024 style program, you'd have SIMD for compute limited problems (Neural Nets, Matricies, Raytracing). Then Async for Sockets, I/O, etc. etc. Which puts traditional threads in this weird jack of trades position: not as good as SIMD methods for raw compute. Not as good as Async for I/O. But threads do both. Fortunately, there seem to be problems with both a lot of I/O and a lot of compute involved simultaneously.
  - titzer 2y ago
    It's not just I/O, it's data pipelining. Threads can be used to do a lot of different kinds of compute in parallel. For example, one could pipeline a multi-step computation, like a compiler: make one thread for parsing, one for typechecking, one for optimizing, and one for codegening, and then have function move as work packages between threads. Or, one could have many threads doing each stage in serial for different functions in parallel. Threads give programmers the flexibility to do a wide variety of parallel processing (and sometimes even get it right). IMHO the jury is still out on whether async I/O is worth it, either in terms of performance or the potential complexity that applications might incur in trying to do it via callback hell. Many programmers find synchronous I/O to be a really, really intuitive programming model, and the lowest levels of the software stack (i.e. syscalls) are almost always synchronous.

rubee64 2y ago

*concurrency

titzer 2y ago

The problem with this article, though it presents model checking and state space exploration well, is that it doesn't present weak memory models[1], which are the reality on all multiprocessor/multicore systems these days. Thus is perpetuates misconceptions about concurrent programming. This is a poor example of model checking because it assumes sequential consistency and actually confuses people by reinforcing incorrect assumptions. [1] With weak memory hardware, it is effectively impossible to write correct programs without using at least one of atomic read-modify-write or barriers, because both compilers and hardware can reorder both reads and writes, to a maddening degree. (I previously posted this comment as a reply to a comment that got flagged.)

lala_lala 2y ago
As I read it, it felt more like an exploration from state space stand point (and not an example of model checking) which to me sounded quite reasonable. Unusual and intuitive I'd say.
- fn-mote 2y ago
  The author does start talking about model checking in the third paragraph and go on using "SPIN", so there's a significant part that is interested in model checking, anyway. I can see where the parent is coming from. I think you can both be right - it can be valuable in any case.
rramadass 2y ago
> Thus is perpetuates misconceptions about concurrent programming ... it assumes sequential consistency and actually confuses people by reinforcing incorrect assumptions. That's not quite true. The article explicitly mentions problems with interleaving of instructions between two processes (aka threads) which is the fundamental problem of concurrency. If you consider only a single thread in isolation its program order is always maintained even though compiler optimizations and hardware OOO execution actually execute the instructions in data order. Consistency Model - https://en.wikipedia.org/wiki/Consistency_model https://en.wikipedia.org/wiki/Consistency_model

rramadass 2y ago

Coincidentally, i am currently going through Distributed Algorithms: An Intuitive Approach (second edition) by Wan Fokkink. It seems really good and is a catalog of classic algorithms for both Shared-Memory and Message-Passing architectures. It is a rather slim book with explanations and precise mathematical notation. Pseudo-code for a subset of these algorithms are given in the appendix. The 1st edition divides the algorithms under two broad sections viz; "Message Passing" (eg. chapter Mutual Exclusion) and "Shared Memory" (eg. chapter Mutual Exclusion II) while the 2nd edition removes these section headings and simply groups under functional categories (eg. both the above under one chapter Mutual Exclusion). Book website - https://mitpress.mit.edu/9780262037662/distributed-algorithms/ https://mitpress.mit.edu/9780262037662/distributed-algorithm...

selimthegrim 2y ago
Thank you for the book recommendations.

pphysch 2y ago

> If you’re implementing without formally verifying your solution through model checking, you only think you’re implementing it correctly. This is a comforting idea, but enumerating every possible state of a real-world (integrated/distributed) software system is a fool's task. Spend less time on formal verification (fancy word for perfectionism) and more time on risk analysis and cybernetics. Instead of praying that nothing ever goes wrong, plan for faults and design systems that integrate human and machine to respond rapidly and effectively. "Correctable" is a much more practical target than "always correct".

divan 2y ago

A bit more visual guide: Visualizing Concurrency in Go (2016) https://divan.dev/posts/go_concurrency_visualize/ https://divan.dev/posts/go_concurrency_visualize/

drewcoo 2y ago

This again? Didn't expect that.