I'm new to seL4 and I'm trying to get seL4 running on an Cortex-A7 with VE extensions (NXP IMX6UL).

One of the experiments I wish to do is measure how fast I can get from POR to seL4 doing something meningful. 

To achive optimal boot speed I have a custom bootloader that does the bare minimum.

The boot flow looks like this;

1. POR

2. Init HW

3. Load & verify blobs for trust zone and seL4

4. Jump to TEE init (OP-TEE)

5. Tee init code returns to bootloader with the CPU in HYP mode

  At this point we're back in the bootloader, there is no MMU, D cache or I cache active

6. Configure MMU

7. Jump to seL4 kernel entry

I'm currently struggling with getting the MMU properly setup and I was hoping that someone here might shed some light on

 what I would need to do. I've looked at the elf-loader and from what I can understand it will setup a basic memory-mapping 

for the kernel only. 

Some of the questions that stand out in my head are :

 1) How should the hand over work between the BL and seL4 with respect to setting up more mappings, for example IO memory. Should the PGD & PMD tables 

    created by the bootloader be shared with the kernel?

 2) What needs to be configured before calling the seL4 entry?

Thanks,

Jonas