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 Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel