Support domain schedule units (us & ticks) by midnightveil · Pull Request #95 · seL4/capdl

midnightveil · 2026-07-07T08:02:43Z

In the work on RFC-20 it was proposed that it would make sense
to remove the (micro)seconds-to-ticks conversions from seL4
and migrate all of (MCS) userspace APIs to be in ticks, to make dealing
with these calculations and their trickiness to instead be done
at user-level - and the tradeoffs one has to make to be no longer
kernel policy.

This PR demonstrates implements this for the capDL initialiser.
For other cases supported by the capDL specification, such
(MCS) budgets and periods currently specified in microseconds,
the capDL initialiser should be able to paper over the change
in kernel APIs without the users needing to deal with this
distinction.

These changes are motivated by the Domain schedules PR to the
seL4 Microkit, which creates a capDL specification for the
(Rust version) of the capDL initialiser to use. At the moment,
this PR is unable to be consistent about the values exposed
to the user for the units of the domain schedule: whilst we can
statically determine the us->ticks conversion for ARM/RISC-V
platforms, on x86 this is a runtime-known value only. Since
the spec is packed at system-build-time, we cannot therefore
specify x86 domain schedules in a consistent set of units.

The concrete specification changes from this PR is the addition
of a 'unit' suffix inside the domain schedule syntax. The
initialiser can then support either ticks (the default without
any units) or microseconds, and it performs a runtime conversion
of this value to ticks for the domain scheduler API.

Canonically, the end marker is left without units as (0, 0), but
we permit inputs of (0, 0 ticks) or (0, 0 us) for consistency.

Note: the meaning of a kernel tick is different between MCS and
non-MCS configurations.

One consequence of taking input in 'us' is that there are cases
where the input is unrepresentable in 'ticks'; and so this
introduces the possiblity of failure in the initialiser that
is unchecked at build-time.

For non-MCS, as kernel ticks are an integer multiple of 1 ms,
the conversion from us to ticks will fail if the conversion is
not exact. This is easy to avoid, one has to specify a 'us' value
that is a multiple of (CONFIG_TIMER_TICK_MS * 1000), something
which does not differ per platform.

For MCS, the kernel tick reflects the underlying timer frequency
(for the domain scheduler). Thus, there exists many frequencies
for which it is impossible to be exact in the conversion from
us to ticks. (those frequencies above 1 MHz, which is most
of them on modern 64-bit platforms). We guarantee a conversion
that is accurate to the nearest tick value, or failure otherwise.
This can be ±1 timer period. If you want to specify durations of
length close to the period between timer ticks, please use ticks
exactly. However, depending on kernel WCET domains of this
duration may not be schedulable.

Original PR description

This is partially an experiment, but to make this useful for userspace programs, it makes sense for the capDL specification to treat the domain schedule values as microseconds, instead of timer ticks.

In the work on RFC-20 it was proposed that it would make sense to remove this (micro)seconds-to-ticks conversions from seL4 and migrate all of userspace APIs to be in ticks, to make dealing with these calculations and their trickiness to instead be done at user-level.

This PR demonstrates that it should be possible to do this for at least the capDL initialiser. For other cases supported by the capDL specification, such as (MCS) budgets and periods currently specified in microseconds, the capDL initialiser should be able to paper over the change in kernel APIs without the users needing to deal with this distinction.

These changes are motivated by the Domain schedules PR to the seL4 Microkit, which creates a capDL specification for the (Rust version) of the capDL initialiser to use. At the moment, this PR is unable to be consistent about the values exposed to the user for the units of the domain schedule: whilst we can statically determine the us->ticks conversion for ARM/RISC-V platforms, on x86 this is a runtime-known value only. Since the spec is packed at system-build-time, we cannot therefore specify x86 domain schedules in a consistent set of units.

