From d9802d179fd5c72e6180cb82be8bfde8bf570f50 Mon Sep 17 00:00:00 2001
From: Anna Lyons <Anna.Lyons@nicta.com.au>
Date: Fri, 9 Oct 2015 16:02:41 +1100
Subject: [PATCH 01/14] Add seL4_NBWait: non blocking wait for notifications
 and endpoints.

---
 haskell/src/SEL4/API/Syscall.lhs              | 16 ++++----
 haskell/src/SEL4/Object/AsyncEndpoint.lhs     | 37 ++++++++++++-------
 haskell/src/SEL4/Object/Endpoint.lhs          | 30 ++++++++-------
 include/api/syscall.xml                       |  1 +
 include/kernel/thread.h                       |  1 +
 include/object/asyncendpoint.h                |  2 +-
 include/object/endpoint.h                     |  2 +-
 libsel4/arch_include/arm/sel4/arch/syscalls.h | 35 ++++++++++++++++++
 libsel4/arch_include/x86/sel4/arch/syscalls.h | 36 ++++++++++++++++++
 libsel4/include/api/syscall.xml               |  1 +
 manual/parts/api.tex                          |  1 +
 manual/parts/api/sel4_nbwait.tex              | 21 +++++++++++
 manual/parts/ipc.tex                          |  1 +
 manual/parts/objects.tex                      |  7 ++++
 src/api/syscall.c                             | 15 +++++---
 src/kernel/thread.c                           |  6 +++
 src/object/asyncendpoint.c                    | 28 ++++++++------
 src/object/endpoint.c                         | 32 +++++++++-------
 18 files changed, 205 insertions(+), 67 deletions(-)
 create mode 100644 manual/parts/api/sel4_nbwait.tex

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/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/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/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 @@
             <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 -->
diff --git a/include/kernel/thread.h b/include/kernel/thread.h
index e8b773f08..977005cb4 100644
--- a/include/kernel/thread.h
+++ b/include/kernel/thread.h
@@ -28,6 +28,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/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 <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);
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/libsel4/arch_include/arm/sel4/arch/syscalls.h b/libsel4/arch_include/arm/sel4/arch/syscalls.h
index 5b25f03cd..03feec1f0 100644
--- a/libsel4/arch_include/arm/sel4/arch/syscalls.h
+++ b/libsel4/arch_include/arm/sel4/arch/syscalls.h
@@ -291,6 +291,41 @@ seL4_WaitWithMRs(seL4_CPtr src, seL4_Word* sender,
     };
 }
 
+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)
 {
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 @@
             <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 -->
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..3e13b18ba
--- /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 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/kernel/thread.c b/src/kernel/thread.c
index 802ed9d45..2187d591b 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)
 {
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;
         }
 

From c99c1b79a0cc79d1a151ad9e415da1e82b0c32bc Mon Sep 17 00:00:00 2001
From: Stephen Sherratt <stephen.sherratt@nicta.com.au>
Date: Tue, 16 Jun 2015 10:10:37 +1000
Subject: [PATCH 02/14] Added a wordRadix constant to x86 kernel.

---
 include/arch/x86/arch/machine.h | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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

From 62727e30a2f737d60bbacfc69eb0bf4defca1fbd Mon Sep 17 00:00:00 2001
From: Stephen Sherratt <stephen.sherratt@nicta.com.au>
Date: Tue, 16 Jun 2015 10:14:14 +1000
Subject: [PATCH 03/14] Using bitfields to track for which priorities there
 exist non-empty ready queues.

Background
seL4 organizes threads into ready queues, of which there is one for each
domain, for each priority level. The ready queue for a given
domain/priority combination can be found by indexing the array
`ksReadyQueues` with "domain*num_priorities + priority".

Current scheduler implementation
To find the non-empty ready queue with the maximum priority for the current domain,
seL4 iterates through `ksReadyQueues`, starting with the element
corresponding to the current domain and maximum possible priority, and
decrementing the priority until a non-empty queue is found. This is
problematic in cases where the only ready threads have low priorities,
as iterating through many elements of an array effectively flushes the
cache.

Changes in this patch
This patch replaces the iteration with a lookup into a table of
bitfields per domain. Using bitfields allows the kernel to determine the
highest priority level with a non-empty ready queue for the current
domain by counting the leading zeroes in bitfields. This removes the
negative cache effects of iterating through an array.

