RFC-24: Add support for Intel APICv

[dreamliner787-9]

This RFC proposes adding in-kernel support for Intel APICv.

Rendered version here: https://github.com/au-ts/seL4-rfcs/blob/x86_apicv/src/proposed/0240-x86_APICv.md

Prototype kernel implementation: seL4/seL4@master...au-ts:seL4:x86_vmm_dev
Example Microkit integration: seL4/microkit@main...au-ts:microkit:apicv_poc
Example usage in our VMM: au-ts/libvmm#198

[midnightveil]

Comment on the implementation: you also need to store the deriveCap from the decode somewhere in a CNode (like with the various TCB methods that do cteInsert. is there an equivalent mini-cnode in the VCPU?). Otherwise, you've still created a use-after-free like ability. Just the deriveCap isn't good enough as it does not store permanent state.

Do we have a place to store those caps at this time? Does that need to be added?

[Indanz]

Why is a new syscall needed? Why can't you just add the VMX_CONTROL_APIC_ACCESS_ADDRESS and VMX_CONTROL_VIRTUAL_APIC_ADDRESS to the set of registers that are context switched and modifiable by the VMM?

invokeVCPUSetAPICvPages just sets those two registers and decodeVCPUSetAPICvPages doesn't do any interesting checks anyway.

Then the diff is really minimal and there isn't really a need for an RFC at all.

Edit: Ah, because those registers take a host physical address, not a guest virtualised address. How inconvenient.

Well, in that case, you totally forgot about cleanup, like Julia already pointed out.

[Indanz]

You don't need to derive caps and embed them anywhere. Such caps are currently not used to cleanup the TCB when the other objects goes away.

In this case, if the TCB goes away, you don't have to do anything. But you do need to clear the VMX registers when the page objects goes away. We can't look up the TCB/VCPU by ASID, as the VSpace may be shared by multiple instances.

In many ways it's similar to the IPC buffer. There the problem is solved by checking the IPC buffer cap every time it's used, but that approach doesn't work here.

If the cap is embedded, on delete of a frame cap you could check if the cte_t is embedded (special flag in cte_t or cap). From there you could retrieve the encompassing TCB object. (This trick could also be used to avoid checking the IPC buffer cap on each call.) However, finaliseCap doesn't get the cte_t, only the cap data, it's necessary to change finaliseSlot to handle this case. I implemented this approach here for an unfinished proof-of-concept.

If the frame is part of the VCPU you still need a way to get derived frame caps. Such derived frame caps must be child objects of the VCPU, otherwise you get use-after-free when deleting the VCPU object. But that's the only tricky bit of this approach. All-in-all this approach seems much simpler, as you don't need to modify common code.

[Indanz]

I think seL4/seL4#1098 is more important, as that fixes security problems, while this is just an optimisation.

[Ivan-Velickovic]

I think seL4/seL4#1098 is more important, as that fixes security problems, while this is just an optimisation.

While we want to have that PRs changes as well, isn't it completely separate to the RFC?

[lsf37]

I'm unclear on what exactly needs to be cleaned up when. There are two scenarios to consider: a) the frame caps that the user has provided are deleted and b) the VPCU object is deleted. I don't think TCBs are involved, although maybe that is different on x86 (I'm mostly familiar with the Arm model). For a), how do we find the connection to the VCPU where we changed hardware state that causes writes/reads to those frames? For b) how do we find the corresponding frames? (do we need to? currently I don't think so, but as soon as a) is fixed there is likely information that needs to be cleaned up from the other direction).

The currently implementation in seL4/seL4@master...au-ts:seL4:x86_vmm_dev is clearly broken for the case a), though. At the very least integrity is broken, but I'm pretty sure I can make the kernel crash with it. I think this is what Julia meant, but just storing derived caps does not fix anything yet. We also don't really need to store caps for tracking connections, a pointer is good enough, but it needs to be pointers in both directions.

For Indan's proposal: we definitely do not want flags in CTEs. Maybe there is something we can do with caps analogous to the mapping information for frames in page tables, but it does sound like a hack.

In seL4 in general, if two objects are bound to each other like here, there needs to be storage available for that binding on each side. If one of those objects is just a frame, that is not possible, and so I don't see how this proposal can work. The user is simply not providing enough storage for the kernel's book keeping.

[Indanz]

While we want to have that PRs changes as well, isn't it completely separate to the RFC?

Technically yes, but from a manpower point of view, no, as both are x86 virtualisation related.

In seL4 in general, if two objects are bound to each other like here, there needs to be storage available for that binding on each side. If one of those objects is just a frame, that is not possible, and so I don't see how this proposal can work. The user is simply not providing enough storage for the kernel's book keeping.

The missing information can be provided implicitly by embedding the cte_t in the object you are looking for.

For Indan's proposal: we definitely do not want flags in CTEs.

Alternatively, a pointer to the slot could be passed to finaliseCap, but my impression was that that would complicate existing already complicated proofs, while adding an extra cleanup step seemed simpler.

Once you do the above trick, it's much cleaner to mark embedded CTEs explicitly with a flag in mdb_node_t than to infer that from the cap data, because that keeps the generic cap code generic. We already have mdbRevocable and mdbFirstBadged, this would be a new mdbEmbedded.

The flag would be used in finaliseSlot to check whether a cap might need additional cleanup before calling finaliseCap. It would replace checks like this with a generic check and then call unlink_slot or something like that, which does the cap type check and clears the mdbEmbedded flag.

Maybe there is something we can do with caps analogous to the mapping information for frames in page tables, but it does sound like a hack.

The only clean alternative I can think of is to expand MDBs to have two next and prev pointers so multi-parent relationships can be tracked properly. Ideally this could replace the current ASID hacks we have too. But it would double the size of caps, which is not entirely bad either, because space in caps is already tight.

[lsf37]