(Note, I haven't actually tested that this works, but I have tested a similar change to rust-seL4 capDL initialiser. This PR is mostly for discussion; this could likely also move to a formal RFC).

lsf37 · 2026-07-07T08:36:19Z

Generally, this would be good addition, but we do need to retain the ability to specify the duration in ticks, so we can't just change the unit. We'll need a mechanism to specify the unit.

The whole point of making the interface be ticks is that the FIXME for AArch32 that is still in there is not nicely solvable in general (the method the kernel currently has is flawed in multiple ways). It does not necessarily need to be fully solved in general, because on the platforms where it is problematic you likely to want to compute in ticks anyway.

I.e. if we use the current (flawed) kernel method for conversion on AArch32 but also have a capDL ticks interface available, the flaws are avoidable for the systems where that matters.

Indanz

I think it makes sense to make things easier to configure for user space, which means doing it in real time instead of ticks. User space doesn't run into the problems that the kernel has as much, so the trade-off is different there.

Indanz · 2026-07-07T08:15:31Z

+     * timer frequency to us at build time, in Hertz */
+    uin64_t timer_frequency = CONFIG_TIMER_FREQUENCY;
+
+    /* FIXME: On ARM32 we need to pull in a 64-bit division helper;


Those should be part of the compiler built-in already: There is an __aeabi_uldivmod which will be used automatically for 64-bit divisions on 32-bit Arm.

This is one of the reasons why doing this in user space is easier than in the kernel.

Well, that's part of libgcc (GCC) or compiler-rt (LLVM), which may or may not be linked in the builds here; however, broadly yes.

I suppose it depends on how verified you want your user space to be, that's the only reason I can think of for not linking to the compiler library in user space. But I don't see anyone putting that amount of effort into this for 32-bit platforms. (And if they do, they can always use the ticks interface if this is a problem for verification.)

OK, it looks like maybe because the frequency is a constant this is elided entirely. That or it is already linked, so this just does work for arm32.

Easy to check with a disassemble. But if the value is constant the division is probably replaced with shifts and multiplies. If frequency is a whole MHz, the calculation can be transformed back to duration_us multiplied by a constant. The maaxboard has frequency 8333333, that's probably a better test.

Indanz · 2026-07-07T08:23:27Z

+            Note: there are some values of us which would cause unrepresentable
+                  values in ticks; we should add a static check to error out.


Yes, that's the main question: How do you deal with non-whole MHz clock frequencies. If there is no exact conversion you at least want to warn the user about this. Ideally the user should be able to specify whether a time needs to be exact or not.

I have made this check.

midnightveil · 2026-07-08T03:36:41Z

Generally, this would be good addition, but we do need to retain the ability to specify the duration in ticks, so we can't just change the unit. We'll need a mechanism to specify the unit.

Hrm. I don't think I know if there's any cases like this, I suppose... Might need to hand-roll something specific for units here. ACK, this is just an implementation thing mostly then.

lsf37 · 2026-07-08T05:50:03Z

Hrm. I don't think I know if there's any cases like this, I suppose... Might need to hand-roll something specific for units here. ACK, this is just an implementation thing mostly then.

Yes, no problem with us from the conceptual side, as long as we can also do ticks.

midnightveil · 2026-07-13T05:24:36Z

I haven't tested this at runtime yet (working on it), but in theory the capDL spec now supports units, parses them, and then sends them to the C loader which either computes ticks at runtime or uses the us value.

Here's what that looks like:

domains {
  schedule: [
    (0, 10),
    (1, 10 ticks),
    (0, 0),
    (2, 2 us),
    -- Canonical representation has no unit on the end markers, but we allow it
    -- as a valid input.
    (0, 0 us),
  ]

The canonicalised becomes:

domains {
  schedule: [(0, 10 ticks), (1, 10 ticks), (0, 0), (2, 2 us), (0, 0)]
  domain_set_start: 3
  index_shift: 1
}

Indanz · 2026-07-13T10:41:13Z

+typedef struct {
+    /* kind of the schedentry: a ticks entry, us entry, or an end marker */
+    CDL_DomainSchedEntryKind_t kind;
+    /* 8-bit domain number */
+    uint8_t domain;
+    /* 56-bit duration */
+    uint64_t duration;
+} CDL_DomainSchedEntry;


