Lambda the Ultimate

Writing practical memory management code with a strictly typed assembly language, by Toshiyuki Maeda, and Akinori Yonezawa.

Memory management (e.g., malloc/free) cannot be implemented in traditional strictly typed programming languages because they do not allow programmers to reuse memory regions, in order to preserve memory safety. Therefore, they depend on external memory management facilities, such as garbage collection. Thus, many important programs that require explicit memory management (e.g., operating systems) have been written in weakly typed programming languages (e.g., C). To address the problem, we designed a new strictly and statically typed assembly language which is flexible and expressive enough to implement memory management. The key idea of our typed assembly language is that it supports variable-length arrays (the arrays whose size is not known until runtime) as language primitives, maintains integer constraints between variables, and keeps track of pointer aliases. Based on the idea, we implemented a prototype implementation of the language. We also implemented a small operating system kernel which provides a memory management facility with the language.

This paper forms part of Toshiyuki Maeda's thesis, where he also uses TALK (OCaml source code available) to build a certified x86 kernel called TOS (source code available). I'm surprised I hadn't heard of this work before, as it seems quite practical.

The paper does not discuss the limitations of TALK, though the thesis does. The most significant disadvantage is described in section 2.8.1:

The type system of TALK is flexible and expressive enough to implement practical memory management code (e.g., malloc/free). However, it is not enough to efficiently implement all the data structures that can be represented in ordinary typed languages, because the type system of TALK restricts pointer manipulation in some cases in order to keep track of aliasing relations between pointers. For example, generic graph data structures including directed acyclic graphs and cyclic graphs cannot be represented naturally in the type system of TALK. This is because once a memory region is encapsulated inside an existential package, the region cannot be accessed until the package is unpacked.

They suggest prior work designed to relax linearity restrictions can be applied to TALK to enable graph structures to be captured.

While TALK is a low-level assembly language, other higher level languages have attempted to capture safe low-level memory management as well.