Skip to content

Runtime Domain Schedules#1511

Merged
lsf37 merged 3 commits intoseL4:masterfrom
Indanz:domain
Mar 24, 2026
Merged

Runtime Domain Schedules#1511
lsf37 merged 3 commits intoseL4:masterfrom
Indanz:domain

Conversation

@Indanz
Copy link
Copy Markdown
Contributor

@Indanz Indanz commented Sep 10, 2025

Implements RFC-20.

TODO:

  • Document new syscalls.
  • Update existing Domains chapter.
  • Add tests to sel4test.
  • Check if generated code is reasonable.
  • Ease verification.

Test with seL4/sel4test#151

@Indanz Indanz marked this pull request as draft September 10, 2025 10:28
@lsf37
Copy link
Copy Markdown
Member

lsf37 commented Sep 10, 2025

Good to see the old domain tests failing -- that means we're actually doing something :). This should disappear once we've updated sel4test accordingly.

@Indanz Indanz force-pushed the domain branch 3 times, most recently from cf74237 to 5a31b7d Compare December 13, 2025 16:13
@Indanz Indanz marked this pull request as ready for review December 13, 2025 16:14
@Indanz
Copy link
Copy Markdown
Contributor Author

Indanz commented Dec 13, 2025

Main changes:

  • Changed to 64-bit only version.
  • Moved all domain code from tcb.c to src/object/domain.c
  • Removed activate argument.

Comment thread CHANGES.md Outdated
Comment thread src/object/domain.c Outdated
Comment thread src/object/domain.c Outdated
Comment thread libsel4/include/interfaces/object-api.xml Outdated
Comment thread libsel4/include/interfaces/object-api.xml Outdated
Comment thread libsel4/include/interfaces/object-api.xml Outdated
Copy link
Copy Markdown
Member

@lsf37 lsf37 left a comment

Choose a reason for hiding this comment

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

This is looking good to me and is implementing the RFC as approved. Will leave out the tick for now so we don't accidentally merge before verification is finished.

@lsf37 lsf37 added the verification Needs formal verification input/change, or is motivated by verification label Dec 15, 2025
@lsf37
Copy link
Copy Markdown
Member

lsf37 commented Dec 15, 2025

  • Rename DomainSetSet to DomainSet?

Given that the change is only breaking if you are using the kernel API directly, we should at least have a deprecation period for the old DomainSetSet if we change it.

Comment thread src/model/statedata.c
Comment thread include/object/domain.h Outdated
Comment thread include/object/domain.h Outdated
Comment thread libsel4/include/interfaces/object-api.xml
Comment thread libsel4/include/interfaces/object-api.xml Outdated
Comment thread src/object/domain.c Outdated
@Indanz Indanz force-pushed the domain branch 3 times, most recently from dc84b9b to 76f0ae6 Compare December 31, 2025 19:12
Useful for configuring domains.

Signed-off-by: Indan Zupancic <indan@nul.nu>
@Indanz Indanz force-pushed the domain branch 3 times, most recently from 4173682 to 7c1551d Compare March 13, 2026 17:20
@lsf37
Copy link
Copy Markdown
Member

lsf37 commented Mar 14, 2026

The end marker change looks good, still need to update the proofs for it.

Comment thread src/object/domain.c Outdated
Implementation of RFC-20.

Signed-off-by: Indan Zupancic <indan@nul.nu>
@lsf37 lsf37 merged commit 27a52dd into seL4:master Mar 24, 2026
36 of 44 checks passed
@lsf37 lsf37 moved this from In Progress to Done in seL4 March'26 release (31 March) Mar 24, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

verification Needs formal verification input/change, or is motivated by verification

Projects

No open projects

Development

Successfully merging this pull request may close these issues.

4 participants