4 ms·
That "Verification of the multicore kernel" thing seems like it could use some bold, underline, and italics. I doubt it is as simple as adding an AArch64 model.
by microcolonel 7y ago
That "Verification of the multicore kernel" thing seems like it could use some bold, underline, and italics. I doubt it is as simple as adding an AArch64 model.
- snvzz 7y agoDefinitely not simple, but simpler than you might imagine. Specifically, I'm referring to the fact that the microkernel can't be run from more than one CPU at once and can't be preempted, which is an important design decision. Its execution time is, however, constrained into the WCET, complete with proof. And that is a very small amount of time, allowing for hard real-time applications to be built on top of seL4.
- microcolonel 7y agoEvery time I learn more about seL4, I fall a bit more in love with it. Can't wait to see what people do in terms of integration over time. I think it would be super cool to see L4Linux updated again, and on seL4 this time; maybe start shifting device drivers into tasks behind a low-overhead abstraction. We're going to have Linux and POSIX applications for a loooong time, but maybe we can make incremental progress toward something a bit less braindead.