Indan Zupancic

> But I really need MCS to be clean and principled. And if there are features that aren't then they need cleaning up. > >And one such principle is that...

Lines 162-165 are doing whatever is needed to run and measure a benchmark. (`cache_func` may clean cache lines or something, to make sure the test is not slowed down by...

> I’ve got a student lined up to measure and improve worst-case (really: bad-case) performance. Getting really the worst-case performance is very hard, especially on more complex hardware with SMP....

The code changes seem like a big improvement overall. Could this be also done for other architectures and have a unified page table API for all supported architectures? Could you...

> From the mapping operation itself as before. Before I used seL4_ARM_PageDirectory_Map(), but that is removed in this change. > If the lookup for the provided address stops at a...

> > Or retain seL4_ARM_PageDirectory_Map(), as doing two different operations with one functions depending on kernel state seems strange. > > Just to confirm, are you suggesting that one option...

I'm terribly sorry, I confused "page mapping" with "page table mapping". I thought you also unified page caps with page table caps. So everywhere I said page table/PT I meant...

It seems wrong to keep track of the same state in two places, and updateTimestamp() is pretty much the only caller of getCurrentTime(). If you want a check that has...

I think that if a check is done it should be in updateTimestamp(), and I agree that x86's setDeadline() should use ksCurTime. setDeadline() is only called by setNextInterrupt() which does:...

> For that issue, the Arm generic timer's virtual timer offset needs to be reset by the Elfloader in EL2 before switching to EL1 when handing over to the kernel...