In seL4 in general, if two objects are bound to each other like here, there needs to be storage available for that binding on each side. If one of those objects is just a frame, that is not possible, and so I don't see how this proposal can work. The user is simply not providing enough storage for the kernel's book keeping.

The missing information can be provided implicitly by embedding the cte_t in the object you are looking for.

No, that is not a good way to embed that information. Embedding ctes in random objects can violate all kinds of assumptions that other code makes. Since this is not verified code I would do something like this only under extreme circumstances. The proofs make essential use of the fact that CTEs can only live in CNodes and TCBs (and that was already not a good idea if you ask me), and extending that breaks every argument that makes that case distinction. That's hundreds. That means, if this feature is without proof (and it has to be, because VT-x is already without proof), there is no reason to believe that all those hundreds of arguments would extend naturally. That in turn means this feature would be messing with the central authority mechanism of the kernel and could break not only the thing it extends, but everything else.

For Indan's proposal: we definitely do not want flags in CTEs.

Alternatively, a pointer to the slot could be passed to finaliseCap, but my impression was that that would complicate existing already complicated proofs, while adding an extra cleanup step seemed simpler.

Once you do the above trick, it's much cleaner to mark embedded CTEs explicitly with a flag in mdb_node_t than to infer that from the cap data, because that keeps the generic cap code generic. We already have mdbRevocable and mdbFirstBadged, this would be a new mdbEmbedded.

Sorry, but all of that sounds absolutely horrible and is not in line with the existing design.

The flag would be used in finaliseSlot to check whether a cap might need additional cleanup before calling finaliseCap. It would replace checks like this with a generic check and then call unlink_slot or something like that, which does the cap type check and clears the mdbEmbedded flag.

That kind of check you are referencing is against the CTE design in seL4 and should be eliminated, not generalised. CTE handling should be position independent and not rely on which object the CTE is in. It creates yet another special case for CTEs and yet another case where normal CTE operations do not apply (no copy/move/etc). It makes the API less uniform and even harder reason about. All of that is in the wrong direction.

Maybe there is something we can do with caps analogous to the mapping information for frames in page tables, but it does sound like a hack.

The only clean alternative I can think of is to expand MDBs to have two next and prev pointers so multi-parent relationships can be tracked properly. Ideally this could replace the current ASID hacks we have too. But it would double the size of caps, which is not entirely bad either, because space in caps is already tight.

Yes, that's one of the reasons caps are just the wrong vehicle for tracking such information. There is no reason to believe that shoehorning other object dependency information into the authority mechanism would make the design better.

The instances where the dependency tracking works fine is where objects have storage for explicitly tracking it. That is what the design should have. Pure frames without extra storage are fundamentally problematic for that.

Frankly, having them embedded in the VCPU would be drastically simpler and I don't buy the performance waste argument. Either you want to use this feature or you don't. Why would you want to use it only for some VCPUs in the same system? But even that could be achieved: you could have two types of VCPU sizes in the same system and you create the one you want at runtime. Sounds like 0 cost to me without creating yet another case of single-use object binding and complexity where none is needed.

People seem to think for some reason that object binding is a good idea, but every single case of it has ended in a complexity disaster for what it achieves. Implementing it with caps would make it even worse. If we can avoid it, then we definitely should.

[lsf37]

Frankly, having them embedded in the VCPU would be drastically simpler and I don't buy the performance waste argument. Either you want to use this feature or you don't. Why would you want to use it only for some VCPUs in the same system? But even that could be achieved: you could have two types of VCPU sizes in the same system and you create the one you want at runtime. Sounds like 0 cost to me without creating yet another case of single-use object binding and complexity where none is needed.

The real argument against this design variant is that the user can no longer map those frames. Can that be solved some other way? Is access to those frames performance critical or could it be via the kernel?

[dreamliner787-9]

Frankly, having them embedded in the VCPU would be drastically simpler

Yes I agree, it was under alternative solution 1 of the RFC as well to solve the resources tracking problem unfolding above. But I didn't implement that solution for the main proposal due to the performance problem below.

Is access to those frames performance critical or could it be via the kernel?

Unfortunately the VMM still need to access the virtual APIC page to emulate certain functions of the APIC that were not hardware accelerated (e.g. the APIC timer, which is used by Linux for scheduling).

You can see the an example of how often and when a VMM need to access the virtual APIC page in the virtual APIC code of our VMM.

For example, when a guest kernel sets a timeout in the APIC timer by writing the initial count to REG_LAPIC_INIT_CNT. We need to read that value from the virtual APIC page plus REG_LAPIC_DCR and REG_LAPIC_TIMER to ascertain now long in host time the timer goes for.

Similarily when a guest kernel reads the current count we also need to read multiple APIC registers to work out what the counter should be and return it to the guest.

If we do this virtual APIC register reads and writes via an invocation it would incur significant performance penalty for the guest. Unless upon a VM Exit due to APIC write, we deliver the relevant virtual APIC registers value via message registers to the VMM to reduce the amount of context switches. Or move some of this logic into the kernel which is bad.

[lsf37]

Unfortunately the VMM still need to access the virtual APIC page to emulate certain functions of the APIC that were not hardware accelerated (e.g. the APIC timer, which is used by Linux for scheduling).

Ok, so we should investigate if we can make the frames available to the user.

I haven't thought this through yet, but what about allowing the use of VCPU caps in map/unmap operations? We might have to add the same kind of mapping info to VCPU caps that frame caps have now so that they can be unmapped again (not exactly nice, but there would be space in the cap). When the VCPU object is deleted, the frame would have to be unmapped the same way other frames are unmapped on deletion. There is no separate frame object, so we never have the case where the frame is deleted and we need to find the VCPU object or the VCPU is deleted and we need to fine the frame.

We can have the case we also get for frames in the other design that the page table is deleted in which the frame mapping resides. This would mean the VPCU page is no longer accessible to the user, but the hardware would still be writing/reading to the physical frames. I think that would be fine -- it's the same for as in other shared frame situations and no different in the other design.