Implementation details
For each domain, a multilevel table of bitfields is maintained which
stores the priority levels within that domain for which there exist
ready threads. On a 32-bit architecture, the top level of the table is a 32-bit bitfield where if
the ith bit is set, there is at least 1 priority level in
[i*32..i*32+31] with a non-empty ready queue. The positions of bits in
this bitfield are used as indices into the second level table, which is
an array of 32-bit bitfields. The ith bit of the jth bitfield in this
array set to 1, indicates that priority level j*32+i has a non-empty
ready queue.
---
 include/kernel/thread.h   | 24 ++++++++++++++++++++++++
 include/model/statedata.h |  2 ++
 src/kernel/thread.c       | 26 +++++++++++++++++---------
 src/model/statedata.c     |  3 +++
 src/object/tcb.c          | 28 ++++++++++++++++++++++++----
 5 files changed, 70 insertions(+), 13 deletions(-)

diff --git a/include/kernel/thread.h b/include/kernel/thread.h
index 977005cb4..78f0d287c 100644
--- 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 PURE 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 PURE word_t
+prio_to_l1index(word_t prio)
+{
+    return (prio >> wordRadix);
+}
+
+static inline PURE word_t
+l1index_to_prio(word_t l1index)
+{
+    return (l1index << wordRadix);
+}
 
 void configureIdleThread(tcb_t *tcb);
 void activateThread(void) 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 <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;
diff --git a/src/kernel/thread.c b/src/kernel/thread.c
index 2187d591b..757793219 100644
--- a/src/kernel/thread.c
+++ b/src/kernel/thread.c
@@ -307,17 +307,25 @@ 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;
+    }
+
+    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);
+        return;
     }
 
     switchToIdleThread();
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/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 <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) {

From 947135a7ad64f58713c70058e32213cdb3a01023 Mon Sep 17 00:00:00 2001
From: Rafal Kolanski <rafal.kolanski@nicta.com.au>
Date: Fri, 16 Oct 2015 20:07:57 +1100
Subject: [PATCH 04/14] chooseThread: favour else clause over explicit return

(easier proofs)
---
 src/kernel/thread.c | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/kernel/thread.c b/src/kernel/thread.c
index 757793219..927439888 100644
--- a/src/kernel/thread.c
+++ b/src/kernel/thread.c
@@ -325,10 +325,9 @@ chooseThread(void)
         assert(thread);
         assert(isRunnable(thread));
         switchToThread(thread);
-        return;
+    } else {
+        switchToIdleThread();
     }
-
-    switchToIdleThread();
 }
 
 void

From 991d7afbd57628cfe08563cf078366ecc10acdb2 Mon Sep 17 00:00:00 2001
From: Rafal Kolanski <rafal.kolanski@nicta.com.au>
Date: Wed, 30 Sep 2015 08:29:19 +1000
Subject: [PATCH 05/14] Wrap __builtin_clz for C Parser (verification)

Create new function "clz" which invokes __builtin_clz
Tell the C parser to not try translate it (DONT_TRANSLATE), but instead
to trust the spec we provide (FNSPEC+MODIFIES).

Squashed the fix by Anna Lyons:

rearrange CLZ in util.h and s/__builtin__clz/__builtin_clz/
---
 include/util.h | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

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:
+  "\<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 */

From 7a16bdc1105f89d4c87ae5735ab7b5c54fcd1740 Mon Sep 17 00:00:00 2001
From: Rafal Kolanski <rafal.kolanski@nicta.com.au>
Date: Mon, 20 Jul 2015 18:05:44 +1000
Subject: [PATCH 06/14] priority-bitmap: update Haskell

---
 haskell/src/SEL4/Kernel/Init.lhs       |  4 +-
 haskell/src/SEL4/Kernel/Thread.lhs     | 94 ++++++++++++++++++++------
 haskell/src/SEL4/Model/StateData.lhs   | 11 +++
 haskell/src/SEL4/Object/CNode.lhs      |  4 +-
 haskell/src/SEL4/Object/Structures.lhs | 20 +++++-
 haskell/src/SEL4/Object/TCB.lhs        | 14 ++--
 6 files changed, 115 insertions(+), 32 deletions(-)

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

From 97f49bfc1bd0c1aec07b9ad2ffcc2d4e12477107 Mon Sep 17 00:00:00 2001
From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Date: Thu, 22 Oct 2015 17:56:30 +1100
Subject: [PATCH 07/14] manual: Fix documented return type of NBWait.

