4 ms·

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

by bakul 3y ago

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. All this has been thought about for decades. I encourage you read KeyKOS related papers on Norm Hardy's site (link in my earlier response). seL4 is of course a very good uK but it still have not taken over the world (its niche is probably high security environments).

gavinhoward 3y ago
> 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.