Linear types and the multicore generalization

This is the chapter where the type system stops being a clever discipline and becomes a load-bearing structural element. We’re going to introduce linear types from scratch, build the intuition for why they matter, and then show that the same mechanism that makes them useful for resource management is what makes multicore code safe.

Linear types are the single most important type-system feature for systems work, and they’re the reason the kernel’s “same code on single and multicore” property is real rather than aspirational.

What linear types are

Start from a familiar place. In ordinary type systems — including the ML we’ve built so far — a value of type int can be used as many times as you like:

let x = 5 in
let y = x + x in     (* x used twice *)
let z = x * 2 in     (* used a third time *)
y + z

You created x, you used it three times, nothing bad happened. This works because ints are copyable: making more of them out of one of them is free and harmless.

Now consider a different value. Suppose you have a file handle:

let f = open_file "data.txt" in
let bytes_a = read f in
let bytes_b = read f in
close f;
read f                   (* uh oh *)

The last read f happens after the file has been closed. The compiler doesn’t catch this. The runtime traps, or worse, returns garbage. This is the use-after-close bug that every C and C++ programmer has shipped to production at some point.

The problem is that f is being treated as copyable when it shouldn’t be. There’s only one real file handle — it’s a resource in the operating system, with a single identity — but the type system lets us use the name f as many times as we want, including after we’ve destroyed the underlying resource.

Linear types are types whose values must be used exactly once. If file_handle were a linear type, the code above wouldn’t compile. The compiler would tell you that f is used four times when it must be used exactly once. To make it compile, you’d have to write it like this:

let f0 = open_file "data.txt" in
let (bytes_a, f1) = read f0 in    (* read consumes f0, returns bytes AND a fresh handle *)
let (bytes_b, f2) = read f1 in    (* uses f1, not f0; f0 is gone *)
close f2                            (* consumes f2; no handle remains *)

Each operation consumes its input handle and produces a fresh one. After read f0 runs, f0 is no longer usable — it’s been consumed. The compiler tracks this. You cannot use f0 again because the type system has marked it as “spent.” The result of read is a pair: the bytes, and a new handle f1 that represents the file’s state after the read. To read again, you use f1. After close f2, no handle exists; the resource is gone, and the type system knows it.

This is linearity. The “exactly once” rule turns resource management from a runtime discipline into a compile-time guarantee. You cannot use-after-close. You cannot double-close. You cannot leak — the compiler will complain that f is used zero times, which is also illegal.

Affine types, the practical sibling

Strict linearity (“exactly once”) is sometimes too strict. What about errors? If open_file succeeds and then your program panics before closing, you’ve failed to use the handle. Real systems usually want a slightly weaker rule: at most once. You can drop a value on the floor (the runtime will clean it up), but you cannot use it twice.

This weaker rule is called affine typing. Rust’s borrow checker is built on affine types: values can be moved (consuming them) or dropped (also consuming them, automatically at end-of-scope), but they cannot be used after being moved. Most production “linear-ish” type systems are actually affine, including the one we’ll specify for CML.

For our purposes, the distinction matters but isn’t critical. When this book says “linear types,” it means “affine types in practice, linear in theory.” If you read other literature, this is the same elision most authors make.

Why this matters for our design

Three uses in CML, in order of obviousness:

First, resources. File handles, network sockets, memory allocations from a region, locks. These exist in the world with a single identity. Linear typing lets us write acquire and release operations that the compiler ensures are paired correctly.

Second, mutable state. A mutable array, conceptually, can’t be aliased — if two parts of the program both hold the array and both modify it, you have a data race. Linear typing lets you encode “this array has one owner at a time” in the type system. Pass it to a function; you no longer own it; the function returns it (possibly modified) and now you own it again.

Third — and this is the one that matters for multicore — capabilities. A capability is “permission to do a thing.” The capability to read from device 0x05. The capability to allocate from arena R. The capability to invoke continuation K. Capabilities are inherently linear: you have one, you can use it, and using it might consume it. The whole structure of “who is allowed to do what” in a multicore system can be encoded as the flow of linear capabilities through the program.

A small example

type linear region    (* a "region" capability — linear *)

effect Region {
  open  : () -> region              (* creates a fresh region capability *)
  alloc : region -> (region, ptr)   (* consumes capability, returns it back *)
  close : region -> ()              (* consumes capability, returns nothing *)
}

let example () : () / {Region} =
  let r0 = perform Region.open () in
  let (r1, p1) = perform Region.alloc r0 in    (* r0 consumed; r1 fresh *)
  let (r2, p2) = perform Region.alloc r1 in    (* r1 consumed; r2 fresh *)
  perform Region.close r2                       (* r2 consumed *)
  (* attempting `perform Region.close r0` here is a type error *)

This is the threading pattern: each operation consumes one capability and produces the next. The compiler counts uses; each must be exactly once. There is no way to use r0 after Region.alloc r0 returns, because r0 is no longer in scope under linearity rules — the value has been moved into the perform.

This pattern is verbose. Real linear-type languages have syntactic sugar to make it readable (Rust’s borrow notation, for instance). For CML, we’ll specify the sugar later; for now, the explicit threading is fine because it makes the semantics visible.

Now: back to the kernel

The cooperative kernel has a process type:

type process = {
  id : int;
  k  : unit continuation;
}

And a scheduler that holds processes in a ready queue, pops one, runs it, files the resulting continuation back.

Now imagine we want to run this on four cores. Each core has its own scheduler. A process running on core 0 might want to migrate to core 1 — perhaps because core 0 is overloaded.

What does migration look like? Conceptually:

