We are running a survey to help us improve the experience for all of our members. If you see the survey appear, please take the time to tell us about your experience if you can.
I can't comment on Linux, usually at the point the OS starts my job is done.
On the MMU side, each core has its own independent MMU. So having different mappings shouldn't be a problem.
My main concern are the things both OSes must share, that is the IC and the SCU.