Hi Damon,
Thanks for getting back to me.
For clarity, I am attempting to get this working on an Odroid XU4. This has been working generally, however I noticed that the overlay dts file doesn't seem to map the full memory region that the linux kernel and u-boot assume to be there. In the DTS file providedhttps://github.com/hardkernel/linux/blob/odroidn2-4.9.y/arch/arm/boot/dts/ex... by hardkernel linux the following memory region is defined:
memory@40000000 {
device_type = "memory";
reg = <0x40000000 0x7EA00000>;
};
And from the U-Boot DTS filehttps://github.com/hardkernel/u-boot/blob/odroidxu4-v2017.05/arch/arm/dts/ex..., essentially the same region is defined as:
memory {
device-type = "memory";
reg = <0x40000000 0x10000000
0x50000000 0x10000000
0x60000000 0x10000000
0x70000000 0x10000000
0x80000000 0x10000000
0x90000000 0x10000000
0xa0000000 0x10000000
0xb0000000 0xea00000>;
}
However the overlay dts filehttps://github.com/seL4/seL4/blob/master/src/plat/exynos5/overlay-exynos5422... provided for the XU4 in the seL4 kernel only reflects a small amount of this memory region:
/* HACK: 0xe0000000..0xff000000 is the largest contiguous region
* in the kernel window; we clamp to that and discard memory
* after the ASID PD hole (0xff200000..0xfff00000). This is a
* workaround for userspace tools (hardware_gen, elfloader, etc)
* which are not yet aware of the memory hole. */
memory@40000000 {
reg = <0x60000000 0x1f000000>;
};
vm-memory@40000000 {
reg = <0x40000000 0x20000000>;
};
Q: Why are there two separate memory regions defined here?
Q: Why is the bulk of the memory provided by the device missing from this file?
Q: The comment that states that this file contains a hack to get around an ASID memory hole, however I don't understand how that hole can exist on this platform, as the memory is supposed to be contiguous from 0x40000000 to 0xbea00000?
Q: I also don't understand how the addresses stated in the comment have anything to do with the XU4's memory region, as the addresses referenced are far higher than the 0xbea00000 address at the end of the XU4's memory region?
Q: How is the kernel load address determined? From my investigations it seems this is simply the first memory region defined in the overlay file (which may explain why there are multiple) however when I attempt to change that region to anything other than 0x60000000 it doesn't seem to work.
I have added the missing memory regions manually, and have had varying success in using different memory regions. For example, I have been able to declare memory from 0x80000000 and up, and specify that as the VM_RAM_BASE which works (wihout python3 installed).
Q: Out of the available memory region (0x40000000 - 0xbea00000), what can I use and what constrains the kernel load address within this available memory?
I have done as you asked and the resulting boot sequences can be found at:
* No-Pythonhttps://pastebin.com/Gnp4bEmG
* With-Pythonhttps://pastebin.com/ZGvsxzFF
The only thing that I can see from this extra logging that may hint at something not being quite right is on line 756 where it attempts to create an object from untyped 0...
I appreciate your help, and hopefully you can shed some light on the other questions I have raised.
Kind regards,
Ben Turner
________________________________________
Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group.
Registered in England & Wales. Registered No: 00267550
http://www.roke.co.uk
_______________________________________
The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and
must not be passed to any third party without permission. This communication is for information only and shall
not create or change any contractual relationship.
________________________________________
From: Lee, Damon (Data61, Kensington NSW)