Support full 48-bit PA on AArch64

[heshamelmatary]

Currently the non-hyp AArch64 port only supports up to 47-bit Physical Address (PA) space due to how virtual memory mapping is implemented and a bitfield generator limitation with device untyped. It does not support 48-bit PAs accordingly. This issue was discussed in #1157 and #1163 when trying to add support for Morello platform that has 48-bit PA. The main (quoted) takeaways are:

• Device untyped represented in the seL4 capability still uses virtual canonical addresses (capPtr ) even though they are not mapped.
• The only way to relax that would be to find all places where that happens and to make special cases, comparing physical instead of virtual addresses in those case. This solution will require major verification efforts.
• One of the assumptions that the 64-bit kernel design currently makes is that the kernel window is large enough to hold all of addressable physical memory. With 48 bits of addressable virtual memory, 47-bit PA limit is probably the larges as there needs to be parts of the kernel virtual address space that isn't used for the direct mapping window. Getting larger than 47-bit would probably require a different approach for the kernel window mapping.
• In hyp mode (which support 48-bit PA), the kernel uses a separate page table for the kernel mappings. This could be a solution if armv8 would support that in non-hyp mode as well.

[Indanz]

How long before the first ARM system actually has more than 128 TB of SDRAM memory and this becomes a practical problem?

Virtual address space size seems to be 52-bits in Aarch64, so there seems enough room to have a 48-bit PA. The actual problem is that seL4 artificially limits VA to 48-bits, see the comment in src/arch/arm/64/model/statedata.c:

/* AArch64 Memory map explanation:
 *
 * EL1 and EL2 kernel build vaddrspace layouts:
 *
 * On AArch64, the EL1 and EL2 builds of the kernel both use approx 512GiB of
 * virtual address space.
 *
 [...]
 * Common Aarch64 address space layout:
 *
 * The reason why 512 GiB was chosen is because assuming a 48-bit virtual
 * address space using a 4KiB Translation Granule (and therefore, 4 levels of
 * page tables):
 *
 * One top-level page-structure entry maps 512 GiB, so by limiting ourselves to
 * 512 GiB, we only need to pre-allocate 1 level0 table (lvl0 is the top level),
 * 1 level1 table, 512 level2 tables (with each level2 entry mapping 2MiB), and
 * skip level3.
 *
 * We do maintain a single level3 table however, which is mapped into the last
 * entry in the last level2 table, such that the last 2MiB are mapped using
 * 4KiB pages instead of 2MiB pages. The reason for this last 2MiB being mapped
 * using small pages is because this last 2MiB is where the kernel maps all the
 * different devices it uses (see map_kernel_devices()). This implies that the
 * kernel can only have up to approx 512GiB of kernel untypeds.
 *
 * If you wish for your AArch64 platform to use more than 512 GiB of virtual
 * memory, you will need to change the number of pre-allocated page tables below
 * to be sufficient to contain the mapping you want. And don't forget to update
 * this comment here afterward.

So I think the better solution is to add support for more than 48-bit VA, not to shoehorn 48-bit PA on top of 48-bit VA, which happens to work for HYP. This would also make it possible to support future bigger PA spaces.

If systems like that are actually used it wouldn't surprise me if 64k page support is wanted too.

[lsf37]

The 48 bit virtual addresses happen to match up with sizes on x64 and RISC-V 64 bit, which means that some of the generic bit field sizes (like those device untyped addresses) are shared and 48 bit wide.

The sharing is mostly for convenience, it's probably possible to add another case there for 52, but we'd have to check if there is sufficient space in all caps for instance. Most look fine and have padding left, but cnode_cap looks like it might not have enough, at least without looking into further storage tricks.

With 3 cases for each pointer storage location it might be time to add an expression language to the bitfield generator, so that we can compute padding instead of having to add a preprocessor IF everywhere.