Skip to content

paging: refactor svsm kernel page table to creata a reusable pagetable crate#1062

Open
ziqiaozhou wants to merge 6 commits into
coconut-svsm:mainfrom
ziqiaozhou:pgtable-refactor
Open

paging: refactor svsm kernel page table to creata a reusable pagetable crate#1062
ziqiaozhou wants to merge 6 commits into
coconut-svsm:mainfrom
ziqiaozhou:pgtable-refactor

Conversation

@ziqiaozhou

@ziqiaozhou ziqiaozhou commented May 13, 2026

Copy link
Copy Markdown
Contributor

This PR factors the kernel’s page-table implementation into a new standalone paging crate, then updates the kernel to consume (and re-export) those generic paging/address/size/util building blocks. It also introduces Verus specification/proof scaffolding for alignment helpers and basic paging constants.

Changes:

  • Added a new paging crate containing generic page-table types (GenericPageTable, PTEntry, PTPage, flags) and x86_64-specific flag/level definitions.
  • Moved/re-exported common utilities and page size constants from kernel into paging, and updated kernel code to use those re-exports.
  • Added Verus spec/proof modules for alignment helpers and page size facts, and wired paging/verus into kernel verification features.

@ziqiaozhou

ziqiaozhou commented May 13, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

As I mentioned in last-week's dev meeting, I refactored the page table code to extract out the general part of the page table implementation from kernel/src/pagetable.rs, in order to

  1. make it more reusable; e.g., Litebox can reuse this paging crate if we make it general and verified.
  2. distinguish the svsm-specific page table properties and general page table properties to simplify the verification efforts.
  3. Once I make the general part verified, users of the crate gain more confidence to use our paging crate instead of other external page table implementations.

Goal of the PR: move general OS-independent and arch-independent page table logic into paging crate; keep the change as minimal as possible;
non-goal of the PR: make the paging crate perfect to fit all OS and arch; support different page granularities (4k vs 16k vs others supported by arm); support 32-bit page table.

Although I tried to keep implementation closer to its original, I still made some minor changes to deduplicate the code and make it easy to be used by non-svsm projects.

  • RawPageTablePart and PageTable share many logic in some similar functions (map/unmap_4k/2M, allocate_pte_xxx, etc.). I merged them into a GenericPageTable struct that supports customized page levels.
  • Some free functions (e.g., supported_flags, private_pte_mask, etc.) are now become a trait associated functions to ArchPagingMeta so that external users of the paging crate can pick their own way to enable arch features and does not need to init the static vars (e.g., PRIVATE_PTE_MASK or FEATURE_MASK).

@ziqiaozhou ziqiaozhou marked this pull request as ready for review May 13, 2026 21:21
@ziqiaozhou

ziqiaozhou commented May 13, 2026

Copy link
Copy Markdown
Contributor Author

@stefano-garzarella can you add verification label to this PR since I moved some verified code into that paging crate from svsm kernel crate? I was able to add that label but cannot do that since this week.
@joergroedel, I moved and deduplicated some code from your original pagetable.rs file. Please take a look to confirm their usage as still as before. I have checked all callers and confirmed that based on my understanding.

@luigix25 luigix25 added the verification PR/issue related to formal verification label May 13, 2026
@ziqiaozhou

ziqiaozhou commented May 13, 2026

Copy link
Copy Markdown
Contributor Author

#1059 will fix the verification failure in this PR.

@ziqiaozhou

ziqiaozhou commented May 13, 2026

Copy link
Copy Markdown
Contributor Author

@joergroedel , svsm kernel picks flush_tlb_global_sync, flush_tlb_global_sync_range or flush_tlb_global_sync_page based on the scope of the change, outside pagetable crate. I think I should move the flush_tlb_xxx out of the paging crate for split_4k to make the pagetable implementation consistant.
NIT: split_4k is never used by any code inside svsm

