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/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) 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 d13d5775..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 @@ -342,11 +343,16 @@ 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: 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)