https://kotlinlang.org logo
#feed
Title
# feed
n

nfrankel

01/16/2019, 9:45 AM
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 👍
n

natpryce

01/16/2019, 10:22 AM
😄
That’s why I like to use a process calculus and model checker when designing concurrent code
e

elizarov

01/16/2019, 11:50 AM
@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.
n

natpryce

01/16/2019, 11:51 AM
(Because I used it at university)
I’m currently trying to learn TLA+, which requires a different way of thinking about modelling
e

elizarov

01/16/2019, 11:52 AM
@natpryce I wrote a trivial version using exactly the same approach
n

natpryce

01/16/2019, 11:54 AM
Well done in writing about that topic without mentioning philosophers and forks 😄
😉 1
e

elizarov

01/16/2019, 11:57 AM
@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.
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
n

natpryce

01/16/2019, 12:24 PM
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
🙏 2
u

uhe

01/16/2019, 12:36 PM
Please keep us posted about any findings, it's super interesting 🙂
t

Timmy

01/16/2019, 7:33 PM
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
👍 3
7 Views