@ziqiaozhou ziqiaozhou changed the title Refactor svsm kernel page table to creata a self-contained and reusable pagetable crate paging: refactor svsm kernel page table to creata a self-contained and reusable pagetable crate May 14, 2026
@stefano-garzarella stefano-garzarella added the needs-rebase The PR needs to be rebased to the latest upstream branch label May 18, 2026
@ziqiaozhou ziqiaozhou changed the title paging: refactor svsm kernel page table to creata a self-contained and reusable pagetable crate paging: refactor svsm kernel page table to creata a reusable pagetable crate May 18, 2026
@stefano-garzarella stefano-garzarella removed the needs-rebase The PR needs to be rebased to the latest upstream branch label May 19, 2026
@ziqiaozhou
paging: move address, sizes, and utility types to paging crate
eef353d 
Create the paging crate and move foundational types from the kernel:
- address.rs (PhysAddr, VirtAddr, Address trait), remove unused
  VirtPhysPair which was introduced 2 years ago and is no longer used by
svsm code.
- sizes.rs (PAGE_SIZE, PAGE_SHIFT, size constants)
- util.rs (align_up, align_down, page_align_up, overlap, bit_mask)
- Associated verus spec/proof files for verification
- paging: move Verus specs and proofs into dedicated dirs
- gate proofs and spec with verus_only

The kernel re-exports these types to maintain API compatibility.
Unit tests for utility functions move to paging/src/util.rs.

Signed-off-by: Ziqiao Zhou <ziqiaozhou@microsoft.com>
@ziqiaozhou ziqiaozhou mentioned this pull request May 20, 2026
Open
@ziqiaozhou

ziqiaozhou commented May 20, 2026

Copy link
Copy Markdown
Contributor Author

Review tips: focus on changes in 2fc8a8e, 8da895a, and f16e21e. Other commits are just moving or copying files.

@ziqiaozhou
paging/lib.rs: change MIT to MIT OR Apache-2.0
0645ad5 
Match the license with other files.

Signed-off-by: Ziqiao Zhou <ziqiaozhou@microsoft.com>
@ziqiaozhou ziqiaozhou mentioned this pull request Jun 3, 2026
Open
ziqiaozhou and others added 4 commits June 10, 2026 16:27
@ziqiaozhou
paging: add traits for generic page table.
645de30 
Introduce the generic paging traits, page-level marker types. Keep the pagetable module unwired until the implementation exists so this commit is self-contained.

Signed-off-by: Ziqiao Zhou <ziqiaozhou@microsoft.com>
@ziqiaozhou
paging: copy kernel page table baseline
0e26f56 
Copy the existing kernel page table implementation into the paging crate without wiring it into the build yet. This gives reviewers a stable baseline so the extraction diff shows old code changing into generic crate code instead of appearing as entirely new code.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Signed-off-by: Ziqiao Zhou <ziqiaozhou@microsoft.com>
@ziqiaozhou
paging: refactor svsm kernel page table to create a reusable pagetabl…
cf1309a 
…e crate

Wire the previously copied page-table baseline (from
`paging: copy kernel page table baseline`) into the `paging` crate as
a generic, architecture-agnostic implementation, and factor x86_64
specifics into their own module.

Refactor in `paging/src/pagetable.rs`:
  - Convert `PageTable`, `PTEntry`, and walk/map/unmap helpers to be
    parameterized over the trait types from `paging::traits`
    (`PagingLevel`, `PagingHandler`, `GenericPageTableFlags`,
    `ArchPagingMeta`, `SelfMap`).
  - Drop all svsm-internal dependencies that were carried over with
    the baseline (`crate::cpu::*`, `crate::mm::*`, `crate::platform`,
    `ImmutAfterInitCell`, `SvsmError`, CR/EFER helpers, encryption-
    mask globals, `paging_init`, etc.). These responsibilities move
    behind the `PagingHandler` / `ArchPagingMeta` traits and will be
    re-supplied by the kernel in a later commit.
  - Re-export the generic trait surface from `pagetable` so downstream
    callers see one module.
  - Introduce `PTE_SHIFT` and rely on `sizes::{PAGE_SHIFT, PAGE_SIZE,
    PAGE_SIZE_2M, PAGE_SIZE_1G, PageSize}` from the paging crate
    instead of `crate::types`.

