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?
On 30/06/2021, Isaac Beckett <isaactbeckett@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).
participants (2)
-
Andrew Warkentin -
Isaac Beckett