Blog

[indolering]

A lot of the essential background for understanding seL4 lives across disconnected research papers, blog posts, and talks. It might be helpful to add a blog to the website (perhaps as part of the new page) to address recurring topics and questions.

As a reference point, the commercial arm of the K-Framework group -- Runtime Verification -- does quite a bit of formal verification work and uses their blog to communicate technical information such as explaining key concepts and discuss proposals. I think a similar approach could benefit seL4 as well.

For example, in the Building a Business Case for Using a Verified Kernel panel, someone mentions the persistent myth that microkernels have inherent performance problems. The benchmarking page could certainly help (I’m hoping to contribute there soon) but a short blog post debunking the myth would give us a clear link to share whenever it comes up.

I’ve used this strategy before: I wrote a piece called For DNSSEC so I wouldn’t need to re-explain the same points repeatedly. It ended up being a handy reference that I've seen used in the wild and was even translated into other languages. A seL4 blog could serve the same purpose for common questions and misconceptions.

Maybe we could rebrand the "news" section as a blog?

[gernotheiser]

I'm tempted to agree that we don't necessarily present the most coherent story to non-experts. Getting an outsider's view and suggestions could be helpful.

Re performance: I've got some pretty compelling data (partially presented in my talk at the Summit) which I was planning to put up on the web site once I've got the cycles to do so. Probably not going to happen before next month (busy with admin and teaching).

[indolering]

I'm tempted to agree that we don't necessarily present the most coherent story to non-experts. Getting an outsider's view and suggestions could be helpful.

The solution to a puzzle is obvious when you know the answer. Usability engineers often resort to usability testing because the back-end programmers struggle to appreciate the puzzles they have created.

The website is a BIG improvement but much of the copy feels like it was borrowed from grant proposals for the DoD. AFAIU the audience you are trying to reach now consists of developers and the c-suite. It would follow that your messaging would be tailored accordingly.

Re performance: I've got some pretty compelling data (partially presented in my talk at the Summit) which I was planning to put up on the web site once I've got the cycles to do so.

I know all about benchmarking crimes and your exacting standards! Could you dump whatever you haven't presented so I could take a look at it?

More broadly, I think it would be helpful to develop a list of talking points supporters can use to respond to common objections. Other than performance, what objections and misconceptions do you commonly have to counter?

[gernotheiser]

Could you dump whatever you haven't presented so I could take a look at it?

I've just given a keynote talk at a workshop, that covers a fair bit of extra material, slides are here: https://trustworthy.systems/publications/papers/Heiser_25%3Akisv.abstract

Performance data is presented in the context of LionsOS, but in terms of networking performance it's really seL4+sDDF (and for the seL4 site it would make sense to present it as that). You'll see some back-of-the-envelope calculations that show why good performance isn't a surprise (with the right design).

[indolering]

Any video of the keynote?

I don't have the OS dev chops to ghost write this article for you. I can help with editing and dumbing it down, however. Just throwing out ideas here (don't worry about hurting my feelings) but what about breaking this into three articles?

How Not to Architect a Microkernel

Primarily concerned with addressing Mach and NT based objections. Explain why IPC overhead is not some fundamental flaw to microkernel design. Explain how seL4/LionsOS does things differently and will avoid the fate of NT/Mach.

seL4: Faster than Linux || LionsOS: Simpler, Safer, and Faster

Something of a continuation of the last article but with a focus on how LionsOS compares to Linux and why it is faster in this real-world benchmark.

Roadmap to a High Assurance Dynamic OS

An article fleshing out your vision for a dynamic OS.