Hi Daniel,
The physical memory is indeed a bit strange. This is for two reasons
1. As described in the comment directly above '1 MiB starting from 0xa7f00000
is reserved by the elfloader for monitor mode hooks', so a continuous region
from 0x80000000 - 0xffffffff could not legally be given
2. A second region from 0xA8000000 - 0xffffffff could be given to capture the
rest of the physical memory in the 32-bit address space, but would be pointless
as the kernel window is 512mb on this platform
In order to work around the 512mb kernel window restriction the remaining of
the 32-bit addressable memory is given as a 'device' with the line
{ TK1_EXTRA_RAM_START, TK1_EXTRA_RAM_START + TK1_EXTRA_RAM_SIZE } in
dev_p_regs
Adrian
On Tue 20-Jun-2017 5:12 AM, Daniel Wang wrote:
Hi all,
I’m trying to get a better understand about the implementation details of seL4
for TK1-SOM.
Most of the code are very clear, but I’m little confused on the available
physical memory in TK1-SOM. I’m wondering why In the hardware.c file
(/kernel/src/plat/tk1/machine/hardware.c), the avail_p_regs[] ={.start =
0x80000000, .end = 0xa7f00000 } instead of 0x80000000 - 0xffffffff?
Thank you very much!
-Dan
_______________________________________________
Devel mailing list
[email protected]<mailto:[email protected]>
https://sel4.systems/lists/listinfo/devel
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
