Indan Zupancic

> just my 2 cents: ecall (the ultimate generic option) on an 100MHz cpu should be around 0.7usec Well, it was bad enough to occasionally fail a clock synchronisation [test](https://github.com/seL4/seL4/pull/863/commits/9721150dcbb982e3f824c480cf6e46a5ba2c05d6)...

The only thing special is `rdtime` being emulated and extremely slow, hence the need for falling back to MTIME. If a hardware implementation of `rdtime` was mandatory we wouldn't have...

I fully agree with this and I always wondered why it is like it is, especially because you really want to use the register-only versions of the IPC functions instead...

The confusing bit is how Elfloader, sel4test and sel4test and the user libraries all depend on other stuff like the kernel and each other. E.g. the UART you need to...

@axel-h already [mentioned](https://sel4.discourse.group/t/kernel-crash-on-x86-but-not-on-x86-64/398/11) in 2021 that this issue should have been solved with plain ASM instead of troublesome naked attribute, so I'm not sure why that wasn't done then and...

You don't have to shoehorn every use case into Microkit via explicit support. All you need is a way to pass specific caps to PDs. (And if you add the...

No? Camkes doesn't support any of that as far as I know. Perhaps you meant capDL. But Microkit is already re-inventing capDL as it does similar things. I don't know...

Mat from Neutrality created some proof-of-concept patches a while back. Motivated by the summit talk he published them: - [Add support for passing Untypeds to PDs](https://github.com/Neutrality-ch/microkit/commit/79bae8efc0e03102232942957c804bf8a4d1d868) - [Add support for...

> Right now I imagine the majority of our users wouldn't know what to do if we gave them untypeds and access to CNodes, the whole reason they're using the...

binutils 2.36 or newer is required according to [this](https://reviews.llvm.org/D96838), otherwise you get that warning. There is a bug report by the same llvm dev for gcc 11 here with some...