I imagine this isn't the right place for this, but i can't find a better one.

The correct one is this (devel@sel4.systems)

I see the performance comparisons at http://l4hq.org/docs/performance.php are run on all different processors. In its current form, the performance numbers here are completely useless. It would be very informative to have real performance benchmarks where the exact same processor is used for every OS in comparison. Otherwise, what am I supposed to do with those number?

You’re right that comparisons across different processors are of limited power, but they aren’t useless either, especially when expressed in cycles (and ideally coupled with an understanding of the underlying hardware, eg the insane pipeline depth and speculation of the Pentium 4).

However, given that these are different implementations spanning 20 years (some written in assembler), it isn’t possible to run them on the same hardware.

The key observation is that no-one has ever done better on any of those processors.

Gernot