Support domain schedule units (us & ticks)

[midnightveil]

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]

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.

[midnightveil]

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]

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]

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
}

[midnightveil]

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

[midnightveil]

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

[Indanz]

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.

[midnightveil]

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).

[Indanz]

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.

[midnightveil]

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.

[Indanz]

us_to_ticks failing only means it prints the error before the entry is being printed, but that's easy to spot as a user because both show the problematic value. That's fine for debug only printing.

If you want to do things properly, you do need to propagate the error instead of using an overflowed value.

[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]

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]

@nspin can you confirm that this would work for the changes seL4/rust-sel4#360?

[nspin]

It would not.

Take a look at how FillEntryContent ensures compatibility:

data FillEntryContent =
      FillEntryContent_Data FillEntryContentFile
    | FillEntryContent_BootInfo FillEntryContentBootInfo
    deriving (Eq, Show, Generic)

instance ToJSON FillEntryContent where
    toJSON = genericToJSON $ sumTypeOptions "FillEntryContent_"
    toEncoding = genericToEncoding $ sumTypeOptions "FillEntryContent_"

#[derive(Debug, Clone, Eq, PartialEq)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
#[derive(rkyv::Archive, rkyv::Serialize)]
pub enum FillEntryContent<D> {
    Data(D),
    BootInfo(FillEntryContentBootInfo),
}

[nspin]

You'll want to do:

data DomainSchedDuration =
      DomainSchedDuration_Ticks Word64
    | DomainSchedDuration_Us Word64
    | DomainSchedDuration_EndMarker
    deriving (Eq, Show, Generic)

instance ToJSON FillEntryContent where
    toJSON = genericToJSON $ sumTypeOptions "DomainSchedDuration_"
    toEncoding = genericToEncoding $ sumTypeOptions "DomainSchedDuration_"

[midnightveil]

Ok, done. I don't know how to test this.

[lsf37]

It should compile at least :-). The json export is still untested in general (still todo), so I'd say it's fine to add without test for now. I'll mark it as experimental in the change log if I don't get to adding tests tomorrow.

[lsf37]

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.

For the capDL loader specs, I think we do want to leave an option open for mixed units, because that's not user-facing and it is slightly more general, but for Microkit and CAmkES we could go with just one unit.

(e.g. you could be happy with some rounding for large domain times on those boards where that matters, but maybe you want to pin down something smaller very precisely. Not sure, this is all very hypothetical, but forbidding it is policy that is not necessary, and capDL is still mechanism. Microkit and CAmkES do implement policy, so there it's fine if we want that policy)

[midnightveil]

Yeah, that's what I said here: seL4/microkit#445 (comment)

[Indanz]

Is the absolute_import needed now we dropped Python 2 support?

[midnightveil]

Probably not. I just copied the existing example. Same with print function and division, tbh...