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#include <autoconf.h> 14#include <sel4/types.h> 15#include <sel4/sel4.h> 16#include <stdio.h> 17#include <allocman/allocman.h> 18#include <allocman/cspace/simple1level.h> 19#include <allocman/mspace/fixed_pool.h> 20#include <allocman/utspace/twinkle.h> 21#include <allocman/cspace/two_level.h> 22#include <allocman/mspace/virtual_pool.h> 23#include <allocman/utspace/trickle.h> 24#include <allocman/bootstrap.h> 25#include <allocman/cspaceops.h> 26#include <string.h> 27#include <sel4utils/vspace.h> 28#include <allocman/vka.h> 29 30#define VIRTUAL_START 0xA0000000 31 32#define MEM_POOL_SIZE (1*1024*1024) 33 34static char initial_mem_pool[MEM_POOL_SIZE]; 35 36allocman_t *test_use_current_cspace_bootinfo() { 37 int error; 38 allocman_t *allocman; 39 vspace_alloc_t vspace; 40 vka_t *vka; 41 allocman = bootstrap_use_bootinfo(seL4_GetBootInfo(), sizeof(initial_mem_pool), initial_mem_pool); 42 assert(allocman); 43 vka = allocman_mspace_alloc(allocman, sizeof(*vka), &error); 44 assert(!error); 45 allocman_make_vka(vka, allocman); 46 sel4util_get_vspace_alloc_leaky(&vspace, seL4_CapInitThreadPD, vka, seL4_GetBootInfo()); 47 48 reservation_t *reservation = vspace_reserve_range_at(&vspace, VIRTUAL_START, MEM_POOL_SIZE, seL4_AllRights, 1); 49 assert(reservation); 50 51 bootstrap_configure_virtual_pool(allocman, VIRTUAL_START, MEM_POOL_SIZE, seL4_CapInitThreadPD); 52 error = allocman_fill_reserves(allocman); 53 assert(!error); 54 return allocman; 55} 56 57void test_use_current_1level_cspace() { 58 int error; 59 seL4_CPtr i; 60 allocman_t *allocman; 61 seL4_BootInfo *bi = seL4_GetBootInfo(); 62 allocman = bootstrap_use_current_1level(seL4_CapInitThreadCNode, bi->initThreadCNodeSizeBits, bi->empty.start, bi->empty.end, sizeof(initial_mem_pool), initial_mem_pool); 63 assert(allocman); 64 /* have to add all our resources manually */ 65 for (i = bi->untyped.start; i < bi->untyped.end; i++) { 66 cspacepath_t slot = allocman_cspace_make_path(allocman, i); 67 uint32_t size_bits = bi->untypedSizeBitsList[i - bi->untyped.start]; 68 uint32_t paddr = bi->untypedPaddrList[i - bi->untyped.start]; 69 error = allocman_utspace_add_uts(allocman, 1, &slot, &size_bits, &paddr); 70 assert(!error); 71 } 72 error = allocman_fill_reserves(allocman); 73 assert(!error); 74} 75 76void test_use_current_cspace() { 77 int error; 78 seL4_CPtr i; 79 allocman_t *allocman; 80 cspace_single_level_t *cspace; 81 utspace_trickle_t *utspace; 82 seL4_BootInfo *bi = seL4_GetBootInfo(); 83 allocman = bootstrap_create_allocman(sizeof(initial_mem_pool), initial_mem_pool); 84 assert(allocman); 85 /* construct a description of our current cspace */ 86 cspace = allocman_mspace_alloc(allocman, sizeof(*cspace), &error); 87 assert(!error); 88 error = cspace_single_level_create(allocman, cspace, (struct cspace_single_level_config) { 89 .cnode = seL4_CapInitThreadCNode, 90 .cnode_size_bits = bi->initThreadCNodeSizeBits, 91 .cnode_guard_bits = seL4_WordBits - bi->initThreadCNodeSizeBits, 92 .first_slot = bi->empty.start, 93 .end_slot = bi->empty.end 94 }); 95 assert(!error); 96 97 error = allocman_attach_cspace(allocman, cspace_single_level_make_interface(cspace)); 98 assert(!error); 99 100 utspace = allocman_mspace_alloc(allocman, sizeof(*utspace), &error); 101 assert(!error); 102 error = allocman_attach_utspace(allocman, utspace_trickle_make_interface(utspace)); 103 assert(!error); 104 105 /* have to add all our resources manually */ 106 for (i = bi->untyped.start; i < bi->untyped.end; i++) { 107 cspacepath_t slot = allocman_cspace_make_path(allocman, i); 108 uint32_t size_bits = bi->untypedSizeBitsList[i - bi->untyped.start]; 109 uint32_t paddr = bi->untypedPaddrList[i - bi->untyped.start]; 110 error = allocman_utspace_add_uts(allocman, 1, &slot, &size_bits); 111 assert(!error); 112 } 113 error = allocman_fill_reserves(allocman); 114 assert(!error); 115} 116 117void test_new_1level_cspace_bootinfo() { 118 int error; 119 allocman_t *allocman; 120 cspace_simple1level_t *boot_cspace; 121 cspacepath_t new_path; 122 allocman = bootstrap_new_1level_bootinfo(seL4_GetBootInfo(), 14, sizeof(initial_mem_pool), initial_mem_pool, &boot_cspace); 123 assert(allocman); 124 error = allocman_fill_reserves(allocman); 125 assert(!error); 126 /* test we can easily use our old cspace */ 127 error = cspace_move_alloc_cptr(allocman, cspace_simple1level_make_interface(boot_cspace), seL4_CapInitThreadTCB, &new_path); 128 assert(!error); 129 /* drop our priority */ 130 error = seL4_TCB_SetPriority(new_path.capPtr, new_path.capPtr, 100); 131 assert(error == seL4_NoError); 132 /* no longer need that boot cspace information */ 133 allocman_mspace_free(allocman, boot_cspace, sizeof(*boot_cspace)); 134} 135 136void test_new_1level_cspace() { 137 bootstrap_info_t *bootstrap; 138 seL4_BootInfo *bi = seL4_GetBootInfo(); 139 cspace_simple1level_t boot_cspace; 140 allocman_t *allocman; 141 cspacepath_t oldroot; 142 cspacepath_t currentroot; 143 cspacepath_t new_path; 144 cspacepath_t tcb; 145 cspacepath_t pd; 146 seL4_CPtr i; 147 int error; 148 bootstrap = bootstrap_create_info(sizeof(initial_mem_pool), initial_mem_pool); 149 assert(bootstrap); 150 /* describe the current cspace */ 151 cspace_simple1level_create(&boot_cspace, (struct cspace_simple1level_config){ 152 .cnode = seL4_CapInitThreadCNode, 153 .cnode_size_bits = bi->initThreadCNodeSizeBits, 154 .cnode_guard_bits = seL4_WordBits - bi->initThreadCNodeSizeBits, 155 .first_slot = bi->empty.start, 156 .end_slot = bi->empty.end - 1 157 }); 158 /* pass to the boot strapper */ 159 currentroot = _cspace_simple1level_make_path(&boot_cspace, seL4_CapInitThreadCNode); 160 bootstrap_set_boot_cspace(bootstrap, cspace_simple1level_make_interface(&boot_cspace), currentroot); 161 /* give the untypeds to the bootstrapper */ 162 for (i = bi->untyped.start; i < bi->untyped.end; i++) { 163 cspacepath_t slot = _cspace_simple1level_make_path(&boot_cspace, i); 164 uint32_t size_bits = bi->untypedSizeBitsList[i - bi->untyped.start]; 165 uint32_t paddr = bi->untypedPaddrList[i - bi->untyped.start]; 166 error = bootstrap_add_untypeds(bootstrap, 1, &slot, &size_bits, &paddr); 167 assert(!error); 168 } 169 /* bootstrapper has enough information to create */ 170 tcb = _cspace_simple1level_make_path(&boot_cspace, seL4_CapInitThreadTCB); 171 pd = _cspace_simple1level_make_path(&boot_cspace, seL4_CapInitThreadPD); 172 allocman = bootstrap_new_1level(bootstrap, 14, tcb, pd, &oldroot); 173 assert(allocman); 174 /* take advantage of knowledge of simple1level cspace and just shift its root :) */ 175 assert(oldroot.capDepth == 32); 176 boot_cspace.config.cnode = oldroot.capPtr; 177 /* now test we can use it */ 178 error = cspace_move_alloc_cptr(allocman, cspace_simple1level_make_interface(&boot_cspace), seL4_CapInitThreadTCB, &new_path); 179 assert(!error); 180 /* drop our priority */ 181 error = seL4_TCB_SetPriority(new_path.capPtr, new_path.capPtr, 100); 182 assert(error == seL4_NoError); 183} 184 185void test_new_2level_cspace_bootinfo() { 186 int error; 187 allocman_t *allocman; 188 cspace_simple1level_t *boot_cspace; 189 cspacepath_t new_path; 190 allocman = bootstrap_new_2level_bootinfo(seL4_GetBootInfo(), 6,10, sizeof(initial_mem_pool), initial_mem_pool, &boot_cspace); 191 assert(allocman); 192 error = allocman_fill_reserves(allocman); 193 assert(!error); 194 /* test we can easily use our old cspace */ 195 error = cspace_move_alloc_cptr(allocman, cspace_simple1level_make_interface(boot_cspace), seL4_CapInitThreadTCB, &new_path); 196 assert(!error); 197 /* drop our priority */ 198 error = seL4_TCB_SetPriority(new_path.capPtr, new_path.capPtr, 100); 199 assert(error == seL4_NoError); 200 /* no longer need that boot cspace information */ 201 allocman_mspace_free(allocman, boot_cspace, sizeof(*boot_cspace)); 202} 203 204void test_new_2level_cspace() { 205 bootstrap_info_t *bootstrap; 206 seL4_BootInfo *bi = seL4_GetBootInfo(); 207 cspace_simple1level_t boot_cspace; 208 allocman_t *allocman; 209 cspacepath_t oldroot; 210 cspacepath_t currentroot; 211 cspacepath_t new_path; 212 cspacepath_t tcb; 213 cspacepath_t pd; 214 seL4_CPtr i; 215 int error; 216 bootstrap = bootstrap_create_info(sizeof(initial_mem_pool), initial_mem_pool); 217 assert(bootstrap); 218 /* describe the current cspace */ 219 cspace_simple1level_create(&boot_cspace, (struct cspace_simple1level_config){ 220 .cnode = seL4_CapInitThreadCNode, 221 .cnode_size_bits = bi->initThreadCNodeSizeBits, 222 .cnode_guard_bits = seL4_WordBits - bi->initThreadCNodeSizeBits, 223 .first_slot = bi->empty.start, 224 .end_slot = bi->empty.end - 1 225 }); 226 /* pass to the boot strapper */ 227 currentroot = _cspace_simple1level_make_path(&boot_cspace, seL4_CapInitThreadCNode); 228 bootstrap_set_boot_cspace(bootstrap, cspace_simple1level_make_interface(&boot_cspace), currentroot); 229 /* give the untypeds to the bootstrapper */ 230 for (i = bi->untyped.start; i < bi->untyped.end; i++) { 231 cspacepath_t slot = _cspace_simple1level_make_path(&boot_cspace, i); 232 uint32_t size_bits = bi->untypedSizeBitsList[i - bi->untyped.start]; 233 uint32_t paddr = bi->untypedPaddrList[i - bi->untyped.start]; 234 error = bootstrap_add_untypeds(bootstrap, 1, &slot, &size_bits, &paddr); 235 assert(!error); 236 } 237 /* bootstrapper has enough information to create */ 238 tcb = _cspace_simple1level_make_path(&boot_cspace, seL4_CapInitThreadTCB); 239 pd = _cspace_simple1level_make_path(&boot_cspace, seL4_CapInitThreadPD); 240 allocman = bootstrap_new_2level(bootstrap, 6, 10, tcb, pd, &oldroot); 241 assert(allocman); 242 /* take advantage of knowledge of simple1level cspace and just shift its root :) */ 243 assert(oldroot.capDepth == 32); 244 boot_cspace.config.cnode = oldroot.capPtr; 245 /* now test we can use it */ 246 error = cspace_move_alloc_cptr(allocman, cspace_simple1level_make_interface(&boot_cspace), seL4_CapInitThreadTCB, &new_path); 247 assert(!error); 248 /* drop our priority */ 249 error = seL4_TCB_SetPriority(new_path.capPtr, new_path.capPtr, 100); 250 assert(error == seL4_NoError); 251} 252 253int main(void) { 254 allocman_t *alloc; 255 alloc = test_use_current_cspace_bootinfo(); 256// test_use_current_1level_cspace(); 257// test_use_current_cspace(); 258// test_new_1level_cspace_bootinfo(); 259// test_new_1level_cspace(); 260// test_new_2level_cspace_bootinfo(); 261// test_new_2level_cspace(); 262 printf("All is well in the universe.\n"); 263 while(1); 264} 265