+/* With 4K pages, we use section maps. */
/*
* ARM64 kernel is guaranteed to be loaded at 2M aligned
* address (as per booting requirements). Hence we can use
* section mapping with 4K (section size = 2M) and not with
* 16K(section size = 32M) or 64K (section size = 512M).
*/
That sounds much better. I hadn't figured out why myself, so thanks for
the explanation :)
However, there's one minor nit: the start of memory below the kernel is
2M aligned, but the offset means that the kernel itself is not loaded at
a 2M aligned address.
So how about:
/*
* The linear mapping and the start of memory are both 2M aligned (per
* the arm64 booting.txt requirements). Hence we can use section mapping
* with 4K (section size = 2M) but not with 16K (section size = 32M) or
* 64K (section size = 512M).
*/