Robbie VanVossen

> I think the mechanism behind SMP + domains needs some design rationale documentation. Ideally we'd do this in an RFC, since this is basically a new feature and how...

Fixed some issues reported by the style checker.

We were using MCS on multicore AARCH64 VMM. We ran into issues without these changes. We implemented these a bit ago, but I am working to see if I can...

https://github.com/seL4/seL4/commit/6a35bf9ee8367e4aca53204fb317f612f10bfbe5 The issue seems to occur when I have multiple VMs running on the same core. Also, the assert doesn't always seem to print, but I always halt when I...

https://github.com/seL4/seL4/commit/d64d1f1dac6de0f4ca2683d55e809f9bb363cb6e This issue seems to occur when we have a a VM that is running on multiple cores. See the log here: [tcb_in_release_queue_error.log](https://github.com/seL4/seL4/files/7676514/tcb_in_release_queue_error.log)

> Ideally we'd want to add a sel4test case that reproduces the problem and reliably shows its absence when fixed. @lsf37 We tried to work on some test cases for...

> I'd started looking into reproducing this, but found that the camkes-vm doesn't support MCS yet. This means there's not a way to reproduce MCS + Hyp + SMP with...