libsel4allocman provides a way to allocate different kinds of resources from the ‘base’ resource type in seL4, which is untyped memory.
It provides by an implementation of the vka_t interface as well as a native interface for accessing features not exposed by vka.
Allocation is complex due to the circular dependencies that exist on allocating resources. These dependencies are loosely described as
Note that these dependencies and complications only exist if you want to be able to track, book keep, free and reuse all allocations. If you want a simpler ‘allocate only’ system, that does not require book keeping to support free, then these problems don't exist.
Initially, because of these circular dependencies, nothing can be allocated. The static pool provides a way to inject one of the dependencies and try and start the cycle.
The static and virtual pools can be thought of as just being another heap. Allocman uses these to allocate book keeping data in preference to the regular C heap due to usage in environments where the C heap is either not implemented or is implemented using allocman.
Two pools are needed, one static and one virtual, because the virtual pool (along with the rest of allocman) require memory in order to bootstrap. Once bootstrapping is done then provided the system does not run out of memory enough space in the virtual pool will also be reserved to ensure that if the virtual pool needs to grow, there is enough memory for any book keeping required.