[andai]

What do they use for that? BSD?

[pclmulqdq]

The ones that use an OS generally use seL4 these days.

[andai]

Thanks. "OS considered harmful" is a satisfying answer, too!