Gerwin Klein

The 48 bit virtual addresses happen to match up with sizes on x64 and RISC-V 64 bit, which means that some of the generic bit field sizes (like those device...

That would need to go through an RFC, yes, but it sounds reasonably simple to do and like a good idea to support. How would the config mechanism work? An...

#410 and #975 implement most of this I think. Anything still missing, @kent-mcleod?

Thanks for getting that started, definite +1 from me to audit all that.

No blockers from the verification side, should be fine to include.

To clarify the `bug` label: there is no functional correctness problem, but it certainly is a kernel WCET problem and it is inconsistent with the intention of `preemptionPoint()`. The user-level...

> On unicore only threads with lower priority are blocked. On unicore nothing else runs, because we are in the kernel and won't get out of the kernel until `preemptionPoint()`...

@Xaphiosis what do you think would be the effort to add repeated page table entries the AArch64 proofs? My feeling is that we should first complete CRefine before we attempt...

I'm all for having them, just need to figure out how much effort they would be to verify and when to schedule that. We have done something similar for AArch32,...

> with some invariant like NODE_STATE(ksCurThread) == NULL || NODE_STATE(ksCurThread)->tcbAffinity == getCurrentCPUIndex(). If at all possible `ksCurThread` should never be NULL and always point to a valid TCB. Everything else...