Indan Zupancic

In this case it's far from obvious how it's generated and grepping the source directory doesn't really work (I tried). Grepping the build directory works slightly better. What CMake build...

Sounds good, but that seems far from trivial because of the many layers of indirection. If all build/%_gen.h files are always generated from a corresponding kernel/%.bpf file perhaps a generic...

If compiling with "-march=armv8.1-a" or "-march=armv8-a+lse", `__atomic_exchange_n()` will [automatically](https://godbolt.org/z/9e4q6b4zx) use `swpal`, so I think platforms with v8.1 should add "lse" to `KernelArmMachFeatureModifiers` instead.

seL4 probably wants to pass the `-mno-outline-atomics` GCC option and set the cpu flags correctly.

You're right, libsel4/autoconf/autoconf.h also includes sel4/gen_config.h.

> I wonder, what are the rules concerning the c_entry_hook() actually. Seems this nicely get's along everywhere, so there are no immediate issues. Yes, I noticed that too. I've been...

> It does seem like c_handle_enfp not acquiring a lock on SMP is a bug as it does access a lot of state that could be being torn down by...

Interestingly, a test I added recently triggers an assertion with this branch: ``` Running test SCHED_CONTEXT_0014 (Test deleting a scheduling context while it runs out of budget on another core)...

For proper SMP verification I think it should be proven that anything outside the global lock only touches node-local data, with the exception of bootup. For non-formal proof the compiler...

> Interestingly, a test I added recently triggers an assertion with this branch: > > ``` > Running test SCHED_CONTEXT_0014 (Test deleting a scheduling context while it runs out of...