Writing a pi-calculus compiler in F# (Part VIII)

Just joining us? We’re writing a compiler for the π-calculus in F#—Part I explains. Continuing from last time? Need a refresher? We finished the compiler and runtime library. Now it’s time to play!

Let’s see if this all works by creating a new C# project. Reference Pirt.dll and echo.dll:

using System.Threading;

class EchoClient

{

static void Main()

{

// create channel 'e'

Channel e = new Channel("e");

// start the echo program

new Thread(new ThreadStart(new Main(e).Run)).Start();

// call echo

Channel k = new Channel("k");

e.Send(k);

Channel f = k.Receive();

f.Send(new Channel("hello!"));

Channel r = new Channel("r");

f.Send(r);

System.Console.WriteLine(r.Receive().Name);

}

Let’s see if it runs:

$ csc /t:exe echoclient.cs /r:pirt.dll /r:echo.dll

Microsoft (R) Visual C# 2005 Compiler version 8.00.50727.42

for Microsoft (R) Windows (R) 2005 Framework version 2.0.50727

$ echoclient

hello!

$ _

Fairly tedious from C#, but it works!

Evaluating the Compiler

Some parts of the compiler are arguably fragile because they rely on other parts behaving just so. Here are some examples:

The code generation for Repeat relies on Par reusing the existing thread for its second process. If Par changed to start two new threads, or reuse the existing thread for the first process instead of the second, Repeat would emit a branch instruction between methods which isn’t allowed in the CLR.
How free variables are passed to processes is defined between Par and some code in gen_closure; the mapping of free variables to fields via constructor parameters is never made explicit. Both of these parts just know what to expect.
gen_closures tears down the process × type ref mapping even as it is being created by gen_proc, which makes gen_closures rely on the fact that gen_proc never needs to look up type refs for a process it has already generated a closure for.
gen_closure knows that gen_proc never uses more than two slots on the evaluation stack, and it uses a constant for the stack depth. The way gen_closure determines the number of local variables, from the extant bindings, is similar.

Although these all seem like egregious shortcomings, I believe there’s a point where making the coupling explicit (usually by extending the context and passing around data to connect two disconnected phases) is becomes more burdensome than remembering certain conventions exist between the two disparate pieces of code.

Variants of the π-Calculus

Messaging and channels make the π-calculus good for modeling distributed systems, but it is rather poor for implementing them! That’s because, in a distributed π system, two processes on different sides of the world can both say receive on channel x, and expect the contention to be resolved. Doing so at such a great distance is brittle or expensive. The join-calculus is similar process calculus with messages and channels, but receiving on a channel is limited to a particular scope, and in a distributed setting it follows intuition that messages must be sent to a well-defined location for the contention can be resolved locally. My research language and compiler, GPSL, is based on the join calculus. I recommend you read Cédric Fournet’s join calculus tutorial.

Another popular application of π-calculus is in modeling cryptographic protocols. The spi calculus uses type systems to ensure the secrecy of channel names.