Linear Types and Program Resource Management

In the previous post "The Case for a Concurrency-oriented VM", I speculated that a VM aimed at concurrency-oriented languages, and with focus on concurrency safety, might be a good thing to have. I also mentioned in passing that linear types might have something to offer in that regard.

Today, I will elaborate on that. In particular, I will show how linear types enable expressing resource management related constraints, and how some common patterns for concurrency-safe resource management can be expressed using linear types.

The context is that of a intermediate program representation to be used as input for a virtual machine — a representation which allows certain safety conditions above and beyond mere type safety to be enforced through locally verifiable rules (but not a representation intended to be produced by hand).

More concretely, this can be seen as part of an attempt to model a complete concurrency-oriented language (Erlang, as it happens) using linear types, aiming towards demonstrating that such a thing as an Erlang VM can be defined in terms of a linear-type based VM.

Resources and life cycles

What is the difference between information and physical matter? One key difference is that whereas physical matter can not be created nor destroyed, information can be copied and destroyed at zero cost. The cost of software, for instance, lies in its design and development - not in manufacturing or distribution (in the original sense). And there are no software landfills; when you erase a file, the zeroes and ones don’t "go anywhere".

Even so, software deals with resources of a physical nature. Some of the values manipulated by software — numbers, for instance — are just bit patterns which can easily be copied, moved around and forgotten. Other values denote some kind of resource — be it a chunk of memory, a file descriptor, or a network connection — which can only be used for one purpose at a time, and which must be disposed of properly when the program is done using it. Resources which have lifes cycles and which need managing.

While many programming languages have static type checking — verification that values are only ever used according to their type, few have static checking of life cycles — verification that values are only used according to where in their life cycle they are.

That kind of checking is possible, though. It just requires a type system with linear types.

Linear types and values

What are linear types? A value of a linear type cannot be copied, and cannot be destroyed — at least not implicitly.

In other words, each value can be used only once, and must be used exactly once.

This may sound odd to most programmers. But take as an example a simple assignment statement of some imperative language:

a = b;

From the traditional point of view, one thing happens here: The bit pattern of b is copied into the location of the variable a.

From the linear point of view, however, three things actually happen: The old value of a is destroyed; the value of b is copied; and the copy is put in a. At least if a is a pre-existing variable, and b is a variable which is read later in the program.

At the level we’re speaking of here, the destruction and the copying step must be made explicit — it is not a given that these steps are permitted; the value in question may be a resource which does not support copying or destruction — or it may be the case that special steps must be taken when copying or destruction happens. (This may sound familiar to C programmers: C classes may have copy constructors and destructors which are used for such special steps.)

In other words: For linear values, there is a one-to-one relation between variables and values — there is such a thing as value ownership.

Resource categories

Now, back to the practical problem with resource management in programs. Assume that we are to program a virtual machine which has only linear types. Can we model the usual kinds of values as linear types, if we are free to add the necessary built-in functions to support them?

First, let’s categorize value types according to how there are managed. (Developers versed in C++, where resources are also managed more or less explicitly, may notice some familiar patterns.)

• Can the value be copied and destroyed trivially?
  If yes: value belongs to category 1; this category includes all values which are merely bit patterns of fixed size: integral and floating-point numbers, booleans, characters, enumeration values, bit masks.
  
• If no (it requires cleanup): are the point(s) of cleanup in the program statically known?
  If yes: (category 2) the value is used linearly, and can be (explicitly) disposed of at the appropriate place(s).
  
• If no (the points of cleanup are not statically known): is the value immutable?
  If yes: (category 3) the value can be either copied in its entirety, and the copies disposed of individually (3a); or the value can be managed through reference counting (3b), in which case a "copy" action consists of incrementing its reference count, and a "destroy" action consists of decrementing its reference count and optionally (if the count reaches zero) disposing of the value.
  
• If no (the value is shared and mutable): is the value used from a single thread only (or, more generally, is it only used in scope of a specific other value which is used linearly)?
  If yes: (category 4) the value can be put in a heap which is linearly owned (i.e., only accessible from one thread at a time).
  
• If no (the value is mutable and shared between threads): (category 5) the value can be protected by a lock; the lock is reference counted and its disposal causes the value to be disposed.
  

It is perhaps worth noting that such a program as the Erlang VM uses all of these management techniques, for different kinds of data:

• Atoms and small integers are contained in a single machine word and are simply copied (category 1).
  
