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 "golang-nuts" group. To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
