Flexible PD Configuration#
Address Space Configuration#
The bulk of the PD configuration process is in managing address space layout. ads_config_t allows the user the provide a list of virtual memory regions (VMR) to create in a given ADS.
Deep-Copied VMRs#
VMRs in the created PD which should share the same content as a VMR in the creator PD but are mapped to different physical pages are considered DISJOINT
VMRs. There is additional effort needed from the creator PD outside of the pd_creation
module to deep-copy a VMR:
Allocate a new MO of the same size as the one mapped to the VMR to deep-copy
Map the MO into the creator PD’s ADS, copy the contents of the deep-copied VMR into the new MO
In the VMR description to give to the ADS config system, set the VMR as
DISJOINT
, but provide the newly allocated MO. The config system will attach this MO, with the copied contents, into a VMR in the new ADS
VMR Descriptions#
Not all fields of the VMR description (vmr_config_t) need to be filled in. Whether a field needs to be filled in depends on its sharing mode. The table below details which fields need to be specified, for each sharing mode:
Option |
SHARED |
DISJOINT |
Default (when optional) |
---|---|---|---|
type |
required |
required |
|
start |
required |
optional |
any available virtual address |
dest_start |
optional |
ignored |
|
region_pages |
required |
required |
|
page_bits |
ignored |
optional |
4K pages |
mo |
ignored |
optional |
new MO will be allocated |
^1
: This field is only optional if the VMR type is a special type, as described in SHARED VMRs.
CPU Configuration#
A CPU may need higher privileges to access a few system registers. In seL4, this corresponds to binding a VCPU object to a TCB, and is done when the elevated_cpu
config option is toggled.
RDE Configuration#
The created PD can be given all or a subset of the RDEs which the creator PD can request from. The convenience function sel4gpi_add_rde_config() can be used to specify that an RDE of a certain resource type and namespace should be shared with the created PD.
Fault Handling#
The creator PD can specify a fault handler for the created PD by setting the fault endpoint in the configuration. If none are specified, a new fault endpoint will be allocated for the PD, which the creator can retrieve to listen on.
Linked PDs#
You may want some PDs to be automatically terminated when another PD exits (for instance, additional threads when the main thread of a process exits). To create a PD which gets terminated when the creator PD exits, the link_with_current
config option can be toggled. For thread-PDs, this option is automatically set if using sel4gpi_configure_thread()
.
Non-standard PD Types#
Spawning a HighJMP PD#
A PD which is capable of HighJMP address-space switching is considered a single PD, which holds two ADSes. CellulOS currently implements HighJMP requiring user-involvement. This means that the HighJMP PD is aware of its separate ADSes and is directly responsible for setting up additional ADSes and switching between them. One can imagine an implementation where the ADS management is pushed into a client-library, where the ADS switching is transparent to the PD. There is nothing preventing such an implementation in CellulOS.
With respect to our current implementation, the HighJMP PD can be created by spawning a process as usual. Once inside the process, the PD can create a new ADS and configure it using sel4gpi_ads_configure().
The VMRs that must be specified for a HighJMP ADS are:
Deep-copied Heap
Deep-coped ELF data segment
Shared Stack
Shared IPC Buffer
Share ELF code segment
Share OSM Data segment (1 page)
Since the stack, IPC buffer, and ELF code segments are all special VMR types, the VMR description can use the convenience option described in SHARED VMRs.
The CPU can then be configured to swap between ADSes on demand using cpu_client_change_vspace()
.
Threads With Isolated Stacks#
In CellulOS, threads with isolated stacks exist in a separate ADS from the main thread, but share most of the main thread’s VMRs. An isolated thread-PD can be created like so:
Create a new
runnable
, allocating new a PD, ADS and CPU. A convenience function sel4gpi_new_runnable() exists for this purpose.Configure the ADS to share ELF regions, the heap, and any other desired VMR with the new thread. Configure the stack and IPC buffer to be disjoint VMRs.
Give the configuration to
sel4gpi_prepared_pd()
Start the thread using
sel4gpi_start_pd()
Warning
Due to the secondary thread existing in a separate ADS, any additional changes to the main thread’s ADS that should be reflected in the secondary thread’s ADS needs to be done manually by the main thread (e.g. by mapping a VMR in both ADSes). This is a known limitation of Cellulos.