• Process contexts are linear (category 2), and is disposed of at specific program points.
  
• Message between processes are copied (category 3a).
  
• Large binary values are managed through reference counting (category 3b).
  
• Other Erlang terms (tuples, lists, bignums, small binaries, etc.) live in a heap which belongs to a process which is a linear value (category 4).
  
• Finally, certain data structures: the process registry, non-private tables, etc., which are mutable and shared among processes, are managed through the use of locks (category 5).
  

(It should be noted that there is another category, program literals, which resemble category 3 but is optimized to be handled like category 1 most of the time. In the Erlang VM, these require very special handling when code is unloaded. This is an advanced management form which I won’t try to cover just yet. Also, variables accessed with atomic hardware operations comprise yet another category, one which is handled much like category 5.)

Intermezzo: Type notation

In what follows, I will have to write a number of function signatures. These signatures involve four type constructors: ⊗, ⊕, ∀ and ∃.

• A ⊗ B is a linear product type — which is like a traditional product type (aka record, struct, or tuple type, depending on language) type except that each of its fields must be used (consumed) exactly once.
  
• A ⊕ B is a linear sum type — which is like a normal sum type (aka tagged union, algebraic datatype, etc.) except that the value it contains (whichever of the variants it is) must be consumed exactly once.
  
• ∀T.A(T) is universal quantification — aka. parametric polymorphism or generics, which is used for e.g. generic container types.
  
• ∃T.A(T) is existential quantification — such as can be used for subtype polymorphism or typeclasses, but in what follows will be used in a more general manner.
  

The points of interest here is firstly the linear nature of values. Secondly: existential types are usually used to link together two values — an object representation and a vtable for that object’s class — and to enforce encapsulation on the type level. But as we shall see, existential quantification can be used in a different manner; notably, one that (unlike the vtable usage) does not involve anything similar to run-time method lookups. We’ll get back to this in the treatment of heaps.

Resource management in a linear virtual machine

Now we should be ready to look at how each of the resource categories can be modelled in a virtual machine with linear types.

In the following, T stands for the type of the resource. Most of the cases are quite unsurprising; the interesting bit is the heap case.

Category 1: bit patterns

For this kind of values, we provide built-in functions ("axioms") for both copying and disposal; copy simply copies the bit pattern, and dispose does nothing:

copy : T → T ⊗ T
dispose : T → ()

Category 2: linear values

This kind of value requires no special functions. Copying is not allowed, and disposal happens explicitly.

Category 3a: resource copying

This kind of values can be copied; each copy is disposed of individually:

copy : T → T ⊗ T
dispose : T → ()

There is of course some dynamic storage allocation in play here, too. In the function signatures shown above, the storage allocation system is an implicit argument to both operations (in malloc-style); one might imagine alternatives where it is presents as an explicit argument.

Category 3b: reference counting

Reference counted values are created with an initial reference count of one. Copying and disposal functions are supplied; copy increments the reference count, and dispose decrements it and frees the resource if the count reaches zero. In the simple form of this, freeing the resource does not require any other parameters:

copy : T → T ⊗ T
dispose : T → ()

Again, the underlying storage allocation system is implied.

Category 4: (defered)

Single-thread heaps is a more graceful strategy than lock protection — but the cruder lock protection mechanism is easier to describe, so we’ll handle that first and return to heaps afterwards.

Category 5: lock-protection

This kind of value is created with a lock and a reference count (initially one). The raw value of type T is not initially available; instead, you get a LockedT. To get access to the value proper, you first need to acquire the lock.
copy and dispose works as for a reference counted value. acquire and release work the lock.

copy : LockedT → LockedT ⊗ LockedT
copy : T → T ⊗ LockedT
dispose : LockedT → ()
acquire : LockedT → T
acquire : LockedT ⊗ Timeout → T ⊕ LockedT
release : T → LockedT

(If the type T can also be managed in other ways, such that not all instances of T can be subjected to, e.g., the release operation, then the function signatures need to be a bit different.)

Category 4: heap allocation in linearly owned heap

This is the most complex case.

The model here is an Erlang-style heap: In Erlang, each process owns a heap, which is a contiguous block of memory divided into an "allocated" area and a "free" area. The heap’s allocation pointer points to the boundary between the two; everything below the boundary is allocated, and everything above is free.

