Hi all, I’m trying to understand the implementation details and physical memory usage of seL4 for Tx1 we have available physical memory in Tx1 is 6GB. DRAM (4GB) - available address range 8000_0000 - FFFF_FFFF DRAM2 (4GB to 6GB) - available address range - 1_0000_0000 - 2_7FFF_FFFF In the hardware.h file (/kernel/include/plat/tx1/plat/machine/hardware.h),the avail_p_regs[] ={.start = 0x80000000, .end = 0xa7f00000 } '1MiB starting from 0xa7f00000 is reserved by the elfloader for monitor mode hooks'.I understand from the code its required only for Tk1. (/projects/tools/elfloader-tool/src/plat/tk1/monitor.S). As per my understanding is not not applicable for Tx1 so we can use contiguous region of physical ram 2GB to 4GB. Also it's allow to use higher physical memory for seL4 kernel ie > 4GB ? Thanks in advance. Regards, Munees