This seems to imply that seL4 is faster than FreeBSD, Linux, Windows is this what was intended to be conveyed?
That said I don't think data exists to show that SeL4 is faster than mainstream OS kernels just much faster than research microkernels which have always been much much slower than mainstream monolithic kernels.
In fact one would reasonably suppose that it would be measurably slower due to increased overhead. This may well be well worth it but this doesn't mean we ought to engage in speculation not backed by data.
The way that microkernels are sometimes slower is, as I said above, on operations that monolithic kernels implement internally, but microkernels leave to userspace processes. For example, ping-pong IPC is something you can measure on L4, and reliably get orders of magnitude better performance than on Linux. But creating a file isn't, because L4 itself doesn't have files—you can implement them in userspace, and that can be done with varying degrees of extra overhead. It might still come out about even with Linux (I think I've seen some results to that effect) but it probably won't be orders of magnitude faster.
The part of your comment I agree with is that measuring performance is complicated.
Seems to be a pretty broad claim without anything to back it up.
First, by omitting the immediately previous qualifier from your quote: "when it comes to fundamental OS services, seL4 is more than an order of magnitude faster...". This omission turns my correct claim into a plausibly false one, one which I have specifically disclaimed, in detail, in three separate comments in this thread already, in order to avoid the kind of confusion that could reasonably produce reactions like yours. The "benchmarks of software performing an actual useful task on both a mainstream OS and SeL4" you ask for are relevant to the plausibly false claim, but not to the correct claim I was actually making.
Second, you falsely claim that I am saying things without anything to back them up. This would be a legitimate criticism if I were talking about performance numbers for some kind of trade secret software, but in fact (with the exception of Microsoft Windows) all of the operating systems discussed here (seL4, FreeBSD, Linux, plausibly Fiasco.OC and Mach) are open source and have abundant published benchmarks, including many in the seL4 papers published by the dude whose blog post we are discussing. There is a very great deal of freely available evidence.
In short, you are lying about what I am saying, and you are lying about the available evidence for evaluating its veracity. Therefore I think the presumption of good faith on your part in this conversation can be soundly dismissed.
I'm not lying about what you said. I even copied the longer section of your quote in the prior post aside from the entire thread being right above on my device and yours.
I'm also not lying about the availability of evidence to prove your claim just asking you to provide a link to such.
You spoke with authority and then get upset and wave your hands about yelling LIAR when asked for supporting links.
Perhaps begin again respectfully or cease discussing.
Running a web browser directly on a microkernel is a reasonable thing to do, and it's likely that Fuchsia will end up doing it, but it will involve a lot of work.
The performance expectations of JS generally do not have anything to do with the operating system, but as explained in the post, when it comes to fundamental OS services, seL4 is more than an order of magnitude faster than even other microkernels, much less FreeBSD, Linux, or Microsoft Windows.
Microkernels generally need higher performance for those things because operations such as read(), which involve just a system call on a monolithic kernel, with context switches into and out of the kernel, involve a full context switch to a separate server process and back on a microkernel.