---
 manual/parts/api/sel4_nbwait.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/manual/parts/api/sel4_nbwait.tex b/manual/parts/api/sel4_nbwait.tex
index 3e13b18ba..17f018834 100644
--- a/manual/parts/api/sel4_nbwait.tex
+++ b/manual/parts/api/sel4_nbwait.tex
@@ -12,7 +12,7 @@
 {sel4_nbwait}
 {NBWait}
 {Perform a non-blocking wait on an endpoint or notification object}
-{static inline seL4\_MessageInfo seL4\_NBWait}
+{static inline seL4\_MessageInfo\_t seL4\_NBWait}
 {
 \param{seL4\_CPtr}{src}{\invokedcapdesc}
 \param{seL4\_Word*}{sender}{\senderdesc}

From 8743737daeaabf84a467a39f7d8ac92479ce11ae Mon Sep 17 00:00:00 2001
From: Adrian Danis <Adrian.Danis@nicta.com.au>
Date: Fri, 23 Oct 2015 15:02:53 +1100
Subject: [PATCH 08/14] Use CONST instead of PURE in thread functions

As these functions do not read any global state they fit
within the subset of PURE that can be declared as CONST
---
 include/kernel/thread.h | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/include/kernel/thread.h b/include/kernel/thread.h
index 78f0d287c..3b62e4817 100644
--- a/include/kernel/thread.h
+++ b/include/kernel/thread.h
@@ -16,7 +16,7 @@
 #include <object/structures.h>
 #include <arch/machine.h>
 
-static inline PURE word_t
+static inline CONST word_t
 ready_queues_index(word_t dom, word_t prio)
 {
     if (CONFIG_NUM_DOMAINS > 1) {
@@ -27,13 +27,13 @@ ready_queues_index(word_t dom, word_t prio)
     }
 }
 
-static inline PURE word_t
+static inline CONST word_t
 prio_to_l1index(word_t prio)
 {
     return (prio >> wordRadix);
 }
 
-static inline PURE word_t
+static inline CONST word_t
 l1index_to_prio(word_t l1index)
 {
     return (l1index << wordRadix);

From bd8954289df1973344fac59ae24d80bf781ae757 Mon Sep 17 00:00:00 2001
From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Date: Wed, 28 Oct 2015 11:12:53 +1100
Subject: [PATCH 09/14] ARM: Remove the use of implicit pseudo instructions in
 assembly.

This commit swaps some instructions that were being permissively accepted by
GAS with their more correct formulation. For example, `mov` was being used with
a 32-bit immediate, though it only supports a 16-bit immediate. GAS lets much
of this misuse slide and treats instructions like `mov` as a pseudo
instruction, though it isn't. Other more strict assemblers reject this. This
commit replaces such instances with `ldr`, the correct pseudo instruction.
---
 src/arch/arm/traps.S | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

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

From aef03c325eb36146cc869b0625922729939d5d9e Mon Sep 17 00:00:00 2001
From: Adrian Danis <Adrian.Danis@nicta.com.au>
Date: Mon, 2 Nov 2015 15:42:00 +1100
Subject: [PATCH 10/14] libsel4: Restrict syscall stub compilation at -O0

The 'WithMRs' variants of the syscall stubs are known to be broken
on ARM with GCC at -O0. This commit prevents the generation and
usage of these stubs when -O0 is set in the common tool configuration
options.

Due to limitations in specifying Kconfig constraints, and to preserve
the existing meaning of the Kconfig variables, the 'LIB_SEl4_STUBS_USE_IPC_BUFFER_ONLY'
config variable has to be duplicated with two variants, one for use
when the user is free to pick either and one hidden for when selection
has to be forced. Also to prevent the sub options from not appearing
in the libsel4 submenu I had to change libsel4 to be a 'true' menu
instead of a 'menuconfig'

This commit closes SELFOUR-187
---
 libsel4/Kconfig                               | 38 ++++++++++++++++---
 libsel4/arch_include/arm/sel4/arch/syscalls.h | 21 +++++-----
 2 files changed, 44 insertions(+), 15 deletions(-)

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 03feec1f0..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,7 @@ 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)
@@ -357,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)
@@ -409,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)
@@ -445,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)
@@ -501,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)

From f32a1d75dcc3442ff5e33ac9110a2f6f2d75d1ba Mon Sep 17 00:00:00 2001
From: Adrian Danis <Adrian.Danis@nicta.com.au>
Date: Fri, 6 Nov 2015 16:36:00 +1100
Subject: [PATCH 11/14] x86: Fix printing when the ioapic is enabled

