“Compiling the π-calculus into a multithreaded typed assembly language” is published

After one year the article I presented in PLACES '08 was published.

We extend a previous work on a multithreaded typed assembly language (MIL) targeted at shared memory multiprocessors, and describe the design of a type-preserving compiler from the π-calculus into MIL. The language enforces a policy on lock usage through a typing system that also ensures race-freedom for typable programs, while allowing for typing various important concurrency patterns. Our translation to MIL generates code that is then linked to a library supporting a generic unbounded buffer monitor, variant of Hoare's bounded buffer monitor, entirely written in MIL. Such a monitor shields client code (the π-calculus compiler in particular) from the hazardous task of direct lock manipulation, while allowing for the representation of π-calculus channels. The compiler produces type correct MIL programs from type correct source code, generating low-contention cooperative multithreaded programs.

Tiago Cogumbreiro, Francisco Martins, and Vasco T. Vasconcelos. Compiling the π-calculus into a multithreaded typed assembly language. ENTCS, 241:57–84, 2009.