effect Migrate {
  to_core : core_id -> ()
}

| Migrate.to_core target, k ->
    send_continuation_to_core target k;
    scheduler ()

The process performs Migrate.to_core 1. The handler captures the continuation k, sends it as a message to core 1’s scheduler, and resumes the local scheduler. Core 1 receives it and runs it.

This is what the unification promised. The mechanism for migration is the same mechanism we’ve used for everything else.

Where it breaks without linearity

But notice: when core 0 sends the continuation to core 1, core 0 has just shipped a value. If core 0 keeps a copy of k and core 1 receives a copy too, and both invoke it, what happens?

The process exists twice. Both cores think they’re running it. The process’s local variables get incremented independently on two cores. If the process holds a file handle, two cores try to read from the same file. If the process is an actor with a mailbox, messages get processed twice. The system’s state diverges. Welcome to a distributed-systems consistency problem.

The fix is: only one core may invoke k. Whichever sends it must lose ownership. Whichever receives it must gain ownership. The continuation is a resource with one identity, and ownership must be tracked.

This is exactly what linear types do.

Continuations are linear by their nature

Make continuation a linear type in CML:

type linear continuation a

Now every operation involving a continuation must thread it explicitly. Invoking a continuation consumes it. Sending it to another core consumes it. You cannot invoke a continuation twice; you cannot keep a copy after sending.

Look at the scheduler’s handler clauses, with linearity now visible:

| Yield k ->     (* k is linear *)
    Queue.push sched.ready { id = p.id; k };   (* consumes k by moving it *)
    scheduler ()

The k enters the handler, gets moved into the process record, gets moved into the ready queue. The handler does not have access to k after the Queue.push. If it tried to also invoke k after pushing, the compiler would reject — k has been moved.

This sounds like a constraint on the kernel author. It is — but a productive one. Every place a continuation is touched, the type system has tracked who owns it. Use-after-resume becomes a compile error. Double-invoke becomes a compile error. Forgetting to file the continuation becomes a compile error (it would be unused, violating linearity).

Now the migration handler:

| Migrate.to_core target, k ->
    perform NoC.send target (encode_continuation k);   (* consumes k *)
    scheduler ()

The continuation k is consumed by NoC.send — it gets serialized into a packet and shipped to target. Core 0 no longer has k. Core 1 will receive a fresh handle to the deserialized continuation in its incoming-message handler. Ownership has transferred. The type system enforces it.

Why this makes single-core and multicore the same code

This is the payoff. The kernel code we’ve written — the scheduler, the handler clauses, spawn, proc_loop, all of it — doesn’t change for multicore. Not a line. What changes is:

1. The Queue.push / Queue.pop operations. On a single core, they’re local data structure operations. On multiple cores, they might be remote-aware: pushing to a “ready queue” might mean pushing to the local queue or sending a message to another core whose queue is the target.

2. The Mem.alloc handler. Single core: bumps a local heap pointer. Multicore: allocates from per-core arenas, with cross-core sharing handled via specific effects.

3. The migration handler clause is added, if you want it. If you don’t, processes run on whatever core they were spawned on, forever.

But the body of the scheduler — the part that does the actual work — is identical. Same match expression, same handler clauses, same logic. The differences are entirely in the implementation of the data structures the scheduler uses.

The reason this works is the handler-as-policy / continuation-as-mechanism separation, plus linearity to make ownership explicit. The kernel writes “file this continuation in the ready queue.” The implementation decides whether that means a memory write or a NoC packet send. The kernel doesn’t have to know, because the type system has already proven the operation is sound — linearity ensures the continuation is consumed exactly once regardless of where it ends up.

This is what people mean when they say “effect handlers + linear types compose.” The handler abstracts the policy. The linear type abstracts the ownership. Together, they make the user of the abstraction (the kernel) invariant under changes in the implementation. Single-core, multicore, distributed, doesn’t matter to the kernel code. It matters to the queue implementation.

What linearity bought us, specifically

Linearity is doing work in three places:

1. At the continuation type. Continuations are linear. They cannot be duplicated. This means k in any handler clause can be moved into a queue, sent over the NoC, or invoked — but only one of these.

2. At process records. A process contains a linear continuation, so by transitive linearity, process is also linear. A process record cannot be in two queues simultaneously. When core 0 sends a process to core 1, core 0 loses it.

3. At any future “shared resource” types. File handles, NIC descriptors, locks, allocator capabilities — all linear. The system’s resource discipline is uniform.

Linearity is not doing work for:

• Ordinary integers, bools, strings, etc. These are copyable.
• Read-only data structures.
• Closures, in general (but closures that capture linear values become linear).
• Effect declarations or handler descriptions.

The discipline targets exactly the things that matter: resources with identity. Everything else stays cheap and copyable.

How CML expresses linearity

A type can be declared linear:

type linear continuation a
type linear file_handle
type linear region

Functions taking linear arguments must consume them — pass them on to another function, store them somewhere, or explicitly drop them. The compiler tracks ownership through pattern matching and let-bindings.

Effect operations whose argument or return type is linear thread ownership through the perform/resume cycle. perform Ready.push p consumes p; the handler receives p and can use it once.

Records with linear fields are themselves linear. Sum types with linear variants are linear in those variants. The discipline propagates up.

The compiler can usually infer linearity, but explicit annotations are encouraged at API boundaries for documentation.

What this chapter committed to

Linear types defined from scratch. Their use for resources, mutable state, and capabilities. The recognition that continuations are inherently linear. The realization that linearity is what makes multicore migration safe by enforcing single-ownership of continuations. The setup for the next chapter, which assembles the full multicore kernel.