During my PhD I worked on analysis of concurrent programs, using the π-calculus as a model of concurrent computation. The π-calculus is like the λ-calculus of concurrency: a minimalistic calculus to represent concurrent computation (as opposed to sequential) that is universal (can compute any computable function). Although there is great beauty in its theory, people often find its syntax cryptic and is semantics too abstract. Another common complaint is that it seems too removed from actual programming languages, and is only a toy for theorists.

To the contrary, I believe the π-calculus has a lot to offer to the wider CS community, if only it was made more accessible. So, to be able to convey the core concepts and ideas to fellow researchers and students, I developed a simple visual simulator for the π-calculus, which I call Stargazer.

Disclaimer: the current version grew out of an initial prototype that I enhanced at each presentation. It is now a bit of a Frankenstein monster inside, and could be made much more efficient. I planned a rewrite before releasing it, but it is clear now that this will never happen. So I decided to fight my perfectionist’s paralysis and just publish what I have got.

Try it at stargazer.emanueledosualdo.com

You can try the simulator online, it runs entirely inside the browser. For best performance, use it with Chrome (although Firefox is also supported).

Try Stargazer

I will publish posts on the π-calculus with examples and explanations exploiting the simulator. For now let me briefly explain the basic concepts.

In the graph above (which is an embedded instance of the simulator) you see the initial configuration of an example π-calculus program. In the π-calculus there is a notion of “thread” (called sequential processes) and synchronisation is done by message passing over channels. In the graph, each active thread is represented by a rectangle and each channel by a dot. Threads are connected to every channel they currently know. The colours of the threads reflect their current local state. This graph is commonly called the communication topology of the system. If you press “play”, the simulator picks at random enabled transitions and fires them. The transitions are specified by the program, which in the above example is the following:

new s. (S[s] | E[s])

S[s] := s(x).νd.( A[x,d] | S[s] )
E[s] := τ.new m.(C[s, m] | E[s]) + τ.νs'.(S[s'] | E[s'] | E[s])
C[s, m] := τ.( Q[s,m] | C1[s,m])
C1[s, m] := m(x).C[s, m]
A[x,d] := x<d>
Q[s,m] := s<m>

If you press “open” you will be able to play with the example in the full simulator. Open the “program” sidebar in Stargazer by pressing the button to see the program’s code which can be freely edited.

Help, issues and feedback

For help on how to use it click on the button in Stargazer, where you will find a brief summary of the syntax. The project is hosted on GitHub. I am planning to put some basic information in the wiki. If you find bugs, have feature requests, ideas or comments you are most welcome to leave a message in the issues page.