The wrinkle is that you need to handle two frames instead of one, but that seems relatively straightforward to me compared to the other design where we would need to change general cap mechanisms. This one is only adding code for things that are new.

It doesn't sound entirely appealing to me, but better than separate objects with the problems of separate lifetimes.

[Indanz]

I haven't thought this through yet, but what about allowing the use of VCPU caps in map/unmap operations? We might have to add the same kind of mapping info to VCPU caps that frame caps have now so that they can be unmapped again (not exactly nice, but there would be space in the cap).

For this the ASID and the virtual address the page is mapped at need to be stored. The x86 VCPU caps have plenty of space left for that.

The wrinkle is that you need to handle two frames instead of one, but that seems relatively straightforward to me compared to the other design where we would need to change general cap mechanisms. This one is only adding code for things that are new.

Selecting between the two pages should be trivial.

I thought directly mapping wouldn't work because you need to be able to map the same VCPU page in multiple VSpaces (both in the guest VSpace and the VMM), but I forgot that you can just copy the VCPU cap. Hence my proposal above to give a way to derive page caps from a VCPU cap instead.

[dreamliner787-9]

but what about allowing the use of VCPU caps in map/unmap operations?

For this the ASID and the virtual address the page is mapped at need to be stored.

Just confirming before I make a new implementation. So we would embed the 2 extra pages in the VCPU object like so:

struct vcpu {
    /* Storage for VMCS region. First field of vcpu_t so they share address.
     * Will use at most 4KiB of memory. Statically reserve 4KiB for convenience. */
    char vmcs[VCPU_VMCS_SIZE];

+#ifdef CONFIG_INTEL_APICV
+    /* Storage for the 2 pages needed for Intel APICv. Place it after the VMCS
+     * to maintain 4KiB alignment. */
+    char apicv_access[VCPU_APICV_ACCESS_PAGE_SIZE];
+    char apicv_virtual_apic[VCPU_APICV_VIRTUAL_APIC_PAGE_SIZE];
+#endif

    word_t io[VCPU_IOBITMAP_SIZE / sizeof(word_t)];

