Merge commit '5d64d156f47c20ae049c0c854797291436f84021' into HEAD

2015-12-02 17:13:07 +11:00 · 2015-12-02 17:13:07 +11:00 · 460c87ddf3
commit 460c87ddf3
parent e17727acab 5d64d156f4
43 changed files with 1289 additions and 152 deletions
--- a/23
+++ b/23
@ -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 \
--- 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
--- 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 
--- 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}
--- 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",
--- 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.

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

--- 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"
--- 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}
--- a/include/api/syscall.xml
+++ b/include/api/syscall.xml
@ -20,6 +20,7 @@
            <syscall name="Wait"      />
            <syscall name="Reply"     />
            <syscall name="Yield"     />
+            <syscall name="NBWait"      />
        </config>
    </api>
    <!-- Syscalls on the unknown syscall path. These definitions will be wrapped in #ifdef name -->
--- a/include/arch/x86/arch/machine.h
+++ b/include/arch/x86/arch/machine.h
@ -18,7 +18,8 @@
 #include <arch/machine/cpu_registers.h>
 #include <arch/model/statedata.h>

-#define wordBits 32
+#define wordRadix 5
+#define wordBits (1 << wordRadix)

 #define IA32_APIC_BASE_MSR      0x01B
 #define IA32_SYSENTER_CS_MSR    0x174
--- a/include/kernel/thread.h
+++ b/include/kernel/thread.h
@ -14,6 +14,30 @@
 #include <types.h>
 #include <util.h>
 #include <object/structures.h>
+#include <arch/machine.h>
+
+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;
--- a/include/model/statedata.h
+++ b/include/model/statedata.h
@ -17,6 +17,8 @@
 #include <arch/model/statedata.h>

 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;
--- a/include/object/asyncendpoint.h
+++ b/include/object/asyncendpoint.h
@ -15,7 +15,7 @@
 #include <object/structures.h>

 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);
--- 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);
--- a/include/plat/am335x/autoconf.h
+++ 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
--- a/include/plat/apq8064/autoconf.h
+++ 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
--- a/include/plat/exynos4/autoconf.h
+++ 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
--- a/include/plat/exynos5/autoconf.h
+++ 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
--- a/include/plat/imx31/autoconf.h
+++ 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
--- a/include/plat/imx6/autoconf.h
+++ 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
--- a/include/plat/omap3/autoconf.h
+++ 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
--- a/include/plat/pc99/autoconf.h
+++ 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
--- a/include/plat/zynq7000/autoconf.h
+++ 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
--- 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:
+  "\<forall>s. \<Gamma> \<turnstile>
+    {\<sigma>. s = \<sigma> \<and> x_' s \<noteq> 0 }
+      \<acute>ret__int :== PROC clz(\<acute>x)
+    \<lbrace> \<acute>ret__int = of_nat (word_clz (x_' s)) \<rbrace>"
+*/
+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 */
--- 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
--- 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)
--- 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)
 {
--- a/libsel4/include/api/syscall.xml
+++ b/libsel4/include/api/syscall.xml
@ -20,6 +20,7 @@
            <syscall name="Wait"      />
            <syscall name="Reply"     />
            <syscall name="Yield"     />
+            <syscall name="NBWait"      />
        </config>
    </api>
    <!-- Syscalls on the unknown syscall path. These definitions will be wrapped in #ifdef name -->
--- 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
--- a/manual/parts/api/sel4_nbwait.tex
+++ 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}}
--- 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.
+
--- 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.
--- 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:
--- 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
 }
--- 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
--- 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
--- 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;
--- 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;
    }

--- 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;
        }

--- a/src/object/tcb.c
+++ b/src/object/tcb.c
@ -24,11 +24,26 @@
 #include <util.h>
 #include <string.h>

-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) {
--- 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;
        }