Indan Zupancic

Yes, you're right, it's more subtle and harder to get right than it seems. Your alternative sounds reasonable, I would do whatever is easiest for verification. `updateAndCheckHandlerEP` is the only...

I like it, it's a lot less code overall. I think all corner cases are handled correctly now. Keeping `validFaultHandler` would be more code, but you could re-use the existing...

It's possible to add multiple methods for the same id to libsel4/include/interfaces/sel4.xml with the following change: ``` diff --git a/tools/invocation_header_gen.py b/tools/invocation_header_gen.py index 6590ab44ea3e..9b2ef72626ab 100755 --- a/tools/invocation_header_gen.py +++ b/tools/invocation_header_gen.py @@ -155,9...

> @Indanz , do you mean that this should make it possible to generate the calls instead of adding them to [virtual_client.h](https://github.com/seL4/seL4/pull/889/files#diff-27cfe93905ae26f3375f6ac8ecf51e55cb2d1bba941c6265cba9ff97d1f22f10)? Yes.

> Thank you for the suggestion @Indanz, those changes worked perfectly. You're welcome. > users of these syscalls now need to consciously consider whether they are setting an endpoint cap...

> A small alternative is that we could explicitly allow the combination of a null cap and a 0 badge value. That does start to feel a bit overly specific...

Only other one I can think of is: - Changing rights on a null-cap

IPI had the same undefined delay because of unrelated writes within the exclusive reservation granule problem as the global lock. I fixed it by moving all IPI state into `...

A next step could be to replace all the compiler built-in atomics with C11 standard atomics. Then we could add models of the algorithms used and check them with [CppMem](http://svr-pes20-cppmem.cl.cam.ac.uk/cppmem/).

With these lock/IPI fixes, #867 can proceed, and when that's done, then #847 (minus the MCS, SMP: Fix ipiStallCoreCallback commit) can finally be merged.