When a new object needs to be allocated, it is first checked whether there is enough space in the "free" area to accommodate an object of the size in question. If there is room, the lowest part of the free area is used for the object, and the allocation pointer is adjusted upwards accordingly.

If there is not enough room, then a garbage collector is called — a moving garbage collector which compacts the live objects into a contiguous area at the beginning of the heap. During this process, a new heap area may be allocated; in any case, after garbage collection, the heap is once again parted in two by the allocation pointer, and there is now room in the free space for the requested object.

There are two things to be aware of here:

1. At allocation time, the garbage collector must know all of the root objects in the heap, in order to preserve all reachable values;
   
2. At allocation time, the location of all live pointers into the heap must be known to the garbage collector, so that it can adjust them appropriately when it moves objects.
   

As an example of how the first invariant can be missed, consider a built-in function which makes two heap allocations. If, after the first allocation, the function does not tuck away the resulting pointer into a location searched by the garbage collector, then if the second allocation triggers a collection, then the first allocated object will be deemed garbage and be collected.

As an example of what can go wrong if the second invariant is not observed, consider the case where the same built-in function does tuck away a copy of the first pointer into a location searched by the garbage collector, but then — after the second allocation — goes on to use the original pointer from a local variables which is not adjusted by the collector: the first object lives, but the pointer used by the built-in function does not point to it (but rather to the place where it used to live).

These are the two major pitfalls to be aware of, and if we are to model such a heap, the type system should guard against them.

Enter the use of existential variables as a means to link two variables.

In this scenario, unlike the others, we will not provide access to the raw value of type T; instead, the individual field of the value can be accessed (if the value is a record; sum type values can be handled similarly).

First of all, we need to have access to the heap itself. It will have two parameters:

Heap[h,a]

of which one, h, denotes the identity of the heap, while the other, a, denotes the current version of the heap. These are not actual types (they will end up coming from an existential quantor) but are of a more technical nature.

Each pointer to a heap object (of type T) is represented by a:

HeapPtr[T,a]

where a denotes the version of the heap for which this pointer is valid. Given that we don’t intend the garbage collector to support objects with finalizers, T can not be of any type — only certain types of objects (those with no-op disposal functions) can be heap-allocated.

Access of a field (of, say, type F) happens through a built-in function:

access_field : ∀h.∀a. Heap[h,a] ⊗ HeapPtr[T,a] → Heap[h,a] ⊗ F

(Here it is not really necessary to have access to the heap itself; proof that the current version is a is enough. The heap interface can be refined to reflect this — and the proof in question need not be present at runtime, and can be optimized away.)

Disposing of a heap pointer is a no-op — the pointer can simply be forgotten about:

dispose : ∀T.∀a. HeapPtr[T,a] → ()

Allocation of a new heap pointer is interesting. Here we may end up with a different version of the heap, because the allocation may trigger garbage collection. Suppose that we are to allocate an object of type F, which requires values of types A and B to construct:

allocate : ∀h.∀a. Heap[h,a] ⊗ _A_ ⊗ _B_ → ∃b.Heap[h,b]

Note that after allocation, all of the old heap pointers of type HeapPtr[h,a] are useless! They can no longer be used as input to access_field (but dispose can still be used on them).

This is exactly what we desire. However, we need some way of registering root pointers for the garbage collector. To this end, we introduce a type:

RootPtr[T,h]

and functions for registering root pointer and get up-to-date pointers back:

register_root : ∀h.∀a.∀T. Heap[h,a] ⊗ HeapPtr[T,a] → Heap[h,a] ⊗ RootPtr[T,h]
read_root : ∀h.∀a.∀T. Heap[h,a] ⊗ RootPtr[T,h] → Heap[h,a] ⊗ HeapPtr[T,a]
dispose_root : ∀h.∀T. RootPtr[T,h] → ()

Finally, we have of course construction and disposal of a heap. These functions allocate, respectively deallocate, the memory areas and bookkeping data structures for the heap:

create_heap : () → ∃h.∃a. Heap[h,a]
dispose : ∀h.∀a. Heap[h,a] → ()

All in all, we can model heaps in a safe way with linear types. It does not matter whether the heap is managed through mark-and-sweep or copying or compacting or generational garbage collection; the scheme presented should work for either kind.

