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
13#pragma once
14
15#include <autoconf.h>
16#include <sel4/types.h>
17#include <allocman/cspace/cspace.h>
18#include <allocman/cspace/single_level.h>
19
20struct cspace_two_level_config {
21    /* A cptr to the first level cnode that we are managing slots in */
22    seL4_CPtr cnode;
23    /* Size in bits of the cnode */
24    size_t cnode_size_bits;
25    /* Guard depth added to this cspace. */
26    size_t cnode_guard_bits;
27    /* First valid slot (as an index) */
28    size_t first_slot;
29    /* Last valid slot + 1 (as an index) */
30    size_t end_slot;
31    /* Size of the second level nodes
32       cnode_size_bits + cnode_guard_bits + level_two_bits <= 32 */
33    size_t level_two_bits;
34    /* if any of the second level cnodes are already created we can describe them here.
35     * up to the user to have put the cspace together in a way that is compatible with
36     * this allocator. The slot range is usual 'valid slot' to 'valid slot +1', with
37     * the cptr range describing a used cap range which can start and stop partially in
38     * any of the level 2 cnodes */
39    size_t start_existing_index;
40    size_t end_existing_index;
41    seL4_CPtr start_existing_slot;
42    seL4_CPtr end_existing_slot;
43};
44
45struct cspace_two_level_node {
46    /* We count how many things we have allocated in each level two cnode.
47       This allows us to quickly know whether it is already full, or of it is
48       empty and we can free it */
49    size_t count;
50    /* The cspace representing the second level */
51    cspace_single_level_t second_level;
52    /* Cookie representing the untyped object used to create the cnode for this
53       second level. This is only valid if we allocated this node, it may have
54       been given to us in bootstrapping */
55    seL4_Word cookie;
56    int cookie_valid;
57};
58
59typedef struct cspace_two_level {
60    /* Remember the config */
61    struct cspace_two_level_config config;
62    /* First level of cspace */
63    cspace_single_level_t first_level;
64    /* Our second level cspaces */
65    struct cspace_two_level_node **second_levels;
66    /* Remember which second level we last tried to allocate a slot from */
67    size_t last_second_level;
68} cspace_two_level_t;
69
70int cspace_two_level_create(struct allocman *alloc, cspace_two_level_t *cspace, struct cspace_two_level_config config);
71void cspace_two_level_destroy(struct allocman *alloc, cspace_two_level_t *cspace);
72
73seL4_CPtr _cspace_two_level_boot_alloc(struct allocman *alloc, void *_cspace, int *error);
74int _cspace_two_level_alloc(struct allocman *alloc, void *_cspace, cspacepath_t *slot);
75void _cspace_two_level_free(struct allocman *alloc, void *_cspace, const cspacepath_t *slot);
76int _cspace_two_level_alloc_at(struct allocman *alloc, void *_cspace, seL4_CPtr slot);
77
78cspacepath_t _cspace_two_level_make_path(void *_cspace, seL4_CPtr slot);
79
80static inline cspace_interface_t cspace_two_level_make_interface(cspace_two_level_t *cspace) {
81    return (cspace_interface_t) {
82        .alloc = _cspace_two_level_alloc,
83        .free = _cspace_two_level_free,
84        .make_path = _cspace_two_level_make_path,
85        /* We do not want to handle recursion, as it shouldn't happen */
86        .properties = ALLOCMAN_DEFAULT_PROPERTIES,
87        .cspace = cspace
88    };
89}
90
91