seL4
allow to preload data from a file into a memory region by specifying an input file in the XML
I'd like to use memory regions to distribute data to my protection domains. Ideally, there would be a setting in the XML snippets of memory regions that specifies an input file. During execution of the microkit tool, the tool opens the input file, embeddeds its content into an ELF section and instructs the microkit loader to load from this section into the specific memory region during system initialization.
Why do this using Microkit instead of by a dedicated loader protection domain?
Because it allows to assume the correct data to be available in the mr from the first instruction executed in a protection domain! If a dedicated loader is used, than one can not just use the data in the mr, one can only start doing so after being signaled from the loader protection domain that the loading has succeeded. In my use case, I'd like to use the data from within the init() function, with the dedicated loader protection domain all my init logic that depends on the mr would have to be moved into the notified function. Also, the functionality is already there, to distribute the code of the individual protection domains.
Additional thoughts
- Should we also communicate the length of the file? If so, how?
Followup from some internal discussion:
@Kswin01 Patch page tables of child PD's into their parent #316 is doing a similar thing from the tool, except it does it by appending a new elf segment and then relying on the existing logic.
For sDDF work with sdfgen we use several objcopy to add information from our tooling into the ELF files for them to use. However, what we want is not to edit the ELF file, but for them to be loaded into memory accessible for the program; editing the ELF files is just a way of achieving this.
For template/switching PDs (another internal project), it might be useful to have a way to embed the ELF files to switch between without needing to somehow embed these or half multiple PDs for the sole purpose of loading ELF files into memory.
- Ivan/Gernot: Not strictly the responsibility of the system description file as it wants to concern itself with seL4 things? Can technically do this via ELF patching?
- Julia: This isn't entirely true because of the child PDs vspace work which is information from the SDF .system file itself.
Julia: This isn't entirely true because of the child PDs vspace work which is information from the SDF .system file itself.
The user is not providing the data in that case and so I don't think it's a fair comparison.
For what it's worth, for a non-Microkit system the way I solved this problem is by having U-boot load a config file to a hard-coded address and mark that region as device memory via KernelCustomDTSOverlay and then map it as shared memory with all the processes that need it. Perhaps not as convenient as Microkit supporting it natively, which seems a useful feature, and it relies on U-boot, but it does allow updating the file content at runtime without rebuilding.
As for achieving the same within the current framework of Microkit, you could, of course, embed the file content into your application's ELF file yourself. But considering Microkit is doing this trickery already, adding support for arbitrary files makes a lot of sense.
Another way of doing it would be embedding the file into the DTB via incbin like FIT does. However, the Microkit loader doesn't pass the DTB on yet.
Maybe Microkit should provide a way to define dependencies between init calls. I think that would be useful to have, as that simplifies system startup. Also, when restarting tasks is supported, dependent tasks can be restarted by default when their dependency needs to be restarted. All in all it would make it easier to create a robust system.