The performance characteristics should (I think) be within a small constant factor of usual GC implementations; the largest difference is in explicit registration of heap root versus other schemes such as stack maps. On the other hand, the scheme presented needs no special tricks to be portable, and it is flexible: for instance, it supports multiple heaps, which can be used for values with very different life cycles or for messages to be sent from one thread to another.

The Case for a Concurrency-oriented VM

In the following, I’ll describe the background for my current long-running project - why I believe it to be a worthwhile endeavour.

The overall line of thought goes like this: concurrency and concurrency-oriented languages are important; we have such languages, but they are few and far between; there exists a non-CO ecosystem (the one around the JVM) which has spawned dozens of languages and allows those languages to cooperate and prosper; which factors have been significant in creating this ecosystem, and how can they be harnessed to improve conditions for concurrency-oriented languages?

We begin at concurrency and how programming languages deal with it.

Concurrency and languages

A fair number of the programs we use every day are doing more than one thing at a time. Every web server, smartphone app, GUI application, operating system, chat server, VoIP system, game server, music player, video player, etc. that you’re using are concurrent programs - either in the sense that they are serving multiple users at once, or in the sense that they have multiple asynchronous event sources they have to react to in a timely manner.

Yet most programming languages - and about all mainstream languages - aren’t very well geared towards making concurrent applications. The programming paradigms one hears most about these days are the Object-oriented and the Functional paradigm. Ever heard of Concurrency-oriented languages? They exist, but there aren’t very many of them - and they are not mainstream but something you have to actively seek out.

What do I mean by being concurrency-oriented, or "geared towards concurrent applications"? (I’ve touched upon this question earlier.)

A number of languages with concurrency support are not much more than a sequential language with threads and locks added. This is not enough to qualify for being a concurrency-oriented language; to be that, you have to take the issues of concurrency seriously. If you take a convential imperative language and add threads, you’d have to subtract something as well.

A typical example of a language-with-threads is Java. Java is an object-oriented language first and a concurrency-supporting language second, at best. Like most languages-with-threads, concurrency support mainly comes as an addition, an afterthought, with a library-ish feel. Sure, the Java syntax contains concurrency-related things - mainly synchronized and volatile - but nothing forces you to use them. You can write a program embodying all of the concurrency pitfalls known to man, and neither compiler nor runtime will object in the slightest.

There are rules about when the concurrency primitives are used safely. They come in the form of the Java Memory Model and Thread Specification, which states what the guarantees are and how to avoid »Surprising behaviours«.^[1]

To be sure, explicitly stated guarantees is a Good Thing. But consider a world in which the type safety of Java amounted to a document stating how to avoid type errors. No static checking, no run-time checking, just rules about when you’re safe…

Smells a lot like C, right? Replace type errors, initialization errors, and memory mismanagement faults with data races and deadlocks - and lack-of-strong-typing becomes lack-of-proper-concurrency-support. Except that whereas the former kind of bugs are more or less deterministic, the latter kind seldom is. Which means that a) it is harder to debug, b) it can not be guarded against by unit tests, and c) the place where you’re likely to discover it is in production.

And just like we’re much better off with the enforced type safety of Java (nobody misses the segmentation faults which are common when developing C or C++ programs), so we’re better off when the language provides some actual guarantees in the face of concurrent activities.

And languages can do that. A language like Erlang, for example, is concurrency-oriented first and functional second - and it shows. Other examples include Oz, CML, Rust, and Clojure (Haskell probably also qualifies these days); each solves the problem of providing safe concurrency in its own way.^[2]

But these languages are each isolated efforts, and they are not mainstream. Which means that they each must struggle on many fronts: evolving syntactically and semantically; keeping up with hardware and OS evolution; providing libraries for the expected functionality of the changing times; and fighting for developer mindshare.

The success of the JVM

Which brings us to the happy ecosystem centered around the JVM.

The Java Virtual Machine is thriving - to the point where it might outlive the language it was originally created for; while Java the language is evolving only slowly, - the JVM is the center (qua facilitator) of a wholly different level of evolution: a multitude of languages of all sorts of paradigms, domains, typing strategies and syntactic styles are targeting the JVM.

Though the VM was originally designed for just one language - Java - it has proven so convenient to generate code for that many language implementers have chosen to do just that. (I’ve done it myself on more than one occasion.)

Why is that?

