Hi Munees, I'm not sure why the TX1 has such a small amount of memory specified. Presumably it was just copied from the TK1 and no one got around to updating it. Certainly more memory can be specified, although I would take into account a couple of things * Whilst we do not currently setup a monitor for the TX1, we may wish to in the future so I would keep that 1MiB hole * The kernel has no problems using the memory >4GiB, but that memory cannot be used by DMA controllers and so any user level managers and allocators need to be aware of this when providing memory to drivers that will be performing DMA Adrian On Wed 13-Dec-2017 9:03 PM, Muneeswaran Rajendran wrote:

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

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel