Hello Genodians,
I have been playing around with Genode on seL4 for the last few days and have a couple of questions.
[1] Did any modifications need to be made to the seL4 source code for Genode to work properly?
[2] I encountered a couple of strange warnings when running the "Hello world" scenario from the Genode foundations book. Below is the clipped console log showing the exact messages.
. . . Booting all finished, dropped to user space Warning: device memory in range [0000000400000000,0000000800000000) is unavailable (due to limited untyped cnode range) // To which device is this referring? Warning: device memory in range [0000000800000000,0000001000000000) is unavailable (due to limited untyped cnode range) Warning: device memory in range [0000001000000000,0000002000000000) is unavailable (due to limited untyped cnode range) . . . boot module 'config' (469 bytes) boot module 'init' (456304 bytes) Warning: need physical memory, but Platform object not constructed yet // I'm assuming this is a non-issue, but wanted to check Warning: need physical memory, but Platform object not constructed yet . . . Genode 24.02 183 MiB RAM and 523285 caps assigned to init Warning: void Core::Rpc_cap_factory::free(Genode::Native_capability) not implemented - resources leaked: 0x1 // What are the implications of this? Warning: void Core::Rpc_cap_factory::free(Genode::Native_capability) not implemented - resources leaked: 0x2 Warning: void Core::Rpc_cap_factory::free(Genode::Native_capability) not implemented - resources leaked: 0x4 [init -> hello] Hello world
I am not yet familiar (still learning) the internals of seL4 and core, so apologies if these questions have obvious answers.
Thanks in advance, Zachary Zollers
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
-
Norman Feske -
Zachary Zollers