For one thing, the JVM is well-specified. Its specification is public and the rules are clear and make sense. Second, part of those rules are embodied in the bytecode verifier - a validation step performed on code when it is loaded into the JVM. Thirdly, the existence of the public specification has meant that the Java language and the JVM implementation(s) have been decoupled (more or less) with respect to their evolution. Java the language has been able to evolve quite a bit without the VM spec changing much (The addition of generics being one example), and the VM on its part has been able to evolve quite much performance-wise. (Besides, several competing VM implementations have come to exist.)

And the HotSpot implementation of Java is a solid piece of software engineering which has put to shame the "interpreted languages must be slow" prejudice, making it a thing of the last century.

What does these things mean for compiler writers targeting the JVM?

Targeting a statically checked bytecode format is a blessing, because many of the most difficult-to-debug kinds of error are revealed at load time, instead of resulting in mysterious memory corruptions. Bytecode verification enforces some useful invariants, reducing debugging time.

Targeting a mature VM yields performance and portability benefits - "write once, run anywhere" is attractive for language implementers as well as application developers.

Consider all the languages which run on the JVM, some of them available only on that platform.
Without that virtual machine, or something else playing the same role, would we have had so many new implementations of such a variety of languages, of such a level of maturity, performance and portability? And provided with such a wide range of libraries?

Most probably not.

The task of implementing a native code generator for just a single platform, along with runtime libraries and a decently performing general-purpose garbage collector, is not trivial.^[3] The number of man-hours which could have gone to debugging segmentation fault and similar mysteries, and to implement just the basic libraries for the new languages, but which have instead been channeled to progress in other areas, are significant. Small wonder that Microsoft chose to copy Java and make their own common cross-language platform (.NET).

Finally, apart from development of compilers, the well-defined-ness of the Java bytecode format has meant that a number of other byte-code processing tools have come to exist: tools for analysis, transformation and instrumentation of Java bytecode.

In summary: The JVM has been, and is, a great facilitator; this is especially due to its general usability, public specification, fine performance (especially after HotSpot), and - not least - bytecode verification following well-defined and well-understood rules.

The shortcomings of the JVM

But the JVM design has drawbacks as well. Some are general nuisances, some are just annoying to compiler implementers targeting the JVM, and some cause it to be less than ideal for languages belonging to certain paradigms. Some are visible to Java developers, others are purely technical.

Issues for language implementers

First of all, the JVM smells of Java.
In a number of ways, the design of the virtual machine would have been different if Java - especially the early versions of Java - had been different.

The JVM is quite class-centric, for instance - the unit of loading and verification is the class. The only kind of type definition is the class. For language implementers, this is a source of mild annoyance: translating most kinds of simple code is simple, but the moment the code uses a new record type, or variant type, or function object, or a function needs to return multiple values - it translates into adding a new separate class file to the compiler output.

The JVM is statically typed - but has no parametrized types. Therefore, type safety breaks slightly every time one of the common container classes from e.g. java.util is used, so runtime checks must be performed. This is because Java prior to 1.5 (where generics where introduced) was poor on this point.
Furthermore, the JVM instruction set has a type check instruction and a type cast instruction - but no "check-and-cast" instruction. I can only assume that this is because Java doesn’t have a language construction such as "type case", but only the combining idiom "if (x instanceof T) {T y = (T) x; …}". Presumably, this pattern is recognized and simplified internally in the common JVM implementations.

JVM methods are limited to 64KB worth of bytecode. While this is rarely a limitation for hand-written Java code, it is occassionally a problem for machine-generated code. (In Erjang, for example, we hit the limit for one version of the interpreter, and also (if memory serves) when compiling one particular Erlang module into Java bytecode.)

A special case of this is that large literals simply can’t be used, because in the Java class file format, a literal value are represented as the sequence of instructions it takes to build the value. Try compiling a literal array of, say, 12,000 elements - at four instructions per array slot, this exceeds the method-length limit, and the compiler quits with the message "code too large".^[4] Certain table-driven algorithms would therefore also be hit by the limit.

The implications for language implementers are that a) one likely kind of candidate for hitting the method-length limit is interpreter loops, and b) compilers to JVM bytecode should know about and handle the limit — which gives rise to a tough implementation decision: just detecting when the limit is overrun and aborting the compilation is an honest, but abstraction-breaking solution; working around the limit in general is presumably possible, but introduces undesired (and seldomly needed) complexity.^[5][6]

Issues related to concurrency

