Gerwin Klein

> It depends if an error would be returned to the caller. If we could simply ignore invalidate without write permission, putting the check in invalidateByVA is OK. But this...

The operation currently requires a FrameCap that covers the area to be flushed. So that part was fine. It did not require further permissions (`write`), though, which is a problem....

> This is seL4_ARM_VSpace_Invalidate_Data(vspace, start, end), which takes a top level page table cap as the first argument. Right, I've been staring at the wrong operation then :-). I thought...

> We only need to check the requested range [start, end). This is where we could put a size limit on the operation: for each invocation, the kernel only processes...

Not sure yet. @kent-mcleod do you have any opinions?

So many points :-). I'll make separate comments for each. >> @kent-mcleod, you have a point that always requiring write for a flush may be too much -- although in...

> @lsf37 My apology here. I just looked at the code; there is check in the kernel to ensure the start and end addresses are in the same page in...

Some thoughts on the previous options, mostly in case we want to come back to them for other such situations: - taking a kernel exception during the `perform` phase: one...

Yes, I think that is a good plan. The only remain question for me is if all architectures require write permission, and for which operations specifically.

After wiping the new instance that showed the same problem, starting from scratch and sanitising the data gained from `mmctl export`, and then importing again, it looks like we may...