Hi Anna,

I’d like to create process with particular size of CSpace and VSpace.

CSpace size is defined in ‘config’ structure, I can set config.one_level_cspace_size_bits member.

I am not sure how to set up VSpace size through ‘reservations’ and ‘num_reservations’ values? Let’s say I need to give to new process 10Mb virtual space.

static inline sel4utils_process_config_t

process_config_create_vspace(sel4utils_process_config_t config, sel4utils_elf_region_t *reservations,  int num_reservations)

{

    config.create_vspace = true;

    config.reservations = reservations;

    config.num_reservations = num_reservations;

    return config;

}

Thank you,

Leonid

Hi Leonid,

I don't understand your first question, which untyped are you wanting to adjust the size of?

As for the second question, you can take a look at the sel4bench project, where all created processes use the same function to get a working allocator through the libsel4benchsupport library bundled with the project [1]. 

We're aware we need more tutorials and I'll add this to the list of desired seL4 tutorials.

Thanks

Anna. 

​

[1] https://github.com/seL4/sel4bench/blob/master/libsel4benchsupport/src/support.c#L390