A related problem is JVM’s bad immutability guarantees. Specifically, there is no such thing as an immutable array. If a part of your code is given an array, or provides public access to one it its arrays, then it can’t assume that other code parts won’t modify the contents of the array at a later point.
Literal arrays are no exception: a VM implementation can’t perform constant folding of lookups into a literal array until it’s proven that that array can’t be leaked to somewhere where it might be mutated; a property which can only be established by inspecting the entire scope of the variable.

The JVM’s support for (shallowly) immutable variables comes in the form of the final field modifier. The intuition of this modifier is simple enough: a final field can be set only once, and must be set before its first use, so it should have the same value throughtout its lifetime.

But in reality, things are a bit more complex - the field modifier has its warts:

• Certain final fields may be inlined at compile time - even across classes, which has the potential for causing surprising inconsistencies.

• Even fields declared final can be modified though reflection(!) - which, of course, doesn’t affect those accesses which have been inlined at compile-time (I believe you could call this a surprise within a surprise).

• There’s another case where the "final fields always have the same value" rule is broken: Final fields can be observed before they gain their value.
  That abstraction breakage is demonstrated in the following program:

  public class JavaFinal {
      final static Object x = JavaFinalHelper.create();
      public static void main(String[] args) {
          System.err.println("Main: x = "+x);
      }
  }
  
  class JavaFinalHelper {
      static {
          System.err.println("Helper: x = "+JavaFinal.x);
      }
      public static Object create() {return new Object();}
  }

  Here, the helper class’s static initializer is run before JavaFinal.x has been set - exposing the null value that field has before it is initialized.

Thus, certain should-be-invariants aren’t.

Finally, and most importantly in this context, there are the shortcomings in the concurrency department.

The JVM provides no checking of the sanity of concurrent access patterns. Java’s static type system which is the basis of the bytecode verification is static in more than one sense: It doesn’t take time into account. If you ever get hands on a reference to an object, then you can at any later point call any (visible) method.

In concurrent systems, concepts like life cycle, ownership, sharing and thread safety become important. The JVM doesn’t provide much support for dealing with these. For that matter, attention to these concepts is important in general for defining library boundaries - which assumptions the library and the library client can make about values passed to and from the library. Quite often, thread safety and access timing questions aren’t addressed by Java libraries' API documentations; Javadoc makes it easy to document the static types involved, but certain questions about the dynamics are not often answered.

From an Erlang point of view, such a thing as thread-local garbage collection is also desirable. I have a hypothesis that no sanely structured concurrent programs genuinely need a globally-GC’ed heap. Whether that is true or not, for global GC you either pay the price of occasional slow major garbage collections - which cost in latency - or, if your garbage collector is sufficiently advanced to do its work incrementally or concurrently with the mutating threads, pay the price of inter-thread synchronization necessary for this to work - which costs in throughput.

For the matter of this text, the verification aspects are the central points.

To sum up: The JVM lacks verification support for such things as sanity of concurrent accesses and immutability/read-only access privileges. As far as concurrency-orientation is concerned, these areas present room for improvement.
And I am not aware of any other generally targetable VMs which fare better in these respects.

The shortcomings of the BEAM

The primary contender for the title of Concurrency-orientated VM is probably the one for Erlang, which is called BEAM. The flavour of concurrency-orientation provided by BEAM includes immutable data structures, shared-nothing actor-based concurrency, light-weight processes, and process-local GC - and a few specific forms of destructive updates.

In some ways, it is very much like the Java VM: It has a mature implementation, was originally intended for just one language, comes from industry (as opposed to academia), and started out as purely interpreted but later grew optional native compilation.

But in other respects, it is very different:
While the JVM has had a public specification at least since 1999, BEAM hasn’t got a complete specification - public or not.^[7]

The most complete instruction set reference I know of is this historical paper, written in 1997 but first released 2012 (prompted, I think, by the 2012 mailing list discussion). And that one only documents the internal representation, not the (somewhat different) instruction set used in BEAM files.

This lack of a specification has consequences:

• As for BEAM code producers: While other languages than Erlang have been developed for BEAM, none produce BEAM code directly - instead, they target an intermediate representation of the Erlang compiler and use that compiler’s backend for producing actual BEAM code.

• As for BEAM consumers: Until fairly recently, no other BEAM VM implementations existed but the official one from Ericsson.

The consumer situation has changed a bit; people have begun making other implementations such as Erjang, Browserl and Ling (which run on, respectively, JVM, Javascript, and bare metal).

