Date
Tags elixir , math , cs , unfinished , projects
Draft Warning! You are reading a draft; this article is marked as unfinished.

Part 1: Intro

This is part one of a two part series where I'll describe an implementation of the ambient calculus in Elixir.

Cool diagram, right? I'll explain this is more detail soon.

image

Ambient Calculus

Briefly, the ambient calculus is a mathematical abstraction and a member of a more general family of "process calculi". Surprisingly simple yet Turing-complete phenomenon are a dime a dozen these days1, but even considering the vast zoo of automata and calculi familiar to computer scientsts, the Ambient Calculus has some properties that make it particularly interesting.

Here's the original paper if you've got time. Alternatively, the summary from wikipedia is inlined below:

The ambient calculus is a process calculus devised by Luca Cardelli and Andrew D. Gordon in 1998, and used to describe and theorise about concurrent systems that include mobility. Here mobility means both computation carried out on mobile devices (i.e. networks that have a dynamic topology), and mobile computation (i.e. executable code that is able to move around the network). The ambient calculus provides a unified framework for modeling both kinds of mobility. It is used to model interactions in such concurrent systems as the Internet.

Elixir

All this talk of concurrent systems and mobile code at the core of the Ambient Calculus immediately got me thinking about an implementation in Elixir, just for fun. It's an intriguing prospect because Elixir, running on top of the Erlang virtual machine, already implicitly supports hot-swapping code, distributed computing, and has lots of sophisticated primitives for expressing ideas about concurrency.

Concurrency primitives

In this section I'll cover very briefly various elixir concurrency concepts that will be most useful in Ambient Calculus implementation later.

  • Nodes are simply an Erlang (or in our case, Elixir) runtime capable of communicating with other such runtimes. From the Erlang point of view, there is some documentation here and from the Elixir point of view you can read about it here. With Elixir you can bootstrap a node like this iex --sname node_name --cookie group_name -S mix. To get a list of known nodes: Node.list(). To get the name of the current Node: Node.self(). Nodes don't automatically connect so you need Node.connect().. we'll talk later about auto-joining clusters later.

  • Processes are actors that run on nodes, basically concurrent functions with message-passing capabilities. In practice these are often not directly used, rather you use one of the things below.

  • Tasks are processes, often short-lived and created dynamically.

  • Agents, as state-wrappers, are a lot like objects except that they are concurrency-friendly by default. Under the hood, these are built out of proccesses, and so they have pids. The explicit pid-passing you need to do to reference certain Agents is similar to the usage of "self" and "this" features in other languages.

  • Supervisors are processes which supervise other processes. Supervisors may be nested.

  • GenServers are often summarized as being the "server-side of a client-server", but that doesn't by itself really seem to fully summarize their generality. Agents and Supervisors are both GenServers.

Project Scope

Using the elixir primitives above, the goal is to make a library/system wherein one can actually experiment with building things made of ambient calculus primitives. Such a system will necessarily have a working knowledge of AC reduction semantics, but it's worth noting that purely symbolic manipulation of the calculus itself is not really in scope here.

The point of the implementation discussed here is to use Ambients, not (symbolically) prove theorems about them, and it's not supposed to be extremely rigorous2 or pure.3

Definitions

To establish a working definition of an Ambient for the purposes of this implementation, let's nail down a few things about ambients that are important.

image

The image above, like the teaser image for this series, is taken from Cardelli's paper. Here you can see a graphical representation of an ambient named n, running programs P1..Pn, with nested ambients m1..mq. This will give you something fairly concrete to keep in mind while we get on with our working definitions for the project.

Properties

By definition, ambients have these properties:

  1. Ambients are kinds of mobile container; they have unique names.
  2. Ambients may hold named "programs"; we'll call that ambient's progspace
  3. Ambients may hold arbitrary key/values; we'll call that the ambient's namespace
  4. Ambients may hold other ambients; we'll call the container a parent and constituents children.

Operations

Ambients also have various core operations, most of which are more or less implied by the properties above. Operations described in the original paper are captured in the Ambient.Algebra code, namely that

  • Ambients may be copied. This operation derives a new ambient from an existing one with an identical namespace / progspace. The new ambient becomes a sibling with the old one, under the same parent ambient
  • Ambients can be entered and exited (operations which change parent/child relationships)
  • Ambients may be opened, i.e. their membrane is dissolved and what was once their namespace/progspace then belongs to the parent ambient.

Certain additional operations are implied for practical use and the fact that in Elixir, Ambients are implemented as GenServers. Those operations are captured in Ambient code here, namely that

  • Ambients may be started, stopped, terminated, etc
  • Programs running inside Ambients may be started, stopped, terminated, etc
  • Ambients may be healthy or unhealthy (depending on whether the processes beneath them are healthy or unhealthy)

Limitations

As discussed in the Project Scope section, the formalisms are treated as inspiration and not as specification. Where the tires meet the road, there are several things I've compromised on.

  • For simplicity's sake I'll be ignoring for now what Cardelli's papers call "capabilities". In the original model, capabilities are published as part of ambient names, and indeed this aspect of ambients is interesting and important for many applications. However, it complicates the model somewhat and it isn't critical for showcasing interesting features of Elixir. An extension that suggests itself though is an API that provides access to progspace, which could be added later.
  • Also regarding ambient names, this is implemented with Elixir atoms. There's support for a large, but limited, number of atoms in the Erlang runtime.. and really atoms should not be generated dynamically. Dealing directly with erlang pids could fix this, but then mapping names to pids requires treatment of registration. Anyway, the naive approach here is good enough for the purposes of the experiment.
  • Lots of undefined behaviour is possible, in many cases this behaviour is already present and acknowledged in the original formal models. For instance suppose you have a program running inside an Ambient and then the open operation is used on that ambient. In an 1 atomic step, the program finds itself inside the progspace of a new ambient with a potentially very different namespace. The calculus doesn't seem specific about such errors, and thanks to Elixir's approach to crash isolation.. maybe this model can gloss over it as well.
  1. For instance classics like Rule 110, Conway's life, but also several video games and card games
  2. For this project, Cardelli's paper is more in the way of inspiration than something that's treated as a specification.
  3. For instance, where message-passing is used it will most often be done directly in the obvious way with Elixir.. not reimplemented from scratch using ambient in/out/open/copy operations.
Part 1 of 2 in "Ambient Calculus in Elixir"   next ⇒
Next article(s)