Thanks for your response. Yes, support for the MaaXBoard is now part of the seL4 mainline (I'm part of the team that added support). For GICv3 we’re using the “sylvain/gicv3” branch of the seL4_projects_libs repo which provides (experimental) support for GICv3 to the CAmkES VMM. Any hints or suggestions on how to progress investigation of the page fault’s underlying cause would be greatly appreciated. Bes regards, Stephen

On 14 Jun 2022, at 18:35, Indan Zupancic wrote:

***This mail has been sent by an external source***

Hello Williams,

On 2022-06-09 17:10, WILLIAMS Stephen via Devel wrote:

...

We’re currently working on formalising VM support for an iMX8 platform (the Avnet MaaXBoard) building upon the existing sylvain/imx8 and sylvain/gicv3 branches.

Mainline seL4 already has support for maaxboard.

AFAIK only thing missing is support for GICv3 in camkes' VMM.

Greetings,

Indan

This message contains information that may be privileged or confidential and is the property of the Capgemini Group. It is intended only for the person to whom it is addressed. If you are not the intended recipient, you are not authorized to read, print, retain, copy, disseminate, distribute, or use this message or any part thereof. If you receive this message in error, please notify the sender immediately and delete all copies of this message.

Hi Stephen, PC 0x200 indicates that the guest has triggered a synchronous exception as according to the architecture manual, Table D1-7 Vector offsets from vector table base address, offset 0x200 maps to Synchronous exception at current Exception level. This causes a prefetch fault as IPA 0x200 doesn't correspond to physical memory in the guest. This indicates that the error has happened very early in the linux boot and it has been unable to create its own virtual mappings and load its own vector handling functions yet. Considering that x0 holds the address of the DTB the guest exception probably happened pretty soon after starting the VM. Maybe its original load address is incorrect or the initial program counter isn't set to the start of the guest image. You can query the guest's fault registers from the seL4 VCPU object to get more information about what the original fault was: seL4_VCPUReg_ESR, seL4_VCPUReg_FAR seL4_VCPUReg_VBAR are some of the register fields that can be returned by a call to seL4_ARM_VCPU_ReadRegs() (https://docs.sel4.systems/projects/sel4/api-doc.html#read-registers-1). On Wed, Jun 15, 2022 at 11:33 PM Indan Zupancic wrote:

Hello Williams,

On 2022-06-09 17:10, WILLIAMS Stephen via Devel wrote:

...

Any suggestions as to the possible cause of the page fault or hints on how to progress with debugging this issue would be greatly appreciated.

Although we don't use camkes' VMM, we had to change our VMM for recent Linux kernel changes, perhaps you're running into the same issue:

- Do not fault on reserved GIC register accesses, but return 0 instead. Newer Linux will check for GICv4 support. - Honour Linux's text_offset instead of hard-coding 0x80000. Newer Linux uses 0x0 instead of 0x80000.

But the above only applies if the fault address is within the GIC device or if Linux crashes immediately, and both are independent from GICv3 itself.

"read prefetch fault @ PC: 0x200 IPA: 0x200" seems to indicate that Linux is trying to execute code from address 0x200, which is probably not what you want.

Greetings,

Indan _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems