On Thu, 8 Dec 2022 at 17:25, Axel Heider <axelhei...@gmx.de> wrote: > >> 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. > > Access is not exposed to userland in the standard configuration > and the standard kernel API has no no timeouts besides zero and > infinite. It's a design thing in the end. Nothing that could not > be hacked around or be changed in the design in the long run. But > my goal is not to hack around, but have a "proper" machine > simulation instead. Which basically falls down to having a generic > machine in mainline that has a few more customization options.
So, my take on this is that I'm open to adding things to the virt board where we don't provide a feature that's useful to guest code. The second UART falls in this category: it lets you do things that you otherwise could not do (like have one UART for firmware and one for a kernel). On the other hand, this case with the sp804 sounds more like QEMU is already providing functional timer facilities and the problem is on the guest software side. To me the "non-hacky" solution sounds like it is "sel4 should provide a better timer related API to userland". I don't really want to work around guest OS deficiencies in QEMU. thanks -- PMM