This structure has padding, I thought it was preferred to avoid that for verification?

Since we're not currently verifying the C version of the loader, we can be leave this for now. When we do at a later point, it'll not be too hard to add a manual padding field, which should not be a breaking change. So I don't think it's a problem for now.

midnightveil · 2026-07-15T06:35:57Z

I will note that if I specify a very large number in the camkes domain file it will silently truncate this to 64 bits which is weird, but I can now test invalid input cases.

init_domains@main.c:2178  Initialising domains...
init_domains@main.c:2184    Domain schedule entry[0]: domain 0 duration: 6000 us
init_domains@main.c:2206    Domain schedule entry[0]: domain 0 ticks: 375000
init_domains@main.c:2184    Domain schedule entry[1]: domain 1 duration: 8000 us
init_domains@main.c:2206    Domain schedule entry[1]: domain 1 ticks: 500000
init_domains@main.c:2184    Domain schedule entry[2]: domain 2 duration: 13371215493478744064 us
us_to_ticks@main.c:2114 [Cond failed: (duration_us / US_IN_SECOND) >= ((1ULL << 56) / timer_frequency)]
        Input us would overflow 64-bits or exceed 56-bit tick maximum
sys_rt_sigprocmask@sys_exit.c:32 Ignoring call to sys_rt_sigprocmask

Style checker was complaining. Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>

In the work on [RFC-20] it was proposed that it would make sense to remove the (micro)seconds-to-ticks conversions from seL4 and migrate all of (MCS) userspace APIs to be in ticks, to make dealing with these calculations and their trickiness to instead be done at user-level - and the tradeoffs one has to make to be no longer kernel policy. This PR demonstrates implements this for the capDL initialiser. For other cases supported by the capDL specification, such (MCS) budgets and periods currently specified in microseconds, the capDL initialiser should be able to paper over the change in kernel APIs without the users needing to deal with this distinction. These changes are motivated by the [Domain schedules] PR to the seL4 Microkit, which creates a capDL specification for the (Rust version) of the capDL initialiser to use. At the moment, this PR is unable to be consistent about the values exposed to the user for the units of the domain schedule: whilst we can statically determine the us->ticks conversion for ARM/RISC-V platforms, on x86 this is a runtime-known value only. Since the spec is packed at system-build-time, we cannot therefore specify x86 domain schedules in a consistent set of units. The concrete specification changes from this PR is the addition of a 'unit' suffix inside the domain schedule syntax. The initialiser can then support either ticks (the default without any units) or microseconds, and it performs a runtime conversion of this value to ticks for the domain scheduler API. Canonically, the end marker is left without units as (0, 0), but we permit inputs of (0, 0 ticks) or (0, 0 us) for consistency. Note: the meaning of a kernel tick is different between MCS and non-MCS configurations. One consequence of taking input in 'us' is that there are cases where the input is unrepresentable in 'ticks'; and so this introduces the possiblity of failure in the initialiser that is unchecked at build-time. For non-MCS, as kernel ticks are an integer multiple of 1 ms, the conversion from us to ticks will fail if the conversion is not exact. This is easy to avoid, one has to specify a 'us' value that is a multiple of (CONFIG_TIMER_TICK_MS * 1000), something which does not differ per platform. For MCS, the kernel tick reflects the underlying timer frequency (for the domain scheduler). Thus, there exists many frequencies for which it is impossible to be exact in the conversion from us to ticks. (those frequencies above 1 MHz, which is most of them on modern 64-bit platforms). We guarantee a conversion that is accurate to the nearest tick value, or failure otherwise. This can be ±1 timer period. If you want to specify durations of length close to the period between timer ticks, please use ticks exactly. However, depending on kernel WCET domains of this duration may not be schedulable. [RFC-20]: seL4/rfcs#33 [Domain schedules]: seL4/microkit#445 Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>

