Support domain schedule units (us & ticks)

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 {

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

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.

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"

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) +++
     "}"
 

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)

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

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 ""

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

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
 }

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
 }

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;