From L3 to seL4 what have we learnt in 20 years of L4 microkernels? [video]

Re:From L3 to seL4 what have we learnt in 20 years of L4 mic... by vacuity on Monday April 15, 2024 @11:10PM (#40048010)

I find it unfortunate, since I think async should be the default model for communication. Similar to message passing with shared memory as an optimization, I wonder if async messaging with sync messaging as an optimization is feasible. Async in general does make reasoning about the program more difficult.

[ Parent | on HN ]

Re:From L3 to seL4 what have we learnt in 20 years of L4 mic... by ahartmetz on Tuesday April 16, 2024 @01:55AM (#40048772)

My intuition is similar to yours, but I trust people who have done the thing more than your or my intuition.

Sync seems to require very responsive receivers, which is a desired property anyway, so maybe the downside isn't that great.

[ Parent | on HN ]

Re:From L3 to seL4 what have we learnt in 20 years of L4 mic... by rurban on Tuesday April 16, 2024 @02:03AM (#40048814)

Mach (with Hurd) went down this rabbithole and utterly failed. Mailboxes were the cause of the desaster.

[ Parent | on HN ]