midnightveil · 2026-07-15T06:44:50Z

OK, this should be ready for re-review now.

Indanz · 2026-07-15T09:56:59Z

+    uint64_t ticks = duration_s * timer_frequency
+                     + ((duration_us_frac * timer_frequency + US_IN_SECOND / 2) / (US_IN_SECOND));


It only doesn't fit because you chose unnecessarily long names for all the variables. :-)

Worth mentioning that you do rounding here.

Yes, I suppose I should mention the same notes I left in the documentation here about the behaviour.

Yes, that would be nice.

Indanz · 2026-07-15T10:13:13Z

+     * timer frequency to us at build time, in Hertz */
+    uin64_t timer_frequency = CONFIG_TIMER_FREQUENCY;
+
+    /* FIXME: On ARM32 we need to pull in a 64-bit division helper;


Easy to check with a disassemble. But if the value is constant the division is probably replaced with shifts and multiplies. If frequency is a whole MHz, the calculation can be transformed back to duration_us multiplied by a constant. The maaxboard has frequency 8333333, that's probably a better test.

Indanz · 2026-07-15T10:17:09Z

+    void *tsc_freq_mhz_addr = (void *)tsc_freq_hdr + sizeof(seL4_BootInfoHeader);
+    uint32_t tsc_freq_mhz = *(uint32_t *)tsc_freq_mhz_addr;


Suggested change

void *tsc_freq_mhz_addr = (void *)tsc_freq_hdr + sizeof(seL4_BootInfoHeader);

uint32_t tsc_freq_mhz = *(uint32_t *)tsc_freq_mhz_addr;

uint32_t tsc_freq_mhz = *(uint32_t *)&tsc_freq_hdr[1];

I don't like this. Maybe I'm wrong here but it feels wrong to treat this like an array of headers.

uint32_t tsc_freq_mhz = *(uint32_t *)(tsc_freq_hdr + 1); also works. And the +1 is exactly the same as + sizeof(seL4_BootInfoHeader), except you know for sure you didn't make a mistake with the type.

But feel free to leave it as it is, it's just a suggestion.

I would prefer to leave as is. I don't like the +1 implicitly being strided by the size of the type.

Indanz · 2026-07-15T11:32:20Z

+            assert(!"unreachable");
+        }
+
+        ZF_LOGD("                                      ticks: %lu", duration_ticks);


This looks weird. Is it for testing only or do you want to keep it? Can combine it with the previous debug print if you move that one to here.

This only gets emitted if compiled with verbose logging. I can't combine it with a previous on one line because ZF_LOG functions (annoyingly) add a newline by default, probably because they prefix each line with the location.

I don't want to move the previous print here because then errors won't have printed out the data. However I guess I could make errors more informative (it just makes us_to_ticks more annoying because then I need to return if an error occurred).

Why can't you just add it as extra output (on the same line) to:

ZF_LOGD(" Domain schedule entry[%lu]: domain %d duration: %llu %s", i + spec->domainIndexShift, entry.domain, (unsigned long long)entry.duration, (entry.kind == CDL_DomainSchedEntryKind_Us) ? "us" : ((entry.kind == CDL_DomainSchedEntryKind_Ticks) ? "ticks" : "[end marker]"));

print?

Moving that one down to here should be fine. Only error is the default case which should be unreachable anyway. And that us_to_ticks prints warnings before this print is fine too, it's clear enough from the output to which entry it belongs.

us_to_ticks can fail. so moving it down won't print out the entry before hand if it does. I guess I could make us_to_ticks propagate an error but that's really annoying.

lsf37

I'm happy with this. I don't have a strong opinion on the C style questions either way. Happy for Julia to decide.

Indanz · 2026-07-19T12:21:21Z

The main open question before merging this is whether we want units for each entry, like implemented here, or a global property on the schedule which chooses the time units, like proposed by @Furao seL4/microkit#445 (comment):

I think a duration_unit or duration_type attribute in the domain_schedule element would be better than making this duration a value and a unit. It would make parsing easier and I can't imagine wanting a schedule that mixes units.

midnightveil requested review from Indanz and lsf37 July 7, 2026 08:03

Indanz reviewed Jul 7, 2026

View reviewed changes

midnightveil commented Jul 13, 2026

View reviewed changes

Comment thread capdl-loader-app/src/main.c Outdated

Indanz reviewed Jul 13, 2026

View reviewed changes

midnightveil commented Jul 13, 2026

View reviewed changes

Comment thread capDL-tool/CapDL/Model.hs

midnightveil mentioned this pull request Jul 14, 2026

Support units in domain schedule declarations seL4/camkes-tool#178

Open

midnightveil force-pushed the julia/microsecond-domsched branch from f8d9ef5 to e28d1f4 Compare July 14, 2026 05:58

midnightveil changed the title ~~capdl-loader-app: spec for domain schedule in us~~ Support domain schedule units (us & ticks) Jul 14, 2026

midnightveil marked this pull request as draft July 14, 2026 06:03

midnightveil mentioned this pull request Jul 15, 2026

Formal Correctness Proos of us_to_ticks conversion in the initialiser #98

Open

midnightveil force-pushed the julia/microsecond-domsched branch from e28d1f4 to b9fce32 Compare July 15, 2026 06:36

midnightveil marked this pull request as ready for review July 15, 2026 06:38

midnightveil mentioned this pull request Jul 15, 2026

domains: support MCS and non-MCS, use units seL4/camkes#38

Open

midnightveil added 2 commits July 15, 2026 16:43

python-capdl-tool: fix style

33e03af

Style checker was complaining. Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>

midnightveil force-pushed the julia/microsecond-domsched branch from b9fce32 to b1df4dc Compare July 15, 2026 06:43

Indanz reviewed Jul 15, 2026

View reviewed changes

midnightveil mentioned this pull request Jul 16, 2026

domains: support units for schedule duration seL4/rust-sel4#360

Open

lsf37 approved these changes Jul 19, 2026

View reviewed changes

		Note: there are some values of us which would cause unrepresentable
		values in ticks; we should add a static check to error out.

		uint64_t ticks = duration_s * timer_frequency
		+ ((duration_us_frac * timer_frequency + US_IN_SECOND / 2) / (US_IN_SECOND));

		void tsc_freq_mhz_addr = (void )tsc_freq_hdr + sizeof(seL4_BootInfoHeader);
		uint32_t tsc_freq_mhz = (uint32_t )tsc_freq_mhz_addr;

	void tsc_freq_mhz_addr = (void )tsc_freq_hdr + sizeof(seL4_BootInfoHeader);
	uint32_t tsc_freq_mhz = (uint32_t )tsc_freq_mhz_addr;
	uint32_t tsc_freq_mhz = (uint32_t )&tsc_freq_hdr[1];

Uh oh!

Conversation

midnightveil commented Jul 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

lsf37 commented Jul 7, 2026

Uh oh!

Indanz left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Indanz Jul 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

midnightveil commented Jul 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

lsf37 commented Jul 8, 2026

Uh oh!

midnightveil commented Jul 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

midnightveil commented Jul 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

midnightveil commented Jul 15, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Indanz Jul 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

midnightveil Jul 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

midnightveil commented Jul 7, 2026 •

edited

Loading

Indanz left a comment •

edited

Loading

Indanz Jul 7, 2026 •

edited

Loading

midnightveil commented Jul 8, 2026 •

edited

Loading

midnightveil commented Jul 13, 2026 •

edited

Loading

midnightveil commented Jul 15, 2026 •

edited

Loading

Indanz Jul 15, 2026 •

edited

Loading

midnightveil Jul 19, 2026 •

edited

Loading