1% 2% Copyright 2014, General Dynamics C4 Systems 3% 4% This software may be distributed and modified according to the terms of 5% the GNU General Public License version 2. Note that NO WARRANTY is provided. 6% See "LICENSE_GPLv2.txt" for details. 7% 8% @TAG(GD_GPL) 9% 10 11This module defines the types and functions related to the kernel 12objects used to represent a capability space. It contains 13implementations of the operations that user-level threads can request 14by invoking a capability table node. It is also responsible for 15creating the "Capability" objects used at higher levels of the kernel. 16 17> module SEL4.Object.CNode ( 18> cteRevoke, cteDelete, cteInsert, cteDeleteOne, 19> ensureNoChildren, ensureEmptySlot, slotCapLongRunningDelete, 20> getSlotCap, locateSlotTCB, locateSlotCNode, locateSlotCap, 21> locateSlotBasic, getReceiveSlots, getCTE, setupReplyMaster, 22> insertInitCap, decodeCNodeInvocation, invokeCNode, 23> updateCap, isFinalCapability, createNewObjects, 24> updateFreeIndex 25> ) where 26 27\begin{impdetails} 28 29> {-# BOOT-IMPORTS: SEL4.Machine SEL4.API.Types SEL4.API.Failures SEL4.Model SEL4.Object.Structures SEL4.API.Invocation #-} 30> {-# BOOT-EXPORTS: ensureNoChildren getSlotCap locateSlotTCB locateSlotCNode locateSlotCap locateSlotBasic ensureEmptySlot insertInitCap cteInsert cteDelete cteDeleteOne decodeCNodeInvocation invokeCNode getCTE updateCap isFinalCapability createNewObjects updateFreeIndex #-} 31 32> import Prelude hiding (Word) 33> import SEL4.API.Types 34> import SEL4.API.Failures 35> import SEL4.API.Invocation 36> import SEL4.API.InvocationLabels 37> import SEL4.Machine 38> import SEL4.Model 39> import SEL4.Object.Structures 40> import SEL4.Object.Interrupt 41> import SEL4.Object.Instances() 42> import SEL4.Object.ObjectType 43> import SEL4.Object.Endpoint(cancelBadgedSends) 44> import {-# SOURCE #-} SEL4.Object.TCB 45> import {-# SOURCE #-} SEL4.Kernel.CSpace 46 47> import Data.Bits 48> import qualified Data.Set 49> import Data.WordLib 50 51\end{impdetails} 52 53\subsection{Capability Node Object Invocations} 54 55The following function decodes a CNode invocation message, and checks for any error conditions. 56 57> decodeCNodeInvocation :: Word -> [Word] -> Capability -> [Capability] -> 58> KernelF SyscallError CNodeInvocation 59> decodeCNodeInvocation label (index:bits:args) 60> cap@(CNodeCap {}) extraCaps 61> = do 62 63The first check is that the invocation type requested is a CNode operation. 64 65> let inv = invocationType label 66> unless (inv `elem` [CNodeRevoke .. CNodeSaveCaller]) $ 67> throw IllegalOperation 68 69All CNode operations require the caller to specify a slot in the capability space mapped by the tree whose root is the invoked node, by providing a pointer in the space defined by the tree and the depth of the tree. 70 71The lookup can be terminated early, and therefore operate on a capability at one of the intermediate levels, by reducing the specified depth and shifting the address to the right by the corresponding number of bits. However, the depth \emph{must} be that of a CNode existing in the specified region of the tree; if not, the operation will fail with a "MissingCapabilityError". 72 73> destSlot <- lookupTargetSlot cap (CPtr index) (fromIntegral bits) 74 75> case (inv `elem` [CNodeCopy .. CNodeMutate], inv, args, extraCaps) of 76 77The "Copy", "Mint", "Move" and "Mutate" operations are similar. Each creates a new capability, and must specify a source slot, in the same manner as the destination. 78 79> (True, _, srcIndex:srcDepth:args, srcRootCap:_) -> do 80 81For these operations, the destination slot must be empty, so a new capability can be created in it. 82 83> ensureEmptySlot destSlot 84 85The source slot is located in a similar way to the destination slot, but starting from an additional root capability provided to the system call. 86 87> srcSlot <- lookupSourceSlot srcRootCap 88> (CPtr srcIndex) (fromIntegral srcDepth) 89 90The source slot must contain a valid capability. 91 92> srcCTE <- withoutFailure $ getCTE srcSlot 93> when (isNullCap $ cteCap srcCTE) $ 94> throw $ FailedLookup True $ MissingCapability { 95> missingCapBitsLeft = fromIntegral srcDepth } 96 97Rights may be masked for the "Copy" and "Mint" operations. The capability data is adjusted on the "Mint" and "Mutate" operations. 98 99> (rights, capData) <- 100> case (inv, args) of 101> (CNodeCopy, rights:_) -> 102> return $! (rightsFromWord rights, Nothing) 103> (CNodeMint, rights:newData:_) -> 104> return $! (rightsFromWord rights, Just newData) 105> (CNodeMove, _) -> 106> return $! (allRights, Nothing) 107> (CNodeMutate, newData:_) -> 108> return $! (allRights, Just newData) 109> _ -> throw TruncatedMessage 110 111The moving system calls, "Move" and "Mutate", are differentiated from the copying system calls, "Copy" and "Mint". 112 113> let isMove = inv `elem` [CNodeMove, CNodeMutate] 114 115The rights and capability data word are applied to the source capability to create a new capability. 116 117> let srcCap = maskCapRights rights $ cteCap srcCTE 118> newCap <- (if isMove then return else deriveCap srcSlot) $ 119> case capData of 120> Just w -> updateCapData isMove w srcCap 121> Nothing -> srcCap 122> when (isNullCap newCap) $ throw IllegalOperation 123> 124> return $! 125> (if isMove then Move else Insert) newCap srcSlot destSlot 126 127The "Revoke", "Delete", "SaveCaller" and "CancelBadgedSends" operations have no additional arguments. The "SaveCaller" call requires the target slot to be empty. 128 129> (_, CNodeRevoke, _, _) -> return $ Revoke destSlot 130> (_, CNodeDelete, _, _) -> return $ Delete destSlot 131> (_, CNodeSaveCaller, _, _) -> do 132> ensureEmptySlot destSlot 133> return $ SaveCaller destSlot 134 135For "CancelBadgedSends", the slot must contain a valid Endpoint capability. 136 137> (_, CNodeCancelBadgedSends, _, _) -> do 138> cte <- withoutFailure $ getCTE destSlot 139> unless (hasCancelSendRights $ cteCap cte) $ throw IllegalOperation 140> return $ CancelBadgedSends $ cteCap cte 141 142The "Rotate" operation atomically moves two capabilities. 143 144> (_, CNodeRotate, 145> pivotNewData:pivotIndex:pivotDepth:srcNewData:srcIndex:srcDepth:_, 146> pivotRootCap:srcRootCap:_) -> do 147 148The source and pivot slots are located in a similar way to the destination slot, but starting from two additional root capabilities provided to the system call. 149 150> srcSlot <- lookupSourceSlot srcRootCap 151> (CPtr srcIndex) (fromIntegral srcDepth) 152> pivotSlot <- lookupPivotSlot pivotRootCap 153> (CPtr pivotIndex) (fromIntegral pivotDepth) 154 155The pivot slot must be distinct from the source and destination slots. 156 157> when (pivotSlot == srcSlot || pivotSlot == destSlot) $ 158> throw IllegalOperation 159 160The destination slot must be empty, unless it is the same as the source slot (in which case its contents will be swapped with those of the pivot slot). 161 162> unless (srcSlot == destSlot) $ ensureEmptySlot destSlot 163 164The source and pivot slots must contain valid capabilities. 165 166> srcCap <- withoutFailure $ liftM cteCap $ getCTE srcSlot 167> when (isNullCap srcCap) $ 168> throw $ FailedLookup True $ MissingCapability { 169> missingCapBitsLeft = fromIntegral srcDepth } 170> pivotCap <- withoutFailure $ liftM cteCap $ getCTE pivotSlot 171> when (isNullCap pivotCap) $ 172> throw $ FailedLookup False $ MissingCapability { 173> missingCapBitsLeft = fromIntegral pivotDepth } 174 175The two moved capabilities are updated with the provided data words. 176 177> let newSrcCap = updateCapData True srcNewData srcCap 178> let newPivotCap = updateCapData True pivotNewData pivotCap 179 180The moved capabilities must not be null. 181 182> when (isNullCap newSrcCap) $ throw IllegalOperation 183> when (isNullCap newPivotCap) $ throw IllegalOperation 184 185> return $! Rotate newSrcCap newPivotCap srcSlot pivotSlot destSlot 186 187Otherwise, the message was too short. 188 189> _ -> throw TruncatedMessage 190 191> decodeCNodeInvocation label _ (CNodeCap {}) _ 192> = throw $ if invocationType label `elem` [CNodeRevoke .. CNodeSaveCaller] 193> then TruncatedMessage 194> else IllegalOperation 195 196> decodeCNodeInvocation _ _ _ _ = fail "decodeCNodeInvocation: invalid cap" 197 198The function "invokeCNode" dispatches an invocation to one of the handlers defined below, given a "CNodeInvocation" object. 199 200> invokeCNode :: CNodeInvocation -> KernelP () 201> 202> invokeCNode (Revoke destSlot) = cteRevoke destSlot 203> 204> invokeCNode (Delete destSlot) = cteDelete destSlot True 205> 206> invokeCNode (CancelBadgedSends (EndpointCap { capEPPtr = ptr, capEPBadge = b})) = 207> withoutPreemption $ unless (b == 0) $ cancelBadgedSends ptr b 208> invokeCNode (CancelBadgedSends _) = fail "should never happen" 209 210> invokeCNode (Insert cap srcSlot destSlot) = 211> withoutPreemption $ cteInsert cap srcSlot destSlot 212> 213> invokeCNode (Move cap srcSlot destSlot) = 214> withoutPreemption $ cteMove cap srcSlot destSlot 215> 216> invokeCNode (Rotate cap1 cap2 slot1 slot2 slot3) = withoutPreemption $ 217> if (slot1 == slot3) 218> then cteSwap cap1 slot1 cap2 slot2 219> else do 220> cteMove cap2 slot2 slot3 221> cteMove cap1 slot1 slot2 222 223> invokeCNode (SaveCaller destSlot) = withoutPreemption $ do 224> thread <- getCurThread 225> srcSlot <- getThreadCallerSlot thread 226> cap <- getSlotCap srcSlot 227> case cap of 228> NullCap -> return () 229> ReplyCap { capReplyMaster = False } -> cteMove cap srcSlot destSlot 230> _ -> fail "caller capability must be null or reply" 231 232\subsection{CNode Operations} 233 234The following functions define the operations that can be performed by a CNode invocation. 235 236\subsubsection{Inserting New Capabilities} 237 238> setUntypedCapAsFull :: Capability -> Capability -> PPtr CTE -> Kernel () 239> setUntypedCapAsFull srcCap newCap srcSlot = do 240> if (isUntypedCap srcCap && isUntypedCap newCap && 241> capPtr srcCap == capPtr newCap && capBlockSize srcCap == capBlockSize newCap) 242> then updateCap srcSlot (srcCap { capFreeIndex = maxFreeIndex (capBlockSize srcCap) }) else return () 243 244Insertion of new capabilities copied from existing capabilities is performed by "cteInsert". The parameters are the physical addresses of the source and destination slots, and the capability to be inserted in the destination slot. This function requires the destination slot to be empty, and assumes that the provided capability is one that may be derived from the contents of the source slot. 245 246> cteInsert :: Capability -> PPtr CTE -> PPtr CTE -> Kernel () 247> cteInsert newCap srcSlot destSlot = do 248 249First, fetch the capability table entry for the source. 250 251> srcCTE <- getCTE srcSlot 252> let srcMDB = cteMDBNode srcCTE 253> let srcCap = cteCap srcCTE 254 255If the newly created capability is allowed to become a parent of other capabilities in the MDB, it must be marked \emph{revocable}. 256 257> let newCapIsRevocable = isCapRevocable newCap srcCap 258 259Create the new capability table entry. Its "MDBNode" is inserted in the mapping database immediately after the existing capability. 260 261The "mdbRevocable" bit is set if the capability is revocable, as determined by the test above. There is a second bit in the MDB, "mdbFirstBadged", that is effective only for endpoint capabilities; it is used to distinguish between capabilities badged by separate "Mint" operations, and marks the leftmost capability in the MDB that was created by the present "Mint" operation. If this capability is deleted, the bit's value will be moved to the next capability to the right (see "cteDelete"). 262 263> let newMDB = srcMDB { 264> mdbPrev = srcSlot, 265> mdbRevocable = newCapIsRevocable, 266> mdbFirstBadged = newCapIsRevocable } 267 268The destination slot must be empty. 269 270> oldCTE <- getCTE destSlot 271> assert (isNullCap $ cteCap oldCTE) 272> "cteInsert to non-empty destination" 273> assert (mdbPrev (cteMDBNode oldCTE) == nullPointer && 274> mdbNext (cteMDBNode oldCTE) == nullPointer) 275> "cteInsert: mdb entry must be empty" 276> setUntypedCapAsFull srcCap newCap srcSlot 277 278Store the new entry in the destination slot and update the mapping database. 279 280> updateCap destSlot newCap 281> updateMDB destSlot (const newMDB) 282> updateMDB srcSlot (\m -> m { mdbNext = destSlot }) 283> updateMDB (mdbNext newMDB) (\m -> m { mdbPrev = destSlot }) 284 285\subsubsection{Moving Capabilities} 286 287> cteMove :: Capability -> PPtr CTE -> PPtr CTE -> Kernel () 288> cteMove newCap srcSlot destSlot = do 289 290The destination slot must be empty. 291 292> oldCTE <- getCTE destSlot 293> assert (isNullCap $ cteCap oldCTE) 294> "cteMove to non-empty destination" 295> assert (mdbPrev (cteMDBNode oldCTE) == nullPointer && 296> mdbNext (cteMDBNode oldCTE) == nullPointer) 297> "cteMove: mdb entry must be empty" 298 299Move the "CTE" into the new slot and update the mapping database. 300 301> cte <- getCTE srcSlot 302> let mdb = cteMDBNode cte 303> updateCap destSlot newCap 304> updateCap srcSlot NullCap 305> updateMDB destSlot (const mdb) 306> updateMDB srcSlot (const nullMDBNode) 307> updateMDB (mdbPrev mdb) (\m -> m { mdbNext = destSlot }) 308> updateMDB (mdbNext mdb) (\m -> m { mdbPrev = destSlot }) 309 310\subsubsection{Swapping Capabilities} 311 312To avoid long-running recursive "Delete" operations, it is sometimes necessary to swap the contents of two slots (which are never visible in the capability space at that time). See the definition of "reduceZombie" for details about when and why this is done. The function "capSwapForDelete" is used to perform these swaps. 313 314> capSwapForDelete :: PPtr CTE -> PPtr CTE -> Kernel () 315> capSwapForDelete slot1 slot2 = when (slot1 /= slot2) $ do 316> cap1 <- liftM cteCap $ getCTE slot1 317> cap2 <- liftM cteCap $ getCTE slot2 318> cteSwap cap1 slot1 cap2 slot2 319 320The following function is used to atomically swap the contents of two slots, which must be distinct and contain valid capabilities. It is used by "capSwapForDelete", and by the "Rotate" system call if the source and destination slots are the same. 321 322Note the order of the MDB updates; this is necessary in case the two capabilities are MDB siblings. 323 324> cteSwap :: Capability -> PPtr CTE -> Capability -> PPtr CTE -> Kernel () 325> cteSwap cap1 slot1 cap2 slot2 = do 326> cte1 <- getCTE slot1 327> updateCap slot1 cap2 328> updateCap slot2 cap1 329> let mdb1 = cteMDBNode cte1 330> updateMDB (mdbPrev mdb1) (\m -> m { mdbNext = slot2 }) 331> updateMDB (mdbNext mdb1) (\m -> m { mdbPrev = slot2 }) 332> cte2 <- getCTE slot2 333> let mdb2 = cteMDBNode cte2 334> updateMDB slot1 (const mdb2) 335> updateMDB slot2 (const mdb1) 336> updateMDB (mdbPrev mdb2) (\m -> m { mdbNext = slot1 }) 337> updateMDB (mdbNext mdb2) (\m -> m { mdbPrev = slot1 }) 338 339\subsubsection{Revoking Capabilities} 340 341The work for the revoke operation is done by "cteRevoke", which revokes all capabilities which are children of the invoked capability in the derivation tree. 342 343> cteRevoke :: PPtr CTE -> KernelP () 344> cteRevoke slot = do 345 346Load the CTE being revoked. 347 348> cte <- withoutPreemption $ getCTE slot 349> let nextPtr = mdbNext $ cteMDBNode cte 350 351Determine whether the CTE is valid, and has children to be deleted. If a child is found, then it is deleted, and we look for another; otherwise the revocation is complete. There is a preemption point immediately after each capability deletion. 352 353> unless ((isNullCap $ cteCap cte) || (nextPtr == nullPointer)) $ do 354> nextCTE <- withoutPreemption $ getCTE nextPtr 355> when (cte `isMDBParentOf` nextCTE) $ do 356> cteDelete nextPtr True 357> preemptionPoint 358> cteRevoke slot 359 360\subsubsection{Deleting Capabilities} 361\label{sec:object.cnode.ops.delete} 362 363This function deletes the capability in a given slot. If it is the last remaining capability for the given object, the object will be destroyed. 364 365The run time of "cteDelete" is unbounded under certain circumstances, so the operation must include preemption points. Specifically, deleting the last capability to a CNode or TCB may recursively call "cteDelete". Keeping the kernel's state consistent during such operations is a complex task. 366 367> cteDelete :: PPtr CTE -> Bool -> KernelP () 368> cteDelete slot exposed = do 369> (success, info) <- finaliseSlot slot exposed 370> when (exposed || success) $ withoutPreemption $ emptySlot slot info 371 372This helper routine empties a slot. The routine may be called on the same 373slot twice as a result of recursion between "cteDelete" and "reduceZombie", 374thus a check is made as to whether the slot is already empty. 375 376Some capabilities require some additional cleanup after the slot has been cleared. 377For example, deleting the final IRQHandlerCap for an IRQ requires clearing the bitmask 378to allow reissue of a new IRQHandlerCap for that IRQ. 379 380The emptySlot helper takes a Capability argument which represents the required cleanup, 381and calls postCapDeletion to actually perform the cleanup. 382 383> emptySlot :: PPtr CTE -> Capability -> Kernel () 384> emptySlot slot info = do 385> clearUntypedFreeIndex slot 386> newCTE <- getCTE slot 387> let mdbNode = cteMDBNode newCTE 388> let prev = mdbPrev mdbNode 389> let next = mdbNext mdbNode 390 391> case (cteCap newCTE) of 392> NullCap -> return () 393> _ -> do 394> updateMDB prev (\mdb -> mdb { mdbNext = next }) 395> updateMDB next (\mdb -> mdb { 396> mdbPrev = prev, 397> mdbFirstBadged = 398> mdbFirstBadged mdb || mdbFirstBadged mdbNode }) 399> updateCap slot NullCap 400> updateMDB slot (const nullMDBNode) 401 402> postCapDeletion info 403 404If the deleted capability is marked as being the leftmost endpoint capability in the tree with a given badge, the next capability to the right in the tree will inherit that property. This is significant only if the next capability is a sibling of the deleted one; otherwise the bit either has no effect or is already set. 405 406This helper routine prepares a slot to be emptied. In most cases, this simply involves taking a finalisation action relevant to the contained capability; that action is implemented in "finaliseCap", in \autoref{sec:object.objecttype.finalise}. However, if the capability contains references to other slots, a Zombie will be returned from "finaliseCap" to indicate this, and the resulting recursive problem must be handled carefully. 407 408The boolean in the return value indicates whether the slot was successfully finalised. When the "exposed" flag is set, this will always be true. The unexposed operation may abort when it encounters a zombie capability that is already pointing at the slot it is in. Zombies are always the final reference to any given object, thus this Zombie must also be the capability that the exposed deletion operation (which is the recursive parent) used to recurse on. This case can be handled by returning control to the recursive parent without taking any action. 409 410The optional IRQ in the return value indicates any IRQ lines whose final IRQ handling capability will be freed by the deletion of the capability in the slot. The 'deletedIRQHandler' function should be called once the slot is empty. 411 412> finaliseSlot :: PPtr CTE -> Bool -> KernelP (Bool, Capability) 413> finaliseSlot slot exposed = do 414 415Load the contents of the slot. 416 417> cte <- withoutPreemption $ getCTE slot 418 419> if isNullCap $ cteCap cte then return (True, NullCap) else do 420 421Determine whether this is a final capability. 422 423> final <- withoutPreemption $ isFinalCapability cte 424 425Perform any type-specific finalisation actions associated with the capability. 426 427> (remainder, info) <- withoutPreemption $ 428> finaliseCap (cteCap cte) final False 429 430At this point, the capability can safely be replaced with the returned 431remainder, which is either a "NullCap" or a "Zombie". If this cap is removable, we 432are finished finalising the slot. If not, we should save the returned cap as a 433potential resume point in the event of preemption, and then attempt to reduce 434further. Once a reduction step is taken we will allow preemption, and then 435continue finalising in this slot. 436 437> if capRemovable remainder slot then return (True, info) else 438> if not exposed && capCyclicZombie remainder slot 439> then do 440> withoutPreemption $ updateCap slot remainder 441> return (False, NullCap) 442> else do 443> withoutPreemption $ updateCap slot remainder 444> reduceZombie remainder slot exposed 445> preemptionPoint 446> finaliseSlot slot exposed 447 448This helper determines if a capability returned by "finaliseCap" can be removed from its slot. "Zombie" capabilities are only removable if they point to zero slots or only to the slot they are in. For all other object types, "finaliseCap" returns "NullCap", to indicate that the capability is removable. 449 450> capRemovable :: Capability -> PPtr CTE -> Bool 451> capRemovable NullCap _ = True 452> capRemovable (Zombie { capZombiePtr = slot', capZombieNumber = n }) slot = 453> (n == 0) || (n == 1 && slot == slot') 454> capRemovable _ _ = error "finaliseCap should only return Zombie or NullCap" 455 456This helper determines if a capability returned by "finaliseCap" is a cyclic Zombie. If so, unexposed deletion operations should abort. 457 458> capCyclicZombie :: Capability -> PPtr CTE -> Bool 459> capCyclicZombie NullCap _ = False 460> capCyclicZombie (Zombie { capZombiePtr = slot' }) slot = 461> slot == slot' 462> capCyclicZombie _ _ = False 463 464This helper takes a reduction step on an unremovable "Zombie" capability. 465 466> reduceZombie :: Capability -> PPtr CTE -> Bool -> KernelP () 467 468Unremovable "Zombie" capabilities must point to at least one slot. 469 470> reduceZombie (Zombie { capZombieNumber = 0 }) _ _ = 471> fail "reduceZombie expected unremovable Zombie" 472 473When the "Zombie" is not exposed, a swap operation is performed, moving the "Zombie" capability into the location it points to. This cannot already be the case, as if it were, the "Zombie" capability itself would be the only exposed capability to itself, and thus the target of the exposed deletion calling for the unexposed one. This in turn requires the "Zombie" to be of size 1, thus removable. 474 475> reduceZombie (Zombie { capZombiePtr = ptr }) slot False = do 476> assert (ptr /= slot) "Cyclic zombie passed to unexposed reduceZombie." 477> capAtPtr <- withoutPreemption $ liftM cteCap $ getCTE ptr 478> case capAtPtr of 479> (Zombie { capZombiePtr = ptr2 }) -> assert (ptr2 /= ptr) 480> "Moving self-referential Zombie aside." 481> _ -> return () 482> withoutPreemption $ capSwapForDelete ptr slot 483 484When the Zombie is exposed, the reduction operation deletes the contents of one of the slots the Zombie points to. The Zombie is then reduced in size. A corner case exists when the deletion operation, which is unexposed, swaps a Zombie capability discovered back into the slot in which our Zombie was or even clears our slot entirely. In this case the deletion operation may even fail to clear the slot. For this reason, we check whether the Zombie is unchanged before shrinking it. 485 486> reduceZombie z@(Zombie { capZombiePtr = ptr, capZombieNumber = n }) slot True = do 487> endSlot <- withoutPreemption $ locateSlotCap z (fromIntegral (n - 1)) 488> cteDelete endSlot False 489> ourCTE <- withoutPreemption $ getCTE slot 490> case (cteCap ourCTE) of 491> NullCap -> return () 492> c2@(Zombie { capZombiePtr = ptr2 }) -> 493> if (ptr == ptr2 && capZombieNumber c2 == n 494> && capZombieType z == capZombieType c2) 495> then withoutPreemption $ do 496> endCTE <- getCTE endSlot 497> assert (isNullCap $ cteCap endCTE) 498> "Expected cteDelete to clear slot or overwrite existing." 499> let newCap = z { capZombieNumber = n-1 } 500> updateCap slot newCap 501> else assert (ptr2 == slot && ptr /= slot) 502> "Expected new Zombie to be self-referential." 503> _ -> fail "Expected recursion to result in Zombie." 504 505> reduceZombie _ _ _ = fail "reduceZombie expected Zombie" 506 507In some cases we call for the deletion of a capability which we know can be deleted without recursion. For this case we have a non-preemptible way of calling the delete operation. For technical reasons this is done here by unfolding the definitions of "cteDelete" and "finaliseSlot". 508 509> cteDeleteOne :: PPtr CTE -> Kernel () 510> cteDeleteOne slot = do 511> cte <- getCTE slot 512> unless (isNullCap $ cteCap cte) $ do 513> final <- isFinalCapability cte 514> (remainder, info) <- finaliseCap (cteCap cte) final True 515> assert (capRemovable remainder slot && isNullCap info) $ 516> "cteDeleteOne: cap should be removable" 517> emptySlot slot NullCap 518 519\subsection{Object Creation} 520 521Create a set of new capabilities (and possibly the objects backing them) and 522insert them in given empty slots. The required parameters are an object type; 523a pointer to the source capability's slot; a list of pointers to empty slots; 524the region of memory where the objects will be created; and an integer 525representing the size of the objects to be created. 526 527> createNewObjects :: ObjectType -> PPtr CTE -> [PPtr CTE] -> PPtr () -> Int -> Bool -> Kernel () 528> createNewObjects newType srcSlot destSlots regionBase userSizeBits isDevice = do 529> let objectSizeBits = getObjectSize newType userSizeBits 530> zipWithM_ (\num slot -> do 531> cap <- createObject newType 532> (PPtr (num `shiftL` objectSizeBits) + regionBase) userSizeBits isDevice 533> insertNewCap srcSlot slot cap) 534> [0 .. fromIntegral (length destSlots - 1)] destSlots 535 536The following function inserts a new revocable cap as a child of another. 537 538> insertNewCap :: PPtr CTE -> PPtr CTE -> Capability -> Kernel () 539> insertNewCap parent slot cap = do 540> next <- liftM (mdbNext . cteMDBNode) $ getCTE parent 541> oldCTE <- getCTE slot 542> assert (isNullCap (cteCap oldCTE) 543> && mdbNext (cteMDBNode oldCTE) == nullPointer 544> && mdbPrev (cteMDBNode oldCTE) == nullPointer) 545> "insertNewCap: slot and mdb entry must be empty" 546> setCTE slot $ CTE cap (MDB next parent True True) 547> updateMDB next $ (\m -> m { mdbPrev = slot }) 548> updateMDB parent $ (\m -> m { mdbNext = slot }) 549> updateNewFreeIndex slot 550 551The following function is used by the bootstrap code to create the initial set of capabilities. 552 553> insertInitCap :: PPtr CTE -> Capability -> Kernel () 554> insertInitCap slot cap = do 555> oldCTE <- getCTE slot 556> assert (isNullCap $ cteCap oldCTE) "insertInitCap: slot must be empty" 557> assert (not $ isNullCap cap) "insertInitCap: cannot insert null" 558> assert (mdbPrev (cteMDBNode oldCTE) == nullPointer && 559> mdbNext (cteMDBNode oldCTE) == nullPointer) 560> "insertInitCap: mdb entry must be empty" 561> updateCap slot cap 562> updateMDB slot (const (nullMDBNode { 563> mdbRevocable = True, 564> mdbFirstBadged = True })) 565 566The following function is called when a thread is restarted, to ensure that the thread's master reply capability exists. This is a special capability that exists only to be the MDB parent of a real reply capability generated by an IPC "Call" operation. It can never be invoked. 567 568> setupReplyMaster :: PPtr TCB -> Kernel () 569> setupReplyMaster thread = do 570> slot <- locateSlotTCB thread tcbReplySlot 571> oldCTE <- getCTE slot 572> when (isNullCap $ cteCap oldCTE) $ do 573> stateAssert (noReplyCapsFor thread) 574> "setupReplyMaster: reply master must not exist" 575> let cap = ReplyCap { capTCBPtr = thread, capReplyMaster = True } 576> let mdb = nullMDBNode { mdbRevocable = True, mdbFirstBadged = True } 577> setCTE slot $ CTE cap mdb 578 579This function is used in the assertion above; it returns "True" if no reply capabilities (masters or otherwise) currently exist for the given thread. In the Haskell model, it always returns "True"; in the Isabelle formalisation of this model, it is strengthened to return "False" if a reply capability for the thread does exist. 580 581> noReplyCapsFor :: PPtr TCB -> KernelState -> Bool 582> noReplyCapsFor _ _ = True 583 584These functions concern the free indices of untyped caps. For verification reasons we also track the free ranges in a ghost variable, which must be updated appropriately when untyped caps might be changed. 585 586> updateTrackedFreeIndex :: PPtr CTE -> Int -> Kernel () 587> updateTrackedFreeIndex slot idx = do 588> cap <- getSlotCap slot 589> modify (\ks -> ks {gsUntypedZeroRanges = 590> case untypedZeroRange cap of 591> Nothing -> gsUntypedZeroRanges ks 592> Just r -> Data.Set.delete r (gsUntypedZeroRanges ks) 593> }) 594> modify (\ks -> ks {gsUntypedZeroRanges = 595> case untypedZeroRange (cap {capFreeIndex = idx}) of 596> Nothing -> gsUntypedZeroRanges ks 597> Just r -> Data.Set.insert r (gsUntypedZeroRanges ks) 598> }) 599 600> updateFreeIndex :: PPtr CTE -> Int -> Kernel () 601> updateFreeIndex slot idx = do 602> updateTrackedFreeIndex slot idx 603> cap <- getSlotCap slot 604> updateCap slot (cap {capFreeIndex = idx}) 605 606> clearUntypedFreeIndex :: PPtr CTE -> Kernel () 607> clearUntypedFreeIndex slot = do 608> cap <- getSlotCap slot 609> case cap of 610> UntypedCap {} -> updateTrackedFreeIndex slot 611> (maxFreeIndex (capBlockSize cap)) 612> _ -> return () 613 614> updateNewFreeIndex :: PPtr CTE -> Kernel () 615> updateNewFreeIndex slot = do 616> cap <- getSlotCap slot 617> case cap of 618> UntypedCap {} -> updateTrackedFreeIndex slot (capFreeIndex cap) 619> _ -> return () 620 621\subsection{MDB Operations} 622\label{sec:object.cnode.mdb} 623 624The Mapping Database (MDB) is used to keep track of the derivation hierarchy of seL4 capabilities, so all existing capabilities to an object can be revoked before that object is reused or deleted. A similar structure is used in L4Ka::Pistachio\cite{Pistachio:URL} to support that kernel's Unmap operation. 625 626The MDB is a double-linked list that is equivalent to a prefix traversal of the derivation tree. It is possible to compare two capabilities to determine whether one is an ancestor of the other in the derivation tree. 627 628> isMDBParentOf :: CTE -> CTE -> Bool 629 630To be the parent of "b", "a" must have the "mdbRevocable" bit set and must have authority over the same physical resources as "b". 631 632> isMDBParentOf (CTE a mdbA) (CTE b mdbB) 633> | not $ mdbRevocable mdbA = False 634> | not $ a `sameRegionAs` b = False 635> | otherwise = case a of 636 637If "a" is an endpoint capability with a badge set, then it is the parent of "b" if and only if "b" has the same badge as "a" and has the "mdbFirstBadged" bit clear. 638 639> EndpointCap { capEPBadge = badge } | badge /= 0 -> 640> (badge == capEPBadge b) && (not $ mdbFirstBadged mdbB) 641> NotificationCap { capNtfnBadge = badge } | badge /= 0 -> 642> (badge == capNtfnBadge b) && (not $ mdbFirstBadged mdbB) 643 644Otherwise, the object is not an endpoint, and "a" is the parent of "b". 645 646> _ -> True 647 648% XXX diagram to illustrate this 649 650In several of the functions in this module, it is necessary to modify the MDB node in a CTE without changing anything else in the CTE, and to skip the operation if the CTE pointer is null. The following function is a helper function used to do so. 651 652> updateMDB :: PPtr CTE -> (MDBNode -> MDBNode) -> Kernel () 653> updateMDB 0 _ = return () 654> updateMDB slot f = do 655> cte <- getCTE slot 656> let mdb = cteMDBNode cte 657> let mdb' = f mdb 658> let cte' = cte { cteMDBNode = mdb' } 659> setCTE slot cte' 660 661\subsection{Error Checking} 662 663Before retyping an untyped memory object, it is necessary to check that the object contains no existing objects. 664 665> ensureNoChildren :: PPtr CTE -> KernelF SyscallError () 666> ensureNoChildren slot = do 667> cte <- withoutFailure $ getCTE slot 668> when (mdbNext (cteMDBNode cte) /= nullPointer) $ do 669> next <- withoutFailure $ getCTE (mdbNext $ cteMDBNode cte) 670> when (cte `isMDBParentOf` next) $ throw RevokeFirst 671 672When creating or deriving new capabilities, the destination slot must be empty. 673 674> ensureEmptySlot :: PPtr CTE -> KernelF SyscallError () 675> ensureEmptySlot slot = do 676> cte <- withoutFailure $ getCTE slot 677> unless (isNullCap $ cteCap cte) $ throw DeleteFirst 678 679\subsection{Accessing Capabilities} 680 681\subsubsection{Locating Slots} 682 683These functions are used for locating a slot at a given offset in a CNode. When 684performing an offset into a regular CNode, the offset is checked against the 685ghost state. This check is skipped for the CNode within TCBs. 686 687> locateSlotBasic :: PPtr CTE -> Word -> Kernel (PPtr CTE) 688> locateSlotBasic cnode offset = do 689> let slotSize = 1 `shiftL` objBits (undefined::CTE) 690> return $ PPtr $ fromPPtr $ cnode + PPtr (slotSize * offset) 691 692> locateSlotTCB :: PPtr TCB -> Word -> Kernel (PPtr CTE) 693> locateSlotTCB tcb offset = locateSlotBasic (PPtr $ fromPPtr tcb) offset 694 695> locateSlotCNode :: PPtr CTE -> Int -> Word -> Kernel (PPtr CTE) 696> locateSlotCNode cnode bits offset = do 697> flip stateAssert "locateSlotCNode: must be in CNode" 698> (\s -> case gsCNodes s (fromPPtr cnode) of 699> Nothing -> False 700> Just n -> n == bits && offset < 2 ^ n) 701> locateSlotBasic cnode offset 702 703> locateSlotCap :: Capability -> Word -> Kernel (PPtr CTE) 704> locateSlotCap (cap @ (CNodeCap {})) offset 705> = locateSlotCNode (capCNodePtr cap) (capCNodeBits cap) offset 706> locateSlotCap (cap @ (ThreadCap {})) offset 707> = locateSlotTCB (capTCBPtr cap) offset 708> locateSlotCap (cap @ (Zombie {})) offset = case capZombieType cap of 709> ZombieTCB -> locateSlotTCB (PPtr $ fromPPtr $ capZombiePtr cap) offset 710> ZombieCNode bits -> locateSlotCNode (capZombiePtr cap) bits offset 711> locateSlotCap _ _ = fail "locateSlotCap: not a cap with slots" 712 713\subsubsection{Loading and Storing Entries} 714 715The following two functions are specialisations of "getObject" and 716"setObject" for the capability table entry object and pointer types. 717 718> getCTE :: PPtr CTE -> Kernel CTE 719> getCTE = getObject 720 721> setCTE :: PPtr CTE -> CTE -> Kernel () 722> setCTE = setObject 723 724Often, only the capability slot of the CTE needs to be modified. 725 726> updateCap :: PPtr CTE -> Capability -> Kernel () 727> updateCap slot newCap = do 728> cte <- getCTE slot 729> setCTE slot (cte { cteCap = newCap }) 730 731\subsubsection{Reading Capabilities} 732 733At higher levels of the kernel model ("SEL4.Kernel" and "SEL4.API"), 734capabilities are represented by the abstract "Capability" type, rather 735than the "CTE" type that is used to store them in memory. 736 737The following functions are used to extract capabilities, in the form 738of "Capability" objects, from the "CTE"s that store them. 739 740> getSlotCap :: PPtr CTE -> Kernel Capability 741> getSlotCap ptr = do 742> cte <- getCTE ptr 743> return $ cteCap cte 744 745\subsubsection{Testing Capabilities} 746 747When deleting a capability, it is necessary to determine whether it is the only existing capability to access a typed object it refers to. When an object's last remaining capability is deleted, the kernel must clean up any internal references it has to the object (in the scheduler's ready queues, the mapping database, and so on). The following function tests a capability to determine whether it is the last. 748 749> isFinalCapability :: CTE -> Kernel Bool 750> isFinalCapability cte@(CTE { cteMDBNode = mdb }) = do 751> prevIsSameObject <- if mdbPrev mdb == nullPointer 752> then return False 753> else do 754> prev <- getCTE (mdbPrev mdb) 755> return $! sameObjectAs (cteCap prev) (cteCap cte) 756> if prevIsSameObject 757> then return False 758> else if mdbNext mdb == nullPointer 759> then return True 760> else do 761> next <- getCTE (mdbNext mdb) 762> return $ not $ sameObjectAs (cteCap cte) (cteCap next) 763 764The "SetSpace" method of the "TCB" object type will refuse to change the address space roots of a thread if removing the existing root capability might cause a long running delete --- see \autoref{sec:object.tcb.decode.setspace} for details. These functions are called to perform that check. 765 766> longRunningDelete :: Capability -> Bool 767> longRunningDelete (ThreadCap {}) = True 768> longRunningDelete (CNodeCap {}) = True 769> longRunningDelete (Zombie {}) = True 770> longRunningDelete _ = False 771 772> slotCapLongRunningDelete :: PPtr CTE -> Kernel Bool 773> slotCapLongRunningDelete slot = do 774> cte <- getCTE slot 775> case cteCap cte of 776> NullCap -> return False 777> _ -> do 778> final <- isFinalCapability cte 779> return $ final && longRunningDelete (cteCap cte) 780 781\subsection{Capability Transfers} 782 783The following function locates the available receive slots for a capability transfer. If a specified slot is non-empty, the message will be truncated rather than using that slot. As with truncation of untyped data, the receiver is expected to either detect this at user level based on a protocol violation, or not care. 784 785Note that the kernel API currently only allows one receive slot to be specified, so the list returned by "getReceiveSlots" only contains one item. However, this may change in future. The code calling this function does not assume that there is only one receive slot. 786 787> getReceiveSlots :: PPtr TCB -> Maybe (PPtr Word) -> 788> Kernel [PPtr CTE] 789> getReceiveSlots thread (Just buffer) = do 790 791Load the receive parameters from the receiving thread's IPC buffer. 792 793> ct <- loadCapTransfer buffer 794 795Look up the specified root CNode, and then the slot at the given index and depth in that CNode's tree. Fail if there is already a valid capability in it, to avoid a potentially slow revocation during the IPC operation. Any faults or errors occurring during the lookup operations are caught here. 796 797> emptyOnFailure $ do 798> let cptr = ctReceiveRoot ct 799> cnode <- unifyFailure $ lookupCap thread cptr 800> slot <- unifyFailure $ lookupTargetSlot 801> cnode (ctReceiveIndex ct) (ctReceiveDepth ct) 802> cte <- withoutFailure $ getCTE slot 803> unless (isNullCap $ cteCap cte) $ throw () 804> return [slot] 805> getReceiveSlots _ Nothing = return [] 806 807This helper function is used to load the capability transfer data from an IPC buffer. 808 809> loadCapTransfer :: PPtr Word -> Kernel CapTransfer 810> loadCapTransfer buffer = do 811> let intSize = fromIntegral wordSize 812> let offset = msgMaxLength + msgMaxExtraCaps + 2 813> capTransferFromWords (buffer + PPtr (offset*intSize)) 814 815> capTransferFromWords :: PPtr Word -> Kernel CapTransfer 816> capTransferFromWords ptr = do 817> let intSize = fromIntegral wordSize 818> w0 <- loadWordUser ptr 819> w1 <- loadWordUser $ ptr + PPtr intSize 820> w2 <- loadWordUser $ ptr + PPtr (2 * intSize) 821> return CT { 822> ctReceiveRoot = CPtr w0, 823> ctReceiveIndex = CPtr w1, 824> ctReceiveDepth = fromIntegral w2 } 825 826 827