Use seL4_UserVSpaceTop for KERNEL_RESERVED_START by midnightveil · Pull Request #112 · seL4/seL4_libs

midnightveil · 2026-06-24T02:57:12Z

This value is consistent across platforms. Note that the previous definition incorrectly rounded down the inclusive addresses used by architectures e.g. AArch64.

Test with: seL4/seL4#1695

This value is consistent across platforms. Note that the previous definition incorrectly rounded down the inclusive addresses used by architectures e.g. AArch64. Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>

midnightveil · 2026-06-25T06:15:14Z

This PR is, strictly speaking, unnecessary: the old behaviour with seL4_UserTop works. But it was useful for testing the seL4_UserVSpaceTop changes, and if we want to consider UserTop deprecated I think we should remove uses of it if we can.

Indanz

Just one nitpick, otherwise it seems fine.

Don't merge before the seL4 change as been merged.

Indanz · 2026-06-30T12:24:37Z

+    /* we only have regions to reserve if the seL4_UserVSpaceTop is less than
+     * the top of the VA range. Why this is ever the case is beyond me...
+     * But it happens for AArch64 hyp-mode with a PA Range of 2^40.
+     */


Suggested change

/* we only have regions to reserve if the seL4_UserVSpaceTop is less than

* the top of the VA range. Why this is ever the case is beyond me...

* But it happens for AArch64 hyp-mode with a PA Range of 2^40.

*/

/* we only have regions to reserve if the seL4_UserVSpaceTop is less than

* the top of the VA range.

* This happens for e.g. AArch64 hyp-mode with a PA Range of 2^40.

*/

It's not e.g., it's the only one I know about (all the other arches worked)

I've adjusted it now aside from that.

In the case of AArch64 hyp-mode with PA_SIZE=40 bits, the kernel only allows us to use 3-level page tables, so the VA range is 0..<2^39, and so the seL4_UserTop/ seL4_UserVSpaceTop of 2^40-1 is bigger than the VA range, which causes TOP_LEVEL_INDEX(2^40-1) to report an index of 0, and hence this code marks all of the memory as kernel-reserved. Which breaks things. Previously we always rounded down the inclusive addresses that AArch64 uses and so it (by-coincidence) landed in the 511th slot of the top-level page table. Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>

lsf37 · 2026-07-01T04:03:15Z


-#define BYTES_FOR_LEVEL(l) BIT(VSPACE_LEVEL_BITS * (l) + PAGE_BITS_4K)
-#define ALIGN_FOR_LEVEL(l) (~(MASK(VSPACE_LEVEL_BITS * (l) + PAGE_BITS_4K)))
+#define BITS_FOR_LEVEL(l) (VSPACE_LEVEL_BITS * (l) + PAGE_BITS_4K)


You didn't introduce this, but this seems just wrong to me. It assumes that VSPACE_LEVEL_BITS is the same for each level on all platforms, which is not the case precisely for AArch64 hyp PA40. In that config, the top level is twice the size of the other levels and this macro therefore returns the wrong size.

I also thought page directories and page tables on AArch32 could translate different numbers of bits in some configs, but I might be misremembering that.

It assumes that VSPACE_LEVEL_BITS is the same for each level on all platforms, which is not the case precisely for AArch64 hyp PA40.

