riscv64: memory paging doesn't seem to work if physBase()>0

[pfzetto]

Hello,
I'm currently in trying to get microkit running on the BananaPI-F3.
Please keep in mind that I'm just starting in the seL4 ecosystem and that the issue could be rooted in a misunderstanding on my part.

The first 512 KiB of the physical address range is reserved and cannot be used for the kernel.
Therefore, physBase() starts at 0x80000.
When setting up the virtual address tables, the microkit tool skips the third level and uses 2MiB "megapages" instead.
It adds physBase() as an offset to the page address of the 2nd level page table (512KiB in the case of the BananaPi-F3).

Chapter 12.4.1 of the RISC-V Volume II: Privileged ISA Extension states:

Any level of PTE may be a leaf PTE, so in addition to 4 KiB pages, Sv39 supports 2 MiB megapages and 1 GiB gigapages, each of which must be virtually and physically aligned to a boundary equal to its size. A page-fault exception is raised if the physical address is insufficiently aligned.

Unsurprisingly the processor traps on a "Load Page fault" as soon as the kernel address (0xffffffff80080000) is loaded (due to the invalid alignment) and the system can't boot.
One fix I've tried is to round the addresses in the 2nd level page table down to 2MiB.
That allows seL4 to start partially, but seL4 fails to start fully due to a failed assertion in sel4/src/arch/riscv/kernel/vspace.c:205 (lu_ret.ptBitsLeft == seL4_PageBits).
I've also tried to increase the reserved area up to 2MiB with the same assertion error.

If you don't have other suggestions, I'll try to add a 3rd level to the generated page table.

I'm using the 15.0.0 brach (881de507fe528490dc5e570c7810a149bad5880f) of seL4 with the current main branch (dd818c11cabc86420c3a882c6730c77e47c6d030) of microkit.

Greetings
Paul

[Indanz]

It seems that RISCV should also set KERNEL_PHYS_ALIGN in seL4/tools/hardware/config.py to align physBase correctly.

Why are you running into these issues and whoever added support for BananaPI-F3 didn't?

The seL4 PR to merge BananaPI-F3 support can be found here.

[pfzetto]

I don't think that the they used Microkit.
From the Dokumentation it seems like they loaded the kernel image directly using uboot.
I think that I'm the first to add support for the BananaPi-F3 to Microkit.

The alignment issue isn't a Kernel Problem. It's an issue with the generated page tables of the Microkit tool.

[Indanz]

Ah, I misunderstood. I thought you got the fault after jumping to the kernel and it was triggered by the kernel setting up its page tables.

(Edit: Also, with the use of physBase I assumed it was kernel code, as it's a kernel thing which isn't really relevant to Microkit.)

[pfzetto]

The page fault occurs on the jump to kernel_entry because the physical address associated with the kernel entry megapage isn't aligned to 2MiB.
It isn't aligned because the Microkit loader determined first_paddr by reading the kernel.elf, which starts at physBase.

The issue in the kernel occurs after I tried to patch this bug in two seperate attempts:

1. round page address down to align with 2MiB (0x0 in this case)
2. set the Kernel Start to 2MiB (0x200000)

Both of these allow seL4 to take over from the jump and I get a few lines on the debug output until the next error occurs.

I haven't had time to debug the kernel issue, but the error message and code comments suggest that it fails to parse the megapages in the loaders page tables.