README.md
1<!---
2 Copyright 2017, Data61
3 Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 ABN 41 687 119 230.
5
6 This software may be distributed and modified according to the terms of
7 the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 See "LICENSE_BSD2.txt" for details.
9
10 @TAG(DATA61_BSD)
11-->
12
13libsel4allocman
14===============
15
16libsel4allocman provides a way to allocate different kinds of resources from the
17'base' resource type in seL4, which is untyped memory.
18
19It provides by an implementation of the `vka_t` interface as well as a native
20interface for accessing features not exposed by vka.
21
22Allocation overview
23-------------------
24
25Allocation is complex due to the circular dependencies that exist on allocating resources. These dependencies
26are loosely described as
27
28 * Capability slots: Allocated from untypeds, book kept in memory
29 * Untypeds / other objects (including frame objects): Allocated from other untypeds, into capability slots,
30 book kept in memory
31 * memory: Requires frame object
32
33Note that these dependencies and complications only exist if you want to be able to track, book keep, free and reuse
34all allocations. If you want a simpler 'allocate only' system, that does not require book keeping to support free,
35then these problems don't exist.
36
37Initially, because of these circular dependencies, nothing can be allocated. The static pool provides a way to inject
38one of the dependencies and try and start the cycle.
39
40The static and virtual pools can be thought of as just being another heap. Allocman uses these to allocate book
41keeping data in preference to the regular C heap due to usage in environments where the C heap is either not
42implemented or is implemented using allocman.
43
44Two pools are needed, one static and one virtual, because the virtual pool (along with the rest of allocman) require
45memory in order to bootstrap. Once bootstrapping is done then provided the system does not run out of memory enough
46space in the virtual pool will also be reserved to ensure that if the virtual pool needs to grow, there is enough
47memory for any book keeping required.
48