Change (not pure refactor):
  - Public `map_2m` / `map_4k` still allocate parent entries using the
    default `parent_flags()` directly; caller-selectable parent flags
    and the `DIRTY` parent default are intentionally deferred to
    follow-up commits.

New `paging/src/x86_64.rs`:
  - Move the x86_64-specific `PTEntryFlags` bitflags out of
    `pagetable.rs` (now `usize`-backed) along with its helpers
    (`exec`, `data`, `data_ro`, `task_exec`, `task_data`,
    `task_data_ro`, and the `writable`/`user`/`nx`/`global`
    accessors).
  - Implement `GenericPageTableFlags` for `PTEntryFlags`, defining
    `PRESENT`/`USER`/`HUGE`, `parent_flags()` (PRESENT | WRITABLE |
    USER | ACCESSED), and `self_map_table_flags()` (PRESENT |
    WRITABLE | ACCESSED | DIRTY | NX).
  - Add `Pml4Level` (4-level PML4) and `PdptLevel` (PDPT-rooted
    3-level sub-tree) type aliases over `traits::PagingLevel{3,2}`.

`paging/src/lib.rs`:
  - Expose the new `pagetable` and `x86_64` modules.

No callers are migrated in this commit; the kernel still uses its own
copy of the page table code. Net diff: +434 / -1418 lines.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Signed-off-by: Ziqiao Zhou <ziqiaozhou@microsoft.com>

x86_64

Signed-off-by: Ziqiao Zhou <ziqiaozhou@microsoft.com>
@ziqiaozhou
kernel: migrate page tables to paging crate
f8f609b 
Replace the kernel-local page table implementation with wrappers around the generic paging crate. Add the SvsmPaging adapter for allocation, address conversion, feature masks, and self-map index configuration while preserving the kernel-facing PageTable and PageTablePart APIs.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Signed-off-by: Ziqiao Zhou <ziqiaozhou@microsoft.com>
joergroedel
joergroedel reviewed Jun 11, 2026
View reviewed changes

@joergroedel joergroedel left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Overall looks great to me. I really like the new abstractions. A detail about the TLB flushing needs to be sorted out.

@joergroedel joergroedel added the in-review PR is under active review and not yet approved label Jun 11, 2026
@joergroedel joergroedel self-assigned this Jun 24, 2026
joergroedel
joergroedel reviewed Jun 24, 2026
View reviewed changes

@joergroedel joergroedel left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As I said before, the overall direction of the changes is great. The new crate looks a lot cleaner and is more generic than our previous implementation.

Two things are on my mind, though. I think I already mentioned the TLB-flushing question, but can not find the comment anymore, so I am putting it here again.

  1. The page-table code itself should not flush the TLB itself on changes, that should be up to the caller. The caller usually has better knowledge of the flushing scope than the page-table code (CPU-set to flush on, global vs. non-global, PCID, ...). What the new paging crate should provide is tracking of which addresses or ranges need to be flushed.
  2. COCONUT-SVSM has another abstraction in the page-table code: PageTablePart. This abstraction holds a sub-page-table which can be mapped into several top-level page-tables. Is there a plan to move that to the generic crate as well?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@joergroedel joergroedel joergroedel left review comments
@msft-jlange msft-jlange Awaiting requested review from msft-jlange msft-jlange is a code owner
@peterfang peterfang Awaiting requested review from peterfang peterfang is a code owner
@stefano-garzarella stefano-garzarella Awaiting requested review from stefano-garzarella stefano-garzarella is a code owner

At least 1 approving review is required to merge this pull request.

Assignees

@joergroedel joergroedel

Labels

in-review PR is under active review and not yet approved verification PR/issue related to formal verification

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@ziqiaozhou @joergroedel @luigix25 @stefano-garzarella