diff --git a/Makefile b/Makefile index c30a93231..ea0cac5ca 100644 --- a/Makefile +++ b/Makefile @@ -208,10 +208,6 @@ STATICHEADERS := $(shell find ${SOURCE_ROOT}/include/ -name "*.h" \ $(shell find ${SOURCE_ROOT}/include/arch/${ARCH} -name "*.h") \ $(shell find ${SOURCE_ROOT}/include/plat/${PLAT} -name "*.h") -ifeq (${HAVE_AUTOCONF}, 1) - STATICHEADERS += $(srctree)/include/generated/autoconf.h -endif - STATICSOURCES = $(foreach file,${C_SOURCES_WITH_PARSE} ${ASM_SOURCES}, \ ${SOURCE_ROOT}/${file}) @@ -352,6 +348,8 @@ endif # Only set CFLAGS if we're building standalone. # common/Makefile.Flags sets NK_CFLAGS in Kbuild environments. ifndef NK_CFLAGS +STATICHEADERS += autoconf.h +DEFINES += -DHAVE_AUTOCONF ifeq (${ARCH}, arm) CFLAGS += -mtune=${CPU} -marm -march=${ARMV} ASFLAGS += -Wa,-mcpu=${CPU} -Wa,-march=${ARMV} @@ -399,15 +397,18 @@ endif ifeq ($(PLAT),allwinnerA20) DEFINES += -DALLWINNERA20 endif -endif # NK_CFLAGS - +endif # ARCH=arm ifeq (${ARCH}, x86) CFLAGS += -m32 -mno-mmx -mno-sse ASFLAGS += -Wa,--32 DEFINES += -DARCH_IA32 LDFLAGS += -Wl,-m,elf_i386 -endif -endif +endif # ARCH=x86 +else # NK_CFLAGS +# Require autoconf to be provided if larger build +$(if ${HAVE_AUTOCONF},,$(error autoconf.h not provided)) +STATICHEADERS += $(srctree)/include/generated/autoconf.h +endif # NK_CFLAGS ifeq (${CPU}, arm1136jf-s) DEFINES += -DARM1136_WORKAROUND @@ -537,6 +538,9 @@ kernel.elf: ${OBJECTS} linker.lds_pp $(Q)${CHANGED} $@ ${CC} ${LDFLAGS} -Wl,-T -Wl,linker.lds_pp \ -o $@ ${OBJECTS} +autoconf.h: include/plat/${PLAT}/autoconf.h + ${Q}cp $< $@ + ############################################################ ### Pattern rules ############################################################ @@ -571,7 +575,6 @@ arch/api/syscall.h: ${SOURCE_ROOT}/include/api/syscall.xsd ${SOURCE_ROOT}/includ $(Q)${SYSCALL_ID_GEN_PATH} --xml $(word 2, $^) \ --kernel_header $@ - #################### # Bitfield generation #################### @@ -638,7 +641,7 @@ endif ### Utility targets ############################################################ -CLEANTARGETS = kernel.elf kernel.elf.strip ${GENHEADERS} ${OBJECTS} \ +CLEANTARGETS = kernel.elf kernel.elf.strip ${GENHEADERS} ${OBJECTS} autoconf.h \ parser.out parsetab.py \ kernel_final.s kernel_final.c kernel_all.c kernel_all.c_pp \ ${PPFILES} ${THEORIES} c-parser.log c-parser-all.log \ diff --git a/haskell/src/SEL4/API/Syscall.lhs b/haskell/src/SEL4/API/Syscall.lhs index fab6f0548..66a0f08ea 100644 --- a/haskell/src/SEL4/API/Syscall.lhs +++ b/haskell/src/SEL4/API/Syscall.lhs @@ -64,6 +64,7 @@ the enumerated type "Syscall": > | SysReply > | SysReplyWait > | SysYield +> | SysNBWait > deriving (Show, Enum, Bounded, Eq) \subsection{Handling Events} @@ -82,12 +83,13 @@ System call events are dispatched here to the appropriate system call handlers, > SysSend -> handleSend True > SysNBSend -> handleSend False > SysCall -> handleCall -> SysWait -> withoutPreemption handleWait +> SysWait -> withoutPreemption $ handleWait True > SysReply -> withoutPreemption handleReply > SysReplyWait -> withoutPreemption $ do > handleReply -> handleWait +> handleWait True > SysYield -> withoutPreemption handleYield +> SysNBWait -> withoutPreemption $ handleWait False \subsubsection{Interrupts} @@ -176,22 +178,22 @@ The "Reply" system call attempts to perform an immediate IPC transfer to the thr The "Wait" system call blocks waiting to receive a message through a specified endpoint. It will fail if the specified capability does not refer to an endpoint object. -> handleWait :: Kernel () -> handleWait = do +> handleWait :: Bool -> Kernel () +> handleWait isBlocking = do > thread <- getCurThread > epCPtr <- asUser thread $ liftM CPtr $ getRegister capRegister > (capFaultOnFailure epCPtr True $ do > epCap <- lookupCap thread epCPtr > case epCap of -> EndpointCap { capEPCanReceive = True } -> +> EndpointCap { capEPCanReceive = True } -> do > withoutFailure $ do > deleteCallerCap thread -> receiveIPC thread epCap +> receiveIPC thread epCap isBlocking > AsyncEndpointCap { capAEPCanReceive = True, capAEPPtr = ptr } -> do > aep <- withoutFailure $ getAsyncEP ptr > boundTCB <- return $ aepBoundTCB aep > if boundTCB == Just thread || boundTCB == Nothing -> then withoutFailure $ receiveAsyncIPC thread epCap +> then withoutFailure $ receiveAsyncIPC thread epCap isBlocking > else throw $ MissingCapability { missingCapBitsLeft = 0 } > _ -> throw $ MissingCapability { missingCapBitsLeft = 0 }) > `catchFailure` handleFault thread diff --git a/haskell/src/SEL4/Kernel/Init.lhs b/haskell/src/SEL4/Kernel/Init.lhs index 4836a205a..2c7be457e 100644 --- a/haskell/src/SEL4/Kernel/Init.lhs +++ b/haskell/src/SEL4/Kernel/Init.lhs @@ -25,6 +25,7 @@ This module contains functions that create a new kernel state and set up the add > import SEL4.API.Failures > import SEL4.Model > import SEL4.Object +> import SEL4.Object.Structures > import SEL4.Machine > import SEL4.Kernel.Thread > import SEL4.Kernel.VSpace @@ -133,7 +134,6 @@ The kernel is bootstrapped by calling "initKernel". The arguments are the addres Define some useful constants. -> let wordSize = finiteBitSize entry > let uiRegion = coverOf $ map (\x -> Region (ptrFromPAddr x, (ptrFromPAddr x) + bit (pageBits))) initFrames > let kernelRegion = coverOf $ map (\x -> Region (ptrFromPAddr x, (ptrFromPAddr x) + bit (pageBits))) kernelFrames > let kePPtr = fst $ fromRegion $ uiRegion @@ -297,7 +297,7 @@ FIXME: Seems we need to setCurThread and setSchedulerAction here, otherwise erro > freemem <- noInitFailure $ gets initFreeMemory > (flip mapM) (take maxNumFreememRegions freemem) > (\reg -> do -> (\f -> mapM (f reg) [4 .. (finiteBitSize (undefined::Word)) - 2]) +> (\f -> mapM (f reg) [4 .. wordBits - 2]) > (\reg bits -> do > reg' <- (if not (isAligned (regStartPAddr reg) (bits + 1)) > && (regEndPAddr reg) - (regStartPAddr reg) >= bit bits diff --git a/haskell/src/SEL4/Kernel/Thread.lhs b/haskell/src/SEL4/Kernel/Thread.lhs index bd98de820..573902725 100644 --- a/haskell/src/SEL4/Kernel/Thread.lhs +++ b/haskell/src/SEL4/Kernel/Thread.lhs @@ -36,6 +36,7 @@ We use the C preprocessor to select a target architecture. > import {-# SOURCE #-} SEL4.Kernel.Init > import Data.Bits +> import Data.Array \end{impdetails} @@ -284,8 +285,7 @@ This function is called when an IPC message includes a capability to transfer. I > _ -> return $ mi { msgExtraCaps = fromIntegral n } > where > transferAgain = transferCapsToSlots ep diminish rcvBuffer (n + 1) caps -> bitN = 1 `shiftL` n -> miCapUnfolded = mi { msgCapsUnwrapped = msgCapsUnwrapped mi .|. bitN } +> miCapUnfolded = mi { msgCapsUnwrapped = msgCapsUnwrapped mi .|. bit n} > (cap, srcSlot) = arg \subsubsection{Asynchronous IPC} @@ -327,29 +327,38 @@ If the current thread is no longer runnable, has used its entire timeslice, an I > setSchedulerAction ResumeCurrentThread Threads are scheduled using a simple multiple-priority round robin algorithm. -It iterates through the ready queues, starting with the highest priority -queue; when it finds a non-empty ready queue, it selects the first -thread in the queue, and makes it the current thread. - +It checks the priority bitmaps to find the highest priority with a non-empty +queue. It selects the first thread in that queue and makes it the current +thread. Note that the ready queues are a separate structure in the kernel model. In a real implementation, to avoid requiring dynamically-allocated kernel memory, these queues would be linked lists using the TCBs themselves as nodes. +> countLeadingZeros :: (Bits b, FiniteBits b) => b -> Int +> countLeadingZeros w = +> length . takeWhile not . reverse . map (testBit w) $ [0 .. finiteBitSize w - 1] + +> wordLog2 :: (Bits b, FiniteBits b) => b -> Int +> wordLog2 w = finiteBitSize w - 1 - countLeadingZeros w + > chooseThread :: Kernel () > chooseThread = do -> curdom <- curDomain -> r <- findM (chooseThread' curdom) (reverse [0 .. maxPriority]) -> when (r == Nothing) $ switchToIdleThread -> where -> chooseThread' :: Domain -> Priority -> Kernel Bool -> chooseThread' qdom prio = do -> q <- getQueue qdom prio -> case q of -> thread : _ -> do -> switchToThread thread -> return True -> [] -> return False +> curdom <- if numDomains > 1 then curDomain else return 0 +> l1 <- getReadyQueuesL1Bitmap curdom +> if l1 /= 0 +> then do +> let l1index = wordLog2 l1 +> l2 <- getReadyQueuesL2Bitmap curdom l1index +> let l2index = wordLog2 l2 +> let prio = l1IndexToPrio l1index .|. fromIntegral l2index +> queue <- getQueue curdom prio +> let thread = head queue +> runnable <- isRunnable thread +> assert runnable "Scheduled a non-runnable thread" +> switchToThread thread +> else +> switchToIdleThread \subsubsection{Switching Threads} @@ -486,6 +495,49 @@ When setting the scheduler state, we check for blocking of the current thread; i The following two functions place a thread at the beginning or end of its priority's ready queue, unless it is already queued. +FIXME DOCUMENT TWEAK AND MOVE + +> prioToL1Index :: Priority -> Int +> prioToL1Index prio = fromIntegral $ prio `shiftR` wordRadix + +> l1IndexToPrio :: Int -> Priority +> l1IndexToPrio i = (fromIntegral i) `shiftL` wordRadix + +> getReadyQueuesL1Bitmap :: Domain -> Kernel (Word) +> getReadyQueuesL1Bitmap tdom = gets (\ks -> ksReadyQueuesL1Bitmap ks ! tdom) + +> modifyReadyQueuesL1Bitmap :: Domain -> (Word -> Word) -> Kernel () +> modifyReadyQueuesL1Bitmap tdom f = do +> l1 <- getReadyQueuesL1Bitmap tdom +> modify (\ks -> ks { ksReadyQueuesL1Bitmap = +> ksReadyQueuesL1Bitmap ks // [(tdom, f l1)]}) + +> getReadyQueuesL2Bitmap :: Domain -> Int -> Kernel (Word) +> getReadyQueuesL2Bitmap tdom i = gets (\ks -> ksReadyQueuesL2Bitmap ks ! (tdom, i)) + +> modifyReadyQueuesL2Bitmap :: Domain -> Int -> (Word -> Word) -> Kernel () +> modifyReadyQueuesL2Bitmap tdom i f = do +> l2 <- getReadyQueuesL2Bitmap tdom i +> modify (\ks -> ks { ksReadyQueuesL2Bitmap = +> ksReadyQueuesL2Bitmap ks // [((tdom, i), f l2)]}) + +> addToBitmap :: Domain -> Priority -> Kernel () +> addToBitmap tdom prio = do +> let l1index = prioToL1Index prio +> let l2bit = fromIntegral ((fromIntegral prio .&. mask wordRadix)::Word) +> modifyReadyQueuesL1Bitmap tdom $ \w -> w .|. bit l1index +> modifyReadyQueuesL2Bitmap tdom l1index +> (\w -> w .|. bit l2bit) + +> removeFromBitmap :: Domain -> Priority -> Kernel () +> removeFromBitmap tdom prio = do +> let l1index = prioToL1Index prio +> let l2bit = fromIntegral((fromIntegral prio .&. mask wordRadix)::Word) +> modifyReadyQueuesL2Bitmap tdom l1index $ \w -> w .&. (complement $ bit l2bit) +> l2 <- getReadyQueuesL2Bitmap tdom l1index +> when (l2 == 0) $ +> modifyReadyQueuesL1Bitmap tdom $ \w -> w .&. (complement $ bit l1index) + > tcbSchedEnqueue :: PPtr TCB -> Kernel () > tcbSchedEnqueue thread = do > queued <- threadGet tcbQueued thread @@ -494,6 +546,7 @@ The following two functions place a thread at the beginning or end of its priori > prio <- threadGet tcbPriority thread > queue <- getQueue tdom prio > setQueue tdom prio $ thread : queue +> when (null queue) $ addToBitmap tdom prio > threadSet (\t -> t { tcbQueued = True }) thread > tcbSchedAppend :: PPtr TCB -> Kernel () @@ -504,6 +557,7 @@ The following two functions place a thread at the beginning or end of its priori > prio <- threadGet tcbPriority thread > queue <- getQueue tdom prio > setQueue tdom prio $ queue ++ [thread] +> when (null queue) $ addToBitmap tdom prio > threadSet (\t -> t { tcbQueued = True }) thread The following function dequeues a thread, if it is queued. @@ -515,7 +569,9 @@ The following function dequeues a thread, if it is queued. > tdom <- threadGet tcbDomain thread > prio <- threadGet tcbPriority thread > queue <- getQueue tdom prio -> setQueue tdom prio $ filter (/=thread) queue +> let queue' = filter (/=thread) queue +> setQueue tdom prio queue' +> when (null queue') $ removeFromBitmap tdom prio > threadSet (\t -> t { tcbQueued = False }) thread \subsubsection{Timer Ticks} diff --git a/haskell/src/SEL4/Model/StateData.lhs b/haskell/src/SEL4/Model/StateData.lhs index e98baa35a..77ceadb23 100644 --- a/haskell/src/SEL4/Model/StateData.lhs +++ b/haskell/src/SEL4/Model/StateData.lhs @@ -77,6 +77,11 @@ The top-level kernel state structure is called "KernelState". It contains: > ksReadyQueues :: Array (Domain, Priority) ReadyQueue, +\item a bitmap for each domain; each bit represents the presence of a runnable thread for a specific priority + +> ksReadyQueuesL1Bitmap :: Array (Domain) Word, +> ksReadyQueuesL2Bitmap :: Array (Domain, Int) Word, + \item a pointer to the current thread's control block; > ksCurThread :: PPtr TCB, @@ -105,6 +110,8 @@ The top-level kernel state structure is called "KernelState". It contains: Note that this definition of "KernelState" assumes a single processor. The behaviour of the kernel on multi-processor systems is not specified by this document. +Note that the priority bitmap is split up into two levels. In order to check to see whether a priority has a runnable thread on a 32-bit system with a maximum priority of 255, we use the high 3 bits of the priority as an index into the level 1 bitmap. If the bit at that index is set, we use those same three bits to obtain a word from the level 2 bitmap. We then use the remaining 5 bits to index into that word. If the bit is set, the queue for that priority is non-empty. + \subsubsection{Monads} Kernel functions are sequences of operations that transform a "KernelState" object. They are encapsulated in the monad "Kernel", which uses "StateT" to add a "KernelState" data structure to the monad that encapsulates the simulated machine, "MachineMonad". This allows functions to read and modify the kernel state. @@ -219,6 +226,10 @@ A new kernel state structure contains an empty physical address space, a set of > ksReadyQueues = > funPartialArray (const []) > ((0, 0), (fromIntegral numDomains, fromIntegral numPriorities)), +> ksReadyQueuesL1Bitmap = funPartialArray (const 0) (0, fromIntegral numDomains), +> ksReadyQueuesL2Bitmap = +> funPartialArray (const 0) +> ((0, 0), (fromIntegral numDomains, numPriorities `div` wordBits + 1)), > ksCurThread = error "No initial thread", > ksIdleThread = error "Idle thread has not been created", > ksSchedulerAction = error "scheduler action has not been set", diff --git a/haskell/src/SEL4/Object/AsyncEndpoint.lhs b/haskell/src/SEL4/Object/AsyncEndpoint.lhs index 2220a527a..35b9bb790 100644 --- a/haskell/src/SEL4/Object/AsyncEndpoint.lhs +++ b/haskell/src/SEL4/Object/AsyncEndpoint.lhs @@ -14,7 +14,7 @@ This module specify the behavior of a asynchronous IPC endpoints. > sendAsyncIPC, receiveAsyncIPC, > aepCancelAll, asyncIPCCancel, completeAsyncIPC, > getAsyncEP, setAsyncEP, doUnbindAEP, unbindAsyncEndpoint, -> unbindMaybeAEP, bindAsyncEndpoint +> unbindMaybeAEP, bindAsyncEndpoint, doNBWaitFailedTransfer > ) where \begin{impdetails} @@ -88,11 +88,17 @@ If the endpoint is active, new values are calculated and stored in the endpoint. \subsection{Receiving Messages} -This function performs an asynchronous IPC receive operation, given a thread pointer and a capability to an asynchronous endpoint. The receive is blocking -- the thread will be blocked on the endpoint till a message arrives. +This function performs an asynchronous IPC receive operation, given a thread pointer and a capability to an asynchronous endpoint. +The receive can be either blocking (the thread will be blocked on the endpoint till a message arrives) or non-blocking +depending on the isBlocking flag. -> receiveAsyncIPC :: PPtr TCB -> Capability -> Kernel () +> doNBWaitFailedTransfer :: PPtr TCB -> Kernel () +> doNBWaitFailedTransfer thread = asUser thread $ setRegister badgeRegister 0 -> receiveAsyncIPC thread cap = do + +> receiveAsyncIPC :: PPtr TCB -> Capability -> Bool -> Kernel () + +> receiveAsyncIPC thread cap isBlocking = do Fetch the asynchronous endpoint, and select the operation based on its state. @@ -102,17 +108,22 @@ Fetch the asynchronous endpoint, and select the operation based on its state. If the asynchronous endpoint is idle, then it becomes a waiting asynchronous endpoint, with the current thread in its queue. The thread is blocked. -> IdleAEP -> do -> setThreadState (BlockedOnAsyncEvent { -> waitingOnAsyncEP = aepptr } ) thread -> setAsyncEP aepptr $ aep {aepObj = WaitingAEP [thread] } +> IdleAEP -> case isBlocking of +> True -> do +> setThreadState (BlockedOnAsyncEvent { +> waitingOnAsyncEP = aepptr } ) thread +> setAsyncEP aepptr $ aep {aepObj = WaitingAEP ([thread]) } +> False -> doNBWaitFailedTransfer thread -If the asynchronous endpoint is already waiting, the current thread is blocked and added to the queue. Note that this case cannot occur when the asynchronous endpoint is bound, as only the associated thread can wait on it. +If the asynchronous endpoint is already waiting, the current thread is blocked and added to the queue. Note that this case cannot occur when the asynchronous endpoint is bound, +as only the associated thread can wait on it. -> WaitingAEP queue -> do -> setThreadState (BlockedOnAsyncEvent { -> waitingOnAsyncEP = aepptr } ) thread -> setAsyncEP aepptr $ aep {aepObj = WaitingAEP (queue ++ [thread]) } +> WaitingAEP queue -> case isBlocking of +> True -> do +> setThreadState (BlockedOnAsyncEvent { +> waitingOnAsyncEP = aepptr } ) thread +> setAsyncEP aepptr $ aep {aepObj = WaitingAEP (queue ++ [thread]) } +> False -> doNBWaitFailedTransfer thread If the asynchronous endpoint is active, the message will be loaded to the MRs of the thread and the endpoint will be marked as idle. diff --git a/haskell/src/SEL4/Object/CNode.lhs b/haskell/src/SEL4/Object/CNode.lhs index 47ffdefb3..2af4f5a4a 100644 --- a/haskell/src/SEL4/Object/CNode.lhs +++ b/haskell/src/SEL4/Object/CNode.lhs @@ -780,13 +780,13 @@ This helper function is used to load the capability transfer data from an IPC bu > loadCapTransfer :: PPtr Word -> Kernel CapTransfer > loadCapTransfer buffer = do -> let intSize = fromIntegral $ finiteBitSize (undefined::Word) `div` 8 +> let intSize = fromIntegral wordSize > let offset = msgMaxLength + msgMaxExtraCaps + 2 > capTransferFromWords (buffer + PPtr (offset*intSize)) > capTransferFromWords :: PPtr Word -> Kernel CapTransfer > capTransferFromWords ptr = do -> let intSize = fromIntegral $ finiteBitSize (undefined::Word) `div` 8 +> let intSize = fromIntegral wordSize > w0 <- loadWordUser ptr > w1 <- loadWordUser $ ptr + PPtr intSize > w2 <- loadWordUser $ ptr + PPtr (2 * intSize) diff --git a/haskell/src/SEL4/Object/Endpoint.lhs b/haskell/src/SEL4/Object/Endpoint.lhs index c0073b8a8..986be4173 100644 --- a/haskell/src/SEL4/Object/Endpoint.lhs +++ b/haskell/src/SEL4/Object/Endpoint.lhs @@ -113,8 +113,8 @@ The IPC receive operation is essentially the same as the send operation, but wit > isActive (AEP (ActiveAEP _) _) = True > isActive _ = False -> receiveIPC :: PPtr TCB -> Capability -> Kernel () -> receiveIPC thread cap@(EndpointCap {}) = do +> receiveIPC :: PPtr TCB -> Capability -> Bool -> Kernel () +> receiveIPC thread cap@(EndpointCap {}) isBlocking = do > let epptr = capEPPtr cap > ep <- getEndpoint epptr > let diminish = not $ capEPCanSend cap @@ -124,16 +124,20 @@ The IPC receive operation is essentially the same as the send operation, but wit > if (isJust aepptr && isActive aep) > then completeAsyncIPC (fromJust aepptr) thread > else case ep of -> IdleEP -> do -> setThreadState (BlockedOnReceive { -> blockingIPCEndpoint = epptr, -> blockingIPCDiminishCaps = diminish }) thread -> setEndpoint epptr $ RecvEP [thread] -> RecvEP queue -> do -> setThreadState (BlockedOnReceive { -> blockingIPCEndpoint = epptr, -> blockingIPCDiminishCaps = diminish }) thread -> setEndpoint epptr $ RecvEP $ queue ++ [thread] +> IdleEP -> case isBlocking of +> True -> do +> setThreadState (BlockedOnReceive { +> blockingIPCEndpoint = epptr, +> blockingIPCDiminishCaps = diminish }) thread +> setEndpoint epptr $ RecvEP [thread] +> False -> doNBWaitFailedTransfer thread +> RecvEP queue -> case isBlocking of +> True -> do +> setThreadState (BlockedOnReceive { +> blockingIPCEndpoint = epptr, +> blockingIPCDiminishCaps = diminish }) thread +> setEndpoint epptr $ RecvEP $ queue ++ [thread] +> False -> doNBWaitFailedTransfer thread > SendEP (sender:queue) -> do > setEndpoint epptr $ case queue of > [] -> IdleEP @@ -155,7 +159,7 @@ The IPC receive operation is essentially the same as the send operation, but wit > _ -> setThreadState Inactive sender > SendEP [] -> fail "Send endpoint queue must not be empty" -> receiveIPC _ _ = fail "receiveIPC: invalid cap" +> receiveIPC _ _ _ = fail "receiveIPC: invalid cap" \subsection{Kernel Invocation Replies} diff --git a/haskell/src/SEL4/Object/Structures.lhs b/haskell/src/SEL4/Object/Structures.lhs index 36be8dacb..0ac49b627 100644 --- a/haskell/src/SEL4/Object/Structures.lhs +++ b/haskell/src/SEL4/Object/Structures.lhs @@ -410,10 +410,26 @@ Each entry in the domain schedule specifies a domain and a length (a number of t > dschLength :: (Domain, Word) -> Word > dschLength = snd -The following function selects one of two alternatives depending on the size of the machine word (32 or 64 bits). +Convenience functions dealing with properties of the machine word: +\begin{itemize} +\item Number of bits in a word +\item Radix $n$ such that $2^n$ is the number of bits in the word +\item Bytes required to store a word +\item Selecting one of two alternatives depending on the size of the machine word + (32 or 64 bits) +\end{itemize} + +> wordBits :: Int +> wordBits = finiteBitSize (undefined::Word) + +> wordRadix :: Int +> wordRadix = wordSizeCase 5 6 + +> wordSize :: Int +> wordSize = wordBits `div` 8 > wordSizeCase :: a -> a -> a -> wordSizeCase a b = case finiteBitSize (undefined::Word) of +> wordSizeCase a b = case wordBits of > 32 -> a > 64 -> b > _ -> error "Unknown word size" diff --git a/haskell/src/SEL4/Object/TCB.lhs b/haskell/src/SEL4/Object/TCB.lhs index b98908d1e..85ad05517 100644 --- a/haskell/src/SEL4/Object/TCB.lhs +++ b/haskell/src/SEL4/Object/TCB.lhs @@ -516,7 +516,7 @@ The "setMRs" function returns the number of words of message data successfully t > setMRs :: PPtr TCB -> Maybe (PPtr Word) -> [Word] -> Kernel Word > setMRs thread buffer messageData = do -> let intSize = fromIntegral $ finiteBitSize (undefined::Word) `div` 8 +> let intSize = fromIntegral wordSize > let hardwareMRs = msgRegisters > let bufferMRs = case buffer of > Just bufferPtr -> @@ -535,7 +535,7 @@ The "setMRs" function returns the number of words of message data successfully t > getMRs :: PPtr TCB -> Maybe (PPtr Word) -> MessageInfo -> > Kernel [Word] > getMRs thread buffer info = do -> let intSize = fromIntegral $ finiteBitSize (undefined::Word) `div` 8 +> let intSize = fromIntegral wordSize > let hardwareMRs = msgRegisters > hardwareMRValues <- asUser thread $ mapM getRegister hardwareMRs > bufferMRValues <- case buffer of @@ -556,7 +556,7 @@ This function's first argument is the maximum number of message registers to cop > PPtr TCB -> Maybe (PPtr Word) -> > Word -> Kernel Word > copyMRs sender sendBuf receiver recvBuf n = do -> let intSize = fromIntegral $ finiteBitSize (undefined::Word) `div` 8 +> let intSize = fromIntegral wordSize > let hardwareMRs = take (fromIntegral n) msgRegisters > forM hardwareMRs $ \r -> do > v <- asUser sender $ getRegister r @@ -577,7 +577,7 @@ The following functions read and set the extra capability fields of the IPC buff > getExtraCPtrs :: Maybe (PPtr Word) -> MessageInfo -> > Kernel [CPtr] > getExtraCPtrs buffer (MI { msgExtraCaps = count }) = do -> let intSize = fromIntegral $ finiteBitSize (undefined::Word) `div` 8 +> let intSize = fromIntegral wordSize > case buffer of > Just bufferPtr -> do > let offset = msgMaxLength+1 @@ -600,7 +600,7 @@ mapM (getExtraCPtr buffer) [0..count-1] > getExtraCPtr :: PPtr Word -> Int -> Kernel CPtr > getExtraCPtr buffer n = do -> let intSize = fromIntegral $ finiteBitSize (undefined::Word) `div` 8 +> let intSize = fromIntegral wordSize > let ptr = buffer + bufferCPtrOffset + > PPtr ((fromIntegral n) * intSize) > cptr <- loadWordUser ptr @@ -610,14 +610,14 @@ Write the unwrapped badge into the IPC buffer for cap n. > setExtraBadge :: PPtr Word -> Word -> Int -> Kernel () > setExtraBadge buffer badge n = do -> let intSize = fromIntegral $ finiteBitSize (undefined::Word) `div` 8 +> let intSize = fromIntegral wordSize > let badgePtr = buffer + bufferCPtrOffset + > PPtr ((fromIntegral n) * intSize) > storeWordUser badgePtr badge > bufferCPtrOffset :: PPtr Word > bufferCPtrOffset = -> let intSize = fromIntegral $ finiteBitSize (undefined::Word) `div` 8 +> let intSize = fromIntegral wordSize > in PPtr ((msgMaxLength+2)*intSize) \subsection{Creating and Destroying the Caller Capability} diff --git a/include/api/syscall.xml b/include/api/syscall.xml index 1c17e9c31..1439680c3 100644 --- a/include/api/syscall.xml +++ b/include/api/syscall.xml @@ -20,6 +20,7 @@ + diff --git a/include/arch/x86/arch/machine.h b/include/arch/x86/arch/machine.h index eba9f5f70..a7c9c83fe 100644 --- a/include/arch/x86/arch/machine.h +++ b/include/arch/x86/arch/machine.h @@ -18,7 +18,8 @@ #include #include -#define wordBits 32 +#define wordRadix 5 +#define wordBits (1 << wordRadix) #define IA32_APIC_BASE_MSR 0x01B #define IA32_SYSENTER_CS_MSR 0x174 diff --git a/include/kernel/thread.h b/include/kernel/thread.h index e8b773f08..3b62e4817 100644 --- a/include/kernel/thread.h +++ b/include/kernel/thread.h @@ -14,6 +14,30 @@ #include #include #include +#include + +static inline CONST word_t +ready_queues_index(word_t dom, word_t prio) +{ + if (CONFIG_NUM_DOMAINS > 1) { + return dom * CONFIG_NUM_PRIORITIES + prio; + } else { + assert(dom == 0); + return prio; + } +} + +static inline CONST word_t +prio_to_l1index(word_t prio) +{ + return (prio >> wordRadix); +} + +static inline CONST word_t +l1index_to_prio(word_t l1index) +{ + return (l1index << wordRadix); +} void configureIdleThread(tcb_t *tcb); void activateThread(void) VISIBLE; @@ -28,6 +52,7 @@ void doNormalTransfer(tcb_t *sender, word_t *sendBuffer, endpoint_t *endpoint, word_t *receiveBuffer, bool_t diminish); void doFaultTransfer(word_t badge, tcb_t *sender, tcb_t *receiver, word_t *receiverIPCBuffer); +void doNBWaitFailedTransfer(tcb_t *thread); void schedule(void); void chooseThread(void); void switchToThread(tcb_t *thread) VISIBLE; diff --git a/include/model/statedata.h b/include/model/statedata.h index 5ca8194da..46b995e84 100644 --- a/include/model/statedata.h +++ b/include/model/statedata.h @@ -17,6 +17,8 @@ #include extern tcb_queue_t ksReadyQueues[] VISIBLE; +extern word_t ksReadyQueuesL1Bitmap[CONFIG_NUM_DOMAINS] VISIBLE; +extern word_t ksReadyQueuesL2Bitmap[CONFIG_NUM_DOMAINS][(CONFIG_NUM_PRIORITIES / wordBits) + 1] VISIBLE; extern tcb_t *ksCurThread VISIBLE; extern tcb_t *ksIdleThread VISIBLE; extern tcb_t *ksSchedulerAction VISIBLE; diff --git a/include/object/asyncendpoint.h b/include/object/asyncendpoint.h index 0283b32be..c76b6abbb 100644 --- a/include/object/asyncendpoint.h +++ b/include/object/asyncendpoint.h @@ -15,7 +15,7 @@ #include void sendAsyncIPC(async_endpoint_t *aepptr, word_t badge); -void receiveAsyncIPC(tcb_t *thread, cap_t cap); +void receiveAsyncIPC(tcb_t *thread, cap_t cap, bool_t isBlocking); void aepCancelAll(async_endpoint_t *aepptr); void asyncIPCCancel(tcb_t *threadPtr, async_endpoint_t *aepptr); void completeAsyncIPC(async_endpoint_t *aepptr, tcb_t *tcb); diff --git a/include/object/endpoint.h b/include/object/endpoint.h index fbb9c684f..c3f423f7c 100644 --- a/include/object/endpoint.h +++ b/include/object/endpoint.h @@ -16,7 +16,7 @@ void sendIPC(bool_t blocking, bool_t do_call, word_t badge, bool_t canGrant, tcb_t *thread, endpoint_t *epptr); -void receiveIPC(tcb_t *thread, cap_t cap); +void receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking); void ipcCancel(tcb_t *tptr); void epCancelAll(endpoint_t *epptr); void epCancelBadgedSends(endpoint_t *epptr, word_t badge); diff --git a/include/plat/am335x/autoconf.h b/include/plat/am335x/autoconf.h new file mode 100644 index 000000000..27af09bc3 --- /dev/null +++ b/include/plat/am335x/autoconf.h @@ -0,0 +1,89 @@ +/* + * Automatically generated C config: don't edit + * Project Configuration + * Mon Nov 9 14:35:33 2015 + */ +#define AUTOCONF_INCLUDED +#define CONFIG_PLAT_AM335X 1 +#define CONFIG_LIB_SEL4_SIMPLE 1 +#define CONFIG_HAVE_CACHE 1 +#define CONFIG_LIB_SEL4_DEBUG 1 +#define CONFIG_LIB_ELF 1 +#define CONFIG_USER_DEBUG_BUILD 1 +#define CONFIG_HAVE_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4 1 +#define CONFIG_LIB_SEL4_VKA 1 +#define CONFIG_HAVE_CRT 1 +#define CONFIG_TIMER_TICK_MS 2 +#define CONFIG_ARM_ERRATA_764369 1 +#define CONFIG_KERNEL_CFLAGS "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT_SEL4_START 1 +#define CONFIG_HAVE_LIBC 1 +#define CONFIG_PRINT_XML 1 +#define CONFIG_USER_COMPILER "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_WORD_SIZE 32 +#define CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS 199 +#define CONFIG_APP_TESTS 1 +#define CONFIG_MAX_NUM_TRACE_POINTS 0 +#define CONFIG_SEL4UTILS_STACK_SIZE 65536 +#define CONFIG_HAVE_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_FASTPATH 1 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_OBJS_SZ 0 +#define CONFIG_HAVE_TIMER 1 +#define CONFIG_SEL4UTILS_CSPACE_SIZE_BITS 17 +#define CONFIG_DOMAIN_SCHEDULE "" +#define CONFIG_ARM_CORTEX_A8 1 +#define CONFIG_BUFFER_OUTPUT 1 +#define CONFIG_LIB_SEL4 1 +#define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1 +#define CONFIG_LIB_SEL4_UTILS 1 +#define CONFIG_RELEASE_BUILD 1 +#define CONFIG_LIB_SEL4_VSPACE 1 +#define CONFIG_LIB_PLATSUPPORT 1 +#define CONFIG_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_SEL4_TEST 1 +#define CONFIG_LIB_VKA_ALLOW_MEMORY_LEAKS 1 +#define CONFIG_LIB_ELFLOADER 1 +#define CONFIG_HAVE_LIB_SEL4_VSPACE 1 +#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 166 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0 +#define CONFIG_CROSS_COMPILER_PREFIX "arm-linux-gnueabi-" +#define CONFIG_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4_TEST 1 +#define CONFIG_LIB_MUSL_C 1 +#define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100 +#define CONFIG_ARCH_ARM_V7A 1 +#define CONFIG_USER_CFLAGS "" +#define CONFIG_HAVE_LIB_SEL4_DEBUG 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_UTILS 1 +#define CONFIG_OPTIMISATION_O2 1 +#define CONFIG_HAVE_LIB_CPIO 1 +#define CONFIG_HAVE_LIB_SEL4_VKA 1 +#define CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS 1 +#define CONFIG_HAVE_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_USER_EXTRA_CFLAGS "-D_XOPEN_SOURCE=700" +#define CONFIG_HAVE_LIB_SEL4_SIMPLE 1 +#define CONFIG_ARCH_ARM 1 +#define CONFIG_HAVE_LIB_ELF 1 +#define CONFIG_HAVE_LIB_PLATSUPPORT 1 +#define CONFIG_NUM_DOMAINS 16 +#define CONFIG_HAVE_LIB_UTILS 1 +#define CONFIG_USER_OPTIMISATION_O2 1 +#define CONFIG_LIB_CPIO 1 +#define CONFIG_RETYPE_FAN_OUT_LIMIT 256 +#define CONFIG_ROOT_CNODE_SIZE_BITS 12 +#define CONFIG_NUM_PRIORITIES 256 +#define CONFIG_TESTPRINTER_REGEX ".*" +#define CONFIG_APP_SEL4TEST 1 +#define CONFIG_HAVE_LIB_SEL4_UTILS 1 +#define CONFIG_KERNEL_COMPILER "" +#define CONFIG_TIME_SLICE 5 +#define CONFIG_KERNEL_EXTRA_CPPFLAGS "" +#define CONFIG_LIBSEL4DEBUG_ALLOC_BUFFER_ENTRIES 128 +#define CONFIG_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576 +#define CONFIG_BUILDSYS_USE_CCACHE 1 diff --git a/include/plat/apq8064/autoconf.h b/include/plat/apq8064/autoconf.h new file mode 100644 index 000000000..90c999bd7 --- /dev/null +++ b/include/plat/apq8064/autoconf.h @@ -0,0 +1,93 @@ +/* + * Automatically generated C config: don't edit + * Project Configuration + * Mon Nov 9 14:38:38 2015 + */ +#define AUTOCONF_INCLUDED +#define CONFIG_LIB_SEL4_SIMPLE 1 +#define CONFIG_HAVE_ARCH_TIMER 1 +#define CONFIG_HAVE_CACHE 1 +#define CONFIG_LIB_SEL4_DEBUG 1 +#define CONFIG_LIB_ELF 1 +#define CONFIG_USER_DEBUG_BUILD 1 +#define CONFIG_HAVE_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4 1 +#define CONFIG_LIB_SEL4_VKA 1 +#define CONFIG_HAVE_CRT 1 +#define CONFIG_EXPORT_PCNT_USER 1 +#define CONFIG_TIMER_TICK_MS 2 +#define CONFIG_ARM_ERRATA_764369 1 +#define CONFIG_KERNEL_CFLAGS "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT_SEL4_START 1 +#define CONFIG_HAVE_LIBC 1 +#define CONFIG_PRINT_XML 1 +#define CONFIG_USER_COMPILER "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_WORD_SIZE 32 +#define CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS 199 +#define CONFIG_APP_TESTS 1 +#define CONFIG_MAX_NUM_TRACE_POINTS 0 +#define CONFIG_SEL4UTILS_STACK_SIZE 65536 +#define CONFIG_HAVE_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_FASTPATH 1 +#define CONFIG_ARM_CORTEX_A15 1 +#define CONFIG_EXPORT_VCNT_USER 1 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_OBJS_SZ 0 +#define CONFIG_HAVE_TIMER 1 +#define CONFIG_SEL4UTILS_CSPACE_SIZE_BITS 17 +#define CONFIG_DOMAIN_SCHEDULE "" +#define CONFIG_BUFFER_OUTPUT 1 +#define CONFIG_ARM_ERRATA_773022 1 +#define CONFIG_LIB_SEL4 1 +#define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1 +#define CONFIG_LIB_SEL4_UTILS 1 +#define CONFIG_RELEASE_BUILD 1 +#define CONFIG_LIB_SEL4_VSPACE 1 +#define CONFIG_LIB_PLATSUPPORT 1 +#define CONFIG_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_SEL4_TEST 1 +#define CONFIG_LIB_VKA_ALLOW_MEMORY_LEAKS 1 +#define CONFIG_LIB_ELFLOADER 1 +#define CONFIG_HAVE_LIB_SEL4_VSPACE 1 +#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 166 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0 +#define CONFIG_CROSS_COMPILER_PREFIX "arm-linux-gnueabi-" +#define CONFIG_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4_TEST 1 +#define CONFIG_LIB_MUSL_C 1 +#define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100 +#define CONFIG_ARCH_ARM_V7A 1 +#define CONFIG_USER_CFLAGS "" +#define CONFIG_HAVE_LIB_SEL4_DEBUG 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_UTILS 1 +#define CONFIG_OPTIMISATION_O2 1 +#define CONFIG_HAVE_LIB_CPIO 1 +#define CONFIG_HAVE_LIB_SEL4_VKA 1 +#define CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS 1 +#define CONFIG_HAVE_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_USER_EXTRA_CFLAGS "-D_XOPEN_SOURCE=700" +#define CONFIG_PLAT_APQ8064 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE 1 +#define CONFIG_ARCH_ARM 1 +#define CONFIG_HAVE_LIB_ELF 1 +#define CONFIG_HAVE_LIB_PLATSUPPORT 1 +#define CONFIG_NUM_DOMAINS 16 +#define CONFIG_HAVE_LIB_UTILS 1 +#define CONFIG_USER_OPTIMISATION_O2 1 +#define CONFIG_LIB_CPIO 1 +#define CONFIG_RETYPE_FAN_OUT_LIMIT 256 +#define CONFIG_ROOT_CNODE_SIZE_BITS 12 +#define CONFIG_NUM_PRIORITIES 256 +#define CONFIG_TESTPRINTER_REGEX ".*" +#define CONFIG_APP_SEL4TEST 1 +#define CONFIG_HAVE_LIB_SEL4_UTILS 1 +#define CONFIG_KERNEL_COMPILER "" +#define CONFIG_TIME_SLICE 5 +#define CONFIG_KERNEL_EXTRA_CPPFLAGS "" +#define CONFIG_LIBSEL4DEBUG_ALLOC_BUFFER_ENTRIES 128 +#define CONFIG_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576 +#define CONFIG_BUILDSYS_USE_CCACHE 1 diff --git a/include/plat/exynos4/autoconf.h b/include/plat/exynos4/autoconf.h new file mode 100644 index 000000000..efdcced0e --- /dev/null +++ b/include/plat/exynos4/autoconf.h @@ -0,0 +1,89 @@ +/* + * Automatically generated C config: don't edit + * Project Configuration + * Mon Nov 9 14:36:10 2015 + */ +#define AUTOCONF_INCLUDED +#define CONFIG_LIB_SEL4_SIMPLE 1 +#define CONFIG_ARM_CORTEX_A9 1 +#define CONFIG_HAVE_CACHE 1 +#define CONFIG_LIB_SEL4_DEBUG 1 +#define CONFIG_LIB_ELF 1 +#define CONFIG_USER_DEBUG_BUILD 1 +#define CONFIG_HAVE_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4 1 +#define CONFIG_LIB_SEL4_VKA 1 +#define CONFIG_HAVE_CRT 1 +#define CONFIG_TIMER_TICK_MS 2 +#define CONFIG_ARM_ERRATA_764369 1 +#define CONFIG_KERNEL_CFLAGS "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT_SEL4_START 1 +#define CONFIG_HAVE_LIBC 1 +#define CONFIG_PRINT_XML 1 +#define CONFIG_USER_COMPILER "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_WORD_SIZE 32 +#define CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS 199 +#define CONFIG_APP_TESTS 1 +#define CONFIG_MAX_NUM_TRACE_POINTS 0 +#define CONFIG_SEL4UTILS_STACK_SIZE 65536 +#define CONFIG_HAVE_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_FASTPATH 1 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_OBJS_SZ 0 +#define CONFIG_HAVE_TIMER 1 +#define CONFIG_SEL4UTILS_CSPACE_SIZE_BITS 17 +#define CONFIG_DOMAIN_SCHEDULE "" +#define CONFIG_BUFFER_OUTPUT 1 +#define CONFIG_LIB_SEL4 1 +#define CONFIG_PLAT_EXYNOS4 1 +#define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1 +#define CONFIG_LIB_SEL4_UTILS 1 +#define CONFIG_RELEASE_BUILD 1 +#define CONFIG_LIB_SEL4_VSPACE 1 +#define CONFIG_LIB_PLATSUPPORT 1 +#define CONFIG_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_SEL4_TEST 1 +#define CONFIG_LIB_VKA_ALLOW_MEMORY_LEAKS 1 +#define CONFIG_LIB_ELFLOADER 1 +#define CONFIG_HAVE_LIB_SEL4_VSPACE 1 +#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 166 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0 +#define CONFIG_CROSS_COMPILER_PREFIX "arm-linux-gnueabi-" +#define CONFIG_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4_TEST 1 +#define CONFIG_LIB_MUSL_C 1 +#define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100 +#define CONFIG_ARCH_ARM_V7A 1 +#define CONFIG_USER_CFLAGS "" +#define CONFIG_HAVE_LIB_SEL4_DEBUG 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_UTILS 1 +#define CONFIG_OPTIMISATION_O2 1 +#define CONFIG_HAVE_LIB_CPIO 1 +#define CONFIG_HAVE_LIB_SEL4_VKA 1 +#define CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS 1 +#define CONFIG_HAVE_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_USER_EXTRA_CFLAGS "-D_XOPEN_SOURCE=700" +#define CONFIG_HAVE_LIB_SEL4_SIMPLE 1 +#define CONFIG_ARCH_ARM 1 +#define CONFIG_HAVE_LIB_ELF 1 +#define CONFIG_HAVE_LIB_PLATSUPPORT 1 +#define CONFIG_NUM_DOMAINS 16 +#define CONFIG_HAVE_LIB_UTILS 1 +#define CONFIG_USER_OPTIMISATION_O2 1 +#define CONFIG_LIB_CPIO 1 +#define CONFIG_RETYPE_FAN_OUT_LIMIT 256 +#define CONFIG_ROOT_CNODE_SIZE_BITS 12 +#define CONFIG_NUM_PRIORITIES 256 +#define CONFIG_TESTPRINTER_REGEX ".*" +#define CONFIG_APP_SEL4TEST 1 +#define CONFIG_HAVE_LIB_SEL4_UTILS 1 +#define CONFIG_KERNEL_COMPILER "" +#define CONFIG_TIME_SLICE 5 +#define CONFIG_KERNEL_EXTRA_CPPFLAGS "" +#define CONFIG_LIBSEL4DEBUG_ALLOC_BUFFER_ENTRIES 128 +#define CONFIG_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576 +#define CONFIG_BUILDSYS_USE_CCACHE 1 diff --git a/include/plat/exynos5/autoconf.h b/include/plat/exynos5/autoconf.h new file mode 100644 index 000000000..72bd9f646 --- /dev/null +++ b/include/plat/exynos5/autoconf.h @@ -0,0 +1,94 @@ +/* + * Automatically generated C config: don't edit + * Project Configuration + * Mon Nov 9 14:37:42 2015 + */ +#define AUTOCONF_INCLUDED +#define CONFIG_LIB_SEL4_SIMPLE 1 +#define CONFIG_HAVE_ARCH_TIMER 1 +#define CONFIG_HAVE_CACHE 1 +#define CONFIG_LIB_SEL4_DEBUG 1 +#define CONFIG_LIB_ELF 1 +#define CONFIG_USER_DEBUG_BUILD 1 +#define CONFIG_HAVE_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4 1 +#define CONFIG_LIB_SEL4_VKA 1 +#define CONFIG_HAVE_CRT 1 +#define CONFIG_EXPORT_PCNT_USER 1 +#define CONFIG_TIMER_TICK_MS 2 +#define CONFIG_ARM_ERRATA_764369 1 +#define CONFIG_KERNEL_CFLAGS "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT_SEL4_START 1 +#define CONFIG_PLAT_EXYNOS5410 1 +#define CONFIG_HAVE_LIBC 1 +#define CONFIG_PRINT_XML 1 +#define CONFIG_USER_COMPILER "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_WORD_SIZE 32 +#define CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS 199 +#define CONFIG_APP_TESTS 1 +#define CONFIG_MAX_NUM_TRACE_POINTS 0 +#define CONFIG_SEL4UTILS_STACK_SIZE 65536 +#define CONFIG_HAVE_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_FASTPATH 1 +#define CONFIG_ARM_CORTEX_A15 1 +#define CONFIG_EXPORT_VCNT_USER 1 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_OBJS_SZ 0 +#define CONFIG_PLAT_EXYNOS54XX 1 +#define CONFIG_HAVE_TIMER 1 +#define CONFIG_SEL4UTILS_CSPACE_SIZE_BITS 17 +#define CONFIG_DOMAIN_SCHEDULE "" +#define CONFIG_BUFFER_OUTPUT 1 +#define CONFIG_ARM_ERRATA_773022 1 +#define CONFIG_LIB_SEL4 1 +#define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1 +#define CONFIG_LIB_SEL4_UTILS 1 +#define CONFIG_RELEASE_BUILD 1 +#define CONFIG_LIB_SEL4_VSPACE 1 +#define CONFIG_LIB_PLATSUPPORT 1 +#define CONFIG_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_SEL4_TEST 1 +#define CONFIG_LIB_VKA_ALLOW_MEMORY_LEAKS 1 +#define CONFIG_LIB_ELFLOADER 1 +#define CONFIG_HAVE_LIB_SEL4_VSPACE 1 +#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 166 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0 +#define CONFIG_CROSS_COMPILER_PREFIX "arm-linux-gnueabi-" +#define CONFIG_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4_TEST 1 +#define CONFIG_LIB_MUSL_C 1 +#define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100 +#define CONFIG_ARCH_ARM_V7A 1 +#define CONFIG_USER_CFLAGS "" +#define CONFIG_HAVE_LIB_SEL4_DEBUG 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_UTILS 1 +#define CONFIG_OPTIMISATION_O2 1 +#define CONFIG_HAVE_LIB_CPIO 1 +#define CONFIG_HAVE_LIB_SEL4_VKA 1 +#define CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS 1 +#define CONFIG_HAVE_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_USER_EXTRA_CFLAGS "-D_XOPEN_SOURCE=700" +#define CONFIG_HAVE_LIB_SEL4_SIMPLE 1 +#define CONFIG_ARCH_ARM 1 +#define CONFIG_HAVE_LIB_ELF 1 +#define CONFIG_HAVE_LIB_PLATSUPPORT 1 +#define CONFIG_NUM_DOMAINS 16 +#define CONFIG_HAVE_LIB_UTILS 1 +#define CONFIG_USER_OPTIMISATION_O2 1 +#define CONFIG_LIB_CPIO 1 +#define CONFIG_RETYPE_FAN_OUT_LIMIT 256 +#define CONFIG_ROOT_CNODE_SIZE_BITS 12 +#define CONFIG_NUM_PRIORITIES 256 +#define CONFIG_TESTPRINTER_REGEX ".*" +#define CONFIG_APP_SEL4TEST 1 +#define CONFIG_HAVE_LIB_SEL4_UTILS 1 +#define CONFIG_KERNEL_COMPILER "" +#define CONFIG_TIME_SLICE 5 +#define CONFIG_KERNEL_EXTRA_CPPFLAGS "" +#define CONFIG_LIBSEL4DEBUG_ALLOC_BUFFER_ENTRIES 128 +#define CONFIG_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576 +#define CONFIG_BUILDSYS_USE_CCACHE 1 diff --git a/include/plat/imx31/autoconf.h b/include/plat/imx31/autoconf.h new file mode 100644 index 000000000..10785b757 --- /dev/null +++ b/include/plat/imx31/autoconf.h @@ -0,0 +1,89 @@ +/* + * Automatically generated C config: don't edit + * Project Configuration + * Mon Nov 9 14:32:34 2015 + */ +#define AUTOCONF_INCLUDED +#define CONFIG_LIB_SEL4_SIMPLE 1 +#define CONFIG_HAVE_CACHE 1 +#define CONFIG_PLAT_KZM 1 +#define CONFIG_LIB_SEL4_DEBUG 1 +#define CONFIG_LIB_ELF 1 +#define CONFIG_USER_DEBUG_BUILD 1 +#define CONFIG_HAVE_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4 1 +#define CONFIG_LIB_SEL4_VKA 1 +#define CONFIG_HAVE_CRT 1 +#define CONFIG_TIMER_TICK_MS 2 +#define CONFIG_ARM_ERRATA_764369 1 +#define CONFIG_KERNEL_CFLAGS "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT_SEL4_START 1 +#define CONFIG_HAVE_LIBC 1 +#define CONFIG_PRINT_XML 1 +#define CONFIG_USER_COMPILER "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_WORD_SIZE 32 +#define CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS 199 +#define CONFIG_APP_TESTS 1 +#define CONFIG_MAX_NUM_TRACE_POINTS 0 +#define CONFIG_SEL4UTILS_STACK_SIZE 65536 +#define CONFIG_HAVE_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_FASTPATH 1 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_OBJS_SZ 0 +#define CONFIG_HAVE_TIMER 1 +#define CONFIG_SEL4UTILS_CSPACE_SIZE_BITS 17 +#define CONFIG_DOMAIN_SCHEDULE "" +#define CONFIG_BUFFER_OUTPUT 1 +#define CONFIG_LIB_SEL4 1 +#define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1 +#define CONFIG_LIB_SEL4_UTILS 1 +#define CONFIG_RELEASE_BUILD 1 +#define CONFIG_LIB_SEL4_VSPACE 1 +#define CONFIG_LIB_PLATSUPPORT 1 +#define CONFIG_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_SEL4_TEST 1 +#define CONFIG_LIB_VKA_ALLOW_MEMORY_LEAKS 1 +#define CONFIG_LIB_ELFLOADER 1 +#define CONFIG_HAVE_LIB_SEL4_VSPACE 1 +#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 166 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0 +#define CONFIG_CROSS_COMPILER_PREFIX "arm-linux-gnueabi-" +#define CONFIG_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4_TEST 1 +#define CONFIG_LIB_MUSL_C 1 +#define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100 +#define CONFIG_USER_CFLAGS "" +#define CONFIG_HAVE_LIB_SEL4_DEBUG 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_UTILS 1 +#define CONFIG_OPTIMISATION_O2 1 +#define CONFIG_HAVE_LIB_CPIO 1 +#define CONFIG_HAVE_LIB_SEL4_VKA 1 +#define CONFIG_ARCH_ARM_V6 1 +#define CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS 1 +#define CONFIG_HAVE_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_USER_EXTRA_CFLAGS "-D_XOPEN_SOURCE=700" +#define CONFIG_HAVE_LIB_SEL4_SIMPLE 1 +#define CONFIG_ARCH_ARM 1 +#define CONFIG_HAVE_LIB_ELF 1 +#define CONFIG_HAVE_LIB_PLATSUPPORT 1 +#define CONFIG_NUM_DOMAINS 16 +#define CONFIG_HAVE_LIB_UTILS 1 +#define CONFIG_USER_OPTIMISATION_O2 1 +#define CONFIG_LIB_CPIO 1 +#define CONFIG_RETYPE_FAN_OUT_LIMIT 256 +#define CONFIG_ROOT_CNODE_SIZE_BITS 12 +#define CONFIG_NUM_PRIORITIES 256 +#define CONFIG_TESTPRINTER_REGEX ".*" +#define CONFIG_APP_SEL4TEST 1 +#define CONFIG_ARM1136JF_S 1 +#define CONFIG_HAVE_LIB_SEL4_UTILS 1 +#define CONFIG_KERNEL_COMPILER "" +#define CONFIG_TIME_SLICE 5 +#define CONFIG_KERNEL_EXTRA_CPPFLAGS "" +#define CONFIG_LIBSEL4DEBUG_ALLOC_BUFFER_ENTRIES 128 +#define CONFIG_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576 +#define CONFIG_BUILDSYS_USE_CCACHE 1 diff --git a/include/plat/imx6/autoconf.h b/include/plat/imx6/autoconf.h new file mode 100644 index 000000000..fad1dd1a8 --- /dev/null +++ b/include/plat/imx6/autoconf.h @@ -0,0 +1,89 @@ +/* + * Automatically generated C config: don't edit + * Project Configuration + * Mon Nov 9 14:36:38 2015 + */ +#define AUTOCONF_INCLUDED +#define CONFIG_LIB_SEL4_SIMPLE 1 +#define CONFIG_ARM_CORTEX_A9 1 +#define CONFIG_HAVE_CACHE 1 +#define CONFIG_LIB_SEL4_DEBUG 1 +#define CONFIG_LIB_ELF 1 +#define CONFIG_USER_DEBUG_BUILD 1 +#define CONFIG_HAVE_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4 1 +#define CONFIG_LIB_SEL4_VKA 1 +#define CONFIG_HAVE_CRT 1 +#define CONFIG_TIMER_TICK_MS 2 +#define CONFIG_ARM_ERRATA_764369 1 +#define CONFIG_KERNEL_CFLAGS "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT_SEL4_START 1 +#define CONFIG_HAVE_LIBC 1 +#define CONFIG_PRINT_XML 1 +#define CONFIG_USER_COMPILER "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_WORD_SIZE 32 +#define CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS 199 +#define CONFIG_APP_TESTS 1 +#define CONFIG_MAX_NUM_TRACE_POINTS 0 +#define CONFIG_SEL4UTILS_STACK_SIZE 65536 +#define CONFIG_HAVE_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_FASTPATH 1 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_OBJS_SZ 0 +#define CONFIG_HAVE_TIMER 1 +#define CONFIG_SEL4UTILS_CSPACE_SIZE_BITS 17 +#define CONFIG_DOMAIN_SCHEDULE "" +#define CONFIG_BUFFER_OUTPUT 1 +#define CONFIG_LIB_SEL4 1 +#define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1 +#define CONFIG_LIB_SEL4_UTILS 1 +#define CONFIG_RELEASE_BUILD 1 +#define CONFIG_LIB_SEL4_VSPACE 1 +#define CONFIG_LIB_PLATSUPPORT 1 +#define CONFIG_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_SEL4_TEST 1 +#define CONFIG_LIB_VKA_ALLOW_MEMORY_LEAKS 1 +#define CONFIG_LIB_ELFLOADER 1 +#define CONFIG_HAVE_LIB_SEL4_VSPACE 1 +#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 166 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0 +#define CONFIG_CROSS_COMPILER_PREFIX "arm-linux-gnueabi-" +#define CONFIG_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4_TEST 1 +#define CONFIG_LIB_MUSL_C 1 +#define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100 +#define CONFIG_ARCH_ARM_V7A 1 +#define CONFIG_USER_CFLAGS "" +#define CONFIG_HAVE_LIB_SEL4_DEBUG 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_UTILS 1 +#define CONFIG_OPTIMISATION_O2 1 +#define CONFIG_HAVE_LIB_CPIO 1 +#define CONFIG_PLAT_IMX6 1 +#define CONFIG_HAVE_LIB_SEL4_VKA 1 +#define CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS 1 +#define CONFIG_HAVE_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_USER_EXTRA_CFLAGS "-D_XOPEN_SOURCE=700" +#define CONFIG_HAVE_LIB_SEL4_SIMPLE 1 +#define CONFIG_ARCH_ARM 1 +#define CONFIG_HAVE_LIB_ELF 1 +#define CONFIG_HAVE_LIB_PLATSUPPORT 1 +#define CONFIG_NUM_DOMAINS 16 +#define CONFIG_HAVE_LIB_UTILS 1 +#define CONFIG_USER_OPTIMISATION_O2 1 +#define CONFIG_LIB_CPIO 1 +#define CONFIG_RETYPE_FAN_OUT_LIMIT 256 +#define CONFIG_ROOT_CNODE_SIZE_BITS 12 +#define CONFIG_NUM_PRIORITIES 256 +#define CONFIG_TESTPRINTER_REGEX ".*" +#define CONFIG_APP_SEL4TEST 1 +#define CONFIG_HAVE_LIB_SEL4_UTILS 1 +#define CONFIG_KERNEL_COMPILER "" +#define CONFIG_TIME_SLICE 5 +#define CONFIG_KERNEL_EXTRA_CPPFLAGS "" +#define CONFIG_LIBSEL4DEBUG_ALLOC_BUFFER_ENTRIES 128 +#define CONFIG_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576 +#define CONFIG_BUILDSYS_USE_CCACHE 1 diff --git a/include/plat/omap3/autoconf.h b/include/plat/omap3/autoconf.h new file mode 100644 index 000000000..ca24d4a1f --- /dev/null +++ b/include/plat/omap3/autoconf.h @@ -0,0 +1,89 @@ +/* + * Automatically generated C config: don't edit + * Project Configuration + * Mon Nov 9 14:34:57 2015 + */ +#define AUTOCONF_INCLUDED +#define CONFIG_LIB_SEL4_SIMPLE 1 +#define CONFIG_HAVE_CACHE 1 +#define CONFIG_LIB_SEL4_DEBUG 1 +#define CONFIG_LIB_ELF 1 +#define CONFIG_USER_DEBUG_BUILD 1 +#define CONFIG_HAVE_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4 1 +#define CONFIG_LIB_SEL4_VKA 1 +#define CONFIG_HAVE_CRT 1 +#define CONFIG_TIMER_TICK_MS 2 +#define CONFIG_ARM_ERRATA_764369 1 +#define CONFIG_KERNEL_CFLAGS "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT_SEL4_START 1 +#define CONFIG_HAVE_LIBC 1 +#define CONFIG_PRINT_XML 1 +#define CONFIG_USER_COMPILER "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_WORD_SIZE 32 +#define CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS 199 +#define CONFIG_APP_TESTS 1 +#define CONFIG_MAX_NUM_TRACE_POINTS 0 +#define CONFIG_SEL4UTILS_STACK_SIZE 65536 +#define CONFIG_HAVE_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_FASTPATH 1 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_OBJS_SZ 0 +#define CONFIG_HAVE_TIMER 1 +#define CONFIG_SEL4UTILS_CSPACE_SIZE_BITS 17 +#define CONFIG_DOMAIN_SCHEDULE "" +#define CONFIG_ARM_CORTEX_A8 1 +#define CONFIG_BUFFER_OUTPUT 1 +#define CONFIG_LIB_SEL4 1 +#define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1 +#define CONFIG_LIB_SEL4_UTILS 1 +#define CONFIG_RELEASE_BUILD 1 +#define CONFIG_LIB_SEL4_VSPACE 1 +#define CONFIG_LIB_PLATSUPPORT 1 +#define CONFIG_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_SEL4_TEST 1 +#define CONFIG_LIB_VKA_ALLOW_MEMORY_LEAKS 1 +#define CONFIG_LIB_ELFLOADER 1 +#define CONFIG_HAVE_LIB_SEL4_VSPACE 1 +#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 166 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0 +#define CONFIG_CROSS_COMPILER_PREFIX "arm-linux-gnueabi-" +#define CONFIG_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4_TEST 1 +#define CONFIG_LIB_MUSL_C 1 +#define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100 +#define CONFIG_ARCH_ARM_V7A 1 +#define CONFIG_USER_CFLAGS "" +#define CONFIG_HAVE_LIB_SEL4_DEBUG 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_UTILS 1 +#define CONFIG_OPTIMISATION_O2 1 +#define CONFIG_HAVE_LIB_CPIO 1 +#define CONFIG_HAVE_LIB_SEL4_VKA 1 +#define CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS 1 +#define CONFIG_HAVE_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_USER_EXTRA_CFLAGS "-D_XOPEN_SOURCE=700" +#define CONFIG_HAVE_LIB_SEL4_SIMPLE 1 +#define CONFIG_ARCH_ARM 1 +#define CONFIG_HAVE_LIB_ELF 1 +#define CONFIG_HAVE_LIB_PLATSUPPORT 1 +#define CONFIG_NUM_DOMAINS 16 +#define CONFIG_HAVE_LIB_UTILS 1 +#define CONFIG_USER_OPTIMISATION_O2 1 +#define CONFIG_LIB_CPIO 1 +#define CONFIG_RETYPE_FAN_OUT_LIMIT 256 +#define CONFIG_ROOT_CNODE_SIZE_BITS 12 +#define CONFIG_NUM_PRIORITIES 256 +#define CONFIG_TESTPRINTER_REGEX ".*" +#define CONFIG_APP_SEL4TEST 1 +#define CONFIG_HAVE_LIB_SEL4_UTILS 1 +#define CONFIG_KERNEL_COMPILER "" +#define CONFIG_TIME_SLICE 5 +#define CONFIG_KERNEL_EXTRA_CPPFLAGS "" +#define CONFIG_LIBSEL4DEBUG_ALLOC_BUFFER_ENTRIES 128 +#define CONFIG_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_PLAT_OMAP3 1 +#define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576 +#define CONFIG_BUILDSYS_USE_CCACHE 1 diff --git a/include/plat/pc99/autoconf.h b/include/plat/pc99/autoconf.h new file mode 100644 index 000000000..1efaf3ecb --- /dev/null +++ b/include/plat/pc99/autoconf.h @@ -0,0 +1,92 @@ +/* + * Automatically generated C config: don't edit + * Project Configuration + * Mon Nov 9 14:40:47 2015 + */ +#define AUTOCONF_INCLUDED +#define CONFIG_LIB_SEL4_SIMPLE 1 +#define CONFIG_HAVE_CACHE 1 +#define CONFIG_LIB_SEL4_DEBUG 1 +#define CONFIG_LIB_ELF 1 +#define CONFIG_USER_DEBUG_BUILD 1 +#define CONFIG_HAVE_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4 1 +#define CONFIG_LIB_SEL4_VKA 1 +#define CONFIG_HAVE_CRT 1 +#define CONFIG_TIMER_TICK_MS 2 +#define CONFIG_IRQ_IOAPIC 1 +#define CONFIG_KERNEL_CFLAGS "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT_SEL4_START 1 +#define CONFIG_LIB_PLAT_SUPPORT_SERIAL_PORT_X86_COM1 1 +#define CONFIG_HAVE_LIBC 1 +#define CONFIG_PRINT_XML 1 +#define CONFIG_USER_COMPILER "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_WORD_SIZE 32 +#define CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS 199 +#define CONFIG_ARCH_X86 1 +#define CONFIG_APP_TESTS 1 +#define CONFIG_MAX_NUM_TRACE_POINTS 0 +#define CONFIG_MAX_NUM_IOAPIC 1 +#define CONFIG_SEL4UTILS_STACK_SIZE 65536 +#define CONFIG_HAVE_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_FASTPATH 1 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_OBJS_SZ 0 +#define CONFIG_HAVE_TIMER 1 +#define CONFIG_SEL4UTILS_CSPACE_SIZE_BITS 17 +#define CONFIG_DOMAIN_SCHEDULE "" +#define CONFIG_BUFFER_OUTPUT 1 +#define CONFIG_LIB_SEL4 1 +#define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1 +#define CONFIG_LIB_SEL4_UTILS 1 +#define CONFIG_RELEASE_BUILD 1 +#define CONFIG_LIB_SEL4_VSPACE 1 +#define CONFIG_LIB_PLATSUPPORT 1 +#define CONFIG_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_SEL4_TEST 1 +#define CONFIG_LIB_VKA_ALLOW_MEMORY_LEAKS 1 +#define CONFIG_HAVE_LIB_SEL4_VSPACE 1 +#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 166 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0 +#define CONFIG_PCI 1 +#define CONFIG_MAX_NUM_NODES 1 +#define CONFIG_CROSS_COMPILER_PREFIX "" +#define CONFIG_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4_TEST 1 +#define CONFIG_IOMMU 1 +#define CONFIG_LIB_MUSL_C 1 +#define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100 +#define CONFIG_USER_CFLAGS "" +#define CONFIG_HAVE_LIB_SEL4_DEBUG 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_UTILS 1 +#define CONFIG_OPTIMISATION_O2 1 +#define CONFIG_HAVE_LIB_CPIO 1 +#define CONFIG_HAVE_LIB_SEL4_VKA 1 +#define CONFIG_HAVE_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_USER_EXTRA_CFLAGS "-D_XOPEN_SOURCE=700" +#define CONFIG_HAVE_LIB_SEL4_SIMPLE 1 +#define CONFIG_HAVE_LIB_ELF 1 +#define CONFIG_HAVE_LIB_PLATSUPPORT 1 +#define CONFIG_NUM_DOMAINS 16 +#define CONFIG_ARCH_IA32 1 +#define CONFIG_HAVE_LIB_UTILS 1 +#define CONFIG_USER_OPTIMISATION_O2 1 +#define CONFIG_LIB_CPIO 1 +#define CONFIG_RETYPE_FAN_OUT_LIMIT 256 +#define CONFIG_ROOT_CNODE_SIZE_BITS 12 +#define CONFIG_NUM_PRIORITIES 256 +#define CONFIG_TESTPRINTER_REGEX ".*" +#define CONFIG_APP_SEL4TEST 1 +#define CONFIG_PLAT_PC99 1 +#define CONFIG_HAVE_LIB_SEL4_UTILS 1 +#define CONFIG_KERNEL_COMPILER "" +#define CONFIG_TIME_SLICE 5 +#define CONFIG_KERNEL_EXTRA_CPPFLAGS "" +#define CONFIG_LIBSEL4DEBUG_ALLOC_BUFFER_ENTRIES 128 +#define CONFIG_MAX_NUM_PASSTHROUGH_DEVICES 20 +#define CONFIG_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576 +#define CONFIG_BUILDSYS_USE_CCACHE 1 diff --git a/include/plat/zynq7000/autoconf.h b/include/plat/zynq7000/autoconf.h new file mode 100644 index 000000000..80a3a09a2 --- /dev/null +++ b/include/plat/zynq7000/autoconf.h @@ -0,0 +1,89 @@ +/* + * Automatically generated C config: don't edit + * Project Configuration + * Mon Nov 9 14:37:01 2015 + */ +#define AUTOCONF_INCLUDED +#define CONFIG_LIB_SEL4_SIMPLE 1 +#define CONFIG_ARM_CORTEX_A9 1 +#define CONFIG_HAVE_CACHE 1 +#define CONFIG_LIB_SEL4_DEBUG 1 +#define CONFIG_LIB_ELF 1 +#define CONFIG_USER_DEBUG_BUILD 1 +#define CONFIG_HAVE_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4 1 +#define CONFIG_LIB_SEL4_VKA 1 +#define CONFIG_HAVE_CRT 1 +#define CONFIG_TIMER_TICK_MS 2 +#define CONFIG_ARM_ERRATA_764369 1 +#define CONFIG_KERNEL_CFLAGS "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT_SEL4_START 1 +#define CONFIG_HAVE_LIBC 1 +#define CONFIG_PRINT_XML 1 +#define CONFIG_USER_COMPILER "" +#define CONFIG_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_WORD_SIZE 32 +#define CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS 199 +#define CONFIG_APP_TESTS 1 +#define CONFIG_MAX_NUM_TRACE_POINTS 0 +#define CONFIG_SEL4UTILS_STACK_SIZE 65536 +#define CONFIG_HAVE_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_FASTPATH 1 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_OBJS_SZ 0 +#define CONFIG_PLAT_ZYNQ7000 1 +#define CONFIG_HAVE_TIMER 1 +#define CONFIG_SEL4UTILS_CSPACE_SIZE_BITS 17 +#define CONFIG_DOMAIN_SCHEDULE "" +#define CONFIG_BUFFER_OUTPUT 1 +#define CONFIG_LIB_SEL4 1 +#define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1 +#define CONFIG_LIB_SEL4_UTILS 1 +#define CONFIG_RELEASE_BUILD 1 +#define CONFIG_LIB_SEL4_VSPACE 1 +#define CONFIG_LIB_PLATSUPPORT 1 +#define CONFIG_LIB_SEL4_ALLOCMAN 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_SEL4_TEST 1 +#define CONFIG_LIB_VKA_ALLOW_MEMORY_LEAKS 1 +#define CONFIG_LIB_ELFLOADER 1 +#define CONFIG_HAVE_LIB_SEL4_VSPACE 1 +#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 166 +#define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0 +#define CONFIG_CROSS_COMPILER_PREFIX "arm-linux-gnueabi-" +#define CONFIG_LIB_SEL4_MUSLC_SYS 1 +#define CONFIG_HAVE_LIB_SEL4_TEST 1 +#define CONFIG_LIB_MUSL_C 1 +#define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100 +#define CONFIG_ARCH_ARM_V7A 1 +#define CONFIG_USER_CFLAGS "" +#define CONFIG_HAVE_LIB_SEL4_DEBUG 1 +#define CONFIG_HAVE_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_SIMPLE_DEFAULT 1 +#define CONFIG_LIB_UTILS 1 +#define CONFIG_OPTIMISATION_O2 1 +#define CONFIG_HAVE_LIB_CPIO 1 +#define CONFIG_HAVE_LIB_SEL4_VKA 1 +#define CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS 1 +#define CONFIG_HAVE_LIB_SEL4_PLAT_SUPPORT 1 +#define CONFIG_USER_EXTRA_CFLAGS "-D_XOPEN_SOURCE=700" +#define CONFIG_HAVE_LIB_SEL4_SIMPLE 1 +#define CONFIG_ARCH_ARM 1 +#define CONFIG_HAVE_LIB_ELF 1 +#define CONFIG_HAVE_LIB_PLATSUPPORT 1 +#define CONFIG_NUM_DOMAINS 16 +#define CONFIG_HAVE_LIB_UTILS 1 +#define CONFIG_USER_OPTIMISATION_O2 1 +#define CONFIG_LIB_CPIO 1 +#define CONFIG_RETYPE_FAN_OUT_LIMIT 256 +#define CONFIG_ROOT_CNODE_SIZE_BITS 12 +#define CONFIG_NUM_PRIORITIES 256 +#define CONFIG_TESTPRINTER_REGEX ".*" +#define CONFIG_APP_SEL4TEST 1 +#define CONFIG_HAVE_LIB_SEL4_UTILS 1 +#define CONFIG_KERNEL_COMPILER "" +#define CONFIG_TIME_SLICE 5 +#define CONFIG_KERNEL_EXTRA_CPPFLAGS "" +#define CONFIG_LIBSEL4DEBUG_ALLOC_BUFFER_ENTRIES 128 +#define CONFIG_LIB_SEL4_SIMPLE_STABLE 1 +#define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576 +#define CONFIG_BUILDSYS_USE_CCACHE 1 diff --git a/include/util.h b/include/util.h index 6e6328868..3bb719073 100644 --- a/include/util.h +++ b/include/util.h @@ -15,8 +15,6 @@ #define IS_ALIGNED(n, b) (!((n) & MASK(b))) #define ROUND_DOWN(n, b) (((n) >> (b)) << (b)) #define ROUND_UP(n, b) (((((n) - 1ul) >> (b)) + 1ul) << (b)) -#define CTZ(x) __builtin_ctz(x) -#define CLZ(x) __builtin_clz(x) #define ARRAY_SIZE(x) (sizeof(x) / sizeof(x[0])) #ifndef __ASSEMBLER__ @@ -74,4 +72,21 @@ int PURE str_to_int(const char* str); #endif /* !__ASSEMBLER__ */ +/** MODIFIES: */ +/** DONT_TRANSLATE */ +/** FNSPEC clz_spec: + "\s. \ \ + {\. s = \ \ x_' s \ 0 } + \ret__int :== PROC clz(\x) + \ \ret__int = of_nat (word_clz (x_' s)) \" +*/ +static inline int +CONST clz(unsigned int x) +{ + return __builtin_clz(x); +} + +#define CTZ(x) __builtin_ctz(x) +#define CLZ(x) clz(x) + #endif /* __UTIL_H */ diff --git a/libsel4/Kconfig b/libsel4/Kconfig index 639b104a1..ecfbc6380 100644 --- a/libsel4/Kconfig +++ b/libsel4/Kconfig @@ -8,13 +8,27 @@ # @TAG(NICTA_BSD) # -menuconfig LIB_SEL4 - bool "libsel4" - default y - select HAVE_LIB_SEL4 - help - seL4 API library +menu "libsel4" + config LIB_SEL4 + bool "libsel4" + default y + select HAVE_LIB_SEL4 + help + seL4 API library +config LIB_SEL4_HAVE_REGISTER_STUBS + bool "Support syscall stubs without IPC buffer" + depends on LIB_SEL4 && !USER_OPTIMISATION_O0 && ARCH_ARM + default y + help + Generate the 'WithMRs' variants of the syscall stubs. These stubs + avoid the use of the IPC buffer where possible and attempt to + place syscall arguments directly into and out of cpu registers. + GCC's register allocation is a hint only and cannot be relied upon, + as a result these stubs are known to be broken, and are disabled, + at -O0 + +if LIB_SEL4_HAVE_REGISTER_STUBS || !(ARCH_ARM) config LIB_SEL4_STUBS_USE_IPC_BUFFER_ONLY bool "use only IPC buffer for syscalls" depends on LIB_SEL4 @@ -24,6 +38,18 @@ config LIB_SEL4_STUBS_USE_IPC_BUFFER_ONLY marshalling and unmarshalling arguments. Without this option set, arguments will be passed in registers where possible for better performance. +endif + +if !(LIB_SEL4_HAVE_REGISTER_STUBS || !(ARCH_ARM)) +menu "libsel4 hidden" + visible if false + config LIB_SEL4_STUBS_USE_IPC_BUFFER_ONLY + bool "Use only IPC buffer for syscalls" + depends on LIB_SEL4 + default y +endmenu +endif config HAVE_LIB_SEL4 bool +endmenu diff --git a/libsel4/arch_include/arm/sel4/arch/syscalls.h b/libsel4/arch_include/arm/sel4/arch/syscalls.h index 5b25f03cd..b16b66d66 100644 --- a/libsel4/arch_include/arm/sel4/arch/syscalls.h +++ b/libsel4/arch_include/arm/sel4/arch/syscalls.h @@ -17,15 +17,6 @@ #define __SWINUM(x) ((x) & 0x00ffffff) -#ifndef __OPTIMIZE__ -/* With no optimisations (-O0) GCC's register allocator clobbers the - * syscall arguments before you reach the 'swi' and you invoke the kernel - * incorrectly. - * See SELFOUR-187 - */ -#warning you are compiling with -O0; syscall WithMRs variants will not work -#endif - static inline void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) { @@ -47,6 +38,7 @@ seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) : "memory"); } +#ifdef CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS static inline void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) @@ -81,6 +73,7 @@ seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, : [swi_num] "i" __SWINUM(seL4_SysSend), "r"(scno) : "memory"); } +#endif static inline void seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) @@ -103,6 +96,7 @@ seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) : "memory"); } +#ifdef CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS static inline void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) @@ -137,6 +131,7 @@ seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, : [swi_num] "i" __SWINUM(seL4_SysNBSend), "r"(scno) : "memory"); } +#endif static inline void seL4_Reply(seL4_MessageInfo_t msgInfo) @@ -158,6 +153,7 @@ seL4_Reply(seL4_MessageInfo_t msgInfo) : "memory"); } +#ifdef CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS static inline void seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) @@ -191,6 +187,7 @@ seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo, : [swi_num] "i" __SWINUM(seL4_SysReply), "r"(scno) : "memory"); } +#endif static inline void seL4_Signal(seL4_CPtr dest) @@ -247,6 +244,7 @@ seL4_Wait(seL4_CPtr src, seL4_Word* sender) }; } +#ifdef CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS static inline seL4_MessageInfo_t seL4_WaitWithMRs(seL4_CPtr src, seL4_Word* sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) @@ -290,6 +288,42 @@ seL4_WaitWithMRs(seL4_CPtr src, seL4_Word* sender, .words = {info.words[0]} }; } +#endif + +static inline seL4_MessageInfo_t +seL4_NBWait(seL4_CPtr src, seL4_Word* sender) +{ + register seL4_Word src_and_badge asm("r0") = (seL4_Word)src; + register seL4_MessageInfo_t info asm("r1"); + + /* Incoming message registers. */ + register seL4_Word msg0 asm("r2"); + register seL4_Word msg1 asm("r3"); + register seL4_Word msg2 asm("r4"); + register seL4_Word msg3 asm("r5"); + + /* Perform the system call. */ + register seL4_Word scno asm("r7") = seL4_SysNBWait; + asm volatile ("swi %[swi_num]" + : "=r" (msg0), "=r" (msg1), "=r" (msg2), "=r" (msg3), + "=r" (info), "+r" (src_and_badge) + : [swi_num] "i" __SWINUM(seL4_SysNBWait), "r"(scno) + : "memory"); + + /* Write the message back out to memory. */ + seL4_SetMR(0, msg0); + seL4_SetMR(1, msg1); + seL4_SetMR(2, msg2); + seL4_SetMR(3, msg3); + + /* Return back sender and message information. */ + if (sender) { + *sender = src_and_badge; + } + return (seL4_MessageInfo_t) { + .words = { info.words[0]} + }; +} static inline seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) @@ -322,6 +356,7 @@ seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) }; } +#ifdef CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS static inline seL4_MessageInfo_t seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) @@ -374,6 +409,7 @@ seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, .words = {info.words[0]} }; } +#endif static inline seL4_MessageInfo_t seL4_ReplyWait(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender) @@ -410,6 +446,7 @@ seL4_ReplyWait(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender) }; } +#ifdef CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS static inline seL4_MessageInfo_t seL4_ReplyWaitWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) @@ -466,6 +503,7 @@ seL4_ReplyWaitWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *send .words = {info.words[0]} }; } +#endif static inline void seL4_Yield(void) diff --git a/libsel4/arch_include/x86/sel4/arch/syscalls.h b/libsel4/arch_include/x86/sel4/arch/syscalls.h index adb9123a8..9e408d8c2 100644 --- a/libsel4/arch_include/x86/sel4/arch/syscalls.h +++ b/libsel4/arch_include/x86/sel4/arch/syscalls.h @@ -243,6 +243,42 @@ seL4_WaitWithMRs(seL4_CPtr src, seL4_Word* sender, return info; } +static inline seL4_MessageInfo_t +seL4_NBWait(seL4_CPtr src, seL4_Word* sender) +{ + seL4_MessageInfo_t info; + seL4_Word badge; + seL4_Word mr0; + seL4_Word mr1; + + asm volatile ( + "pushl %%ebp \n" + "movl %%esp, %%ecx \n" + "leal 1f, %%edx \n" + "1: \n" + "sysenter \n" + "movl %%ebp, %%ecx \n" + "popl %%ebp \n" + : + "=b" (badge), + "=S" (info.words[0]), + "=D" (mr0), + "=c" (mr1) + : "a" (seL4_SysNBWait), + "b" (src) + : "%edx", "memory" + ); + + seL4_SetMR(0, mr0); + seL4_SetMR(1, mr1); + + if (sender) { + *sender = badge; + } + + return info; +} + static inline seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) { diff --git a/libsel4/include/api/syscall.xml b/libsel4/include/api/syscall.xml index aab20db6a..7cacabea4 100644 --- a/libsel4/include/api/syscall.xml +++ b/libsel4/include/api/syscall.xml @@ -20,6 +20,7 @@ + diff --git a/manual/parts/api.tex b/manual/parts/api.tex index 2db4332ee..35820c7d0 100644 --- a/manual/parts/api.tex +++ b/manual/parts/api.tex @@ -245,6 +245,7 @@ complete the \apifunc{seL4\_Untyped\_Retype}{untyped_retype} request. \inputapidoc{sel4_reply} \inputapidoc{sel4_nbsend} \inputapidoc{sel4_replywait} +\inputapidoc{sel4_nbwait} \inputapidoc{sel4_yield} \inputapidoc{sel4_signal} \clearpage diff --git a/manual/parts/api/sel4_nbwait.tex b/manual/parts/api/sel4_nbwait.tex new file mode 100644 index 000000000..17f018834 --- /dev/null +++ b/manual/parts/api/sel4_nbwait.tex @@ -0,0 +1,21 @@ +% +% Copyright 2014, General Dynamics C4 Systems +% +% This software may be distributed and modified according to the terms of +% the GNU General Public License version 2. Note that NO WARRANTY is provided. +% See "LICENSE_GPLv2.txt" for details. +% +% @TAG(GD_GPL) +% + +\apidoc +{sel4_nbwait} +{NBWait} +{Perform a non-blocking wait on an endpoint or notification object} +{static inline seL4\_MessageInfo\_t seL4\_NBWait} +{ +\param{seL4\_CPtr}{src}{\invokedcapdesc} +\param{seL4\_Word*}{sender}{\senderdesc} +} +{\messageinforetdesc} +{See \autoref{sec:sys_nbwait}} diff --git a/manual/parts/ipc.tex b/manual/parts/ipc.tex index 9f3adfaf5..59bd12bf0 100644 --- a/manual/parts/ipc.tex +++ b/manual/parts/ipc.tex @@ -256,3 +256,4 @@ transferred and the \texttt{extraCaps} field in the receiver's IPC buffer is set to the number of capabilities transferred up to failure. No error message will be returned to the receiving thread in any of the above cases. + diff --git a/manual/parts/objects.tex b/manual/parts/objects.tex index 4a429ab0d..862e70ccb 100644 --- a/manual/parts/objects.tex +++ b/manual/parts/objects.tex @@ -99,6 +99,7 @@ capabilities through the system is controlled by a \label{sec:sys_reply} \label{sec:sys_nbsend} \label{sec:sys_replywait} +\label{sec:sys_nbwait} \label{sec:sys_yield} The seL4 kernel provides a message-passing service for communication between @@ -197,6 +198,12 @@ The complete set of system calls is: a single kernel system call instead of two. The transition from the reply to the wait phase is also atomic. + \item[\apifunc{seL4\_NBWait}{sel4_nbwait}] is used by a thread to check for + messages waiting to be sent through an notification without blocking on + that notification. This system call works only on notification object + capabilities, raising a fault (see section \ref{sec:faults}) when attempted + with other capability types. + \item[\apifunc{seL4\_Yield}{sel4_yield}] is the only system call that does not require a capability to be used. It forfeits the remainder of the calling thread's timeslice and causes invocation of the kernel's scheduler. diff --git a/src/api/syscall.c b/src/api/syscall.c index 97d372c9a..03d38d44a 100644 --- a/src/api/syscall.c +++ b/src/api/syscall.c @@ -309,7 +309,7 @@ handleReply(void) } static void -handleWait(void) +handleWait(bool_t isBlocking) { word_t epCPtr; lookupCap_ret_t lu_ret; @@ -326,7 +326,6 @@ handleWait(void) switch (cap_get_capType(lu_ret.cap)) { case cap_endpoint_cap: - if (unlikely(!cap_endpoint_cap_get_capCanReceive(lu_ret.cap))) { current_lookup_fault = lookup_fault_missing_capability_new(0); current_fault = fault_cap_fault_new(epCPtr, true); @@ -335,7 +334,7 @@ handleWait(void) } deleteCallerCap(ksCurThread); - receiveIPC(ksCurThread, lu_ret.cap); + receiveIPC(ksCurThread, lu_ret.cap, isBlocking); break; case cap_async_endpoint_cap: { @@ -351,7 +350,7 @@ handleWait(void) break; } - receiveAsyncIPC(ksCurThread, lu_ret.cap); + receiveAsyncIPC(ksCurThread, lu_ret.cap, isBlocking); break; } default: @@ -408,7 +407,7 @@ handleSyscall(syscall_t syscall) break; case SysWait: - handleWait(); + handleWait(true); break; case SysReply: @@ -417,7 +416,11 @@ handleSyscall(syscall_t syscall) case SysReplyWait: handleReply(); - handleWait(); + handleWait(true); + break; + + case SysNBWait: + handleWait(false); break; case SysYield: diff --git a/src/arch/arm/machine/errata.c b/src/arch/arm/machine/errata.c index 8006ac051..94fcf2950 100644 --- a/src/arch/arm/machine/errata.c +++ b/src/arch/arm/machine/errata.c @@ -73,7 +73,6 @@ BOOT_CODE void __attribute__((externally_visible)) arm_errata(void) errata_arm1136(); #endif #ifdef CONFIG_ARM_ERRATA_773022 - (void)errata_armA15_773022; errata_armA15_773022(); #endif } diff --git a/src/arch/arm/traps.S b/src/arch/arm/traps.S index 8a61b1ffa..f07f53485 100644 --- a/src/arch/arm/traps.S +++ b/src/arch/arm/traps.S @@ -64,7 +64,7 @@ BEGIN_FUNC(arm_undefined_inst_exception) ldr r8, [sp] sub r8, r8, #4 str r8, [sp, #(PT_FaultInstruction - PT_LR_svc)] - mov sp, #(PPTR_KERNEL_STACK_TOP) + ldr sp, =(PPTR_KERNEL_STACK_TOP) ldr r7, =ksCurThread @@ -98,7 +98,7 @@ BEGIN_FUNC(arm_swi_syscall) stmdb sp, {r0-lr}^ /* Load the kernel's real stack pointer */ - mov sp, #(PPTR_KERNEL_STACK_TOP) + ldr sp, =(PPTR_KERNEL_STACK_TOP) #ifdef FASTPATH /* @@ -122,7 +122,7 @@ BEGIN_FUNC(arm_swi_syscall) ldr r8, =ksCurThread /* Check that syscall number is in range */ - sub r2, r0, #SYSCALL_MIN + add r2, r0, #(-SYSCALL_MIN) cmp r2, #(SYSCALL_MAX - SYSCALL_MIN + 1) bhs arm_swi_undefined_syscall @@ -144,7 +144,7 @@ BEGIN_FUNC(slowpath) * trashed. */ ldr r7, =ksCurThread - mov sp, #(PPTR_KERNEL_STACK_TOP) + ldr sp, =(PPTR_KERNEL_STACK_TOP) blx handleSyscall RET_TO_USER r7 END_FUNC(slowpath) @@ -180,7 +180,7 @@ BEGIN_FUNC(arm_prefetch_abort_exception) /* Store faulting address in TCB and call handleVMFaultEvent. */ str r8, [sp, #(PT_FaultInstruction - PT_LR_svc)] - mov sp, #(PPTR_KERNEL_STACK_TOP) + ldr sp, =(PPTR_KERNEL_STACK_TOP) ldr r7, =ksCurThread mov r0, #VM_EVENT_PREFETCH_ABORT @@ -191,7 +191,7 @@ BEGIN_FUNC(arm_prefetch_abort_exception) kernel_prefetch_fault: #ifdef DEBUG mov r0, r8 - mov sp, #(PPTR_KERNEL_STACK_TOP) + ldr sp, =(PPTR_KERNEL_STACK_TOP) blx kernelPrefetchAbort /* Fallthrough to infinite loop should we foolishly return. */ #endif @@ -227,7 +227,7 @@ BEGIN_FUNC(arm_data_abort_exception) /* Store faulting address in TCB and call handleVMFaultEvent. */ str r8, [sp, #(PT_FaultInstruction - PT_LR_svc)] - mov sp, #(PPTR_KERNEL_STACK_TOP) + ldr sp, =(PPTR_KERNEL_STACK_TOP) ldr r7, =ksCurThread mov r0, #VM_EVENT_DATA_ABORT @@ -238,7 +238,7 @@ BEGIN_FUNC(arm_data_abort_exception) kernel_data_fault: #ifdef DEBUG mov r0, r8 - mov sp, #(PPTR_KERNEL_STACK_TOP) + ldr sp, =(PPTR_KERNEL_STACK_TOP) blx kernelDataAbort /* Fallthrough to infinite loop should we foolishly return. */ #endif @@ -264,7 +264,7 @@ BEGIN_FUNC(arm_irq_exception) str r8, [sp, #(PT_FaultInstruction - PT_LR_svc)] ldr r7, =ksCurThread - mov sp, #(PPTR_KERNEL_STACK_TOP) + ldr sp, =(PPTR_KERNEL_STACK_TOP) blx handleInterruptEntry RET_TO_USER r7 diff --git a/src/kernel/thread.c b/src/kernel/thread.c index 802ed9d45..927439888 100644 --- a/src/kernel/thread.c +++ b/src/kernel/thread.c @@ -261,6 +261,12 @@ transferCaps(message_info_t info, extra_caps_t caps, return message_info_set_msgExtraCaps(info, i); } +void doNBWaitFailedTransfer(tcb_t *thread) +{ + /* Set the badge register to 0 to indicate there was no message */ + setRegister(thread, badgeRegister, 0); +} + static void nextDomain(void) { @@ -301,20 +307,27 @@ schedule(void) void chooseThread(void) { - int p; + word_t prio; + word_t dom; tcb_t *thread; - for (p = seL4_MaxPrio; p != -1; p--) { - unsigned int domprio = ksCurDomain * CONFIG_NUM_PRIORITIES + p; - thread = ksReadyQueues[domprio].head; - if (thread != NULL) { - assert(isRunnable(thread)); - switchToThread(thread); - return; - } + if (CONFIG_NUM_DOMAINS > 1) { + dom = ksCurDomain; + } else { + dom = 0; } - switchToIdleThread(); + if (likely(ksReadyQueuesL1Bitmap[dom])) { + word_t l1index = (wordBits - 1) - CLZ(ksReadyQueuesL1Bitmap[dom]); + word_t l2index = (wordBits - 1) - CLZ(ksReadyQueuesL2Bitmap[dom][l1index]); + prio = l1index_to_prio(l1index) | l2index; + thread = ksReadyQueues[ready_queues_index(dom, prio)].head; + assert(thread); + assert(isRunnable(thread)); + switchToThread(thread); + } else { + switchToIdleThread(); + } } void diff --git a/src/model/statedata.c b/src/model/statedata.c index 4ecd17712..d189b5c5f 100644 --- a/src/model/statedata.c +++ b/src/model/statedata.c @@ -16,6 +16,9 @@ /* Pointer to the head of the scheduler queue for each priority */ tcb_queue_t ksReadyQueues[NUM_READY_QUEUES]; +word_t ksReadyQueuesL1Bitmap[CONFIG_NUM_DOMAINS]; +word_t ksReadyQueuesL2Bitmap[CONFIG_NUM_DOMAINS][(CONFIG_NUM_PRIORITIES / wordBits) + 1]; +compile_assert(ksReadyQueuesL1BitmapBigEnough, (CONFIG_NUM_PRIORITIES / wordBits) <= wordBits) /* Current thread TCB pointer */ tcb_t *ksCurThread; diff --git a/src/object/asyncendpoint.c b/src/object/asyncendpoint.c index 5eccee778..ece87ab99 100644 --- a/src/object/asyncendpoint.c +++ b/src/object/asyncendpoint.c @@ -106,7 +106,7 @@ sendAsyncIPC(async_endpoint_t *aepptr, word_t badge) } void -receiveAsyncIPC(tcb_t *thread, cap_t cap) +receiveAsyncIPC(tcb_t *thread, cap_t cap, bool_t isBlocking) { async_endpoint_t *aepptr; @@ -117,19 +117,23 @@ receiveAsyncIPC(tcb_t *thread, cap_t cap) case AEPState_Waiting: { tcb_queue_t aep_queue; - /* Block thread on endpoint */ - thread_state_ptr_set_tsType(&thread->tcbState, - ThreadState_BlockedOnAsyncEvent); - thread_state_ptr_set_blockingIPCEndpoint(&thread->tcbState, - AEP_REF(aepptr)); - scheduleTCB(thread); + if (isBlocking) { + /* Block thread on endpoint */ + thread_state_ptr_set_tsType(&thread->tcbState, + ThreadState_BlockedOnAsyncEvent); + thread_state_ptr_set_blockingIPCEndpoint(&thread->tcbState, + AEP_REF(aepptr)); + scheduleTCB(thread); - /* Enqueue TCB */ - aep_queue = aep_ptr_get_queue(aepptr); - aep_queue = tcbEPAppend(thread, aep_queue); + /* Enqueue TCB */ + aep_queue = aep_ptr_get_queue(aepptr); + aep_queue = tcbEPAppend(thread, aep_queue); - async_endpoint_ptr_set_state(aepptr, AEPState_Waiting); - aep_ptr_set_queue(aepptr, aep_queue); + async_endpoint_ptr_set_state(aepptr, AEPState_Waiting); + aep_ptr_set_queue(aepptr, aep_queue); + } else { + doNBWaitFailedTransfer(thread); + } break; } diff --git a/src/object/endpoint.c b/src/object/endpoint.c index af4fed638..ea5d6d4fd 100644 --- a/src/object/endpoint.c +++ b/src/object/endpoint.c @@ -111,7 +111,7 @@ sendIPC(bool_t blocking, bool_t do_call, word_t badge, } void -receiveIPC(tcb_t *thread, cap_t cap) +receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking) { endpoint_t *epptr; bool_t diminish; @@ -133,21 +133,25 @@ receiveIPC(tcb_t *thread, cap_t cap) case EPState_Recv: { tcb_queue_t queue; - /* Set thread state to BlockedOnReceive */ - thread_state_ptr_set_tsType(&thread->tcbState, - ThreadState_BlockedOnReceive); - thread_state_ptr_set_blockingIPCEndpoint( - &thread->tcbState, EP_REF(epptr)); - thread_state_ptr_set_blockingIPCDiminishCaps( - &thread->tcbState, diminish); + if (isBlocking) { + /* Set thread state to BlockedOnReceive */ + thread_state_ptr_set_tsType(&thread->tcbState, + ThreadState_BlockedOnReceive); + thread_state_ptr_set_blockingIPCEndpoint( + &thread->tcbState, EP_REF(epptr)); + thread_state_ptr_set_blockingIPCDiminishCaps( + &thread->tcbState, diminish); - scheduleTCB(thread); + scheduleTCB(thread); - /* Place calling thread in endpoint queue */ - queue = ep_ptr_get_queue(epptr); - queue = tcbEPAppend(thread, queue); - endpoint_ptr_set_state(epptr, EPState_Recv); - ep_ptr_set_queue(epptr, queue); + /* Place calling thread in endpoint queue */ + queue = ep_ptr_get_queue(epptr); + queue = tcbEPAppend(thread, queue); + endpoint_ptr_set_state(epptr, EPState_Recv); + ep_ptr_set_queue(epptr, queue); + } else { + doNBWaitFailedTransfer(thread); + } break; } diff --git a/src/object/tcb.c b/src/object/tcb.c index c3cb959d9..1920a6620 100644 --- a/src/object/tcb.c +++ b/src/object/tcb.c @@ -24,11 +24,26 @@ #include #include -static inline PURE -unsigned int -ready_queues_index(unsigned int dom, unsigned int prio) +static inline void +addToBitmap(word_t dom, word_t prio) { - return dom * CONFIG_NUM_PRIORITIES + prio; + word_t l1index; + + l1index = prio_to_l1index(prio); + ksReadyQueuesL1Bitmap[dom] |= BIT(l1index); + ksReadyQueuesL2Bitmap[dom][l1index] |= BIT(prio & MASK(wordRadix)); +} + +static inline void +removeFromBitmap(word_t dom, word_t prio) +{ + word_t l1index; + + l1index = prio_to_l1index(prio); + ksReadyQueuesL2Bitmap[dom][l1index] &= ~BIT(prio & MASK(wordRadix)); + if (unlikely(!ksReadyQueuesL2Bitmap[dom][l1index])) { + ksReadyQueuesL1Bitmap[dom] &= ~BIT(l1index); + } } /* Add TCB to the head of a scheduler queue */ @@ -48,6 +63,7 @@ tcbSchedEnqueue(tcb_t *tcb) if (!queue.end) { /* Empty list */ queue.end = tcb; + addToBitmap(dom, prio); } else { queue.head->tcbSchedPrev = tcb; } @@ -78,6 +94,7 @@ tcbSchedAppend(tcb_t *tcb) if (!queue.head) { /* Empty list */ queue.head = tcb; + addToBitmap(dom, prio); } else { queue.end->tcbSchedNext = tcb; } @@ -110,6 +127,9 @@ tcbSchedDequeue(tcb_t *tcb) tcb->tcbSchedPrev->tcbSchedNext = tcb->tcbSchedNext; } else { queue.head = tcb->tcbSchedNext; + if (likely(!tcb->tcbSchedNext)) { + removeFromBitmap(dom, prio); + } } if (tcb->tcbSchedNext) { diff --git a/src/plat/pc99/machine/ioapic.c b/src/plat/pc99/machine/ioapic.c index 5ef8e2fad..2d3df5c34 100644 --- a/src/plat/pc99/machine/ioapic.c +++ b/src/plat/pc99/machine/ioapic.c @@ -139,7 +139,7 @@ void ioapic_mask_irq(bool_t mask, irq_t irq) ioredtbl_state[irq] &= ~IOREDTBL_LOW_INTERRUPT_MASK; #if defined DEBUG || defined RELEASE_PRINTF if (!done_set_mode[irq]) { - printf("Unmasking IOAPIC source %d on ioapic %d without ever setting its mode!\n", index, ioapic); + printf("Unmasking IOAPIC source %ld on ioapic %ld without ever setting its mode!\n", index, ioapic); /* Set the flag so we don't repeatedly warn */ done_set_mode[irq] = 1; }