---
 src/plat/pc99/machine/ioapic.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

From f6ae69f0f0ccd0c42eefd2b8b012e1420843d2ae Mon Sep 17 00:00:00 2001
From: Adrian Danis <Adrian.Danis@nicta.com.au>
Date: Fri, 6 Nov 2015 14:22:03 +1100
Subject: [PATCH 12/14] Use autoconf generated header for standalone kernel
 builds

Configuring standalone kernel builds (such as those used by verification)
has been done in a completely different way to how the kernel is
configured for project builds. As the kernel gains additional options
it becomes difficult to maintain standalone kernel builds without
tediously exporting these additional options, such tedious work is
what autoconf.h is meant to address

The new configuration strategy requires a include/plat/PLAT/autoconf.h
file to exist for any platform that wants to hae standalone builds
performed on it. This configuration also becomes the *verified*
configuration, and makes it clear for projects to build the kernel
in the verified configuration.
---
 Makefile                         | 16 ++++--
 include/plat/am335x/autoconf.h   | 89 ++++++++++++++++++++++++++++++
 include/plat/apq8064/autoconf.h  | 93 +++++++++++++++++++++++++++++++
 include/plat/exynos4/autoconf.h  | 89 ++++++++++++++++++++++++++++++
 include/plat/exynos5/autoconf.h  | 94 ++++++++++++++++++++++++++++++++
 include/plat/imx31/autoconf.h    | 89 ++++++++++++++++++++++++++++++
 include/plat/imx6/autoconf.h     | 89 ++++++++++++++++++++++++++++++
 include/plat/omap3/autoconf.h    | 89 ++++++++++++++++++++++++++++++
 include/plat/pc99/autoconf.h     | 92 +++++++++++++++++++++++++++++++
 include/plat/zynq7000/autoconf.h | 89 ++++++++++++++++++++++++++++++
 10 files changed, 823 insertions(+), 6 deletions(-)
 create mode 100644 include/plat/am335x/autoconf.h
 create mode 100644 include/plat/apq8064/autoconf.h
 create mode 100644 include/plat/exynos4/autoconf.h
 create mode 100644 include/plat/exynos5/autoconf.h
 create mode 100644 include/plat/imx31/autoconf.h
 create mode 100644 include/plat/imx6/autoconf.h
 create mode 100644 include/plat/omap3/autoconf.h
 create mode 100644 include/plat/pc99/autoconf.h
 create mode 100644 include/plat/zynq7000/autoconf.h

diff --git a/Makefile b/Makefile
index c30a93231..5912b9fc6 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,6 +397,10 @@ endif
 ifeq ($(PLAT),allwinnerA20)
 DEFINES += -DALLWINNERA20
 endif
+else
+# 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 (${ARCH}, x86)
@@ -537,6 +539,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 +576,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 +642,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/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

From d342e9b05de61a49bc6d0bdf546d12cb4b62b620 Mon Sep 17 00:00:00 2001
From: Matthew Fernandez <matthew.fernandez@gmail.com>
Date: Mon, 9 Nov 2015 08:08:58 +1100
Subject: [PATCH 13/14] ARM A15: Remove statement with no effect.

This looks to me like a statement to suppress unused function warnings that
accidentally got shuffled inside the ifdef. This change has no effect on
verification.
---
 src/arch/arm/machine/errata.c | 1 -
 1 file changed, 1 deletion(-)

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
 }

From 5d64d156f47c20ae049c0c854797291436f84021 Mon Sep 17 00:00:00 2001
From: Adrian Danis <Adrian.Danis@nicta.com.au>
Date: Mon, 9 Nov 2015 15:01:08 +1100
Subject: [PATCH 14/14] Correct Makefile from commit
 f6ae69f0f0ccd0c42eefd2b8b012e1420843d2ae

The Makefile proior to f6ae69f0f0ccd0c42eefd2b8b012e1420843d2ae was
incorrectly commented. This commit fixes the commenting the resulting
incorrect comment
---
 Makefile | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/Makefile b/Makefile
index 5912b9fc6..ea0cac5ca 100644
--- a/Makefile
+++ b/Makefile
@@ -397,19 +397,18 @@ endif
 ifeq ($(PLAT),allwinnerA20)
 DEFINES += -DALLWINNERA20
 endif
-else
-# 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
-
+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