yyshen

> It may be time to consider using an alternative approach for implementing the cache maintenance operations. The `seL4_ARM_Page_Invalidate_Data` invocation potentially still needs to work even if the mapping the...

> 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...

> > 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...

> Not sure I have been following all this correctly, but any sort of cache management is a privilege. If anyone could do it, they can impact performance of other...

> > 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...

@lsf37 Which one of the three choices you would like to try out? PR #215 disables EL0 cache maintenance instructions explicitly.

> > Not sure I have been following all this correctly, but any sort of cache management is a privilege. If anyone could do it, they can impact performance of...

> > > Not sure I have been following all this correctly, but any sort of cache management is a privilege. If anyone could do it, they can impact performance...

> 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...

> > My opinion is that we find a way to place the actual mapping information into the frame cap and as part of decode reject the operation as invalid...