    /* Place the fpu state here so that it is aligned */
    user_fpu_state_t fpuState;

+#ifdef CONFIG_INTEL_APICV
+    asid_t apicv_access_mapped_asid;
+    asid_t apicv_virtual_apic_mapped_asid;
+    word_t apicv_access_mapped_gpa;
+    word_t apicv_virtual_apic_mapped_vaddr;
+#endif

Then we add 4 new x86 VCPU invocations:

• seL4_X86_VCPU_MapApicAccessPage(seL4_X86_VCPU _service, seL4_X86_EPTPML4 eptpml4, seL4_Word gpa)
• seL4_X86_VCPU_MapVirtualApicPage(seL4_X86_VCPU _service, seL4_CPtr vspace, seL4_Word vaddr, seL4_CapRights_t rights, seL4_X86_VMAttributes attr)
• seL4_X86_VCPU_UnmapApicAccessPage(seL4_X86_VCPU _service)
• seL4_X86_VCPU_UnmapVirtualApicPage(seL4_X86_VCPU _service)

These will have similar semantics to the normal map/unmap operations. Have I understood you both correctly? @lsf37 @Indanz

[Indanz]

• asid_t apicv_access_mapped_asid;
• asid_t apicv_virtual_apic_mapped_asid;
• word_t apicv_access_mapped_gpa;
• word_t apicv_virtual_apic_mapped_vaddr;

If each page only needs to be mapped once, then yes, having this information in the VCPU object itself would work and would be the better solution.

However, once it must be possible to map the same page multiple times, then you need to store the ASID + virtual address in the VCPU cap itself instead of in the VCPU object.

* `seL4_X86_VCPU_MapApicAccessPage(seL4_X86_VCPU _service, seL4_X86_EPTPML4 eptpml4, seL4_Word gpa)`

* `seL4_X86_VCPU_MapVirtualApicPage(seL4_X86_VCPU _service, seL4_CPtr vspace, seL4_Word vaddr, seL4_CapRights_t rights, seL4_X86_VMAttributes attr)`

Personally I would not add new syscalls, but use the existing map ones and extend them to also work on VCPU caps. And then add two special flags to seL4_X86_VMAttributes, one for APIC access page and one for the virtual APIC page.

[dreamliner787-9]

Personally I would not add new syscalls, but use the existing map ones and extend them to also work on VCPU caps. And then add two special flags to seL4_X86_VMAttributes, one for APIC access page and one for the virtual APIC page.

Ah cool I didn't think of that, hence I proposed adding the new syscalls. But the flag approach is a lot better.

[midnightveil]

Personally I would not add new syscalls, but use the existing map ones and extend them to also work on VCPU caps. And then add two special flags to seL4_X86_VMAttributes, one for APIC access page and one for the virtual APIC page.

I don't think this is possible — for (bad and should be changed) reasons page mapping operations are specified as invocations on the frame cap, not the page table. So we can't add to the existing frame cap invocations as we won't have a frame capability to do an invocation on.

Though it might make more sense to add these as invocations on the page table capabilities if we're adding new syscalls anyway, though that would make the API quite confusing.

[Indanz]

I don't think this is possible — for (bad and should be changed) reasons page mapping operations are specified as invocations on the frame cap, not the page table. So we can't add to the existing frame cap invocations as we won't have a frame capability to do an invocation on.

Yes, but that doesn't matter in this case. It just means that the VCPU object has to implement the X86PageMap, X86PageUnmap and X86PageMapEPT invocations. As those identifiers are unique, any object can implement them.

Edit: To clarify, the API xml needs no change, other than perhaps documentation. You don't add these invocations to the VCPU object in the XML, as that indeed won't work.

Whether the VCPU object does its own thing or redirects it to the page code (with or without a temp frame cte_t) is an implementation detail.

[lsf37]

These will have similar semantics to the normal map/unmap operations. Have I understood you both correctly? @lsf37 @Indanz

Sorry, have been travelling for a while. Yes, embedding the pages like this is what I meant. As Indan already indicated, the mapping info should probably go into the caps (like we have it now in the frame caps), and I do think you are right that we will unfortunately need these as invocations on the VCPU caps because as Julia said, map/unmap is an invocation of the frame cap not the page table cap.

It might still be possible to share the code between them in the way I think Indan means -- not sure if that ends up more or less messy than the duplication we would get otherwise. We'll probably have to try it and see.

(Edit: the main trick in sharing the code between VCPU and frame caps will be to do this in a way that doesn't break verification on non-VT-x configs)

[Indanz]

It might still be possible to share the code between them in the way I think Indan means -- not sure if that ends up more or less messy than the duplication we would get otherwise. We'll probably have to try it and see.

Yes, hard to tell beforehand if my suggestion is better or worse than just duplicating code.

My idea was to call the page decode functions directly from the VCPU code. But to do that, you need a temporary local cte_t with a page cap setup properly and pass that instead of the vcpu cap/cte_t. Then it's just a wrapper that does some VCPU related bookkeeping around the page calls.

However, looking at the actual code, for invoke it seems much simpler to call createSafeMappingEntries_PTE and invalidatePageStructureCacheASID directly. Decode has a lot of boiler plate that would need to be duplicated though (around 100 lines of code).

Maybe the useful checking code in decodeX86FrameInvocation can be somehow shared, but not without verification changes. All in all unclear which approach is better.

[lsf37]

I read over this part of @Indanz early reply too quickly. Maybe there is something we can do:

In this case, if the TCB goes away, you don't have to do anything. But you do need to clear the VMX registers when the page objects goes away. We can't look up the TCB/VCPU by ASID, as the VSpace may be shared by multiple instances.

Do we need to do this VMX register clearing immediately or only on next context switch?

Because if its only on next context switch, we could do the following (not sure this is feasible, just throwing it out there because it could be a relatively painless option):

• use the TCB to store the ACPI frame cap in a TCB slot (no new CTE location, no special verification pain)
• no special handling for the ACPI frame cap in revocation. Both at TCB revocation and and at ACPI frame revocation/deletion, we just do the normal finaliseCap, which will unmap the frame and set the cap to NullCap
• on context switch to a VCPU thread we check the cap slot. If it is NullCap we clear the VMX registers.

For this, we don't need a back pointer from the frame, because the cap guarantees existence of the frame (the frame can only go away when the cap has already been finalised and deleted).

[midnightveil]

Provided that the cost of doing that check isn't prohibitive (I somewhat doubt it would be, given how expensive the hardware vmenter cost already is, and that it should be a couple extra branches and loads), I would be happy with that as a solution, especially if it's easier than some of the other solutions proposed here.

[Indanz]

On 2026-08-03 06:57, Gerwin Klein wrote: Do we need to do this VMX register clearing immediately or only on next context switch?

That's a somewhat difficult to answer question, which depends on the exact CPU behaviour and whether it's SMP or not. Assuming the cpu can access the page as long as it's set in a VMX register, then I think they must be cleared by the time the syscall returns. However, this only applies to the hw VMX registers, the saved ones we can update at VCPU load time. That should be practically free. It's trivial to clear the VMX registers immediately if we're running on the correct core. We can compare the physical address of the deleted page with the VMX register values. However, then we need a way to know when to do this or do it for every page. If we already do IPIs on page deletion, then we can piggy back on that. Otherwise it gets very expensive for SMP. Another question is how to unmap an ACPIv frame if the cap is embedded in the VCPU.

[midnightveil]

If we already do IPIs on page
deletion, then we can piggy back on that. Otherwise it gets very
expensive for SMP.

Looks like finaliseCap -> unmapPage and unmapPageTable both just unmap the page and then do TLB invalidate (which will IPI to remote core) only if mapped. Which I suppose is fine as long as it is safe to modify page tables concurrently with a running thread. Deleting ASID seems slightly unsafe though but maybe works out fine.

---

For non-SMP this seems fine but yeah for SMP, let's say you have;

• Core 0 running a VM and nothing else
• Core 1 deletes the frame cap for APICv
• Core 2 reuses it for something else

There would be an issue if Core 0 never pops back into the kernel.

I suppose the "simplest" fix to make SMP work would be to store a single bit in the frame cap stating "used for APICv" and if you see that when deleting you do a broadcast "no-op" IPI to force a vmexit->vmenter sequence which would clear the flag. Or, if there's enough information to check cross-core "running a VM" state (I think there would be) it can be several unicast IPIs. Even more logic would be for every other core, look at the TCB slots for ksCurThread and check if that page is the same as the currently deleted page before doing an IPI.

[Indanz]

I suppose the "simplest" fix to make SMP work would be to store a single bit in the frame cap stating "used for APICv" and if you see that when deleting you do a broadcast "no-op" IPI to force a vmexit->vmenter sequence which would clear the flag.

That's what I thought too, but then I realised that that is actually incredibly tricky to get right, because that flag is not guaranteed to be set on the cap that contains the last mapping. And you can't willy-nilly clear the VMX register for non-last mappings, because it may have been re-mapped or mapped multiple times or something.

No, only safe choice is broadcast IPI on all page deletions. If there already is a TLB invalidate broadcast, then we can add this to that (but no IPI if not mapped is a problem). Only extra info we need to pass is the physical address. Checking whether a VM is running and then clearing any matching VMX registers should be almost free compared to the IPI overhead.

(Maybe there is a bit free in the PTE pointing to the ACPIv page, but that's the only alternative hack I can think of right now.)

[Indanz]

Ah, ha! Idea:

• Reserve one ASID value for APICv values.
• On page unmap, if ASID matches the special value, clear VMX register.
• For SMP, add a broadcast IPI which clears VMX registers for a specified physical address.

Edit: But I admit I have no idea how ASIDs are managed on x86, never looked at it. I assume they use them, but I can't find anything in the manual about it for x86... Quick source grep seems to show they have ASID pools etc.

[lsf37]

Ah, ha! Idea:

• Reserve one ASID value for APICv values.
• On page unmap, if ASID matches the special value, clear VMX register.
• For SMP, add a broadcast IPI which clears VMX registers for a specified physical address.

Does that mean you could only have one VM, though? Because an unmap of anybody else's APIC frame would lead to clearing the VMX register on whatever is running currently. Or do we have enough information to check if that register refers to the frame that is being unmapped? But if a different VM is running, we'd still have no way of finding the one where we actually need to clear the register.

Another question is how to unmap an ACPIv frame if the cap is embedded in the VCPU.

Embedding caps in the VCPU is not feasible (it's a linear blow-up in proof cost for everything that currently has to make a case distinction between CNode and TCB, and that is a lot of places). The point of my proposal is to use TCB slots (the CTEs in the TCB) which already exist as a concept it the verification, i.e. doing one more of these is not so bad.

[lsf37]

No, only safe choice is broadcast IPI on all page deletions.

Agreed. I thought we're already doing that. Are we not? I don't quite remember what the problem was, but something along the lines that you could be deleting the page the current thread on another core is currently running on. Maybe I'm confusing that with TCB deletions.

(Note that it's only final delete, not general unmap. Deletion of a large untyped is already very likely to stall for at least the TCB reasons if you've been allocating any TCBs from it).

[midnightveil]

That's what I thought too, but then I realised that that is actually incredibly tricky to get right, because that flag is not guaranteed to be set on the cap that contains the last mapping.

But that's not an issue? As long as we prevent copying of caps with the APICv bit set (which should be fine; except for (maybe?) when caps move around during cleanup it should not be possible for user to even reference a frame-with-APICv cap to make copies of it. Even if that's not possible, we just made the copy/derive/whatever operation clear that bit in the same way it works for page mapping information.

Then, in the exact same way that page-mapped frame cap cleanup works we know if we finaliseCap and it has it set then we can remove it.

And you can't willy-nilly clear the VMX register for non-last mappings, because it may have been re-mapped or mapped multiple times or something.

Well, we probably want to disallow mapping the same frame as multiple APICv. That sounds like a bad idea. However, that's probably not necessary, since it's the user shooting themselves in the foot.

I'm confused here because under Gerwin's proposal we never directly clear VMX registers; only when we start doing vmenter we do a check of the TCB slot for this and don't set it if the cap is invalid. All we need to do is force a context switch for it to be safe.

---

Doing this APICv bit is an optimisation to reduce the frequency of when we need to do broadcast (or even unicast) IPIs to deal with the currently-running-VM-on-other-core using that frame.

[midnightveil]

Agreed. I thought we're already doing that. Are we not? I don't quite remember what the problem was, but something along the lines that you could be deleting the page the current thread on another core is currently running on. Maybe I'm confusing that with TCB deletions.

(Note that it's only final delete, not general unmap. Deletion of a large untyped is already very likely to stall for at least the TCB reasons if you've been allocating any TCBs from it).

There's no explicit TCB stall for deleting a ASIDPool, VSpace, Page Table, or Page. After it has been removed from the page table we do a broadcast TLB invalidate (on Arm64) for the ASID.

However, even if there was, the behaviour would be (almost) the same (aside from minor timing differences in exactly where it faults) as either way the page is being unmapped; provided that architecturally it is OK to clear out the PTE or base page table (TTBR/etc) whilst a thread is using it. And by architecturally OK I mean "doesn't cause some kind of special error that's not just an invalid translation fault".

[lsf37]

I suppose the "simplest" fix to make SMP work would be to store a single bit in the frame cap stating "used for APICv" and if you see that when deleting you do a broadcast "no-op" IPI to force a vmexit->vmenter sequence which would clear the flag.

That's what I thought too, but then I realised that that is actually incredibly tricky to get right, because that flag is not guaranteed to be set on the cap that contains the last mapping. And you can't willy-nilly clear the VMX register for non-last mappings, because it may have been re-mapped or mapped multiple times or something.

I don't think clearing the VMX register is a problem. If having an ACPI frame cap in the TCB is the authority for setting that register, then the register should be cleared as soon as that slot becomes a NullCap.

Which come to think of it makes my sentence here wrong:

(Note that it's only final delete, not general unmap. Deletion of a large untyped is already very likely to stall for at least the TCB reasons if you've been allocating any TCBs from it).

I've mixing two concepts there: deletion of a single cap, e.g. in the TCB slot "ACPI frame cap", and deletion of the frame itself (via deletion of the last cap to the frame). We need to clear the VMX register already when we delete the cap in the TCB slot, not only when the frame is deleted.

The ways such a TCB slot cap can be deleted are:

• revocation + deletion of the TCB
• revocation of the parent of the ACPI frame cap (either untyped or just a regular frame cap)
• explicit syscall for unmapping the ACPI frame (which I suppose we should be adding)

The problematic one, as usual, is revocation (maybe partial) of the cap leading to the slot being cleared. The other two options are working on the TCB and can figure out where it runs. Frame cap revocation would not know where it is removing the cap, and as annoying as that sounds that is intended and should not change (or at least would be expensive to change). Hence my idea of checking the slot at context switch.

As for adding bits to frame caps: on 64 bit architectures that could work, on 32 bit architectures we are out of bits in frame caps. The only way to get more bits would be to globally reduce the number of ASID bits. One thing that is sort-of equivalent and that could work is making a new cap type that is another kind of frame cap that is only useable for ACPI frames and that can use some kind of extra knowledge about these frames to gain another bit somewhere. I'm not sure that is feasible, though.

If you had a different type (but no other new bits), you could potentially encode and enforce that these could only live in a particular TCB slot, because there is no other way to make them or to move them and you have checked that deletion/revocation will also never move them anywhere else. Master reply caps on non-MCS sort-of have this behaviour. It's not a great design and the reply cap invariants are definitely not nice, but it could work. And I can't believe I'm saying this, but if you know that this cap type can only live in a TCB slot, you can compute the TCB address and get to the TCB from there in finaliseCap (depending on cap type is fine, and this is just more of that), so you know which VMX registers to clear. I don't like this design, it will force at least two global special invariants if we prove this, but it seems to avoid everything else that is expensive and should work. It will also lead to subtle special-casing in isMDBParentOf, because the new frame cap type would be a child of a normal frame which is a different type. But that also can be done, it's just not nice.

[Indanz]

Does that mean you could only have one VM, though? Because an unmap of anybody else's APIC frame would lead to clearing the VMX register on whatever is running currently. Or do we have enough information to check if that register refers to the frame that is being unmapped? But if a different VM is running, we'd still have no way of finding the one where we actually need to clear the register.

The above assumes you unmap the APIC frame before assigning it to another VCPU. If the user does that, then we can check by physical address. There is no way to check whether a frame is already used as an APIC frame, except if we can encode that information in the PTE.

To properly track it we need a whole ASID pool just for APIC mappings. Or if we have enough bits, use VCPU ASID or VMID + core as "ASID".

But if you want to enforce this 1:1 mapping that strongly, it's probably easier to embed the frame in the VCPU object, which avoids all the life time problems.

Another question is how to unmap an ACPIv frame if the cap is embedded in the VCPU.

Embedding caps in the VCPU is not feasible (it's a linear blow-up in proof cost for everything that currently has to make a case distinction between CNode and TCB, and that is a lot of places). The point of my proposal is to use TCB slots (the CTEs in the TCB) which already exist as a concept it the verification, i.e. doing one more of these is not so bad.

Ah, apologies, I missed that. Same question stands: How do you "unmap" it manually as a user? (That is, clear the VMX register and disallow the page to be used that way.) Would a revoke on the user's page cap delete the embedded cap in the TCB?

Note that it's only final delete, not general unmap.

I don't think we can assume that the embedded cap is the final one. So it needs to happen every time an embedded cap is deleted. We can detect if this is the case with the ASID trick.

But that's not an issue?

I think I got the idea we need to do something special on last unmap in my head, while that's actually not the case, it's when the VCPU's cap gets deleted instead. And for that it could be some info in the cap itself, like you said.

[midnightveil]

As for adding bits to frame caps: on 64 bit architectures that could work, on 32 bit architectures we are out of bits in frame caps. The only way to get more bits would be to globally reduce the number of ASID bits. One thing that is sort-of equivalent and that could work is making a new cap type that is another kind of frame cap that is only useable for ACPI frames and that can use some kind of extra knowledge about these frames to gain another bit somewhere. I'm not sure that is feasible, though.

Yeah I was thinking about that. I was assuming it would be extra proof effort, but in essence the extra APICv bit is doing the same thing where we already have "frame_cap" has special subtypes "unmapped", "mapped" and "Apicv". (maybe apocv + mapped/unmapped?).

I'm not sure if it's worth supporting APICv on 32-bit, or if it's even possible. I feel like it's definitely not worth verifying it on 32-bit x86.

[lsf37]

Another question is how to unmap an ACPIv frame if the cap is embedded in the VCPU.

Embedding caps in the VCPU is not feasible (it's a linear blow-up in proof cost for everything that currently has to make a case distinction between CNode and TCB, and that is a lot of places). The point of my proposal is to use TCB slots (the CTEs in the TCB) which already exist as a concept it the verification, i.e. doing one more of these is not so bad.

Ah, apologies, I missed that. Same question stands: How do you "unmap" it manually as a user? (That is, clear the VMX register and disallow the page to be used that way.) Would a revoke on the user's page cap delete the embedded cap in the TCB?

I was initially thinking by revoking the original frame cap that was used to derive the ACPI frame cap, but we should probably have a TCB invocation that can explicitly unmap and clear the slot. Maybe not. I'm not sure. It's not strictly necessary (because revoke would work), so minimality would say "no", but it forces duplication (keeping another cap around just so you can revoke), and we don't support many delegation levels on frame caps, so all of that would be awkward, so I'm currently thinking more that there should be an explicit invocation.

Note that it's only final delete, not general unmap.

I don't think we can assume that the embedded cap is the final one. So it needs to happen every time an embedded cap is deleted.

Yes, you're right.

[lsf37]

As for adding bits to frame caps: on 64 bit architectures that could work, on 32 bit architectures we are out of bits in frame caps. The only way to get more bits would be to globally reduce the number of ASID bits. One thing that is sort-of equivalent and that could work is making a new cap type that is another kind of frame cap that is only useable for ACPI frames and that can use some kind of extra knowledge about these frames to gain another bit somewhere. I'm not sure that is feasible, though.

Yeah I was thinking about that. I was assuming it would be extra proof effort, but in essence the extra APICv bit is doing the same thing where we already have "frame_cap" has special subtypes "unmapped", "mapped" and "Apicv". (maybe apocv + mapped/unmapped?).

I'm not sure if it's worth supporting APICv on 32-bit, or if it's even possible. I feel like it's definitely not worth verifying it on 32-bit x86.

Oh, that is a good point! This is x86 specific and we can just not support it on 32-bit x86. I'd be fine with that. So then bits are available, I think. (Edit: confirmed, there are 4 bits of padding left)

And the whole cap type thing would also become a tiny bit less bad, because isMDBParentOf would just not treat it as a separate type, while finaliseCap can check the bit and do treat it as a different type of frame cap.

[Indanz]

So I guess the choice is between:

1. Embed the APICv frame in the VCPU object and give a way to either get page caps to that or to map it somewhere else.
   This requires a way to either derive frame caps from a VCPU cap, or to use a VCPU cap as a frame cap. Cleanup is automatic.
2. Embed normal page caps in the TCB when used for APICv.
   For cleanup this requires a cap check on VCPU schedule and a forced reschedule on all cores on deletion of an embedded APICv cap, which we can detect by adding one bit to page caps.

I think I still prefer option 1.

[midnightveil]

Oh, that is a good point! This is x86 specific and we can just not support it on 32-bit x86. I'd be fine with that. So then bits are available, I think. (Edit: confirmed, there are 4 bits of padding left)

Thinking about it again: we could still support it on x86 32-bit, just we can't support the APICv-bit "optimisation", i.e. it would require a broadcast IPI on every page delete. Which would be fine for static systems.

(More generally though it's probably not worth writing that code anyway, I don't really see the point in adding extra work for a platform no one would be building new systems on)

[lsf37]

If you had a different type (but no other new bits), you could potentially encode and enforce that these could only live in a particular TCB slot, because there is no other way to make them or to move them and you have checked that deletion/revocation will also never move them anywhere else. Master reply caps on non-MCS sort-of have this behaviour. It's not a great design and the reply cap invariants are definitely not nice, but it could work. And I can't believe I'm saying this, but if you know that this cap type can only live in a TCB slot, you can compute the TCB address and get to the TCB from there in finaliseCap (depending on cap type is fine, and this is just more of that), so you know which VMX registers to clear. I don't like this design, it will force at least two global special invariants if we prove this, but it seems to avoid everything else that is expensive and should work. It will also lead to subtle special-casing in isMDBParentOf, because the new frame cap type would be a child of a normal frame which is a different type. But that also can be done, it's just not nice.

Sorry, that proposal from me is also wrong, finaliseCap doesn't get the slot, only the cap. That's exactly the thing that I didn't want to change, because it was expensive, so my "compute TCB from cap" doesn't work.

[lsf37]

Oh, that is a good point! This is x86 specific and we can just not support it on 32-bit x86. I'd be fine with that. So then bits are available, I think. (Edit: confirmed, there are 4 bits of padding left)

Thinking about it again: we could still support it on x86 32-bit, just we can't support the APICv-bit "optimisation", i.e. it would require a broadcast IPI on every page delete. Which would be fine for static systems.

(More generally though it's probably not worth writing that code anyway, I don't really see the point in adding extra work for a platform no one would be building new systems on)

Yes, I agree. I do want to discuss deprecating 32-bit x86 entirely at some point.

[midnightveil]

So I guess the choice is between:

1. Embed the APICv frame in the VCPU object and give a way to either get page caps to that or to map it somewhere else.
   This requires a way to either derive frame caps from a VCPU cap, or to use a VCPU cap as a frame cap. Cleanup is automatic.

2. Embed normal page caps in the TCB when used for APICv.
   For cleanup this requires a cap check on VCPU schedule and a forced reschedule on all cores on deletion of an embedded APICv cap, which we can detect by adding one bit to page caps.

I think I still prefer option 1.

If there's not going to be verification-related issues with being able to map VCPU objects as frames I think I agree it would be cleaner to just make the VCPU bigger, yeah. And I suppose it removes the technically-exists-but-neglible performance cost of continually checking on context switch for NullCap there option.

[lsf37]

If there's not going to be verification-related issues with being able to map VCPU objects as frames I think I agree it would be cleaner to just make the VCPU bigger, yeah.

One thing people might not like is that the overall object still has to be aligned to its size and that the frame has to be aligned to its size (so it can be treated like a normal frame from the rest of mapping code's perspective). So this might waste some memory between the objects. Although VCPUBits seems to be 14 on x86 and seL4_PageBits is 12, so maybe there is actually space in the VCPU object already anyway, I'm not sure. In the worst case VCPUBits grows to 15, though.

It will be a special case in mapping and possibly unmapping invocations (or more like new invocations), and VCPU caps will have to carry the usual frame information.

If the page is unmapped, but the object still exists, we don't need to do anything special, right? The user will just take a translation fault.

As far as I can see, this all should check out.

[Indanz]

On 2026-08-04 02:39, Gerwin Klein wrote: It will be a special case in mapping and possibly unmapping invocations (or more like new invocations), and VCPU caps will have to carry the usual frame information.

Or do what I'd do and turn a vcpu cap into a frame cap when it's used for mapping. Then you only need extra code in MTBisParentOf for delete and revocation, and a new map invocation on the vcpu object. Or add a vcpu method to turn the cap into a frame cap. I think that would be cleanest and truly trivial. (We also need a way to enable and disable APICv of course. But that's independent from the mapping.)

If the page is unmapped, but the object still exists, we don't need to do anything special, right? The user will just take a translation fault.

All the special vmx register stuff is tied to the vcpu, nothing special needs to be done on the (un)mapping side.

As far as I can see, this all should check out.

It seems very straightforward to me. Main fiddle is to ensure that the alignment requirement doesn't blow up the object size.

[Indanz]

Just the page part, not the actual APICv implementation: seL4/seL4@master...Indanz:seL4:APICv

Edit: replaced big diff with link.

[Indanz]

@midnightveil points out the above should only be allowed on derived caps and not the original, otherwise you can't clean up the VCPU object. And also would prefer it created a new cap instead of changing the existing one, like normal CNode operations do. I also forgot to update Arch_sameRegionAs.

Anyway, those are just details, the main thing is that it seems much simpler to create page caps from VCPU objects directly than the alternative solutions.

[lsf37]

On 2026-08-04 02:39, Gerwin Klein wrote: It will be a special case in mapping and possibly unmapping invocations (or more like new invocations), and VCPU caps will have to carry the usual frame information.

Or do what I'd do and turn a vcpu cap into a frame cap when it's used for mapping. Then you only need extra code in MTBisParentOf for delete and revocation, and a new map invocation on the vcpu object. Or add a vcpu method to turn the cap into a frame cap. I think that would be cleanest and truly trivial. (We also need a way to enable and disable APICv of course. But that's independent from the mapping.)

Sorry, we definitely cannot simply make a cap into another type on the fly with a potentially different object pointer and then have two types of object cap to the same memory object with different views. That breaks so many invariants that I can't even estimate the amount of breakage. It also doesn't work. The cap mapping info will be changed in map and the new cap will be stored somewhere. Now you suddenly have a frame cap sitting where there was a VCPU cap before and no other kernel op will know that it was a VCPU cap and e.g. the CDT assumptions on being chunked by object type will be completely wrong.

Generally, changing types is something that should be constrained to extremely few choke points (retype and explicit derivation). In general, changing a cap type into another existing cap type is pretty much guaranteed to break things. If at all, it'd need to be a new type that has a clear derivation relation to the old type, like IRQControl and IRQHandler and similar ones, and even there it only works because you are making a new cap, you never change the type of an existing cap.

[dreamliner787-9]

Just making sure I'm on the same page as everyone else: the direction seems to be embedding both 4 KiB APICv (APIC access and virtual APIC) frames into struct vcpu. In our configuration that takes the object size from 2^14 to 2^15. The frames need 4 KiB alignment within the object, which is satisfied by placing them immediately after the VMCS. I also agree on not supporting APICv on 32-bit x86 at all.

That leaves the question of how userspace gets frame caps to those embedded pages, so it can map one into the VM's EPT and the other into the VMM's VSpace.

Like Gerwin's suggestion, a type change has to produce a new cap with a derivation relation to the old one, rather than mutating an existing cap in place (the IRQControl to IRQHandler pattern). One option is a new x86-64 only cap type created by an invocation on the VCPU cap:

seL4_X86_VCPU_DeriveAPICvFrame(vcpu, page_sel, dest_cnode, dest_index, dest_depth)

The new cap lands in the destination slot as a CDT child of the VCPU cap. The VCPU cap itself is untouched. The new cap carries what a 4 KiB frame cap carries (base address, ASID, mapped address, rights, attributes) plus one bit selecting which of the two pages it refers to. Map and unmap become new invocation labels on this type, covering both VSpace and EPT mappings.

The appeal is that finaliseCap needs nothing beyond the cap itself, since the mapping information is in the cap exactly as it is for a normal frame. Deleting or revoking the VCPU cap tears down its CDT children first, so no mapping can outlive the object, and the VMX registers never need clearing out of band. This does need a case in Arch_sameRegionAs so that a 4 KiB cap pointing inside a VCPU object region is recognised as that VCPU's child rather than an unrelated region.

Separately, there is something I failed to consider in the original proposal, and it changes where one of the two pages should live.

Some background on how the APIC-access page works. The page's contents are never used. What matters is only its physical address. When the guest accesses its APIC at the usual physical address 0xFEE00000, the CPU translates that through EPT (Stage 2 PT) to a host physical address, and then compares that result against the APIC-access address stored in the VMCS. If they match, the access is treated as an APIC access and handled by hardware. If they do not match, it is an ordinary memory access and APIC virtualisation simply does not engage.

Consider an SMP guest: there is one EPT shared by all the VCPUs in the VM, and every VCPU uses the same guest physical APIC address. So every VCPU's access to 0xFEE00000 translates to the same single host physical page, whichever page the EPT happens to map there. If each VCPU has its own private access page embedded in its own object, then at most one VCPU's VMCS can name that page. Every other VCPU compares against a different address, gets no match, and silently loses APIC virtualisation with no error anywhere.

So the APIC-access page is inherently per-VM rather than per-VCPU, and embedding it in struct vcpu does not work for SMP guests. KVM allocates it once per VM for this reason: int kvm_alloc_apic_access_page(struct kvm *kvm) takes a struct kvm * rather than a struct kvm_vcpu *vcpu and is guarded so it only ever runs once per VM.

The virtual-APIC page is genuinely per-VCPU, since it holds that VCPU's own APIC state, and belongs in struct vcpu as proposed. For the access page, the natural per-VM object we already have is the EPT PML4, so one option is to embed it there and derive its cap from the EPTPML4 cap by the same mechanism described above. Since its contents are never read or written by the CPU, this is purely a question of which object owns the storage.

[midnightveil]

For the access page, the natural per-VM object we already have is the EPT PML4

I wouldn't necessarily call this "natural", it's a page table structure...

Do existing SMP VMs (i.e. Microkit) have different page tables for each CPU, or just one? From the sounds if it the APIC access page forces unique set of page tables per CPU.

If each VCPU has its own private access page embedded in its own object, then at most one VCPU's VMCS can name that page. Every other VCPU compares against a different address, gets no match, and silently loses APIC virtualisation with no error anywhere.

Right, so we do need a way to associate a frame cap (possibly device, for multikernel) with a VM. I don't necessarily think we need to prevent the user from shooting themselves in the foot with a different address per VCPU, as long as hardware is OK with it, but it definitely needs to be possible.

---

I am slightly confused, though, about how the hardware works here. How is the APIC access page (used internally by the CPU? is the VMM supposed to be able to map it? what if it does?) supposed to be different per CPU, if the Virtual APIC page accessed by the VMM is shared. Does the virtual APIC page know about multiple CPUs, implicitly?

(I was interpreting APIC here to be like an LAPIC (per-core), not an IOAPIC (global). Is that wrong?)

---

That seems to imply Option 2 (from Indan's message earlier) that Gerwin proposed, where we check it on every vmenter, is the best solution we have at this time.