Shared NAND mutable

[apt1002]

Most VMs will have some memory locations that are known to be unshared or immutable. Examples:

• Code, in VMs that forbid self-modifying code, is immutable.
• Stack locations, if not accessible using normal memory access VM instructions, are unshared.
• Pure functional data structures are immutable.
• Newly allocated data structures are unshared.

We're calling this property "shared NAND mutable", or "SNM", until we can think of a better name.

Motivation

It would be useful for Mijit to know about SNM memory locations, because it helps to prove that load and store instructions can be reordered, and thereby to find additional optimization opportunities. For example, consider the following code (in an imaginary high-level language):

a = 0;
b = 1;
use(a);

In the high-level language it is obvious that when a is used its value will be 0. That knowledge is likely to be useful for optimising the code. However in the VM code emitted by the compiler it might be less obvious what is going on. The VM code might be something like this:

store 0 at a
store 1 at b
load r0 from a
use r0

Now, in order to find the optimisations, it is first necessary to reorder the load and store instructions as follows:

store 0 at a
load r0 from a
store 1 at b
use r0

This requires proving that a and b are different memory locations. Many techniques are available for the proof, most of which work in simple cases but otherwise usually fail or are impractical. SNM complements those other techniques, succeeding in many interesting cases where they fail.

In this example, we only need to know that one of a and b is SNM to apply the technique; the other can be any memory location. Since we are storing to an SNM location, it must be mutable, and therefore unshared, and since the two locations exist at the same time they must be different.

Other similar cases include:

load a
store b
load a // Would like to replace this with a move.

store a // Would like to delete this.
load b
store a

Hopefully it is clear that these tricks are strategically important; missing these opportunities would prevent other optimizations.

Proposal

Mijit load and store instructions are annotated with hints. Add to those hints a flag indicating that the memory location is SNM.

The hint is not checked by Mijit; if it is used incorrectly then Mijit will optimize the code in ways that are unsound, resulting in undefined behaviour. Undefined behaviour is ugly, but we accept it because the alternative appears to be worse.

The SNM hint requires a formal definition. It would be nice to provide a valgrind-like tool that runs a program slowly and checks at run time that the hints are correctly used. However, this appears to be quite difficult.

The formal definition requires the following concepts:

• Every SNM memory location must be part of a struct in a unique way.
• Every access to an SNM location must be marked as such, and no others.
• There must be a way of counting the number of pointers to a struct. To be excluded from the count, dead pointers must be explicitly destroyed, e.g. by overwriting them with null pointers.
• It is illegal to store to an SNM location while there is more than one pointer to its struct.

[apt1002]

Implementation note: In this design, the moment when an SNM pointer dies is semantically important. For example, consider the following code, in which all memory accesses are to SNM locations:

load from r0
store r0 at a
// drop r0
load r1 from a
store at r1

We can move the load and store at a as early as we like, revealing a possible optimisation (which, for clarity, I will not do):

store r0 at a
load r1 from a
load from r0
// drop r0
store at r1

However, r0 is dead when we store at r1, so we cannot exchange the load from r0 with the store at r1. There is a dependency chain "load -> drop -> store".

[apt1002]

Two years on, I have clearer ideas on this subject. Relying on instruction order to represent dependencies between loads and stores is a bad idea because (a) it doesn't do that very well, and (b) it constrains the optimizer too much. Instead, I'd like to lean into the "shared NAND mutable" (hereafter "shnam") idea.

Overview

Mijit's entire memory model should be shnam. There is no need to mark particular memory accesses as shnam because they all are. The memory model should be unsafe; the Mijit code includes hints about the way memory access instructions interact, and if the hints are not true the behaviour is undefined.

I'm satisfied that many common memory models can be encoded into such a model, including separate memories for code, stack and heap, virtual registers, immutable shared memory, heap allocated memory, stack allocated memory, memory protected by a lock, memory belonging to an actor, and so on. In particular, dumb flat memory can be encoded if necessary. And these various models compose nicely; for example you can have segregated code and stack within an otherwise flat memory model.

Concepts

The goal is to allow the optimizer to assume that when it sees a store to x.f followed by a load from x.f the value that is loaded is the same value that was stored. In particular, it must be allowed to ignore an intervening store to y.f, on the grounds that x and y are not allowed to point to the same object.

This requires a disciplined way of using pointers. Each pointer notionally has "permissions" allowing it to be used to access certain areas of memory. Specifically, there is set of locations it can load from, and a set that it can store to. The latter is a subset of the former; there are no write-only locations. The shnam rule is that if one pointer can store to a location then no other pointer can load from the same location.

There are six main ways that one pointer can be used to compute another:

• Compute the address of an element of an array.
• Compute the address of a field of a struct.
• Use one pointer to load another from memory.
• Push an object onto a stack, and take its address.
• Allocate an object from a heap, and take its address.
• Send a message from one agent (thread?) to another.

In each of these cases, the permissions of the new pointer are carved out of those of the old pointer. When the new pointer is no longer needed, its permissions are usually returned to the old pointer. Thus, the permissions of a pointer change over time, and Mijit needs to be aware of these changes.

Mijit does not otherwise need to be aware of the permissions attached to each pointer. If challenged, the author of the Mijit code should be able to say what the permissions of every pointer are, and prove that the shnam rule is followed. However, Mijit won't ever make such a challenge. It will blindly trust the author. If that trust is misplaced, the behaviour is undefined.

The "send" primitive

We add one primitive send to the Mijit language to inform Mijit of changes to the pointer permissions. It is syntactically an arithmetic instruction: it takes two pointers x and y and returns a fresh pointer that is numerically equal to x but which has additional permissions taken from y. In native code send is a no-op; it's only purpose is to constrain the optimizer.

A typical use of send is as follows:

• Suppose p points to an array.
• Based on p and an array index, compute a pointer q that points to an array element.
  Since there is a dataflow dependency from p to q there is no need to use "send" yet; it is obvious that the permissions of q have been carved out of p.
• Use q to access the array element.
• Compute p' = send(p, q).
  Permissions of q (in this case all of them) are merged with those of p to make a new pointer p'.
• Thereafter, only access the array using p', not p.

Undefined behaviour

There are certain things you are not allowed to do. For example:

• Break the shnam rule, i.e. store to a location using one pointer and load from the same locations using another (in either order). You must use send to transfer permissions from one pointer to the other.
• Store to a location twice using the same pointer. You must use send to obtain a numerically equal pointer that you can use for the second store operation.
• Store to a location using a pointer, use the pointer to compute another pointer, and access the same location using the new pointer. This is in fact a special case of one of the first two violations; the memory accesses are unordered.
• Construct a pointer from an integer, and use it to access memory. You must use send to give the pointer some permissions, taking them from some other pointer (which could be null).

[apt1002]

I've now added Action::Send and the optimizer knows what it means.

This is a backwards-incompatible change to the Mijit instruction set. Code using Mijit will require modifications in order to work on the new version (likely to be 0.2.4).