my take on this if the designer of kotlin coroutines that make concurrent processing easier makes such a mistake what chances do we have?

😄

@natpryce That helps. I’ve also used model checker (hand-written) to verify all examples in this post. However, it makes sense to build some intuition on what kind of communication patterns are “safe” and which require attention to work property. That is what I’ve tried to show.

The tool I know is https://www.doc.ic.ac.uk/ltsa/

@natpryce I wrote a trivial version using exactly the same approach

Well done in writing about that topic without mentioning philosophers and forks 😄

@natpryce Can you do a favor? Can you try to specify this particular problem in TLA+ and try to verify the original (non-working) and fixed solution. I’d like to see how much TLA+ code it is going to take.

I don’t know enough TLA+ at the moment. I am an absolute beginner

Please keep us posted about any findings, it's super interesting 🙂

Thought I'd give it a try with Promela/Spin (note that I have no idea what I'm doing). Spin shows the original design has a deadlock and the fixed select version is deadlock free. https://gist.github.com/TimothyEarley/47e3c32c6966ee1ea6b2a87cd1da903f