On Wed, Sep 29, 2021 at 6:23 PM William ML Leslie
On Wed, 29 Sept 2021 at 18:10, erickaoakes--- via Devel
wrote: Hi Kent,
Unfortunately setting up passthrough devices on x86 for camkes-vm apps is pretty painful.
It appears that your answer is specific to QEMU x64? Is setting up passthrough devices on x64 bare metal similarly painful?
Yea, essentially CAMKES is missing a plugin for calculating the hardware resources that a particular PCI device would need. There is a plugin for doing this with Arm and RISCV using flattened device trees, but it would be more complicated for x86 because the device hierarchy is dynamically calculated at startup so a plugin would need to be able to either run a program on the platform and dump this information in a format that the camkes tooling could then turn into seL4 hardware caps or some other way of precalculating what hardware resources a device will end up with. Because there's no plugin for doing this, it currently must be done manually as I described above.
That sounds about as painful as parsing the ACPI MCFG table from scratch. Has anyone done this on seL4?
It'd be pretty useful if we had a program that could be run on a target platform during build time or as a one-off for a platform with a fixed hardware layout that could generate an FDT spec that could be fed back into camkes when producing a system image. As far as I'm aware this isn't roadmapped currently.
-- William Leslie
Q: What is your boss's password? A: "Authentication", clearly
Notice: Likely much of this email is, by the nature of copyright, covered under copyright law. You absolutely MAY reproduce any part of it in accordance with the copyright law of the nation you are reading this in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without prior contractual agreement. _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems