Real-life type system check example

There is an example I love when talking about compile-time checks and high-performance computing: Philipp Oppermann wrote a type-safe paging system for a kernel with only two traits. Let's first understand the problem and then try the solution.

When a program uses the memory on a computer, it must separate virtual memory from physical memory. This is because each program running in the OS will think that the whole address space is theirs. This means that in a 64-bit machine, each program will think it has 16 exbibytes (EiB) of memory, 2⁶⁴ bytes.

That is, of course, not the case for any computer in the world, so what the kernel does is to move memory out of RAM to the HDD/SSD, and put in RAM the required memory. For this to work properly, memory has to be managed in chunks, since it doesn't make sense to move in and out individual memory addresses. These are called pages, and they are usually 4 KiB in size for x86_64 processors (the case for most laptops and desktop computers).

For the paging to be easily manageable, a paging hierarchy gets created. Every 512 pages get added to an index called a P1 table, and every 512 P1 tables get added to a P2 table. That goes on recursively until all pages have been assigned, which will be 4 levels. That is what it's called: 4-level paging.

The idea is that a kernel should be able to ask a table for one of its pages, and if it's a P4 table, it should be able to ask for a P3, then for a P2, then for a P1, and finally load the page referenced by that P1. This address gets passed in a 64-bit registry, so all the data is there. The problem is that it could be easy to end up with tons of code duplication for each table type, or we could end up with a solution that works for all pages but that has to check the current page at runtime if it wants to return the next table (if it's a P4-P2 table) or the actual page (if it's a P1 table).

The first case is really error-prone, and difficult to maintain, while the second one not only continues being error-prone, but it even requires checks at runtime, making it slower. Rust can do better.

The solution is to define a trait that all pages have, let's call it PageTable, and a trait that only higher-order tables have (tables that cannot directly return a page but that they need to return another page table). Let's call it HighTable. Since all HighTable types are also PageTable, one trait will inherit from the other:

pub trait PageTable {}

pub enum P4 {}
pub enum P3 {}
pub enum P2 {}
pub enum P1 {}

impl PageTable for P4 {}
impl PageTable for P3 {}
impl PageTable for P2 {}
impl PageTable for P1 {}

This creates four enumerations representing page table levels. The reason for using enumerations instead of structures is that empty enumerations cannot be instantiated, which will avoid some typos. Then we write the HighTable trait:

pub trait HighTable: PageTable {
    type NextTable: PageTable;
}

impl HighTable for P4 {
    type NextTable = P3;
}

impl HighTable for P3 {
    type NextTable = P2;
}

impl HighTable for P2 {
    type NextTable = P1;
}

As you can see, we add an associated type to each enumeration to represent the next level of paging. But, of course, in the case of the last level, it will not have another page table below.

This allows you to define functions associated to HighTable that will not be accessible to a P1 table and so on. And it lets you create a Page type that will contain the contents of a Page (a byte array, more or less) that is generic over what level it is.

Rust will ensure that you cannot try to get the next table of a P1 table at compile time, and at runtime, these enumerations will disappear, as they are zero-sized. The logic will be safe, though, and checked at compile time with no overhead.