Skip to content

Conversation

@Indanz
Copy link
Contributor

@Indanz Indanz commented Sep 10, 2025

Implements RFC-20.

TODO:

  • Rename DomainSetSet to DomainSet?
  • Update manual.
  • Add tests to sel4test.
  • Check if generated code is reasonable.
  • Ease verification.

@Indanz Indanz marked this pull request as draft September 10, 2025 10:28
@lsf37
Copy link
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
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.

Copy link
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
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.

@Indanz Indanz force-pushed the domain branch 2 times, most recently from 8478ad1 to dc84b9b Compare December 29, 2025 21:43
Implements RFC-20.

Signed-off-by: Indan Zupancic <indan@nul.nu>
Useful for configuring domains.

Signed-off-by: Indan Zupancic <indan@nul.nu>
#define DSCHED_MAX_DURATION (UINT64_MAX >> DSCHED_DOMAIN_BITS)
#define DSCHED_DURATION_MASK DSCHED_MAX_DURATION

static dschedule_t dschedule_make(dom_t domain, uint64_t duration)
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
static dschedule_t dschedule_make(dom_t domain, uint64_t duration)
static inline dschedule_t dschedule_make(dom_t domain, uint64_t duration)

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

Development

Successfully merging this pull request may close these issues.

3 participants