5 ms·

A 400 cycle IPC doesn't seem too bad. [1] Also, I came up with an idea to get around that, something I call "hardware pipes." [2] [3] The idea is that the OS

A 400 cycle IPC doesn't seem too bad. [1] Also, I came up with an idea to get around that, something I call "hardware pipes." [2] [3] The idea is that the OS can map the same page(s) into both processes, and one process can write into the memory to send a message, while the other reads. Add another page for communication the other direction. You would use something like futexes for synchronization. Besides needing to wake up a process that went to sleep waiting, the OS should not have to be involved, so context switches are minimized at the cost of atomic instructions. Of course, it would be even better if there was hardware support for such shared memory pipes, but I think it could be done with what we have now. [1]: https://sel4.systems/About/Performance/home.pml https://sel4.systems/About/Performance/home.pml [2]: https://gavinhoward.com/2020/07/testing-the-feasibility-of-hardware-pipes/ https://gavinhoward.com/2020/07/testing-the-feasibility-of-h... [3]: https://gavinhoward.com/2020/12/testing-the-feasibility-of-hardware-pipes-2-exploring-designs/ https://gavinhoward.com/2020/12/testing-the-feasibility-of-h...

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.

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.