Compiling the pi-calculus into a Multithreaded Typed Assembly Language

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 pi-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 pi-calculus compiler in particular) from the hazardous task of direct lock manipulation, while allowing for the representation of pi-calculus channels. The compiler produces type correct MIL programs from type correct source code, generating low-contention cooperative multithreaded programs.