On 30/06/2021, Isaac Beckett <isaactbeckett(a)gmail.com> wrote:
Hello! Operating system noob here, I understand that
in most mainstream
operating systems (Linux, BSDs, MacOS, Windows) drivers are part of the
kernel. And in micro kernel operating systems like Minix and seL4, drivers
are part of user space. But Minix is a lot closer to a traditional POSIX
kernel, and seems to implement some of that (IE posix threads, IPC) in the
kernel, which makes the environment for a driver programmer a bit more
familiar. How do drivers work in seL4, then? How does a driver obtain
permission for hardware access from the kernel? I imagine it works with a
capability delegated by the root task, but how do you solve chicken and the
egg type problems, like loading driver code, without driver code already
loaded? Is it an initramfs like Linux/Unix? Also, what if seL4 is being used
_as_ the firmware/bootloader? Obviously it can load the seL4 kernel and user
space OS components from a file system to put them in the booting OS’
memory, but how does it load drivers for itself? I’m assuming there’s some
low level platform specific code, but is that code verified or part of the
proofs?
Hardware access is indeed done through capabilities provided to the
root task by the kernel (device untyped objects for MMIO and I/O port
objects for x86 PMIO).
When a disk/flash filesystem is present, the drivers and other
components necessary to access it are loaded along with the kernel and
root task, although how the root task finds and starts them is
OS-dependent. CAmkES puts them in a cpio archive and links it into the
root task. UX/RT (the OS I'm writing) will place the kernel, root
server, and all other components needed to mount the system volume
within an initramfs-like filesystem image and the loader will build a
Multiboot info structure with a module tag for each file in the image
(this is better suited to a general-purpose OS like UX/RT with boot
images built from multiple packages than the linking-based model used
by CAmkES).