From 58f96a779c1c954a04efeffb790d549111504cc0 Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Wed, 15 Jul 2026 16:42:50 +1000 Subject: [PATCH 1/3] python-capdl-tool: fix style Style checker was complaining. Signed-off-by: Julia Vassiliki --- python-capdl-tool/capdl/util.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/python-capdl-tool/capdl/util.py b/python-capdl-tool/capdl/util.py index d13d5775..6d48f071 100644 --- a/python-capdl-tool/capdl/util.py +++ b/python-capdl-tool/capdl/util.py @@ -342,8 +342,8 @@ def ctz(size_bytes): Count trailing zeros in a python integer. The value must be greater than 0. """ - assert(size_bytes > 0) - assert(isinstance(size_bytes, six.integer_types)) + assert (size_bytes > 0) + assert (isinstance(size_bytes, six.integer_types)) low = size_bytes & -size_bytes low_bit = -1 while low: From 57e35afcd63f3c2503d480ce35ab7b81b06235ef Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Tue, 7 Jul 2026 17:55:59 +1000 Subject: [PATCH 2/3] Support domain schedule units (us & ticks) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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]: https://github.com/seL4/rfcs/pull/33 [Domain schedules]: https://github.com/seL4/microkit/pull/445 Signed-off-by: Julia Vassiliki --- capDL-tool/CapDL/AST.hs | 9 ++- capDL-tool/CapDL/MakeModel.hs | 22 ++++-- capDL-tool/CapDL/Model.hs | 20 ++++- capDL-tool/CapDL/Parser.hs | 18 +++-- capDL-tool/CapDL/PrintC.hs | 18 +++-- capDL-tool/CapDL/PrintModel.hs | 12 ++- capDL-tool/CapDL/PrintXml.hs | 10 ++- capDL-tool/doc/capDL.md | 17 +++- capDL-tool/example-arm.cdl | 10 ++- capDL-tool/example-arm.right | 2 +- capdl-loader-app/include/capdl.h | 19 ++++- capdl-loader-app/src/main.c | 109 ++++++++++++++++++++++++-- python-capdl-tool/capdl/Spec.py | 14 ++-- python-capdl-tool/capdl/__init__.py | 2 +- python-capdl-tool/capdl/util.py | 6 ++ python-capdl-tool/examples/domains.py | 28 +++++++ 16 files changed, 267 insertions(+), 49 deletions(-) create mode 100644 python-capdl-tool/examples/domains.py diff --git a/capDL-tool/CapDL/AST.hs b/capDL-tool/CapDL/AST.hs index 67147461..c1aa8d99 100644 --- a/capDL-tool/CapDL/AST.hs +++ b/capDL-tool/CapDL/AST.hs @@ -201,9 +201,16 @@ data KODecl = KODecl { object :: KO } deriving (Show, Eq) +data DomainSchedEntryUnitDecl + = DomainSchedEntryUnitTicksDecl + | DomainSchedEntryUnitUsDecl + deriving (Show, Eq) + +type DomainSchedEntryDecl = (Word, Word64, Maybe DomainSchedEntryUnitDecl) + data DomainDeclItem = DomScheduleDecl { - domSchedule :: [(Word, Word64)] } + domSchedule :: [DomainSchedEntryDecl] } | DomStartDecl { domStart :: Maybe Word } | DomIdxShiftDecl { diff --git a/capDL-tool/CapDL/MakeModel.hs b/capDL-tool/CapDL/MakeModel.hs index c6e24f7f..5d20231a 100644 --- a/capDL-tool/CapDL/MakeModel.hs +++ b/capDL-tool/CapDL/MakeModel.hs @@ -1013,9 +1013,15 @@ isDomIdxShiftDecl :: DomainDeclItem -> Bool isDomIdxShiftDecl (DomIdxShiftDecl _) = True isDomIdxShiftDecl _ = False +getDomScheduleEntry :: DomainSchedEntryDecl -> DomScheduleEntry +getDomScheduleEntry (dom, 0, _) = (dom, DomScheduleDurationEnd) +getDomScheduleEntry (dom, duration, Just DomainSchedEntryUnitUsDecl) = (dom, DomScheduleDurationUs duration) +getDomScheduleEntry (dom, duration, Just DomainSchedEntryUnitTicksDecl) = (dom, DomScheduleDurationTicks duration) +getDomScheduleEntry (dom, duration, Nothing) = (dom, DomScheduleDurationTicks duration) + getDomSchedule :: [DomainDeclItem] -> Maybe DomSchedule getDomSchedule [] = Nothing -getDomSchedule [DomScheduleDecl sched] = Just sched +getDomSchedule [DomScheduleDecl sched] = Just (map getDomScheduleEntry sched) getDomSchedule _ = error "Must declare at most one domains section" getDomStart :: [DomainDeclItem] -> Maybe Word @@ -1028,16 +1034,18 @@ getDomIdxShift [] = 0 getDomIdxShift [DomIdxShiftDecl shift] = shift getDomIdxShift _ = error "Must declare at most one domain index shift" -checkDomainItem :: (Word, Word64) -> Bool +checkDomainItem :: DomScheduleEntry -> Bool checkDomainItem (domain, duration) = let itemStr = "Domain schedule item " ++ show (domain, duration) ++ ": " in - if duration == 0 && domain /= 0 - then error $ itemStr ++ "Duration cannot be zero for non-end-markers. End marker is (0, 0)." + if duration == DomScheduleDurationEnd && domain /= 0 + then error $ itemStr ++ "Domain cannot be non-zero for duration 0. End marker is (0, 0)." else if domain > 255 then error $ itemStr ++ "Domain must be in [0 .. 255]" - else if duration >= 2^56 - then error $ itemStr ++ "Duration must be less than 2^56" + else if (case duration of + DomScheduleDurationTicks ticks -> ticks >= 2^56 + _ -> False) + then error $ itemStr ++ "Duration (ticks) must be less than 2^56" else True checkDomains :: Model a -> Model a @@ -1047,7 +1055,7 @@ checkDomains m@(Model _ _ _ _ _ (Just sched) dstart _) show (length sched - 1) ++ "] for the given schedule." | not $ all checkDomainItem sched = error "Invalid domain schedule" -- actual error will be raised in checkDomainItem - | isJust dstart && sched !! fromIntegral (fromJust dstart) == (0, 0) = + | isJust dstart && (sched !! fromIntegral (fromJust dstart)) == (0, DomScheduleDurationEnd) = error $ "Start index (" ++ show (fromJust dstart) ++ ") must not point to the end marker (0, 0) in the schedule." | otherwise = m diff --git a/capDL-tool/CapDL/Model.hs b/capDL-tool/CapDL/Model.hs index a6c1476b..91edd71f 100644 --- a/capDL-tool/CapDL/Model.hs +++ b/capDL-tool/CapDL/Model.hs @@ -312,7 +312,25 @@ getUTCover = Map.findWithDefault [] type CDT = Map CapRef CapRef -type DomSchedule = [(Word, Word64)] +-- seL4 sees the domain schedule in ticks, and represents the end marker +-- as the value (0, 0), i.e. 0 ticks is the end marker. +-- In the capDL model, as we also want to handle 'us' units as well as 'ticks', +-- we also explicitly model the end marker. We thus enforce that the ticks/us +-- values are always non-zero. One reason for this is our sanity checks around +-- end markers benefit from being able to check this directly, and it does not +-- matter what the '0' value units are. +data DomScheduleDuration + = DomScheduleDurationTicks { + ticks :: Word64 } + | DomScheduleDurationUs { + us :: Word64 } + | DomScheduleDurationEnd + deriving (Show, Eq) + +-- pair of (domain, duration) +type DomScheduleEntry = (Word, DomScheduleDuration) + +type DomSchedule = [DomScheduleEntry] -- -- The state of the system. diff --git a/capDL-tool/CapDL/Parser.hs b/capDL-tool/CapDL/Parser.hs index aa4e8f45..eab2a18a 100644 --- a/capDL-tool/CapDL/Parser.hs +++ b/capDL-tool/CapDL/Parser.hs @@ -12,7 +12,6 @@ import Prelude () import Prelude.Compat import CapDL.AST import CapDL.ParserUtils -import Data.Word (Word64) import Text.ParserCombinators.Parsec @@ -100,13 +99,18 @@ cap_decls = do reserved "caps" braces $ many (try cap_name_decl <|> try cap_decl) -word_pair :: MapParser (Word, Word64) -word_pair = +dom_sched_entry :: MapParser DomainSchedEntryDecl +dom_sched_entry = parens $ do - a <- number + domain <- number comma - b <- integer64 - return (a, b) + duration <- integer64 + unit <- (do reserved "ticks" + return $ Just DomainSchedEntryUnitTicksDecl) + <|> (do reserved "us" + return $ Just DomainSchedEntryUnitUsDecl) + <|> (do return Nothing) + return (domain, duration, unit) dom_content :: MapParser DomainDeclItem dom_content = @@ -119,7 +123,7 @@ dom_content = do reserved "schedule" colon - fmap DomScheduleDecl $ brackets $ sepEndBy1 word_pair comma + fmap DomScheduleDecl $ brackets $ sepEndBy1 dom_sched_entry comma <|> do reserved "index_shift" diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs index 17f3f3c8..e06f07a0 100644 --- a/capDL-tool/CapDL/PrintC.hs +++ b/capDL-tool/CapDL/PrintC.hs @@ -23,7 +23,6 @@ import qualified Data.Map as Map import Data.Map (Map) import qualified Data.Set as Set import Data.Bits -import Data.Word (Word64) import Numeric (showHex) import Text.PrettyPrint @@ -507,16 +506,21 @@ showASIDPoolDerivations objs ms = joinBy ",\n" [" " ++ idStr | idStr <- array] +++ "}," -showDomainScheduleItem :: (Word, Word64) -> String +showDomainScheduleItem :: (Word, DomScheduleDuration) -> String showDomainScheduleItem (domain, duration) = - let dbits = 56 - mask n = (1 `shiftL` n) - 1 - entry = fromIntegral domain `shiftL` dbits .|. duration .&. mask dbits - in hex entry + let (value, unit) = case duration of + DomScheduleDurationTicks ticks -> (ticks, "CDL_DomainSchedEntryKind_Ticks") + DomScheduleDurationUs us -> (us, "CDL_DomainSchedEntryKind_Us") + DomScheduleDurationEnd -> (0, "CDL_DomainSchedEntryKind_End") + in "{" +++ + ".kind = " ++ unit ++ "," +++ + ".domain = " ++ (show domain) ++ "," +++ + ".duration = " ++ (show value) +++ + "}" showDomainSchedule :: DomSchedule -> String showDomainSchedule dsched = - "(uint64_t[]){" +++ + "(CDL_DomainSchedEntry[]){" +++ " " ++ joinBy ", " (map showDomainScheduleItem dsched) +++ "}" diff --git a/capDL-tool/CapDL/PrintModel.hs b/capDL-tool/CapDL/PrintModel.hs index 06f2b062..33be70d4 100644 --- a/capDL-tool/CapDL/PrintModel.hs +++ b/capDL-tool/CapDL/PrintModel.hs @@ -12,7 +12,6 @@ import CapDL.PrintUtils import Prelude () import Prelude.Compat hiding ((<>)) import Text.PrettyPrint -import Data.Word (Word64) import Data.List.Compat import qualified Data.Map as Map @@ -205,11 +204,16 @@ prettyMappings (Model _ ms irqNode cdt untypedCovers _ _ _) = text "}" $+$ text "" -prettyWordPair :: (Word, Word64) -> Doc -prettyWordPair (a,b) = parens (num a <> comma <+> integer (toInteger b)) +prettyScheduleEntry :: DomScheduleEntry -> Doc +prettyScheduleEntry (domain, duration) = + let (value, unit) = case duration of + DomScheduleDurationTicks ticks -> (ticks, Just "ticks") + DomScheduleDurationUs us -> (us, Just "us") + DomScheduleDurationEnd -> (0, Nothing) + in parens (num domain <> comma <+> integer (toInteger value) <> text (maybe "" (\unit -> " " ++ unit) unit)) prettySchedule :: DomSchedule -> Doc -prettySchedule sched = fsep $ punctuate comma (map prettyWordPair sched) +prettySchedule sched = fsep $ punctuate comma (map prettyScheduleEntry sched) prettyDomains :: Maybe DomSchedule -> Maybe Word -> Word -> Doc prettyDomains Nothing _ _ = mempty diff --git a/capDL-tool/CapDL/PrintXml.hs b/capDL-tool/CapDL/PrintXml.hs index 42e3d9a3..d145f524 100644 --- a/capDL-tool/CapDL/PrintXml.hs +++ b/capDL-tool/CapDL/PrintXml.hs @@ -10,7 +10,6 @@ import CapDL.PrintUtils import Prelude hiding ((<>)) import Text.PrettyPrint -import Data.Word (Word64) import Data.Maybe (fromMaybe) import qualified Data.Map as Map import qualified Data.Set as Set @@ -238,9 +237,14 @@ printCDT :: CDT -> Doc printCDT cdt = xmlSurround "cdt" [] $ vcat (map printCDTRelation (Map.toList cdt)) -printSchedItem :: (Word, Word64) -> Doc +printSchedDuration :: DomScheduleDuration -> String +printSchedDuration (DomScheduleDurationTicks ticks) = show ticks ++ " ticks" +printSchedDuration (DomScheduleDurationUs us) = show us ++ " us" +printSchedDuration (DomScheduleDurationEnd) = "0" + +printSchedItem :: (Word, DomScheduleDuration) -> Doc printSchedItem (dom, duration) = - text $ emptyTag "item" [("domain", show dom), ("duration", show duration)] + text $ emptyTag "item" [("domain", show dom), ("duration", printSchedDuration duration)] printDomSched :: Maybe DomSchedule -> Maybe Word -> Word -> Doc printDomSched Nothing _ _ = text "" diff --git a/capDL-tool/doc/capDL.md b/capDL-tool/doc/capDL.md index 09063fb6..aabb8ff1 100644 --- a/capDL-tool/doc/capDL.md +++ b/capDL-tool/doc/capDL.md @@ -158,7 +158,8 @@ in section [Modules](#modules). | 'index_shift' ':' number sched_decl ::= 'schedule' ':' '[' sched_item (',' sched_item)* ','? ']' - sched_item ::= '(' number ',' number ')' + sched_unit ::= 'ticks' | 'us' + sched_item ::= '(' number ',' number sched_unit? ')' ### Modules @@ -525,7 +526,8 @@ ASIDControlCap is specified by `asid_control` and IOSpaceMasterCap by | 'index_shift' ':' number sched_decl ::= 'schedule' ':' '[' sched_item (',' sched_item)* ','? ']' - sched_item ::= '(' number ',' number ')' + sched_unit ::= 'ticks' | 'us' + sched_item ::= '(' number ',' number sched_unit? ')' The Domain schedule declaration is optional and only required for system initialisation, not for reasoning about capability distribution. @@ -535,6 +537,17 @@ the domain and the second component the duration. (0, 0) denotes a schedule end marker. At most one domain schedule declaration is accepted. See [RFC-20] for detail on domain schedule semantics. +The duration is specified either in units of ticks or microseconds (us). +Without a unit specifier, it defaults to ticks. This means schedule items +can appear as `(0, 5)` (domain 0, 5 ticks), `(1, 7 ticks)` (domain 1, 7 ticks), +or `(2, 2000 us)` (domain 2, 2000 us). On non-MCS, tick values are multiples +of the KernelTimerTickMS value specified in the kernel build configuration. +When specifying durations in microseconds, the initialiser enforces the values +are exact multiples of the period between ticks. In contrast, on MCS configs, +tick values correspond to a platform-specific frequency. Thus, when specifying +microseconds on MCS, we instead guarantee that the us-to-tick conversion +is accurate to the nearest tick, or if not possible, it fails. + The optional `domain_set_start` value (0 if left out) denotes which item of the provided domain schedule the initialiser will switch to when initialiser execution ends, using the seL4 API `DomainSetStart`. At most one start index diff --git a/capDL-tool/example-arm.cdl b/capDL-tool/example-arm.cdl index 93de6033..9874960d 100644 --- a/capDL-tool/example-arm.cdl +++ b/capDL-tool/example-arm.cdl @@ -144,7 +144,15 @@ cap_test { } domains { - schedule: [(0, 10), (1, 10), (0, 0), (2, 2)] + 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), + ] index_shift: 1 domain_set_start: 3 } diff --git a/capDL-tool/example-arm.right b/capDL-tool/example-arm.right index 9321af9f..46d4046e 100644 --- a/capDL-tool/example-arm.right +++ b/capDL-tool/example-arm.right @@ -106,7 +106,7 @@ objects { } domains { - schedule: [(0, 10), (1, 10), (0, 0), (2, 2)] + schedule: [(0, 10 ticks), (1, 10 ticks), (0, 0), (2, 2 us), (0, 0)] domain_set_start: 3 index_shift: 1 } diff --git a/capdl-loader-app/include/capdl.h b/capdl-loader-app/include/capdl.h index 6a6b7ef1..0589a908 100644 --- a/capdl-loader-app/include/capdl.h +++ b/capdl-loader-app/include/capdl.h @@ -402,6 +402,21 @@ typedef struct { CDL_ObjID *children; } CDL_UntypedDerivation; +typedef enum { + CDL_DomainSchedEntryKind_Ticks = 0, + CDL_DomainSchedEntryKind_Us, + CDL_DomainSchedEntryKind_End, +} CDL_DomainSchedEntryKind_t; + +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; + /* CapDLModel: is described by a map from ObjectIDs (array index) to Objects */ typedef struct { seL4_Word num; @@ -421,9 +436,9 @@ typedef struct { CDL_ObjID *asid_slots; /* Array of size domainScheduleLength where each entry consists of an - 8-bit domain number (highest 8 bits) and 56 bit duration (low bits) in ticks. + domain and duration (in either ticks or us). NULL, if no domain schedule should be configured. */ - uint64_t *domainSchedule; + CDL_DomainSchedEntry *domainSchedule; /* Length of the domain schedule array. Must be > 0 if domainSchedule is not NULL. */ seL4_Word domainScheduleLength; diff --git a/capdl-loader-app/src/main.c b/capdl-loader-app/src/main.c index 2f72bc40..86011143 100644 --- a/capdl-loader-app/src/main.c +++ b/capdl-loader-app/src/main.c @@ -2092,6 +2092,77 @@ static void mark_vspace_roots(CDL_Model *spec) } #endif +#ifdef CONFIG_KERNEL_MCS + +#define US_IN_SECOND (uint64_t)1000000 + +_Static_assert(sizeof(seL4_Time) == sizeof(uint64_t), + "Correctness of these calculations depends on this"); + +static seL4_Time us_to_ticks(uint64_t duration_us) +{ +#if defined(CONFIG_ARCH_ARM) || defined(CONFIG_ARCH_RISCV) + /* For ARM, AArch64, and RISC-V platforms the build system provides the + * timer frequency to us at build time, in Hertz */ + uint64_t f = CONFIG_TIMER_FREQUENCY; + + /** + * TODO: Formal correctness of this implementation. + * https://github.com/seL4/capdl/issues/98 + * + * The goal of this implementation is that the output ticks should be + * equal to the (round-nearest) of the convert input us. Else, it should + * fail. + */ + + ZF_LOGF_IF((duration_us / US_IN_SECOND) >= ((1ULL << 56) / f), + "Input us would overflow 64-bits or exceed 56-bit tick maximum"); + + uint64_t s = duration_us / US_IN_SECOND; + uint64_t us = duration_us % US_IN_SECOND; + + /* The '+ US_IN_SECOND / 2' is to implement round-nearest behaviour */ + uint64_t ticks = s * f + ((us * f + US_IN_SECOND / 2) / (US_IN_SECOND)); + return (seL4_Time)ticks; + +#elif defined(CONFIG_ARCH_X86) || defined(CONFIG_ARCH_X86_64) + seL4_BootInfoHeader *tsc_freq_hdr = extended_bootinfo_table[SEL4_BOOTINFO_HEADER_X86_TSC_FREQ]; + ZF_LOGF_IF(tsc_freq == NULL, + "Unable to determine timer frequency as no TSC frequency provided in bootinfo"); + /* For x86 platforms, the timer frequency is provided in MHz by the bootinfo */ + void *tsc_freq_mhz_addr = (void *)tsc_freq_hdr + sizeof(seL4_BootInfoHeader); + uint32_t tsc_freq_mhz = *(uint32_t *)tsc_freq_mhz_addr; + + uint64_t ticks; + if (__builtin_mul_overflow(duration_us, tsc_freq_mhz, &ticks)) { + ZF_LOGF("Output would overflow when computing ticks for duration %ld us @ freq %d MHz", duration_us, tsc_freq_mhz); + } + + return (seL4_Time)ticks; +#else +#error "Unknown architecture" +#endif +} + +#else /* CONFIG_KERNEL_MCS */ + +static seL4_Time us_to_ticks(uint64_t duration_us) +{ + /* On non-MCS, 1 tick is equivalent to 1 TIMER_TICK_MS, or an integer multiple + * of 1 millisecond. */ + + uint64_t period_us = 1000ULL * CONFIG_TIMER_TICK_MS; + uint64_t ticks = duration_us / period_us; + uint64_t remainder = duration_us % period_us; + ZF_LOGF_IF(remainder != 0, + "domain schedule duration %lu is not an integer multiple of CONFIG_TIMER_TICK_MS (%d ms)\n", + duration_us, CONFIG_TIMER_TICK_MS); + + return ticks; +} + +#endif /* CONFIG_KERNEL_MCS */ + static void init_domains(CDL_Model *spec) { if (CONFIG_NUM_DOMAINS == 1 && spec->domainSchedule == NULL) { @@ -2114,13 +2185,37 @@ static void init_domains(CDL_Model *spec) assert(spec->domainScheduleLength > 0); for (seL4_Word i = 0; i < spec->domainScheduleLength; i++) { - uint64_t entry = spec->domainSchedule[i]; - /* avoid MASK macro, because it contains a word size guard */ - uint64_t duration = entry & ((1ull << 56) - 1ull); - seL4_DomainSet_ScheduleConfigure(seL4_CapDomain, - i + spec->domainIndexShift, - entry >> 56, /* domain */ - duration); + CDL_DomainSchedEntry entry = spec->domainSchedule[i]; + + 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]")); + + seL4_Time duration_ticks; + switch (entry.kind) { + case CDL_DomainSchedEntryKind_Ticks: + duration_ticks = (seL4_Time)entry.duration; + break; + case CDL_DomainSchedEntryKind_Us: + duration_ticks = us_to_ticks(entry.duration); + assert(duration_ticks != 0); + break; + case CDL_DomainSchedEntryKind_End: + assert(entry.duration == 0); + duration_ticks = 0; + break; + default: + assert(!"unreachable"); + } + + ZF_LOGD(" ticks: %lu", duration_ticks); + + int error = seL4_DomainSet_ScheduleConfigure(seL4_CapDomain, + i + spec->domainIndexShift, + entry.domain, + duration_ticks); + ZF_LOGF_IFERR(error, ""); } } diff --git a/python-capdl-tool/capdl/Spec.py b/python-capdl-tool/capdl/Spec.py index 0622a762..6a71b44e 100644 --- a/python-capdl-tool/capdl/Spec.py +++ b/python-capdl-tool/capdl/Spec.py @@ -8,7 +8,7 @@ unicode_literals from .Object import IRQ, Object -from .util import lookup_architecture +from .util import lookup_architecture, DomainDurationUnit class Spec(object): @@ -41,11 +41,15 @@ def add_object(self, obj): assert isinstance(obj, Object) self.objs.add(obj) - def add_schedule_item(self, domain, duration): - self.schedule.append((domain, duration)) + def add_schedule_item(self, domain, duration, duration_unit=DomainDurationUnit.Ticks): + assert isinstance(duration_unit, DomainDurationUnit) + self.schedule.append((domain, duration, duration_unit)) def add_schedule(self, schedule): - self.schedule.extend(schedule) + # We iterate manually and do *schedule so that default arguments of + # add_schedule_item can be applied. + for schedule_item in schedule: + self.add_schedule_item(*schedule_item) def merge(self, other): assert isinstance(other, Spec) @@ -65,7 +69,7 @@ def __iter__(self): def show_schedule(self): if not self.schedule: return '' - items = ', '.join('(%d, %d)' % (d, t) for d, t in self.schedule) + items = ', '.join('(%d, %d %s)' % (d, t, u.value) for d, t, u in self.schedule) set_start = self.domain_set_start or 0 return '\ndomains {\n' \ ' schedule: [%s]\n' \ diff --git a/python-capdl-tool/capdl/__init__.py b/python-capdl-tool/capdl/__init__.py index 88f407c2..e27656b5 100644 --- a/python-capdl-tool/capdl/__init__.py +++ b/python-capdl-tool/capdl/__init__.py @@ -18,4 +18,4 @@ from .Allocator import ObjectAllocator, CSpaceAllocator, AddressSpaceAllocator, AllocatorState from .PageCollection import PageCollection, create_address_space from .util import page_index, page_sizes, page_table_coverage, \ - page_table_index, page_table_vaddr, page_vaddr, lookup_architecture, valid_architectures + page_table_index, page_table_vaddr, page_vaddr, lookup_architecture, valid_architectures, DomainDurationUnit diff --git a/python-capdl-tool/capdl/util.py b/python-capdl-tool/capdl/util.py index 6d48f071..a4c14b07 100644 --- a/python-capdl-tool/capdl/util.py +++ b/python-capdl-tool/capdl/util.py @@ -13,6 +13,7 @@ import abc +from aenum import Enum import six from six.moves import range @@ -350,3 +351,8 @@ def ctz(size_bytes): low = low >> 1 low_bit += 1 return low_bit + + +class DomainDurationUnit(Enum): + Ticks = "ticks" + Us = "us" diff --git a/python-capdl-tool/examples/domains.py b/python-capdl-tool/examples/domains.py new file mode 100644 index 00000000..1a57ea51 --- /dev/null +++ b/python-capdl-tool/examples/domains.py @@ -0,0 +1,28 @@ +# +# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) +# +# SPDX-License-Identifier: BSD-2-Clause +# + +from __future__ import absolute_import, division, print_function, \ + unicode_literals + +# Add the root directory of this repository to your PYTHONPATH environment +# variable to enable the following import. +import capdl + +# Let's make a TCB: +tcb_a = capdl.TCB('tcb_a', domain=0) +tcb_b = capdl.TCB('tcb_b', domain=1) + +# Let's create a spec from all this and output it: +spec = capdl.Spec(arch="aarch64") +for obj in [tcb_a, tcb_b]: + spec.add_object(obj) + + +# domain, duration +spec.add_schedule_item(0, 1000) +spec.add_schedule_item(1, 1000, capdl.DomainDurationUnit.Us) + +print(spec) From aea3d02cec032218f8bb08bef1a85b3d2fde8c4e Mon Sep 17 00:00:00 2001 From: Julia Vassiliki Date: Mon, 20 Jul 2026 14:08:18 +1000 Subject: [PATCH 3/3] capDL-tool: update domains in JSON representation This matches the corresponding [Rust PR]( https://github.com/seL4/rust-sel4/pull/360). Signed-off-by: Julia Vassiliki --- capDL-tool/CapDL/PrintJSON.hs | 30 ++++++++++++++++++++++++------ 1 file changed, 24 insertions(+), 6 deletions(-) diff --git a/capDL-tool/CapDL/PrintJSON.hs b/capDL-tool/CapDL/PrintJSON.hs index 8c9219cf..901e7e41 100644 --- a/capDL-tool/CapDL/PrintJSON.hs +++ b/capDL-tool/CapDL/PrintJSON.hs @@ -57,9 +57,22 @@ data Spec = Spec , untyped_covers :: [UntypedCover] } deriving (Eq, Show, Generic, ToJSON, FromJSON) +data DomainSchedDuration = + DomainSchedDurationTicks Word64 + | DomainSchedDurationUs Word64 + | DomainSchedDurationEndMarker + deriving (Eq, Show, Generic) + +instance ToJSON DomainSchedDuration where + toJSON = genericToJSON $ sumTypeOptions "DomainSchedDuration_" + toEncoding = genericToEncoding $ sumTypeOptions "DomainSchedDuration_" + +instance FromJSON DomainSchedDuration where + parseJSON = genericParseJSON $ sumTypeOptions "DomainSchedDuration_" + data DomainSchedEntry = DomainSchedEntry - { id :: Word8 - , time :: Word64 + { domain :: Word8 + , duration :: DomainSchedDuration } deriving (Eq, Show, Generic, ToJSON, FromJSON) data Range a = Range @@ -371,10 +384,7 @@ translate :: C.ObjectSizeMap -> C.Model Word -> Spec translate objSizeMap (C.Model arch objMap irqNode _ coverMap optDomSchedule domStart domIdxShift) = Spec { objects , irqs - , domain_schedule = fmap (map (\(id, time) -> DomainSchedEntry - { id = fromIntegral id - , time - })) optDomSchedule + , domain_schedule = domainSchedule , domain_set_start = domStart , domain_idx_shift = Just domIdxShift , asid_slots = asidSlots @@ -408,6 +418,14 @@ translate objSizeMap (C.Model arch objMap irqNode _ coverMap optDomSchedule domS | (irq, obj) <- M.toAscList irqNode ] + domainSchedule = fmap (map (\(domain, duration) -> DomainSchedEntry + { domain = fromIntegral domain + , duration = case duration of + C.DomScheduleDurationTicks ticks -> DomainSchedDurationTicks ticks + C.DomScheduleDurationUs us -> DomainSchedDurationUs us + C.DomScheduleDurationEnd -> DomainSchedDurationEndMarker + })) optDomSchedule + asidSlots = assert (map fst table `isPrefixOf` [1..]) (map snd table) where table = sortBy (comparing fst)