Open Ivan-Velickovic opened 1 year ago
One observation is that the kernel doesn't track whether a mapping is cached or uncached. I wouldn't expect the architecture to have a problem with cache maintenance operations on mappings that are uncached, but maybe the seL4 design would wish to block cache maintenance operations on uncached mappings done through the vspace cap?
If seL4 doesn't care and the hardware doesn't care, why bother?
If seL4 doesn't care and the hardware doesn't care, why bother?
It's not blocking now, but the point is that there could be an ambient authority situation where an uncached mapping implies an authority to manage caches for that mapped region. But you're right its probably a non-issue at this point because seL4 already doesn't care in other ways (ie there's no rights for restricting the ability to map something cached vs uncached).
@Indanz can you please check if you're now happy with Ivan's changes?
While we're expecting the tests to currently fail, it looks to me like some of the operations are returning a different kind of error, e.g. cap lookup fault instead of illegal operation.
While we're expecting the tests to currently fail, it looks to me like some of the operations are returning a different kind of error, e.g. cap lookup fault instead of illegal operation.
yea I don't know what's going on. I'll have a look tomorrow.
(rebased and tweaked under which configs we should expect an error)
Now passes on all runs for all boards. We still need to fix up the review comments, though.
This PR aims to add test coverage for https://github.com/seL4/seL4/issues/214. More specifically. it implement tests for the scenarios outlined here: https://github.com/seL4/seL4/issues/214#issuecomment-1558628554.
I have left out testing of
VMKernelReadOnly
mappings as I believe there is no way to produce this mapping from user-space.