Oh! I missed that. I guessed the S2_START_L1 changes the exact size of PTs? (i.e. it's 1024 not 512 there? Or something?)

Then my comment on the bootstrap check is actually wrong: the UserVSpaceTop is not, in fact, higher than the VA size?

Yes, the top-level table under S2_START_L1 translates 10 bits, the lower ones 9. I.e. 10 + 9 + 9 + 12 = 40. Without S2_START_L1, they are all the same, i.e. 4*9 + 12 =48 (which I think means the top half of the top level is not actually usable when translating IPA to PA, both at 44 bits).

Right. Then that check should instead become an assert; if it's not true then something went wrong with our map calculations.

I suppose we should duplicate what seL4 does here:

/* Extract the n-level PT index from a virtual address: * - n is page table level counting from the root page table, * - NUM_PT_LEVELS are either 3 or 4 page table levels depending * on whether the address range being translated is 48bits, 44 bits or 40 bits. * - If translating an address in the kernel addrspace NUM_PT_LEVELS = 4 always. * - PageTables always have 512 slots (PT_INDEX_BITS = 9) but if there are only * 3 total levels then the root level is implemented with 4 concatenated tables * meaning 2048 slots (UPT_LEVELS = 3 => seL4_VSpaceIndexBits = 12) * * PT_LEVEL_SHIFT(n) == PT_INDEX_BITS * (NUM_PT_LEVELS - n) + seL4_PageBits * GET_PT_INDEX(addr, n) == (addr >> PT_LEVEL_SHIFT(n)) & MASK(PT_INDEX_BITS) */ #ifdef AARCH64_VSPACE_S2_START_L1 #define UPT_LEVELS 3 #define ULVL_FRM_ARM_PT_LVL(n) ((n)-1) #else #define UPT_LEVELS 4 #define ULVL_FRM_ARM_PT_LVL(n) (n) #endif #define KPT_LEVELS 4 #define KLVL_FRM_ARM_PT_LVL(n) (n) #define KPT_LEVEL_SHIFT(n) (((PT_INDEX_BITS) * (((KPT_LEVELS) - 1) - (n))) + seL4_PageBits) #define GET_KPT_INDEX(addr, n) (((addr) >> KPT_LEVEL_SHIFT(n)) & MASK(PT_INDEX_BITS)) #define GET_KLVL_PGSIZE(n) BIT(KPT_LEVEL_SHIFT((n))) #define UPT_LEVEL_SHIFT(n) (((PT_INDEX_BITS) * (((UPT_LEVELS) - 1) - (n))) + seL4_PageBits) #define UPT_INDEX_MASK(n) (n == 0 ? seL4_VSpaceIndexBits : PT_INDEX_BITS) #define GET_UPT_INDEX(addr, n) (((addr) >> UPT_LEVEL_SHIFT(n)) & MASK(UPT_INDEX_MASK(n))) #define GET_ULVL_PGSIZE_BITS(n) UPT_LEVEL_SHIFT((n)) #define GET_ULVL_PGSIZE(n) BIT(UPT_LEVEL_SHIFT((n)))

It's possible that the code before never tried to compute the total and never needed to know the number of bits translated at the top level, yes. That could have worked.

It wouldn't because user space doesn't manage the top level, the kernel does. All the user page tables are the same size I think.

It's possible that the code before never tried to compute the total and never needed to know the number of bits translated at the top level, yes. That could have worked.

It wouldn't because user space doesn't manage the top level, the kernel does.

The user does manage all levels: it has to retype top-level page tables and know their size (apart from the initial thread), and it can map pages into the top level, depending on architecture.

All the user page tables are the same size I think.

It's a bit of a wild assumption to make given how diverse page table structures are, but it's possible that it works out for what we currently support, because for all the 32 bit architectures we have (where there is just chaos, really), there are only 2 levels in total, and the 64 bit architectures all seem more sane.

What I mean is that the number of index bits for each non-top level page table determines how many bits it resolves and hence is relevant for page table management in user space. For intermediate levels you need to know the boundary between sibling page tables, because that determines whether you need to allocate a new page table or can keep using the exiting one. There is always only one top level, so user space doesn't need to care about how many index bits it has.

Well, it's no coincidence that everyone ends up being compatible in choosing page sizes. Either explicitly to be compatible and reduce the porting pain, or by making the same trade-offs and ending at the same result. And once you have that, using a small page sized area for one page table level is only natural. And if you try to be as space efficient as possible, with 4k pages you end up with 10 bits index for 32-bit and 9 bits index for 64-bit platforms. The top level being a different size is much easier to deal with.

And if you try to be as space efficient as possible, with 4k pages you end up with 10 bits index for 32-bit and 9 bits index for 64-bit platforms. The top level being a different size is much easier to deal with.

But of course those numbers are not true AArch32 EL2 for instance. The assumption that all page table levels underneath the top-level at least amongst themselves translate the same number of of bits still works, because there is only one such level on AArch32 (but that number is different between EL1 and EL2 tables).

AArch32 HYP uses Large Physical Address Extension (LPAE) for 40-bit physical address space, so I would count that as a 64-bit platform as far as address translation goes.

lsf37 · 2026-07-01T04:15:31Z

+     * a PA Range of 2^40. Otherwise, we would be reserving random indices
+     * at the bottom of the virtual address range due to wrapping.
+     */
+    if (seL4_UserVSpaceTop <= VSPACE_VA_TOP) {


Just to double-check, the reason this works now is because seL4_UserVSpaceTop is not <= VSPACE_VA_TOP on AArch64 hyp PA40? I.e. it's not trying to access the TOP_LEVEL_INDEX, which in this case would be 0. Is that correct?

If we fix the macro above, VSPACE_VA_TOP would become mask 40, which should be the same as seL4_UserVSpaceTop for that config, which means the condition is now true.

The code overall seems a bit strange, because there are no kernel reserved regions in EL2 kernels, neither on AArch32 nor AArch64. Maybe it happened to work out before because it unnecessarily reserved one entry for the kernel even though it didn't need to, not sure.

So maybe the condition should instead be on CONFIG_ARM_HYPERVISOR_SUPPORT? I think currently all other kernel configs do have reserved regions in the top-level table.

It might have been working out for PA44, because the top half of the top table is reserved because IPAs are 44 bits, not 48 bits (and the table could otherwise translate 48 bits).

Which means my condition on just CONFIG_ARM_HYPERVISOR_SUPPORT would be wrong, because I guess the library should know that it can't allocate there (not because it is kernel-reserved, just because these addresses don't exist on that hardware).

Maybe it happened to work out before because it unnecessarily reserved one entry for the kernel even though it didn't need to, not sure

Yes, it was, because of the round down of the AArch64 inclusive value.

It might have been working out for PA44, because the top half of the top table is reserved because IPAs are 44 bits, not 48 bits (and the table could otherwise translate 48 bit

Yeah, it was like 0x1f vs 0x20.

I printed these out: seL4/seL4#1695 (comment)

Indanz · 2026-07-03T10:17:48Z

All hw tests fail with "No 'HW_SSH' key provided", not sure what's going on.

I would like to see a successful test before merging this, just in case.

lsf37 · 2026-07-03T10:32:10Z

All hw tests fail with "No 'HW_SSH' key provided", not sure what's going on.

Apparently we have never done a PR hw-test from this repo, the access to the machine queue keys wasn't configured. That's now done and I have restarted the test.

lsf37 · 2026-07-03T10:41:38Z

We should not merge it like this, even if it happens to work. The macro VSPACE_VA_TOP is definitely wrong.

Use seL4_UserVSpaceTop for KERNEL_RESERVED_START

e2095b6

This value is consistent across platforms. Note that the previous definition incorrectly rounded down the inclusive addresses used by architectures e.g. AArch64. Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>

midnightveil mentioned this pull request Jun 24, 2026

libsel4: add new seL4_UserVSpaceTop constant seL4/seL4#1695

Merged

Indanz reviewed Jun 24, 2026

View reviewed changes

Comment thread libsel4utils/include/sel4utils/vspace.h

lsf37 reviewed Jun 25, 2026

View reviewed changes

Comment thread libsel4utils/src/vspace/bootstrap.c Outdated

midnightveil force-pushed the julia/user-vspace-top branch from 39daf24 to 0ea9e2f Compare June 25, 2026 05:15

midnightveil requested a review from Indanz June 30, 2026 07:42

Indanz approved these changes Jun 30, 2026

View reviewed changes

midnightveil force-pushed the julia/user-vspace-top branch from 0ea9e2f to 56304ce Compare July 1, 2026 02:31

midnightveil requested a review from lsf37 July 1, 2026 02:31

lsf37 reviewed Jul 1, 2026

View reviewed changes

Indanz added the hw-test sel4test hardware builds + runs for this PR label Jul 2, 2026

midnightveil mentioned this pull request Jul 8, 2026

IOMMU: Add IOMMU Support seL4/rust-sel4#358

Merged

midnightveil removed the hw-test sel4test hardware builds + runs for this PR label Jul 8, 2026

midnightveil marked this pull request as draft July 8, 2026 09:55

Conversation

midnightveil commented Jun 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

midnightveil commented Jun 25, 2026

Uh oh!

Indanz left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

midnightveil Jul 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lsf37 Jul 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lsf37 Jul 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Indanz commented Jul 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

lsf37 commented Jul 3, 2026

Uh oh!

lsf37 commented Jul 3, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

midnightveil commented Jun 24, 2026 •

edited

Loading

midnightveil Jul 1, 2026 •

edited

Loading

lsf37 Jul 3, 2026 •

edited

Loading

lsf37 Jul 1, 2026 •

edited

Loading

Indanz commented Jul 3, 2026 •

edited

Loading