% % 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) % \chapter{\label{ch:ipc}Message Passing (IPC)} The seL4 microkernel provides a message-passing IPC mechanism for communication between threads. The same mechanism is also used for communication with kernel-provided services. Messages are sent by invoking a capability to a kernel object. Messages sent to \obj{Endpoint}s are destined for other threads, while messages sent to other objects are processed by the kernel. This chapter describes the common message format, endpoints, and how they can be used for communication between applications. \section{Message Registers} \label{sec:messageinfo} Each message contains a number of message words and optionally a number of capabilities. The message words are sent to or received from a thread by placing them in its \emph{message registers}. The message registers are numbered and the first few message registers are implemented using physical CPU registers, while the rest are backed by a fixed region of memory called the \emph{IPC buffer}. The reason for this design is efficiency: very short messages need not use the memory. The IPC buffer is assigned to the calling thread (see \autoref{sec:threads} and \autoref{api:tcb_setipcbuffer}). %FIXME: seL4_TCB_SetIPCBuffer is only mentioned in the API reference! Every IPC message also has a tag (structure \texttt{seL4\_MessageInfo\_t}). The tag consists of four fields: the label, message length, number of capabilities (the \texttt{extraCaps} field) and the \texttt{capsUnwrapped} field. The message length and number of capabilities determine either the number of message registers and capabilities that the sending thread wishes to transfer, or the number of message registers and capabilities that were actually transferred. The label is not interpreted by the kernel and is passed unmodified as the first data payload of the message. The label may, for example, be used to specify a requested operation. The \texttt{capsUnwrapped} field is used only on the receive side, to indicate the manner in which capabilities were received. It is described in \autoref{sec:cap-transfer}. % FIXME: a little too low-level, perhaps? \newcommand{\ipcparam}[4]{\texttt{#1} \emph{#2}&\texttt{#3}\\ } \begin{table}[htb] \begin{center} \begin{tabularx}{\textwidth}{p{0.28\textwidth}p{0.18\textwidth}X} \toprule \textbf{Type} & \textbf{Name} & \textbf{Description} \\ \midrule \ipcparam{seL4\_MessageInfo\_t}{}{tag}{Message tag} \ipcparam{seL4\_Word[]}{}{msg}{Message contents} \ipcparam{seL4\_Word}{}{userData}{Base address of the structure, used by supporting user libraries} \ipcparam{seL4\_CPtr[]}{(in)}{caps}{Capabilities to transfer} \ipcparam{seL4\_CapData\_t[]}{(out)}{badges}{Badges for endpoint capabilities received} \ipcparam{seL4\_CPtr}{}{receiveCNode}{CPTR to a CNode from which to find the receive slot} \ipcparam{seL4\_CPtr}{}{receiveIndex}{CPTR to the receive slot relative to \texttt{receiveCNode}} \ipcparam{seL4\_Word}{}{receiveDepth}{Number of bits of \texttt{receiveIndex} to use} \bottomrule \end{tabularx} \caption{\label{tbl:ipcbuffer}Fields of the \texttt{seL4\_IPCBuffer} structure. Note that \texttt{badges} and \texttt{caps} use the same area of memory in the structure.} \end{center} \end{table} The kernel assumes that the IPC buffer contains a structure of type \texttt{seL4\_IPCBuffer} as defined in \autoref{tbl:ipcbuffer}. The kernel uses as many physical registers as possible to transfer IPC messages. When more arguments are transferred than physical message registers are available, the kernel begins using the IPC buffer's \texttt{msg} field to transfer arguments. However, it leaves room in this array for the physical message registers. For example, if an IPC transfer or kernel object invocation required 4 message registers (and there are only 2 physical message registers available on this architecture) then arguments 1 and 2 would be transferred via message registers and arguments 3 and 4 would be in \texttt{msg[2]} and \texttt{msg[3]}. This allows the user-level object-invocation stubs to copy the arguments passed in physical registers to the space left in the \texttt{msg} array if desired. The situation is similar for the tag field. There is space for this field in the \texttt{seL4\_IPCBuffer} structure, which the kernel ignores. User level stubs may wish to copy the message tag from its CPU register to this field, although the user level stubs provided with the kernel do not do this. \section{Endpoints} \obj{Endpoint}s allow a small amount of data and capabilities (namely the IPC buffer) to be transferred between two threads. \obj{Endpoint} objects are invoked directly using the seL4 system calls described in \autoref{sec:syscalls}. IPC \obj{Endpoints} uses a rendezvous model and as such is synchronous and blocking. An \obj{Endpoint} object may queue threads either to send or to receive. If no receiver is ready, threads performing the \apifunc{seL4\_Send}{sel4_send} or \apifunc{seL4\_Call}{sel4_call} system calls will wait in a queue for the first available receiver. Likewise, if no sender is ready, threads performing the \apifunc{seL4\_Recv}{sel4_recv} system call or the second half of \apifunc{seL4\_ReplyRecv}{sel4_replyrecv} will wait for the first available sender. \subsection{Endpoint Badges\label{s:ep-badge}} \label{sec:ep-badges} Endpoint capabilities may be \emph{minted} to create a new endpoint capability with a \emph{badge} attached to it, a data word chosen by the invoker of the \emph{mint} operation. When a message is sent to an endpoint using a badged capability, the badge is transferred to the receiving thread's \texttt{badge} register. An endpoint capability with a zero badge is said to be \emph{unbadged}. Such a capability can be badged with the \apifunc{seL4\_CNode\_Mutate}{cnode_mutate} or \apifunc{seL4\_CNode\_Mint}{cnode_mint} invocations on the \obj{CNode} containing the capability. Endpoint capabilities with badges cannot be unbadged, rebadged or used to create child capabilities with different badges. Only the low 28 bits of the badge are available for use. The kernel will silently ignore any usage of the high 4 bits. \subsection{Capability Transfer} \label{sec:cap-transfer} Messages may contain capabilities, which will be transferred to the receiver, provided that the endpoint capability invoked by the sending thread has Grant rights. An attempt to send capabilities using an endpoint capability without the Grant right will result in transfer of the raw message, without any capability transfer. Capabilities to be sent in a message are specified in the sending thread's IPC buffer in the \texttt{caps} field. Each entry in that array is interpreted as a CPTR in the sending thread's capability space. The number of capabilities to send is specified in the \texttt{extraCaps} field of the message tag. The receiver specifies the slot in which it is willing to receive a capability, with three fields within the IPC buffer: \texttt{receiveCNode}, \texttt{receiveIndex} and \texttt{receiveDepth}. These fields specify the root CNode, capability address and number of bits to resolve, respectively, to find the slot in which to put the capability. Capability addressing is described in \autoref{sec:cap_addressing}. A received capability has the same rights as the original, except if the \emph{receiving} endpoint capability lacks the Write right. In this case, the rights on the sent capability are \emph{diminished}, by stripping the Write right from the received copy of the capability. Note that receiving threads may specify only one receive slot, whereas a sending thread may include multiple capabilities in the message. Messages containing more than one capability may be interpreted by kernel objects. They may also be sent to receiving threads in the case where some of the extra capabilities in the message can be \emph{unwrapped}. If the n-th capability in the message refers to the endpoint through which the message is sent, the capability is \emph{unwrapped}: its badge is placed into the n-th position of the receiver's badges array, and the kernel sets the n-th bit (counting from the least significant) in the \texttt{capsUnwrapped} field of the message tag. The capability itself is not transferred, so the receive slot may be used for another capability. If a receiver gets a message whose tag has an \texttt{extraCaps} of 2 and a \texttt{capsUnwrapped} of 2, then the first capability in the message was transferred to the specified receive slot and the second capability was unwrapped, placing its badge in \texttt{badges[1]}. There may have been a third capability in the sender's message which could not be unwrapped. \subsection{Errors} Errors in capability transfers can occur at two places: in the send phase or in the receive phase. In the send phase, all capabilities that the caller is attempting to send are looked up to ensure that they exist before the send is initiated in the kernel. If the lookup fails for any reason, \apifunc{seL4\_Send}{sel4_send} and \apifunc{seL4\_Call}{sel4_call} system calls immediately abort and no IPC or capability transfer takes place. The system call will return a lookup failure error as described in \autoref{sec:errors}. In the receive phase, seL4 transfers capabilities in the order that they are found in the sending thread's IPC buffer \texttt{caps} array and terminates as soon as an error is encountered. Possible error conditions are: \begin{itemize} \item A source capability cannot be looked up. Although the presence of the source capabilities is checked when the sending thread performs the send system call, this error may still occur. The sending thread may have been blocked on the endpoint for some time before it was paired with a receiving thread. During this time, its CSpace may have changed and the source capability pointers may no longer be valid. \item The destination slot cannot be looked up. Unlike the send system call, the \apifunc{seL4\_Recv}{sel4_recv} system call does not check that the destination slot exists and is empty before it initiates the receive. Hence, the \apifunc{seL4\_Recv}{sel4_recv} system call will not fail with an error if the destination slot is invalid and will instead transfer badged capabilities until an attempt to save a capability to the destination slot is made. \item The capability being transferred cannot be derived. See \autoref{sec:cap_derivation} for details. \end{itemize} An error will not void the entire transfer, it will just end it prematurely. The capabilities processed before the failure are still 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.