technology from back to front

Static analysis of Erlang communication

I had a brief email exchange with the developers of
[Dialyzer](http://www.it.uu.se/research/group/hipe/dialyzer/), the
static analyzer (some might call it a type checker) for
[Erlang](http://www.erlang.org/) 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](http://www.kb.ecei.tohoku.ac.jp/~koba/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](http://www.cs.chalmers.se/~karol/Papers/PhD.pdf), 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.

by
matthias
on
26/06/06
 
 


eight − = 4

2000-14 LShift Ltd, 1st Floor, Hoxton Point, 6 Rufus Street, London, N1 6PE, UK+44 (0)20 7729 7060   Contact us