A modern programming language that makes developers happier.

kotlinlang

<https://medium.com/@elizarov/deadlocks-in-non-hierarchical-csp-e5910d137cc>

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

a great post-mortem of sort in all cases :+1:

That’s why I like to use a process calculus and model checker when designing concurrent code

<@U0EACPP46> 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/>

I’m currently trying to learn TLA+, which requires a different way of thinking about modelling

<@U0EACPP46> I wrote a trivial version using exactly the same approach

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

<@U0EACPP46> 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.

You can take a look at how much effort it takes to specify it via my simple CFSM checker (take a look at .cfsm files): <https://github.com/elizarov/DeadlocksInCSP/tree/master/src/verifier>

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

But I can certainly use it as a way of learning

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

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>