Skip to content

Fixes for crates/sel4 and crates/sel4-capdl-initializer - #278

Merged
nspin merged 9 commits into
seL4:mainfrom
au-ts:capdl-vmattr-fix
Sep 1, 2025
Merged

Fixes for crates/sel4 and crates/sel4-capdl-initializer#278
nspin merged 9 commits into
seL4:mainfrom
au-ts:capdl-vmattr-fix

Conversation

@dreamliner787-9

@dreamliner787-9 dreamliner787-9 commented Aug 5, 2025

Copy link
Copy Markdown
Contributor

crates/sel4:

  • Fixed ARM SMC initial cap macro condition.
  • Added RISC-V specific IRQ invocation.
  • Added x86 vCPU object blueprint and set TCB invocation.

crates/sel4-capdl-initializer:

  • Fixed incorrect default VM Attributes on ARM that can cause seL4 to halt when touching device memory on physical platforms.
  • Added ARM SMC and RISC-V IRQ objects to CapDL spec.
  • Added vCPU bind TCB call for x86.

@dreamliner787-9
dreamliner787-9 requested a review from nspin as a code owner August 5, 2025 00:48
@dreamliner787-9 dreamliner787-9 changed the title crates/sel4-capdl-initializer: fix incorrect VM attributes on ARM. Fixes for crates/sel4 and crates/sel4-capdl-initializer Aug 5, 2025
Comment thread crates/sel4-capdl-initializer/core/src/lib.rs Outdated
Comment thread crates/sel4-capdl-initializer/types/src/when_sel4.rs Outdated
@dreamliner787-9
dreamliner787-9 force-pushed the capdl-vmattr-fix branch 2 times, most recently from dedcc07 to 9985cf8 Compare August 5, 2025 03:05
dreamliner787-9 added a commit to au-ts/microkit that referenced this pull request Aug 14, 2025
…ed on PR seL4/rust-sel4#278

Signed-off-by: Bill Nguyen <bill.nguyen@student.unsw.edu.au>

@nspin nspin 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.

This all looks great, thank you for these fixes.

Sorry it's taken me a little while to get around to reviewing them.

See comments above.

Comment thread crates/sel4-capdl-initializer/types/src/when_sel4.rs
Comment thread crates/sel4-capdl-initializer/types/src/when_sel4.rs Outdated
Comment thread crates/sel4-capdl-initializer/core/src/lib.rs Outdated
Comment thread crates/sel4/src/arch/riscv/invocations.rs Outdated
Comment thread crates/sel4-capdl-initializer/core/src/lib.rs Outdated
This wasn't a problem on QEMU. But on physical
platform, R/W to device memory will cause seL4 to halt.

Signed-off-by: Bill Nguyen <bill.nguyen@student.unsw.edu.au>
Signed-off-by: Bill Nguyen <bill.nguyen@student.unsw.edu.au>
@dreamliner787-9

Copy link
Copy Markdown
Contributor Author

Hi Nick, thank you for your review. I've fixed all the issues you highlighted. Please let me know what you think.

@nspin nspin 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.

Looks great, thanks.

I added one more comment for a change I missed in my first review. After that change we'll merge.

Comment thread crates/sel4-capdl-initializer/core/src/lib.rs Outdated
This works by creating a "fake" ARM SMC object, which is
assigned the initial thread's SMC cap. Then we can mint
it to any CSpace just like other object types.

Signed-off-by: Bill Nguyen <bill.nguyen@student.unsw.edu.au>
Signed-off-by: Bill Nguyen <bill.nguyen@student.unsw.edu.au>
Signed-off-by: Bill Nguyen <bill.nguyen@student.unsw.edu.au>
Signed-off-by: Bill Nguyen <bill.nguyen@student.unsw.edu.au>
Signed-off-by: Bill Nguyen <bill.nguyen@student.unsw.edu.au>
Signed-off-by: Bill Nguyen <bill.nguyen@student.unsw.edu.au>
Signed-off-by: Bill Nguyen <bill.nguyen@student.unsw.edu.au>
@nspin
nspin merged commit 285045d into seL4:main Sep 1, 2025
14 checks passed
@nspin

nspin commented Sep 1, 2025

Copy link
Copy Markdown
Member

Merged, thanks!

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants