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.