The Mailbox Calculus – MC for short [DeLiguoroPadovani18] – is a mild extension of the asynchronoys π-calculus that can be used to model networks of processes that communicate through unordered and first-class mailboxes. MC processes selectively receive messages from mailboxes by means of their tag rather than by their order of arrival. The Mailbox Calculus subsumes the actor model [HewittEtAl73].

MC is equipped with a behavioral typing discipline ensuring that well-typed processes are mailbox conformant (no unexpected message is ever received) and deadlock free (in a terminated process all mailboxes are empty and there are no unperformed actions). The Mailbox Calculus Checker – MC² for short – is a tool to check whether an MC process is well typed.

Below is an example of MC² script defining a lock shared by two users. MC² determines that all the processes in the script are well typed, implying that no lock is ever released when it is free and that the system does not deadlock.

interface Lock { Acquire(User!), Release() }
interface User { Reply(Lock!) }

process Lock(self : Lock?) =
  case self ? *Acquire of
  { free ▸ done
  & Acquire(user) ▸
    { user!Reply(self)
    | case self ? Release·*Acquire of
      { Release ▸ Lock(self) } }
  & Release ▸ self?fail "free lock released" }

process User(self : User?, lock : Lock!) =
  { lock!Acquire(self)
  | case self ? Reply of
    { Reply(lock) ▸ lock!Release | self?free.done } }

process Main =
  new lock : Lock in
  new user₁ : User in
  new user₂ : User in
  { Lock(lock) | User(user₁, lock) | User(user₂, lock) }

You need both GCC and GHC to compile MC². Use of the Haskell Platform (full version) and Cabal is recommended.

MC² also needs an external solver to decide the validity of Presburger formulas. Currently, MC² can be configured to use either the LASH toolset (this is the default choice) or Z3. Configuring MC² for Z3 is simpler and can be done using only official Cabal packages, but requires nonetheless the installation of Z3 alongside MC². Using LASH requires some manual work (detailed below) but results in a self-contained executable. Also, LASH outperforms Z3 in processing the Presburger formulas generated by MC².

Depending on the solver you choose, follow the instructions in the corresponding section below before [compiling MC²][].

1. Download and unpack LASH in the same folder containing README.md, rename the top-level folder to lash and cd there:

   wget http://www.montefiore.ulg.ac.be/~boigelot/research/lash/releases/lash-v0.92.tar.gz
   tar xvfz lash-v0.92.tar.gz
   mv lash-v0.92 lash
   cd lash
   

2. On 64-bit architectures it is necessary to patch LASH:

   patch -p1 <../lash64.diff
   

3. Compile LASH, go back to the main folder and configure CobaltBlue:

   make
   cd ..
   cabal configure
   

1. Install Z3. The procedure varies depending on your OS and preferred package manager. On MacOS with homebrew, for example, this is achieved issuing the command

   brew install z3
   

2. Configure MC² specifying the Z3 flag:

   cabal configure -fZ3
   

1. Compile MC²:

   cabal build
   

2. Check whether the provided examples are type checked successfully:

   make check_examples
   

• The type system on which MC² is based has been described in the paper Mailbox Types for Unordered Interactions by Ugo de'Liguoro and Luca Padovani [DeLiguoroPadovani18].

The MC² distribution includes an Emacs mode that provides basic syntax highlighting for MC processes. Add the line

(load "<path to>/mc.el")

to your .emacs initialization file.

[HewittEtAl73]: Carl Hewitt, Peter Bishop and Richard Steiger: A Universal Modular ACTOR Formalism for Artificial Intelligence, Proceedings of IJCAI, 1973.

[DeLiguoroPadovani18]: Ugo de'Liguoro and Luca Padovani: Mailbox Types for Unordered Interactions, Proceedings of ECOOP, 2018.