CobaltBlue — Behavioral Type Checking for Concurrent Objects


Cobalt is a behaviorally typed, mildly sugared version of the Objective Join Calculus (1) that can be used to write simple programs consisting of (concurrent) object definitions along with the corresponding object protocols. CobaltBlue is a tool that performs protocol and deadlock analysis of Cobalt programs: it checks that each object in the program is consistent with — and is used according to — its protocol; it checks that, if the program halts, all messages with relevant arguments have been consumed. The tool implements (an extension of) the type system described in (2) and (3).

Below is a summary of Cobalt’s main features and a simple example of (ill-typed) Cobalt program modeling a lock. image

For questions, suggestions and bug reports please contact Luca Padovani.


Installation Instructions

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

CobaltBlue also needs an external solver to decide the validity of Presburger formulas. Currently, CobaltBlue can be configured to use either the LASH toolset (this is the default choice) or Z3. Configuring CobaltBlue for Z3 is simpler and can be done using only official Cabal packages, but requires nonetheless the installation of Z3 alongside CobalBlue. 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 CobaltBlue.

Depending on the solver you choose, follow the instructions in the corresponding section below before compiling CobaltBlue.

Configuring CobaltBlue for LASH

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

    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:

    cd ..
    cabal configure

Configuring CobaltBlue for Z3

  1. Z3 can be installed in a number of ways 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 CobaltBlue specifying the Z3 flag:

    cabal configure -fZ3

Compiling CobaltBlue

  1. Compile CobaltBlue:

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

    make check_examples


Emacs mode

The CobaltBlue distribution includes an Emacs mode that provides basic syntax highlighting for Cobalt programs. Add the line

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

to your .emacs initialization file.

$LastChangedDate: 2017–11–06 20:41:47 +0100 (Mon, 06 Nov 2017) $

  1. Cédric Fournet, Cosimo Laneve, Luc Maranget and Didier Rémy: Inheritance in the Join Calculus, Journal of Logic and Algebraic Programming, 2003.  ↩

  2. Silvia Crafa and Luca Padovani: The Chemical Approach to Typestate–Oriented Programming, Proceedings of OOPSLA, 2015.  ↩

  3. Silvia Crafa and Luca Padovani: The Chemical Approach to Typestate–Oriented Programming, ACM Transactions on Programming Languages and Systems, 2017.  ↩

  4. Luca Padovani: Deadlock–Free Typestate–Oriented Programming, Technical Report HAL 01628801, 2017.  ↩