# Write tracking for Nim

*2013-08-25*

While the exact details of Nim's new improved concurrency model are still somewhat unclear, the next steps are perfectly clear at least. Nim will get *write tracking* as part of Nim's general effect system.

Write tracking is an alternative to adding "immutable" or "const" to the type system. I don't like to add "const" to Nim's type system as that complicates the language tremendously and both C++'s and D's approaches to "const" leave a lot to be desired: For instance in C++ you cannot pass a `vector<string>` to a `vector<const string>`. In my opinion this is a major wart in the type system and I'd rather not have "const" then at all. Fortunately there is a more expressive and flexible alternative: Use the effect system instead of the type system:

type PNode = ref object next: PNode data: string proc len(n: PNode): natural {.writes: [].} = var it = n while it != nil: inc result it = it.next

The compiler can infer that `len` does not modify any memory (the modifications to the local `it` do not count); there is no need to clutter up the type system with a notion of immutability. As usual for Nim's effect system, you can also annotate the write effects yourself and then the compiler checks that you didn't screw up.

Lets look at one more example to see the beauty of an effects system. Here is some code written in a hypothetical version of Nim that added an `immutable` mode to its type system:

proc identity[M: immutable|mutable](x: M PNode): M PNode = x

As `identity` simply returns its passed argument, it should return the value in the same *mode* as `x`. This requires `identity` to become a generic even though exactly same code for immutable PNode and mutable PNode will be produced when instantiating `identity`. This means immutability leads to more generic functions and thus instantiations and the linker needs to merge all these definitions later. This is unfortunate. Furthermore for a systems programming language generics that do not expand to different machine code but only exist to make the type system happy are even more unfortunate.

Here is the trivial version with write tracking:

proc identity(x: PNode): PNode {.writes: [].} = x

Since we don't introduce (im)mutability modes there is no need for generics for this piece of code. Instead the fact that `identity` is harmless is encoded in the `writes: []` effect.

# Paths

The `writes` pragma takes a list of *paths*. A path is an lvalue expression like `obj.x[i].y`. The *root* of a path is the symbol that can be determined as the owner; `obj` in the example. The list of paths is also called the *write set*.

The paths that are interesting for the `writes` effect are these paths where the owner is either a parameter, a global variable or a thread local variable:

var gId = 0 proc genId(): natural {.writes: [gId].} = gId += 1 return gId

Here the effect systems shows its strength: Imagine there was a `genId2` that writes to some other global variable; then `genId` and `genId2` can be executed in parallel even though they are not free of side effects!

Adding immutability to the type system looks more and more inferior.

# Write set analysis

For the analysis to work we need to consider every path, including paths whose root is a local variable:

proc select(cond: bool, a, b: PNode): PNode {.writes: [].} = if cond: a else: b proc p(a, b: PNode) = var x = select(randomNumber==0, a, b) x.data = "abc"

The write set of `p` is `[a.data, b.data]` as it cannot be known which node `select` returns. Note that `select` itself doesn't modify anything and that the modifications `p` performs happen through the local variable `x` which aliases either the parameter `a` or `b`.

Another thing to consider is that the write set can be infinite:

proc p(list: PNode) = var it = list while it != nil: it.data = "abc" it = it.next

Here `p`'s write set is `[list.data, list.next.data, list.next.next.data, ...]`, in other words the whole list (of unknown length) is modified. We can introduce a new operator `@` to deal with this problem: `[email protected]` then means "some or every 'data' field reachable from 'list' is modified". However a simpler solution is to just approximate the write set with `[list[]]` which means "anything reachable from 'list' may be modified" (`x[]` means pointer dereference in Nim). The first version of the write tracking implementation will do just that.

# Tracking algorithm

The algorithm to determine write sets works in two passes over the AST. No fix point iterations are necessary. The complexity is O(n) where `n` is the size of the AST.

## Pass 1: write set computation for locals

The first pass computes the set of possible roots for every local variable `v`. `v` is either used in an assignment or passed to a function. The following rules are used to determine `writeset(v)`:

v = w # where 'w' is another local variable --> writeset(v).incl(w)

It's important to model the dependency of `v` from `w` explicitly. Note that we cannot simply merge `w`'s write set with `v`'s as `w`'s write set has not yet been computed completely. This means that we later need to *expand* the write sets and ensure that cycles are handled properly; for instance `writeset(v) == {w} and writeset(w) == {v, g}` implies `writeset(v) == writeset(w) == {g}` (where `v`, `w` are locals and `g` is a global).

A cycle in the write set dependencies can also imply an infinite write set:

proc p(list: PNode) = var it = list while it != nil: let next = it.next it.data = "abc" it = next --> writeset(it) = {list, next} writeset(next) = {it}

(A self cycle suffices for that.)

In general an infinite write set can only be produced by cycles or by recursion:

proc r(list: PNode) = if list == nil: return r(list.next) list.data = "abc"

We detect this case by treating parameters like local variables in the proc body and pretend the assignment `list = list.next` occurs in the body, this leads to `writeset(list) = {list}`. An alternative is to weaken the meaning of `writes: [list.data]` so that it means "any 'data' field reachable from 'list' might be modified".

The following rule deals with the fact that aliasing can be introduced via function application:

v = f(path(a), ..., path(b), ...) # unless 'f' is 'new' (see below) --> writeset(v).incl(a) iff 'v' may alias 'path(a)' writeset(v).incl(b) iff 'v' may alias 'path(b)'

Here `path(x)` denotes a path expression whose root is `x`. The rule really needs to deal with arbitrary nesting (including no function application at all):

v = f(...g(path(a)), ...) --> writeset(v).incl(a) iff 'v' may alias 'path(a)'

Interestingly `addr` is not special at all and might even be considered part of a path:

v = addr(path(x)) --> writeset(v).incl(x)

## Pass 2: write set computation for the routine

In the following a *relevant symbol* is either a global variable, a parameter or a thread local variable.

The AST is searched for assignments of the form `path(x) = ...`. Every `path` that affects a relevant symbol is added to the write set. This `add` operation needs to take a subsumption relation into account: `[x[], x.abc]` is the same as `[x[]]` (anything reachable from `x` may be modified; this already includes `x.abc`).

If `x` is a local, look up its write set `w` and do for every relevant symbol `s` in `w`: writesEffect.add(path(s)). If `x` is a relevant symbol, do: writesEffect.add(path(x)).

# Optimization: new pragma

The algorithm as described above has a major weakness as the following example highlights:

proc newNode(next: PNode): PNode {.writes: [].} = return PNode(next: next, data: "") proc p(a: PNode) = var x = newNode(a) x.data = "abc"

`p`'s write set would be computed to be `[a.data]`. Strictly speaking this is not *wrong* as the write set is a static approximation of what might be modified. However, it is unsatisfying. `newNode` always returns a *new* node, there is no way `p` can modify `a.data`!

The solution is to infer that `newNode` always allocates a new node:

proc newNode(next: PNode): PNode {.writes: [], new.} = return PNode(next: next, data: "") proc p(a: PNode) {.writes: [].} = # since 'newNode' returns a fresh object, we know 'x' doesn't alias 'a' # here: var x = newNode(a) x.data = "abc"

As usual, the annotation `new` can be explicitly added for the cases where it cannot be inferred (when the proc's body is not avaliable).

Since it is now obvious `p` has no side effects and doesn't modify the object pointed to by `a` the compiler could emit a warning or even an error; `p` only consists of dead code.