allocman_t *bootstrap_use_current_simple(simple_t *simple, size_t pool_size, 
void *pool) {
    allocman_t *allocman;
    int error;
    /* Initialize inside the current 1 level cspace as defined by simple */
    allocman = bootstrap_use_current_1level(simple_get_cnode(simple), 
simple_get_cnode_size_bits(simple), simple_last_valid_cap(simple) + 1, 
BIT(simple_get_cnode_size_bits(simple)), pool_size, pool);
    if (!allocman) {
        LOG_ERROR("Failed to initialize an allocman");
        return allocman;
    }
     .......
    return allocman;
}

The params of "bootstrap_use_current_1level" below:
        cnode_size = simple_get_cnode_size_bits(simple), like 23, it is 8M
        endslot = BIT(simple_get_cnode_size_bits(simple)), also 8M

        I think we don't have so many endslot, because per slot is not only one 
byte
                                                                                
            Thank you very much
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Reply via email to