But the lack of a specification - a clear definition of what is and what isn’t allowed - means that there are differences in what the implementations can run.

At least two example of this are known to me:

1. Erjang assumes that exception handlers are set up in a execution path independent manner. While this is presumably true for code generated by the Erlang compiler, I can imagine BEAM code in which this isn’t the case, and which the official BEAM implementation will run cheerfully, while Erjang will balk at it.

2. There is a gotcha hidden in the external instruction set - there are nine instructions for calling functions: three for local calls (call, call_last, call_only - depending on whether it’s a tail call, and whether there’s a stackframe to deallocate); three for external calls (call_ext, call_ext_last, call_ext_only); two for calls with dynamic module and/or function name (apply, apply_last); and one for calling function objects (call_fun).
   
   Can you guess what the trap is?
   
   Erlang is a language with guaranteed proper tail recursion, but the only instruction for calling function objects is a non-tail-call.
   How can that work??
   
   By cheating. The official BEAM rewrites the instruction set used in BEAM files into a richer instruction set used internally. The rewriting rules contain a rule which recognizes the instruction sequence "call_fun; deallocate; return" and rewrite it into the internal tail-call version of call_fun.
   
   The Erlang compiler, obviously, is in on the joke, and generates code accordingly.

This call_fun gotcha was one that both Erjang and Browserl missed. I only discovered it accidentally, and fixed it in Erjang, but as far as I can tell, Browserl doesn’t handle that corner case (yet).

So: a clear, public specification does matter. A specification backed by a formal checking mechanism such as a bytecode verifier is even better.^[8]

From a "multiple different languages on one VM" viewpoint, there are of course other issues as well - for instance, the BEAM is rather Erlang-centered.

• No in-process destructive updates are supported - even where it would be safe.

• Only the concurrency primitives needed by Erlang are present - and the form in which they are present is so high-level that there is very little flexibility for other languages to be very non-Erlang. A process can’t have more than one inbox; the set of supported transactions on tables are fixed; binaries support efficient appending but not prepending; and so on.

In summary: The BEAM is a mature, well-tuned, and actively evolving VM for running Erlang programs, but lacks probably the flexibility and (as things stand) certainly the well-defined-ness necessary for it to be viewed as a general platform for concurrency-orientated languages.

What would a concurrency-oriented VM look like?

If the JVM isn’t it, and the BEAM isn’t it, what would a concurrency-oriented VM then look like?

The BEAM offers concurrency safety, in that it does not allow^[9] shared mutable state without clearly defined transactions; this is a property we want.

The JVM guarantees the absence of certain kinds of errors, because its rules make the necessary invariants locally verifiable. We also want that. More specifically, the rule should guarantee against not only type errors, but also concurrency-related errors (data race conditions).

The JVM also enforces these invariants by verifying code at load time - rather than trust the compiler to generate only valid code. We want that, too - because we intend for there to be more than one compiler, for more than one language.

Both the JVM and the BEAM support "native functions" - functions implemented in C or similar - e.g. for interfacing with third-party libraries or for performance-sensitive parts of a program. It would be foolish to constrain the applications of a new VM by not supporting this. However, the aim should be to encourage as much as possible to be written in a concurrency-safe language - i.e. while library integration would be a good reason for using native functions, performance shouldn’t be; there should not be things which are inherently slow to implement on the VM.^[10]

Thus, while the rule "all data structures are immutable" (as known from Erlang) makes it easy to guarantee against data races, it is not good enough - it either makes it impossible to implement certain things efficiently, or encourages diving into a lower-level language to escape the rules. We want a bit more generality than that, also for the sake of supporting other paradigms than Erlang’s - mutating operations should be supported as long as they are safe and can be proven (reasonably easily) to be so.

For example, one step up, we have the rule "all data structures which are ever visible by more than one process/thread to another must be immutable", which is much more flexible yet also guarantees against data races (and can be made locally verifiable). Even higher up that ladder, shared mutable data are allowed, as long as proper synchonization is in place.

The design I have in mind is based on the concept of linear types, which appear to be a good match, in that they make it possible to capture lifecycles of objects in the type system - which goes a long way towards making certain concurrency-related guarantees locally verifiable (because half of concurrency is timing).

I plan to elaborate on linear types and their use as basis for a VM in future posts.

Acknowledgements

I would like to thank Peter Mechlenborg and Thomas In Sook Holmen for their help with forming this text.