The Causality Project

Causality is a project aiming at providing a tool for describing causal semantics of concurrent programming languages. This is done by writing a monadic interpreter of the programming language. This interpreter can then be used to explore all the possible (causal) executions of a program, or explore certain executions. For instance, in the case of shared-memory programs, different executions correspond to different ways of resolving races (ie. conflicting accesses on the same resource: variable, locks, …). This is crucial to be able to see all the possible executions, even the one that hard to reproduce.

Causality libraries

The project is still in its infancy and there are several implementation of this core concept. But, all share the same conceptual construction. The goal is to explore the behaviour of the program sequentially, and deterministically: the monadic interpreter can be seen as a way to compile a concurrent programs to a sequential and deterministic program. Unlike usual technique of exploration, here the exploration of all executions are woven together: computational events do not reside within executions, but they all exist together in the same space, along with some information to know which events are compatible (ie. belong to the same execution). That creates naturally an event structure.

The implementations use different technique to realise this goal.

  1. The first version used a local state / continuation monad + mutable state. The mutable state, spread across the library made it hard to reason about what is going on and made it hard to be reentrant.

  2. The second version solved this purity issue by adding a global state to the monad so that the code is now pure (except for name generation). However, the semantics is highly not compositional and in particular when computing t ∥ u, actions of t and u are woven together in a complicated sequence that make it hard to see that the operation is even commutative.

  3. The third version tackled this issue by moving to a more compositional setting. We use now a somewhat optimised representation for closure operators on a specific domains, that allows us to define t ∥ u using a well-studied fixpoint formula.

Uses of the library

For now, the main use of the library, as a demo of the capabilities is a concurrent semantics for a subset of OCaml available here.