LShift Ltd.

Static analysis of Erlang communication

June 26th, 2006 matthias

I had a brief email exchange with the developers of Dialyzer, the static analyzer (some might call it a type checker) for Erlang programs. Currently Dialyzer only performs analysis on the functional fragment of Erlang and I was enquiring whether to extend that to handle communication. That would allow the detection of basic input/output mismatches, e.g. when a message is sent to a process that does not match any of the patterns it is willing to receive.

Going further, one might be able to employ the various techniques developed for process algebras to reason about the concurrent behaviour of Erlang programs and, for example, detect deadlocks and enforce information flow security properties. A good example of such a tool is TyPiCal. It would be amazing to have something like that for Erlang. After all, what makes Erlang interesting is not the functional programming aspect currently checked by Dialyzer, but its support for concurrency, distribution and fault-tolerance. It is incredibly difficult to correctly implement systems that involve the latter. If there is any area of programming in which we want the help of static analysis then this is it!

Anyway, it turns out that there are no immediate plans to extend Dialyzer in that direction. However, I was pointed at some related research that I had hitherto been unaware of: Karol Ostrovský’s PhD thesis, which in Part II describes the

• sound instantiation of Kobayashi’s generic type system for the pi-calculus to session types,

• extension of session types to multi-session types (which, afaict, handle sessions that involve asynchronous comms, and servers that handle multiple sessions without spawning),

• application of multi-session types to type check communication of Erlang processes.

Overall this looks like a promising attempt at constructing a process-algebra-based type system that is decidable and yet expressive enough to reason about non-trivial real-world protocols (IMAP4 is used as an example). The theory behind it seems to be quite involved, but that could just be due to the presentation format - a thesis rather than a paper. It will be interesting to see whether this research is carried any further and eventually materialises in tools for Erlang.

Entry Filed under: Technology, Programming, Tools, Erlang