3 ms·
Formal verification is one thing, but being able to write a test suite for a device driver where you simply mock a small kernel API must be a game-changer. Not
by lobster_johnson 11y ago
Formal verification is one thing, but being able to write a test suite for a device driver where you simply mock a small kernel API must be a game-changer. Not to mention that a formal protocol with a small surface area should make it easier to build OS-independent drivers.
- chei0aiV 11y agohttp://lkml.iu.edu/hypermail/linux/kernel/1511.0/01898.html http://lkml.iu.edu/hypermail/linux/kernel/1511.0/01898.html
- nanolith 11y agoCertainly, having a well-defined interface makes both empirical testing and portability easier. Microkernels get this by default. To be fair though, modern monolithic kernels have pretty decent abstraction mechanisms that do make it easy to test drivers. Hypervisors and fast emulators have dramatically changed operating system and device driver development, removing a lot of the pain in this process. I remember testing device drivers on bare metal because we had no choice. Now, I can fire up a GDB server in KVM and step through code. Monolithic or microkernel, testing and debugging is so much easier now than it was even 15 years ago.