Gerwin Klein

This is now breaking proofs again and the branch seems out of date with master. It looks like some of the build failures for armv8 are because of that. Can...

> My bad, will do that in future, thought it was better style to have small changes bunched up in prior commits as opposed to multiple small commits. I'll refrain...

> Actually, there is a "compare" button next to every force push log entry in Github which does exactly that. Fair enough, they do have that now. But I still...

(The proofs don't see the MCS C code yet, they are still in the stage before that, so no point in running them, really)

These changes do not look Aarch64 or SMP or HYP specific, so @mktnk3 or @michaelmcinerney might be able to say something about them from the proof side.

In particular: do we have any invariants about the release queue that say something about these two situations?

> I agree that we expect the thread is expected to be runnable when possibleSwitchTo is called, and the proofs establish that information as needed, but it is often provided...

> Hi @Furao, are you able to provide any more information about the motivation for these changes. Instructions for how we could potentially reproduce them? Ideally we'd want to add...

> It's possible to add this support optionally so that people without 3.19 don't get it, but the build still works. Since it's fairly simple JSON output, would it be...

> This discussion might be relevant: #411 Thanks for the pointer, I was looking for that one. > Is this PR a result of discussion on https://sel4.discourse.group/t/pre-rfc-to-effortlessly-develop-sel4-systems-in-rust/539/? Was there any...