On Thu, 8 Dec 2022 at 16:59, Axel Heider <axelhei...@gmx.de> wrote: > > Peter, > > >> This patch adds timer peripherals to the arm-virt machine.>> > > Is there a reason you can't use the CPU's built-in generic timer > > device ? That is what typical guest code does on this system. > > I'm a bit reluctant to add more devices to the virt board > > because over time it gradually gets increasingly complicated, > > and every new device model we expose to the guest is another > > thing that's part of the security attack surface for guest > > code trying to escape from a KVM VM. > > For the seL4 specific case, this is currently not possible in > the standard configuration. It's only exposed for a special > debug and benchmarking configuration.
It's not clear to me what you mean here -- the generic timer in the CPU exists in all configurations, so there should be no obstacle to seL4 using it. > The catch we have here is, that the virt machine is a nice > generic ARM (and RISC-V) machine for OS testing purposes also, > but it sometimes lacks things (see my other patched for the > UART). So, I wonder what would be the best option to continue > here. Should we consider defining another generic machine > profile that is more suited for the system emulation use case. > This is what OS developer could use then. Or could the virt > machine get some config parameters to customize it further. > So the "Machine-specific options" would support a "sp804=on" > that would add two timer peripherals then? > > The really cool customization option would be passing a DTB > to QEMU that describes exactly what "virt" machine is to be > emulated. This is a firm "no" -- it sounds on the surface like a good idea but it doesn't actually work in practice -- DTB files don't provide enough info to be able to build a board from, except in some specific restricted situations like the Xilinx one. -- PMM
