5 ms·
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 t
by 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 agoAs 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 agoThe 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
- threatofrain 2y agoIMO some of the confusion is in conflating execution with the natural properties of a program. Concurrency is the property of a program or algorithm, and this property allows you to execute the program with partial or complete re-ordering (which is the peak of what some people call embarrassingly parallel). How you wish to execute on this property is up to you.
- rramadass 2y agoConcurrency should always be studied from higher-level logical program/algorithm execution properties with a focus on both shared-memory and message-passing architectures. Only after the above should one even look at lower-level hardware memory consistency model, cache coherence model, atomic instructions, memory barriers etc. For example, learning to use a logical shared-memory "Mutex" is far easier than the fact that it is internally implemented using atomic instructions, memory barriers etc. Some relevant details in a previous comment of mine - https://news.ycombinator.com/item?id=42422867 https://news.ycombinator.com/item?id=42422867 See also this book - https://news.ycombinator.com/item?id=42472334 https://news.ycombinator.com/item?id=42472334
- titzer 2y ago> Concurrency should always be studied I disagree. If we want people to understand, then we should teach computer systems bottom-up and thus understand the bottom-level behaviors before being surprised that our bad (i.e. wrong) abstractions are leaking later. If you want to train programmers to accomplish parallel programming tasks via plugging together nice abstractions, that's all well and good, but that's a completely different kind of instruction than trying to teach them how things work. If we only do the latter then we'll never have experts again.
- deleted 2y ago[deleted]
- rramadass 2y ago