I think there are two main difficulties
- Having a good tool to extract an accurate communication model from
source code is actually very difficult because of the flexibility of Go,
like calling an interface function without knowing which implementation to
use - this could change the underlying communication (and hence model) of
the program, so we have to approximate
- Modelling and the cost of checking - even if we have a 100% accurate
model of the communication (e.g. a N-buffer channel, where we know exactly
what will happen if buffer is 1-full, 2-full, ... N-full), and that
theoretically it's possible to check it, it just could be too impractical
to check (e.g. check all execution paths) that it's not cost-effective for
a static check, hence we need better model that can check more.
So despite it looks very attractive to find deadlocks at static time, it's
a very difficult problem both theoretically and practically. Luckily there
are enough deadlock detection research work on process calculi, so the more
we can reduce the gap between theory and practice, the closer we are to a
useful deadlock detector tool. (i.e. more research needed)
p.s. I'm the author of the tool.
On Wednesday, 14 September 2016 13:17:19 UTC+1, Haddock wrote:
>> One WIP http://www.doc.ic.ac.uk/~cn06/pub/2016/dingo/
> Man, this is cool! Thanks for the link. They say their deadlock detector
> only works for unbounded buffers. Nevertheless, this closes a very
> important gap. If I only think of the years I spent reproducing deadlocks
> and race conditions ... Reproducing them is hard and fixing them in the
> usual non-CSP setting is sometimes even harder (CSP helps a great deal to
> make this easier).
You received this message because you are subscribed to the Google Groups
To unsubscribe from this group and stop receiving emails from it, send an email
For more options, visit https://groups.google.com/d/optout.