Hello Zachary,
[1] Did any modifications need to be made to the seL4 source code for Genode to work properly?
You can review our (few) modifications here:
https://github.com/genodelabs/genode/tree/master/repos/base-sel4/patches
Warning: device memory in range [0000000400000000,0000000800000000) is unavailable (due to limited untyped cnode range) // To which device is this referring?
This diagnostic message occurs during the initialization of core's model of the machine's physical address-space layout. At this point, we distinct only between RAM, reserved, and MMIO. The ranges are not related to individual devices at this point. The notion of devices enters the picture not before using the platform driver, which knows PCI.
Genode's core (roottask) keeps a statically dimensioned (NUM_PHYS_SEL_LOG2) cnode array for referring to "untyped" memory (think of physical memory). If the kernel's boot info reports address ranges exceeding these array bounds, they are ignored (and logged). In practice, this can be a potential problem if a device is mapped within such a range. A user-level device driver for such a device would fail to obtain the device's MMIO range because core would deny it.
In the past, most device resources used to be mapped below 4G. Unfortunately, this assumption does not hold on modern platforms anymore.
To find out how this limitation affects you in particular, you may review the I/O bars of the PCI devices present in your machine.
Warning: void Core::Rpc_cap_factory::free(Genode::Native_capability) not implemented - resources leaked: 0x1 // What are the implications of this?
This limitation affects long running servers in dynamic scenarios. Imagine a GUI server where clients appear and disappear over time. When a client appears, the GUI server creates an RPC session object for the client, allocating a capability, and returns this capability to the client for interacting with the session. Once the client closes the session, this capability should be destroyed. But it is not. It is just no longer used. So after many session-open-close cycles, the GUI server's cap quota would become depleted, rendering the GUI server unable to handle new clients.
In static scenarios, this resource leak won't bite you. But it would impede dynamic scenarios like Sculpt OS. However, since we found seL4 not ideally suited for highly dynamic Genode systems anyway, the limitation remained unaddressed, yet logged.
Cheers Norman