Does that mean on a microkernel you'd essentially have double the amount of code execution for a driver (i.e. driver makes a call to the kernel, kernel verifies and then executes rather than the driver just executing the call) meaning double the latency? Seems like it would cause a lot of problems.