Capability spaces

Capability spaces (CSpaces) are kernel resources designed to hold an addressable table of capability slots, or “cslots”, in which capabilities are stored that can be used by tasks which can address their enclosing cspace.

Tasks refer to a capability stored in their cspace via a capability address, or “caddr”, and pass these addresses in as arguments to system calls to perform operations against the capabilities at the corresponding address.

A capability slot is 2⁶ bits (64 bytes) and a capability space stores 2^R capability slots, where the radix, R, is configurable at the time the CSpace is allocated. A CSpace with a radix of 8, for example, stores 256 capability slots, which requires 16 KiB of memory. The last slot of any CSpace is reserved for the kernel to store runtime state concerning the CSpace.

Capability slot operations

A capability space provides a number of functions which operate on the capability slots in the CSpace. These include:

• Destroy: Destroys a capability and replaces its capability slot with a Null capability. The reference count of the resource in question is decremented, and if there are no further references, the resource is reclaimed (e.g. by returning its memory to a Memory capability). All capabilities can be destroyed but the last reference to a capability which is in-use cannot always be destroyed; for example one must unmap all pages in an address space before destroying the last reference to a VSpace capability.
• Copy: Copies a capability from one slot to another, incrementing the reference count. Some capabilities can be copied as often as one wishes, but most support only up to 256 copies before ERANGE is returned. Some capability types cannot be copied (namely Reply capabilities).
• Move: Moves a capability from one capability slot to another without updating the reference count, leaving a Null capability in the source slot. All capabilities can be moved.

Capability addressing

A CSpace may contain capabilities for other CSpaces among its cslots. Through the capability addressing system, one may address capabilities stored in nested CSpaces. These addresses are resolved in a manner similar to seL4 through guarded page tables.

A CSpace capability contains both the radix of the cspace, denoting how many capability slots it contains, as well as a guard value with a variable number of bits. Resolving a capability address through possibly nested CSpaces takes their guards into account, so that a CSpace may be constructed to resolve addresses in any manner the user wishes.

When looking up a capability from its address, the kernel begins with the root CSpace associated with the caller’s task. It checks the most significant bits of the address against the guard bits of the capability, and, if they match, shifts it away and uses the next R bits to identify a capability slot. If any unprocessed bits remain in the address, and the indicated slot stores a CSpace capability, the process continues with that CSpace.

Consider the following set of CSpaces:

CSpace A holds a capability that references CSpace B, and CSpace B holds a reference to CSpace C. Each has a variety of radii and guards. For the task shown here to invoke the Page capability in CSpace C, the 32-bit capability address 0x5DE1F0CA is used.

The first four bits are matched against the 4-bit guard of CSpace A, 0b0101 (0x5), then the next 8 bits are used to identify a slot among the 2⁸ slots in CSpace A. 20 bits remain, 0x1F0CA, and so resolution continues from CSpace B. CSpace B has a radix of 4 and no guard bits, so the next 4 most-significant bits, 0x1, are used to identify a slot. 16 bits remain, so the resolver continues to CSpace C and resolves the guard bits 0b11110000 (0xF0). The final 8 bits identify one of the 2⁸ slots in CSpace C, namely slot 0xCA, where the Page capability resides.

By arranging capability spaces with the necessary radii and guard bits, one may construct any desired 32-bit capability address space.