> You may still have N crossings: user process -> uK -> fileserver -> uK [-> generic Disk driver -> uK] -> specific device driver -> ... and concurrently some t

> You may still have N crossings: user process -> uK -> fileserver -> uK [-> generic Disk driver -> uK] -> specific device driver -> ... and concurrently some thread/process scheduling has to happen as there may be many such things in flight at the same time. Done right, a design such as mine should cut those crossings in half: user process -> fileserver [-> generic Disk driver] -> specific device driver -> ... IMO, seL4 hasn't taken over for a few reasons, but the biggest is that it has a poor API.