diff --git a/haskell/doc/figures/clientserver.mp b/haskell/doc/figures/clientserver.mp index 7ec574280b160d2f60509313152cb6dbe10bc9b3..ff0a5ece62682474d74b75dab4b25b7cf875936b 100644 --- a/haskell/doc/figures/clientserver.mp +++ b/haskell/doc/figures/clientserver.mp @@ -35,7 +35,7 @@ boxjoin(); circleit.send("Reply"); send.dx = send.dy; send.w = kep.e + (15bp, 0bp); drawboxed(send); -circleit.wait("Wait"); wait.dx = wait.dy; +circleit.wait("Recv"); wait.dx = wait.dy; wait.c = (xpart send.c, ypart ko.c); drawboxed(wait); boxit.kernel(); diff --git a/haskell/doc/figures/ipctransfer.mp b/haskell/doc/figures/ipctransfer.mp index 770e4b5c877a66bc27dd18dc321ac9e4c0a1b7f8..3f0a455bcef0cba7d46bfebdef94d61eb3305c60 100644 --- a/haskell/doc/figures/ipctransfer.mp +++ b/haskell/doc/figures/ipctransfer.mp @@ -74,11 +74,11 @@ drawboxed(re, rf, rg); label.top("Recipient CSpace", re.n); drawarrow(rb.e{right} .. re.ne{dir 225}); -% Wait System Call +% Recv System Call pair wsc; wsc = rf.e + (36bp, 0bp); drawarrow wsc--rf.e dashed withdots; -label.rt("Wait", wsc); +label.rt("Recv", wsc); % Endpoint boxjoin(); diff --git a/haskell/doc/overview.tex b/haskell/doc/overview.tex index 78327647bdb0945452eb417b79c9dc8a9e401a15..d75d23b8ef6fbdae5226c915f0638846bf85d11b 100644 --- a/haskell/doc/overview.tex +++ b/haskell/doc/overview.tex @@ -38,15 +38,10 @@ capability has been created, its contents are only visible to the kernel. \subsection{Capability Invocation} Capabilities may be \emph{invoked} by passing their CSpace addresses to one of -the kernel's two basic operations --- \emph{Send} and \emph{Wait}. The former +the kernel's two basic operations --- \emph{Send} and \emph{Recv}. The former is used to send a message to the object represented by the capability, and the latter to wait for a reply. -All communication channels in seL4 are one-way; under normal circumstances, a -user-level thread will never perform both Send and Wait operations using a -single capability. In fact, many capabilities will only allow one of these two -operations, and attempting to perform the other will fail. - The potential recipients or senders of a message through an invoked capability depend on the type of the kernel object that the capability refers to. For most object types, the kernel itself is the recipient of the message; however, @@ -57,15 +52,15 @@ messages may also be sent to other user-level threads. The basic inter-process communication (or \emph{IPC}) operation is coordinated using \emph{endpoint} objects. An endpoint is a small kernel object which contains a queue of threads, and a state flag that indicates whether the -threads in the queue are waiting for Send operations or Wait operations. It +threads in the queue are waiting for Send operations or Recv operations. It acts as a one-way channel for communication between one or more senders and one or more recipients. Unlike previous versions of L4, the global identities of the participants in IPC are not exposed; threads send and receive IPC using only the local addresses of their endpoints. -Multiple threads may perform Send or Wait operations on the same endpoint. +Multiple threads may perform Send or Recv operations on the same endpoint. When a pair of threads invoke an endpoint, performing a Send operation and a -Wait operation respectively, the kernel will perform a \emph{message transfer} +Recv operation respectively, the kernel will perform a \emph{message transfer} between them. Threads which cannot immediately be paired are suspended until a partner arrives. If multiple threads are suspended on one endpoint, the kernel's algorithm for choosing a thread to resume is not specified, but @@ -161,14 +156,14 @@ A non-blocking invocation will not fail or fault if the invoked capability is absent, and will not suspend the sender if no partner is waiting on the endpoint. It is the untrusted recipient's responsibility to provide a valid endpoint capability -and to perform a Wait operation on it before the message is sent; otherwise +and to perform a Recv operation on it before the message is sent; otherwise the message will be silently dropped. The kernel does not inform the sender that the non-blocking invocation has been dropped, as doing so would open a covert channel. \subsubsection{Calls and Replies} -Synchronous IPC is often used to implement remote procedure calls (or \emph{RPC}). In order to simplify the process of sending and replying to RPC, the kernel provides special versions of the Send and Wait operations designed specifically for use on the client and server sides of an RPC interface. +IPC is often used to implement remote procedure calls (or \emph{RPC}). In order to simplify the process of sending and replying to RPC, the kernel provides special versions of the Send and Recv operations designed specifically for use on the client and server sides of an RPC interface. To send an RPC, the client marshals arguments in the same way as for an ordinary Send operation, and then performs a \emph{Call} operation. The only difference between Send and Call is that when the message is transferred, a Call will block the sending thread, create a \emph{resume capability} that wakes the sender when invoked, and transfer it to a special slot belonging to the receiving thread: the \emph{caller slot}. This transfer is subject to the same restrictions as an explicit capability transfer: it only happens if the sender possesses the grant right for the endpoint, and the receiver must have the send right on the endpoint or it will receive a read-only capability (which in this case is effectively a null capability). @@ -178,7 +173,7 @@ When the resume capability is invoked --- either when the receiver uses Reply, o The Reply operation is always non-blocking. If the resume capability is not valid --- because the sender used Send rather than Call, the sender has already been resumed, the resume capability has been saved in the CSpace, or even if there has never been a sender yet --- then the Reply operation does nothing. -Servers generally run a loop which waits for a message, handles the received message, sends a reply and then returns to waiting. To avoid excessive switching between user and kernel modes, the kernel provides a \emph{ReplyWait} operation, which is simply a Reply followed by Wait. +Servers generally run a loop which waits for a message, handles the received message, sends a reply and then returns to waiting. To avoid excessive switching between user and kernel modes, the kernel provides a \emph{ReplyRecv} operation, which is simply a Reply followed by Recv. \subsection{System Calls} @@ -525,20 +520,19 @@ of an event. The kernel provides a \emph{signal} operation for this purpose. It is implemented using \emph{notification} objects, which contain a fixed size buffer of two machine words -- identifier and message word. Each notification capability is marked with a badge, which is set when -the capability is created. A thread may perform \emph{Send} or \emph{Wait} +the capability is created. A thread may perform \emph{Send} or \emph{Recv} operations on a notification, by invoking the corresponding capability. -When a Send operation is performed, the badge of the invoked capability and the -user specified message are bitwise ORed with the corresponding values in the +When a Send operation is performed, the badge of the invoked capability is bitwise ORed with the corresponding values in the endpoint to produce its new contents. This operation is guaranteed not to block a sufficiently authorised sender, even if there is no thread waiting to receive -the message. The Wait operation, on the other hand, is blocking --- if the +the message. The Recv operation, on the other hand, can be blocking --- unless the operation is specifically non-blocking, if the buffer is empty, the thread is blocked until a message arrives. However, in -case of a non-empty buffer, the Wait operation will read the contents of the +case of a non-empty buffer, the Recv operation will read the contents of the buffer, reset it to zero, and returns the value immediately. -Similar to synchronous endpoints, multiple threads may perform Signal or Wait +Similar to synchronous endpoints, multiple threads may perform Signal or Recv operations on the same notification. When there are multiple messages sent to an endpoint before any thread attempts to receive from it, the identifier and the message delivered to the receiver are the bitwise OR of diff --git a/haskell/doc/refman.tex b/haskell/doc/refman.tex index 33ee6107b1b13241e31578f925323aab135895cf..1bf16338d5d0272dd3da04300cde9b3b6a58be82 100644 --- a/haskell/doc/refman.tex +++ b/haskell/doc/refman.tex @@ -76,7 +76,7 @@ \typeout{If TeX stops here, run mkfunctions.pl to generate functions.aux} \input{functions.aux} -\hyphenation{C-Space C-Spaces C-Node C-Nodes Has-kell Send-Wait Ex-change-Reg-ist-ers Thread-Con-trol} +\hyphenation{C-Space C-Spaces C-Node C-Nodes Has-kell Send-Recv Ex-change-Reg-ist-ers Thread-Con-trol} \begin{document} diff --git a/haskell/src/SEL4/API/Syscall.lhs b/haskell/src/SEL4/API/Syscall.lhs index 9e64b6b497b46a0828a77da07591c6adfc64d577..d2332bef6df81c2c81accf322a60045e0bef1032 100644 --- a/haskell/src/SEL4/API/Syscall.lhs +++ b/haskell/src/SEL4/API/Syscall.lhs @@ -60,11 +60,11 @@ the enumerated type "Syscall": > = SysSend > | SysNBSend > | SysCall -> | SysWait +> | SysRecv > | SysReply -> | SysReplyWait +> | SysReplyRecv > | SysYield -> | SysNBWait +> | SysNBRecv > deriving (Show, Enum, Bounded, Eq) \subsection{Handling Events} @@ -83,13 +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 True +> SysRecv -> withoutPreemption $ handleRecv True > SysReply -> withoutPreemption handleReply -> SysReplyWait -> withoutPreemption $ do +> SysReplyRecv -> withoutPreemption $ do > handleReply -> handleWait True +> handleRecv True > SysYield -> withoutPreemption handleYield -> SysNBWait -> withoutPreemption $ handleWait False +> SysNBRecv -> withoutPreemption $ handleRecv False \subsubsection{Interrupts} @@ -153,9 +153,9 @@ The "Call" system call is similar to "Send", but it also requests a reply. For k \subsubsection{Reply System Call} -The "Reply" system call attempts to perform an immediate IPC transfer to the thread that sent the message received by the last successful "Wait" call. If this is not possible, the reply will be silently dropped. The transfer will succeed if: +The "Reply" system call attempts to perform an immediate IPC transfer to the thread that sent the message received by the last successful "Recv" call. If this is not possible, the reply will be silently dropped. The transfer will succeed if: \begin{itemize} - \item there has been no other "Reply" call since the last successful "Wait" call; + \item there has been no other "Reply" call since the last successful "Recv" call; \item the sender used "Call" to generate a reply capability; \item the sender has not been halted or restarted while waiting for a reply; and \item the reply capability has not been moved aside. @@ -174,12 +174,12 @@ The "Reply" system call attempts to perform an immediate IPC transfer to the thr > NullCap -> return () > _ -> fail "handleReply: invalid caller cap" -\subsubsection{Wait System Call} +\subsubsection{Recv System Call} -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. +The "Recv" 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 :: Bool -> Kernel () -> handleWait isBlocking = do +> handleRecv :: Bool -> Kernel () +> handleRecv isBlocking = do > thread <- getCurThread > epCPtr <- asUser thread $ liftM CPtr $ getRegister capRegister > (capFaultOnFailure epCPtr True $ do diff --git a/haskell/src/SEL4/Kernel/Thread.lhs b/haskell/src/SEL4/Kernel/Thread.lhs index a9f2182f69f8d7cd057da62a901e47ef853d63db..2997ee98fcf3a7fa1680c56e39deb5b3f5575f58 100644 --- a/haskell/src/SEL4/Kernel/Thread.lhs +++ b/haskell/src/SEL4/Kernel/Thread.lhs @@ -168,7 +168,7 @@ If the sent message is a fault IPC, the stored fault is transferred. > Just _ -> do > doFaultTransfer badge sender receiver receiveBuffer -Replies sent by the "Reply" and "ReplyWait" system calls can either be normal IPC replies, or fault replies. In the former case, the transfer is the same as for an IPC send, but there is never a fault, capability grants are always allowed, the badge is always 0, and capabilities are never received with diminished rights. +Replies sent by the "Reply" and "ReplyRecv" system calls can either be normal IPC replies, or fault replies. In the former case, the transfer is the same as for an IPC send, but there is never a fault, capability grants are always allowed, the badge is always 0, and capabilities are never received with diminished rights. > doReplyTransfer :: PPtr TCB -> PPtr TCB -> PPtr CTE -> Kernel () > doReplyTransfer sender receiver slot = do diff --git a/haskell/src/SEL4/Object/Endpoint.lhs b/haskell/src/SEL4/Object/Endpoint.lhs index 65af1e49eadd1416709e515b9a9fc45af6e64ff8..a540953f5f701fb193beecac0a06139207d9d50f 100644 --- a/haskell/src/SEL4/Object/Endpoint.lhs +++ b/haskell/src/SEL4/Object/Endpoint.lhs @@ -130,14 +130,14 @@ The IPC receive operation is essentially the same as the send operation, but wit > blockingObject = epptr, > blockingIPCDiminishCaps = diminish }) thread > setEndpoint epptr $ RecvEP [thread] -> False -> doNBWaitFailedTransfer thread +> False -> doNBRecvFailedTransfer thread > RecvEP queue -> case isBlocking of > True -> do > setThreadState (BlockedOnReceive { > blockingObject = epptr, > blockingIPCDiminishCaps = diminish }) thread > setEndpoint epptr $ RecvEP $ queue ++ [thread] -> False -> doNBWaitFailedTransfer thread +> False -> doNBRecvFailedTransfer thread > SendEP (sender:queue) -> do > setEndpoint epptr $ case queue of > [] -> IdleEP diff --git a/haskell/src/SEL4/Object/Notification.lhs b/haskell/src/SEL4/Object/Notification.lhs index 9ad150293fecdd253d63114189a26a6401b717ea..3593341c5429a70d6b538d8cbc6dd494c2706293 100644 --- a/haskell/src/SEL4/Object/Notification.lhs +++ b/haskell/src/SEL4/Object/Notification.lhs @@ -14,7 +14,7 @@ This module specifies the behavior of notification objects. > sendSignal, receiveSignal, > cancelAllSignals, cancelSignal, completeSignal, > getNotification, setNotification, doUnbindNotification, unbindNotification, -> unbindMaybeNotification, bindNotification, doNBWaitFailedTransfer +> unbindMaybeNotification, bindNotification, doNBRecvFailedTransfer > ) where \begin{impdetails} @@ -90,8 +90,8 @@ If the notification object is active, new values are calculated and stored in th This function performs an receive signal operation, given a thread pointer and a capability to a notification object. The receive can be either blocking (the thread will be blocked on the notification until a signal arrives) or non-blocking depending on the isBlocking flag. -> doNBWaitFailedTransfer :: PPtr TCB -> Kernel () -> doNBWaitFailedTransfer thread = asUser thread $ setRegister badgeRegister 0 +> doNBRecvFailedTransfer :: PPtr TCB -> Kernel () +> doNBRecvFailedTransfer thread = asUser thread $ setRegister badgeRegister 0 > receiveSignal :: PPtr TCB -> Capability -> Bool -> Kernel () @@ -111,7 +111,7 @@ If the notification object is idle, then it becomes a waiting notification objec > setThreadState (BlockedOnNotification { > waitingOnNotification = ntfnPtr } ) thread > setNotification ntfnPtr $ ntfn {ntfnObj = WaitingNtfn ([thread]) } -> False -> doNBWaitFailedTransfer thread +> False -> doNBRecvFailedTransfer thread If the notification object is already waiting, the current thread is blocked and added to the queue. Note that this case cannot occur when the notification object is bound, as only the associated thread can wait on it. @@ -120,7 +120,7 @@ If the notification object is already waiting, the current thread is blocked and > setThreadState (BlockedOnNotification { > waitingOnNotification = ntfnPtr } ) thread > setNotification ntfnPtr $ ntfn {ntfnObj = WaitingNtfn (queue ++ [thread]) } -> False -> doNBWaitFailedTransfer thread +> False -> doNBRecvFailedTransfer thread If the notification object is active, the badge of the invoked notification object capability will be loaded to the badge of the receiving thread and the notification object will be marked as idle. diff --git a/haskell/src/SEL4/Object/ObjectType.lhs b/haskell/src/SEL4/Object/ObjectType.lhs index 0fa38503c6a843f114a211439f57e0fe78856d6c..bf15436130fdba9efeafb5daaf1f9672c83a7751 100644 --- a/haskell/src/SEL4/Object/ObjectType.lhs +++ b/haskell/src/SEL4/Object/ObjectType.lhs @@ -413,7 +413,7 @@ New threads are placed in the current security domain, which must be the domain \subsection{Invoking Objects} -The following functions are used to handle messages that are sent to kernel objects by user level code using a "Send" or "SendWait" system call. +The following functions are used to handle messages that are sent to kernel objects by user level code using a "Send" or "SendRecv" system call. The "decodeInvocation" function parses the message, determines the operation that is being performed, and checks for any error conditions. If it returns successfully, the invocation is guaranteed to complete without any errors. diff --git a/haskell/src/SEL4/Object/TCB.lhs b/haskell/src/SEL4/Object/TCB.lhs index f2ae0d45c7fb79cfa67b45fe8aee58d6dff2d398..7ed6cfeb03cb94c41251a6006a6ddb3d2baf773c 100644 --- a/haskell/src/SEL4/Object/TCB.lhs +++ b/haskell/src/SEL4/Object/TCB.lhs @@ -641,7 +641,7 @@ When a message is transferred after a "Call" operation or a fault, the kernel pl > "Caller cap must not already exist" > cteInsert (ReplyCap sender False) replySlot callerSlot -When a new "Wait" operation begins, the caller slot in the waiting thread's TCB is cleared. This removes any ambiguity about the source of the capability in the caller slot: if one is present, it was always generated by the most recent "Wait". +When a new "Recv" operation begins, the caller slot in the waiting thread's TCB is cleared. This removes any ambiguity about the source of the capability in the caller slot: if one is present, it was always generated by the most recent "Recv". > deleteCallerCap :: PPtr TCB -> Kernel () > deleteCallerCap receiver = do diff --git a/include/api/syscall.xml b/include/api/syscall.xml index 1439680c3b260974316e3c72d2550da9ff2f6957..980bdd50f692316d27c245c1b4444443d0f1b9ec 100644 --- a/include/api/syscall.xml +++ b/include/api/syscall.xml @@ -14,13 +14,13 @@ <api> <config> <syscall name="Call" /> - <syscall name="ReplyWait" /> + <syscall name="ReplyRecv" /> <syscall name="Send" /> <syscall name="NBSend" /> - <syscall name="Wait" /> + <syscall name="Recv" /> <syscall name="Reply" /> <syscall name="Yield" /> - <syscall name="NBWait" /> + <syscall name="NBRecv" /> </config> </api> <!-- Syscalls on the unknown syscall path. These definitions will be wrapped in #ifdef name --> diff --git a/include/arch/arm/arch/fastpath/fastpath.h b/include/arch/arm/arch/fastpath/fastpath.h index a6fb15cfc04b06e0a9c04466d4bf1af4edb3798c..e5a52c2f728944815442f1746c98ca245701df6b 100644 --- a/include/arch/arm/arch/fastpath/fastpath.h +++ b/include/arch/arm/arch/fastpath/fastpath.h @@ -20,7 +20,7 @@ * assumptions. Because compile_asserts are hard to do in assembler, * we place them here */ compile_assert(SysCall_Minus1, SysCall == -1) -compile_assert(SysReplyWait_Minus2, SysReplyWait == -2) +compile_assert(SysReplyRecv_Minus2, SysReplyRecv == -2) /** DONT_TRANSLATE */ static inline void @@ -118,8 +118,8 @@ VISIBLE NORETURN; void fastpath_call(word_t cptr, word_t r_msgInfo) VISIBLE NORETURN SECTION(".vectors.fastpath_call"); -void fastpath_reply_wait(word_t cptr, word_t r_msgInfo) -VISIBLE NORETURN SECTION(".vectors.fastpath_reply_wait"); +void fastpath_reply_recv(word_t cptr, word_t r_msgInfo) +VISIBLE NORETURN SECTION(".vectors.fastpath_reply_recv"); #endif diff --git a/include/arch/x86/arch/fastpath/fastpath.h b/include/arch/x86/arch/fastpath/fastpath.h index 578ce421e19863a47c5ed14fba318d022d546e12..6a90cf50df0968ba590d0fc8e6b8b28150640013 100644 --- a/include/arch/x86/arch/fastpath/fastpath.h +++ b/include/arch/x86/arch/fastpath/fastpath.h @@ -184,7 +184,7 @@ NORETURN; void fastpath_call(word_t cptr, word_t r_msgInfo) VISIBLE FASTCALL NORETURN; -void fastpath_reply_wait(word_t cptr, word_t r_msgInfo) +void fastpath_reply_recv(word_t cptr, word_t r_msgInfo) VISIBLE FASTCALL NORETURN; #endif diff --git a/include/kernel/thread.h b/include/kernel/thread.h index 3b62e4817eb698002419fb0b6ce5b942931d2d6c..7d92748cd3025179dbd8be4a9bc89a6d00bbb9a3 100644 --- a/include/kernel/thread.h +++ b/include/kernel/thread.h @@ -52,7 +52,7 @@ void doNormalTransfer(tcb_t *sender, word_t *sendBuffer, endpoint_t *endpoint, word_t *receiveBuffer, bool_t diminish); void doFaultTransfer(word_t badge, tcb_t *sender, tcb_t *receiver, word_t *receiverIPCBuffer); -void doNBWaitFailedTransfer(tcb_t *thread); +void doNBRecvFailedTransfer(tcb_t *thread); void schedule(void); void chooseThread(void); void switchToThread(tcb_t *thread) VISIBLE; diff --git a/libsel4/arch_include/arm/sel4/arch/deprecated.h b/libsel4/arch_include/arm/sel4/arch/deprecated.h new file mode 100644 index 0000000000000000000000000000000000000000..82be1c29b91aeccce760cb94b2b7e48e3233cc86 --- /dev/null +++ b/libsel4/arch_include/arm/sel4/arch/deprecated.h @@ -0,0 +1,27 @@ +/* + * Copyright 2014, NICTA + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(NICTA_BSD) + */ + +#ifndef __LIBSEL4_ARCH_DEPRECATED_H +#define __LIBSEL4_ARCH_DEPRECATED_H + +#include <autoconf.h> +#include <sel4/types.h> +#include <sel4/arch/syscalls.h> + +#ifdef CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS +static inline seL4_MessageInfo_t __attribute__((deprecated("Use seL4_ReplyRecvWithMRs"))) +seL4_ReplyWaitWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, + seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) +{ + return seL4_ReplyRecvWithMRs(src, msgInfo, sender, mr0, mr1, mr2, mr3); +} + +#endif /* CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS */ +#endif /* __ARCH_DEPRECATED_H__ */ diff --git a/libsel4/arch_include/arm/sel4/arch/syscalls.h b/libsel4/arch_include/arm/sel4/arch/syscalls.h index 84ffc2c8f9472175dbd5c469ac5c2886e28ebf1d..d4ce45fe907482b98543d7a04d5ab06e8d35552c 100644 --- a/libsel4/arch_include/arm/sel4/arch/syscalls.h +++ b/libsel4/arch_include/arm/sel4/arch/syscalls.h @@ -204,7 +204,7 @@ seL4_Signal(seL4_CPtr dest) } static inline seL4_MessageInfo_t -seL4_Wait(seL4_CPtr src, seL4_Word* sender) +seL4_Recv(seL4_CPtr src, seL4_Word* sender) { register seL4_Word src_and_badge asm("r0") = (seL4_Word)src; register seL4_MessageInfo_t info asm("r1"); @@ -216,11 +216,11 @@ seL4_Wait(seL4_CPtr src, seL4_Word* sender) register seL4_Word msg3 asm("r5"); /* Perform the system call. */ - register seL4_Word scno asm("r7") = seL4_SysWait; + register seL4_Word scno asm("r7") = seL4_SysRecv; asm volatile ("swi %[swi_num]" : "=r" (msg0), "=r" (msg1), "=r" (msg2), "=r" (msg3), "=r" (info), "+r" (src_and_badge) - : [swi_num] "i" __SWINUM(seL4_SysWait), "r"(scno) + : [swi_num] "i" __SWINUM(seL4_SysRecv), "r"(scno) : "memory"); /* Write the message back out to memory. */ @@ -238,9 +238,15 @@ seL4_Wait(seL4_CPtr src, seL4_Word* sender) }; } +static inline void +seL4_Wait(seL4_CPtr src, seL4_Word *sender) +{ + seL4_Recv(src, sender); +} + #ifdef CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS static inline seL4_MessageInfo_t -seL4_WaitWithMRs(seL4_CPtr src, seL4_Word* sender, +seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) { register seL4_Word src_and_badge asm("r0") = (seL4_Word)src; @@ -253,11 +259,11 @@ seL4_WaitWithMRs(seL4_CPtr src, seL4_Word* sender, register seL4_Word msg3 asm("r5"); /* Perform the system call. */ - register seL4_Word scno asm("r7") = seL4_SysWait; + register seL4_Word scno asm("r7") = seL4_SysRecv; asm volatile ("swi %[swi_num]" : "=r" (msg0), "=r" (msg1), "=r" (msg2), "=r" (msg3), "=r" (info.words[0]), "+r" (src_and_badge) - : [swi_num] "i" __SWINUM(seL4_SysWait), "r"(scno) + : [swi_num] "i" __SWINUM(seL4_SysRecv), "r"(scno) : "memory"); /* Write the message back out to memory. */ @@ -282,10 +288,11 @@ 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) +seL4_NBRecv(seL4_CPtr src, seL4_Word* sender) { register seL4_Word src_and_badge asm("r0") = (seL4_Word)src; register seL4_MessageInfo_t info asm("r1"); @@ -297,11 +304,11 @@ seL4_NBWait(seL4_CPtr src, seL4_Word* sender) register seL4_Word msg3 asm("r5"); /* Perform the system call. */ - register seL4_Word scno asm("r7") = seL4_SysNBWait; + register seL4_Word scno asm("r7") = seL4_SysNBRecv; 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) + : [swi_num] "i" __SWINUM(seL4_SysNBRecv), "r"(scno) : "memory"); /* Write the message back out to memory. */ @@ -319,6 +326,12 @@ seL4_NBWait(seL4_CPtr src, seL4_Word* sender) }; } +static inline seL4_MessageInfo_t +seL4_Poll(seL4_CPtr src, seL4_Word* sender) +{ + return seL4_NBRecv(src, sender); +} + static inline seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) { @@ -406,7 +419,7 @@ seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, #endif static inline seL4_MessageInfo_t -seL4_ReplyWait(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender) +seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender) { register seL4_Word src_and_badge asm("r0") = (seL4_Word)src; register seL4_MessageInfo_t info asm("r1") = msgInfo; @@ -418,11 +431,11 @@ seL4_ReplyWait(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender) register seL4_Word msg3 asm("r5") = seL4_GetMR(3); /* Perform the syscall. */ - register seL4_Word scno asm("r7") = seL4_SysReplyWait; + register seL4_Word scno asm("r7") = seL4_SysReplyRecv; asm volatile ("swi %[swi_num]" : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3), "+r" (info), "+r" (src_and_badge) - : [swi_num] "i" __SWINUM(seL4_SysReplyWait), "r"(scno) + : [swi_num] "i" __SWINUM(seL4_SysReplyRecv), "r"(scno) : "memory"); /* Write the message back out to memory. */ @@ -442,7 +455,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_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3) { register seL4_Word src_and_badge asm("r0") = (seL4_Word)src; @@ -453,7 +466,7 @@ seL4_ReplyWaitWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *send register seL4_Word msg1 asm("r3"); register seL4_Word msg2 asm("r4"); register seL4_Word msg3 asm("r5"); - register seL4_Word scno asm("r7") = seL4_SysReplyWait; + register seL4_Word scno asm("r7") = seL4_SysReplyRecv; if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) { msg0 = *mr0; @@ -472,7 +485,7 @@ seL4_ReplyWaitWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *send asm volatile ("swi %[swi_num]" : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3), "+r" (info), "+r" (src_and_badge) - : [swi_num] "i" __SWINUM(seL4_SysReplyWait), "r"(scno) + : [swi_num] "i" __SWINUM(seL4_SysReplyRecv), "r"(scno) : "memory"); /* Write out the data back to memory. */ diff --git a/libsel4/arch_include/x86/sel4/arch/deprecated.h b/libsel4/arch_include/x86/sel4/arch/deprecated.h new file mode 100644 index 0000000000000000000000000000000000000000..698b2b51503c83d2196273a7b97eea56a28127b9 --- /dev/null +++ b/libsel4/arch_include/x86/sel4/arch/deprecated.h @@ -0,0 +1,26 @@ +/* + * Copyright 2014, NICTA + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(NICTA_BSD) + */ + +#ifndef __LIBSEL4_ARCH_DEPRECATED_H +#define __LIBSEL4_ARCH_DEPRECATED_H + +#include <autoconf.h> +#include <sel4/types.h> +#include <sel4/arch/syscalls.h> + +#ifdef CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS +static inline seL4_MessageInfo_t __attribute__((deprecated("Use seL4_ReplyRecvWithMRs"))) +seL4_ReplyWaitWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, + seL4_Word *mr0, seL4_Word *mr1) +{ + return seL4_ReplyRecvWithMRs(src, msgInfo, sender, mr0, mr1); +} +#endif /* CONFIG_LIB_SEL4_HAVE_REGISTER_STUBS */ +#endif /* __ARCH_DEPRECATED_H__ */ diff --git a/libsel4/arch_include/x86/sel4/arch/syscalls.h b/libsel4/arch_include/x86/sel4/arch/syscalls.h index 4a45660dabe7df7266e885c69519ced5d4ab54fd..d277a1164a96a74154eaaab5c83700d7356e6c5d 100644 --- a/libsel4/arch_include/x86/sel4/arch/syscalls.h +++ b/libsel4/arch_include/x86/sel4/arch/syscalls.h @@ -161,7 +161,7 @@ seL4_Signal(seL4_CPtr dest) } static inline seL4_MessageInfo_t -seL4_Wait(seL4_CPtr src, seL4_Word* sender) +seL4_Recv(seL4_CPtr src, seL4_Word* sender) { seL4_MessageInfo_t info; seL4_Word badge; @@ -181,7 +181,7 @@ seL4_Wait(seL4_CPtr src, seL4_Word* sender) "=S" (info.words[0]), "=D" (mr0), "=c" (mr1) - : "a" (seL4_SysWait), + : "a" (seL4_SysRecv), "b" (src) : "%edx", "memory" ); @@ -196,8 +196,14 @@ seL4_Wait(seL4_CPtr src, seL4_Word* sender) return info; } +static inline void +seL4_Wait(seL4_CPtr src, seL4_Word *sender) +{ + seL4_Recv(src, sender); +} + static inline seL4_MessageInfo_t -seL4_WaitWithMRs(seL4_CPtr src, seL4_Word* sender, +seL4_RecvWithMRs(seL4_CPtr src, seL4_Word* sender, seL4_Word *mr0, seL4_Word *mr1) { seL4_MessageInfo_t info; @@ -218,7 +224,7 @@ seL4_WaitWithMRs(seL4_CPtr src, seL4_Word* sender, "=S" (info.words[0]), "=D" (msg0), "=c" (msg1) - : "a" (seL4_SysWait), + : "a" (seL4_SysRecv), "b" (src) : "%edx", "memory" ); @@ -238,7 +244,7 @@ seL4_WaitWithMRs(seL4_CPtr src, seL4_Word* sender, } static inline seL4_MessageInfo_t -seL4_NBWait(seL4_CPtr src, seL4_Word* sender) +seL4_NBRecv(seL4_CPtr src, seL4_Word* sender) { seL4_MessageInfo_t info; seL4_Word badge; @@ -258,7 +264,7 @@ seL4_NBWait(seL4_CPtr src, seL4_Word* sender) "=S" (info.words[0]), "=D" (mr0), "=c" (mr1) - : "a" (seL4_SysNBWait), + : "a" (seL4_SysNBRecv), "b" (src) : "%edx", "memory" ); @@ -273,6 +279,12 @@ seL4_NBWait(seL4_CPtr src, seL4_Word* sender) return info; } +static inline seL4_MessageInfo_t +seL4_Poll(seL4_CPtr src, seL4_Word *sender) +{ + return seL4_NBRecv(src, sender); +} + static inline seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo) { @@ -356,7 +368,7 @@ seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, } static inline seL4_MessageInfo_t -seL4_ReplyWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender) +seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender) { seL4_MessageInfo_t info; seL4_Word badge; @@ -377,7 +389,7 @@ seL4_ReplyWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender) "=S" (info.words[0]), "=D" (mr0), "=c" (mr1) - : "a" (seL4_SysReplyWait), + : "a" (seL4_SysReplyRecv), "b" (dest), "S" (msgInfo.words[0]), "D" (mr0), @@ -396,7 +408,7 @@ seL4_ReplyWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender) } static inline seL4_MessageInfo_t -seL4_ReplyWaitWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender, +seL4_ReplyRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_Word *mr0, seL4_Word *mr1) { seL4_MessageInfo_t info; @@ -425,7 +437,7 @@ seL4_ReplyWaitWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sen "=S" (info.words[0]), "=D" (msg0), "=c" (msg1) - : "a" (seL4_SysReplyWait), + : "a" (seL4_SysReplyRecv), "b" (dest), "S" (msgInfo.words[0]), "D" (msg0), diff --git a/libsel4/include/api/syscall.xml b/libsel4/include/api/syscall.xml index 7cacabea4042a789731edbd4169e4c30ca62a073..cbaed650c50f3ce3f2fd7c387eb0a18df800db6b 100644 --- a/libsel4/include/api/syscall.xml +++ b/libsel4/include/api/syscall.xml @@ -14,13 +14,13 @@ <api> <config> <syscall name="Call" /> - <syscall name="ReplyWait" /> + <syscall name="ReplyRecv" /> <syscall name="Send" /> <syscall name="NBSend" /> - <syscall name="Wait" /> + <syscall name="Recv" /> <syscall name="Reply" /> <syscall name="Yield" /> - <syscall name="NBWait" /> + <syscall name="NBRecv" /> </config> </api> <!-- Syscalls on the unknown syscall path. These definitions will be wrapped in #ifdef name --> diff --git a/libsel4/include/sel4/deprecated.h b/libsel4/include/sel4/deprecated.h index 17d4f3e0a7562230186c8d6b055d84afe798bf9f..c6e85c440274a0bcf673066830fea8a77e32e7c9 100644 --- a/libsel4/include/sel4/deprecated.h +++ b/libsel4/include/sel4/deprecated.h @@ -11,6 +11,8 @@ #ifndef __LIBSEL4_DEPRECATED_H #define __LIBSEL4_DEPRECATED_H +#include <sel4/arch/deprecated.h> + static inline int __attribute__((deprecated("use seL4_IRQHandler_SetNotification"))) seL4_IRQHandler_SetEndpoint(seL4_CPtr irq_handler, seL4_CPtr endpoint) { @@ -23,4 +25,11 @@ seL4_Notify(seL4_CPtr dest, __attribute__((unused)) seL4_Word msg) seL4_Signal(dest); } +static inline seL4_MessageInfo_t __attribute__((deprecated("Use seL4_ReplyRecv"))) +seL4_ReplyWait(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender) +{ + return seL4_ReplyRecv(src, msgInfo, sender); +} + #endif // __LIBSEL4_DEPRECATED_H + diff --git a/manual/parts/api.tex b/manual/parts/api.tex index 35820c7d033b9e51d09e748914af2a7a6c95b81a..964adf5142ad32015afc5ed39198b9f985a2043a 100644 --- a/manual/parts/api.tex +++ b/manual/parts/api.tex @@ -240,14 +240,16 @@ complete the \apifunc{seL4\_Untyped\_Retype}{untyped_retype} request. \section{System Calls} \inputapidoc{sel4_send} -\inputapidoc{sel4_wait} +\inputapidoc{sel4_recv} \inputapidoc{sel4_call} \inputapidoc{sel4_reply} \inputapidoc{sel4_nbsend} -\inputapidoc{sel4_replywait} -\inputapidoc{sel4_nbwait} +\inputapidoc{sel4_replyrecv} +\inputapidoc{sel4_nbrecv} \inputapidoc{sel4_yield} \inputapidoc{sel4_signal} +\inputapidoc{sel4_wait} +\inputapidoc{sel4_poll} \clearpage \section{Architecture-Independent Object Methods} diff --git a/manual/parts/api/sel4_nbrecv.tex b/manual/parts/api/sel4_nbrecv.tex new file mode 100644 index 0000000000000000000000000000000000000000..85f7a9dd027aa25850317762e505e84da3226188 --- /dev/null +++ b/manual/parts/api/sel4_nbrecv.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_nbrecv} +{NBRecv} +{Recieve a message from an endpoint but do not block in the case that no messages are pending} +{static inline seL4\_MessageInfo\_t seL4\_NBRecv} +{ +\param{seL4\_CPtr}{src}{\invokedcapdesc} +\param{seL4\_Word*}{sender}{\senderdesc} +} +{\messageinforetdesc} +{See \autoref{sec:sys_nbrecv}} diff --git a/manual/parts/api/sel4_poll.tex b/manual/parts/api/sel4_poll.tex new file mode 100644 index 0000000000000000000000000000000000000000..2799dca7089b5cec07e0d69d88a79a673b6280d7 --- /dev/null +++ b/manual/parts/api/sel4_poll.tex @@ -0,0 +1,29 @@ +% +% 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_poll} +{Poll} +{Perform a non-blocking recv on a notification object.} +{static inline void seL4\_Poll} +{ +\param{seL4\_CPtr}{src}{\invokedcapdesc} +\param{seL4\_Word*}{sender}{\senderdesc} +} +{\noret} +{ +This is not a proper system call +known by the kernel. Rather, it is a convenience +wrapper provided by the seL4 userland library which calls +\apifunc{seL4\_NBRecv}{sel4_nbrecv}. It is +useful for doing a non-blocking wait on a notification. + +See the description of \apifunc{seL4\_NBRecv}{sel4_nbrecv} in \autoref{sec:sys_nbrecv} +} diff --git a/manual/parts/api/sel4_nbwait.tex b/manual/parts/api/sel4_recv.tex similarity index 68% rename from manual/parts/api/sel4_nbwait.tex rename to manual/parts/api/sel4_recv.tex index 17f018834f13f60bd6ba96246cea07363744eba3..2b18494de854079c281abe9532916d3019bd9ec7 100644 --- a/manual/parts/api/sel4_nbwait.tex +++ b/manual/parts/api/sel4_recv.tex @@ -9,13 +9,13 @@ % \apidoc -{sel4_nbwait} -{NBWait} -{Perform a non-blocking wait on an endpoint or notification object} -{static inline seL4\_MessageInfo\_t seL4\_NBWait} +{sel4_recv} +{Recv} +{Block until a message is received on an endpoint} +{static inline seL4\_MessageInfo\_t seL4\_Recv} { \param{seL4\_CPtr}{src}{\invokedcapdesc} \param{seL4\_Word*}{sender}{\senderdesc} } {\messageinforetdesc} -{See \autoref{sec:sys_nbwait}} +{See \autoref{sec:sys_recv}} diff --git a/manual/parts/api/sel4_replywait.tex b/manual/parts/api/sel4_replyrecv.tex similarity index 71% rename from manual/parts/api/sel4_replywait.tex rename to manual/parts/api/sel4_replyrecv.tex index dc5f894f74e5230f2d446b5a7a7de98efc9ceae3..4f283f0be285b700643c7c20b9df0d482776b8ca 100644 --- a/manual/parts/api/sel4_replywait.tex +++ b/manual/parts/api/sel4_replyrecv.tex @@ -9,14 +9,14 @@ % \apidoc -{sel4_replywait} -{Reply Wait} -{Perform a reply followed by a wait in one system call} -{static inline seL4\_MessageInfo\_t seL4\_ReplyWait} +{sel4_replyrecv} +{Reply Recv} +{Perform a reply followed by a recv in one system call} +{static inline seL4\_MessageInfo\_t seL4\_ReplyRecv} { \param{seL4\_CPtr}{dest}{\invokedcapdesc} \param{seL4\_MessageInfo\_t}{msgInfo}{\messageinfodesc} \param{seL4\_Word*}{sender}{\senderdesc} } {\messageinforetdesc} -{See \autoref{sec:sys_replywait}} +{See \autoref{sec:sys_replyrecv}} diff --git a/manual/parts/api/sel4_wait.tex b/manual/parts/api/sel4_wait.tex index 3a69bdcfeb86f58a626216808e97b448e14dabfa..cf49bbf30df3b19d0a5de2b14e8e1ab33c26a24d 100644 --- a/manual/parts/api/sel4_wait.tex +++ b/manual/parts/api/sel4_wait.tex @@ -11,11 +11,18 @@ \apidoc {sel4_wait} {Wait} -{Wait on an endpoint or notification} -{static inline seL4\_MessageInfo\_t seL4\_Wait} +{Perform a receive on a notification object.} +{static inline void seL4\_Wait} { \param{seL4\_CPtr}{src}{\invokedcapdesc} \param{seL4\_Word*}{sender}{\senderdesc} } -{\messageinforetdesc} -{See \autoref{sec:sys_wait}} +{\noret} +{This is not a proper system call +known by the kernel. Rather, it is a convenience +wrapper provided by the seL4 userland library which calls +\apifunc{seL4\_Recv}{sel4_recv}. + +See the description of \apifunc{seL4\_Recv}{sel4_recv} in \autoref{sec:sys_recv} +} + diff --git a/manual/parts/cspace.tex b/manual/parts/cspace.tex index 3d0cd5f9bfde6ecb3016c74df5217ff688c9675d..78e27455445eae645a75088ac5cd4d7199f857cc 100644 --- a/manual/parts/cspace.tex +++ b/manual/parts/cspace.tex @@ -150,7 +150,7 @@ silently downgraded to those of the source. \toprule Type & Read & Write & Grant \\ \midrule - \obj{Endpoint} & Required to wait. & Required to send. & Required to send capabilities (including reply capabilities).\\ + \obj{Endpoint} & Required to receive. & Required to send. & Required to send capabilities (including reply capabilities).\\ \obj{Notification} & Required to wait. & Required to signal. & N/A \\ \obj{Page} & Required to map the page readable. & Required to map the page writable. & N/A \\ \bottomrule diff --git a/manual/parts/io.tex b/manual/parts/io.tex index f8770ce97a608959087e3e7223043e44f3be17bb..893be38a9992d28f6fd5513272132e7bfeb2e72c 100644 --- a/manual/parts/io.tex +++ b/manual/parts/io.tex @@ -16,9 +16,10 @@ Interrupts are delivered as notifications. A thread may configure the kernel to signal a particular \obj{Notification} object each time a certain interrupt triggers. Threads may then wait for -interrupts to occur by calling \apifunc{seL4\_Wait}{sel4_wait} on +interrupts to occur by calling \apifunc{seL4\_Wait}{sel4_wait} or +\apifunc{seL4\_Poll}{sel4_poll} on that \obj{Notification}. In the notification word returned from -\apifunc{seL4\_Wait}{sel4_wait}, bit $n$ (modulo +either call, bit $n$ (modulo word size) represents IRQ $n$, the bit will be set if the corresponding IRQ was raised. This supports the use of a single handler for multiple IRQs. @@ -30,7 +31,8 @@ configure a certain interrupt. They have three methods: \item[\apifunc{seL4\_IRQHandler\_SetNotification}{irq_handlersetnotification}] specifies the \obj{Notification} the kernel should \apifunc{signal}{sel4_signal} when an interrupt occurs. A driver - may then call \apifunc{seL4\_Wait}{sel4_wait} on this notification to + may then call \apifunc{seL4\_Wait}{sel4_wait} or \apifunc{seL4\_Poll}{sel4_poll} + on this notification to wait for interrupts to arrive. \item[\apifunc{seL4\_IRQHandler\_Ack}{irq_handleracknowledge}] diff --git a/manual/parts/ipc.tex b/manual/parts/ipc.tex index 59bd12bf01091fed9c40bc008fd313d298dd4465..045c236a34207cc4d3ad82ffff72f5775444920d 100644 --- a/manual/parts/ipc.tex +++ b/manual/parts/ipc.tex @@ -150,8 +150,8 @@ 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\_Wait}{sel4_wait} -system call or the second half of \apifunc{seL4\_ReplyWait}{sel4_replywait} +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}} @@ -239,9 +239,9 @@ conditions are: no longer be valid. \item The destination slot cannot be looked up. Unlike the send - system call, the \apifunc{seL4\_Wait}{sel4_wait} system call does not check that the - destination slot exists and is empty before it initiates the wait. - Hence, the \apifunc{seL4\_Wait}{sel4_wait} system call will not fail with an error if the + 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. diff --git a/manual/parts/notifications.tex b/manual/parts/notifications.tex index 35d8bd5dcc9fece39fd855bc5888021d7c677e26..e5ad5e18f38145999975ae5ecee090d53373471c 100644 --- a/manual/parts/notifications.tex +++ b/manual/parts/notifications.tex @@ -28,7 +28,7 @@ capabilities, badged \obj{Notification} capabilities cannot be unbadged, rebadged or used to create child capabilities with different badges. \label{s:notif-badge} -\section{Signalling and Waiting} +\section{Signalling, Polling and Waiting} The \apifunc{seL4\_Signal}{sel4_signal} method updates the notification word by bit-wise \texttt{or}-ing it with the \emph{badge} @@ -46,6 +46,10 @@ invoker blocks. Else, the call returns immediately, setting the notification word to zero and returning to the invoker the previous notification-word value. +The \apifunc{seL4\_Poll}{sel4_poll} is the same as \apifunc{seL4\_Wait}{sel4_wait}, except if +no signals are pending (the notification word is 0) the call will return immediately +without blocking. + If threads are waiting on the \obj{Notification} object at the time \apifunc{seL4\_Signal}{sel4_signal} is invoked, the first queued thread receives the notification. All other threads keep waiting until the @@ -62,8 +66,8 @@ an unbadged capability has no effect. \obj{Notification} objects and \obj{TCB}s can be bound together in a 1-to-1 relationship through the \apifunc{seL4\_TCB\_BindNotification}{tcb_bindnotification} invocation. When a -\obj{Notification} is bound to a \obj{TCB}, messages to that notification -will be delivered even if the thread is waiting on an IPC +\obj{Notification} is bound to a \obj{TCB}, signals to that notification object +will be delivered even if the thread is receiving from an IPC endpoint. To distinguish whether the received message was a notification or an IPC, developers should check the badge value. By reserving a specific badge (or range of badges) for capabilities to the bound diff --git a/manual/parts/objects.tex b/manual/parts/objects.tex index 862e70ccbb2607e6cb23d9895ada3c9b4671a156..fb61b40617f34c9e5a3aad04ca2ec563b1162f05 100644 --- a/manual/parts/objects.tex +++ b/manual/parts/objects.tex @@ -94,12 +94,12 @@ capabilities through the system is controlled by a \section{System Calls} \label{sec:syscalls} \label{sec:sys_send} -\label{sec:sys_wait} +\label{sec:sys_recv} \label{sec:sys_call} \label{sec:sys_reply} \label{sec:sys_nbsend} -\label{sec:sys_replywait} -\label{sec:sys_nbwait} +\label{sec:sys_replyrecv} +\label{sec:sys_nbrecv} \label{sec:sys_yield} The seL4 kernel provides a message-passing service for communication between @@ -144,7 +144,7 @@ The complete set of system calls is: \apifunc{seL4\_Send}{sel4_send}, no error code or response will be returned. \item[\apifunc{seL4\_Call}{sel4_call}] combines \apifunc{seL4\_Send}{sel4_send} - and \apifunc{seL4\_Wait}{sel4_wait}. The call + and \apifunc{seL4\_Recv}{sel4_recv}. The call blocks the sending thread until its message is delivered and a reply message is received. When the sent message is delivered to another thread (via an \obj{Endpoint}), the kernel adds an @@ -158,11 +158,11 @@ The complete set of system calls is: efficiency reasons (combining two operations into a single system call). It differs from \apifunc{seL4\_Send}{sel4_send} immediately followed by - \apifunc{seL4\_Wait}{sel4_wait} in two ways: + \apifunc{seL4\_Recv}{sel4_recv} in two ways: \begin{enumerate} \item the single-use reply capability is created to establish a reply channel with minimal trust; - \item the transition from send to wait phase is atomic, meaning it + \item the transition from send to recv phase is atomic, meaning it cannot be preempted, and the receiver can reply without any risk of blocking. \end{enumerate} @@ -171,7 +171,7 @@ The complete set of system calls is: \apifunc{seL4\_Call}{sel4_call} allows the kernel to return an error code or other response through the reply message. - \item[\apifunc{seL4\_Wait}{sel4_wait}] is used by a thread to receive + \item[\apifunc{seL4\_Recv}{sel4_recv}] is used by a thread to receive messages through endpoints or notifications. If no sender or notification is pending, the caller will block until a message or notification can be delivered. This system call works only on @@ -192,15 +192,15 @@ The complete set of system calls is: capability into regular capability space, where it can be used with \apifunc{seL4\_Send}{sel4_send}. - \item[\apifunc{seL4\_ReplyWait}{sel4_replywait}] combines \apifunc{seL4\_Reply}{sel4_reply} and - \apifunc{seL4\_Wait}{sel4_wait}. It exists mostly for efficiency reasons: the common case of + \item[\apifunc{seL4\_ReplyRecv}{sel4_replyrecv}] combines \apifunc{seL4\_Reply}{sel4_reply} and + \apifunc{seL4\_Recv}{sel4_recv}. It exists mostly for efficiency reasons: the common case of replying to a request and waiting for the next can be performed in a single kernel system call instead of two. The transition from - the reply to the wait phase is also atomic. + the reply to the receive 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 + \item[\apifunc{seL4\_NBRecv}{sel4_nbrecv}] is used by a thread to check for + signals pending on a notification object or messages pending on an endpoint without blocking. + This system call works only on endpoints and notification object capabilities, raising a fault (see section \ref{sec:faults}) when attempted with other capability types. @@ -251,7 +251,8 @@ manipulation, and combination of these kernel objects: provide a simple signalling mechanism. A \obj{Notification} is a word-size array of flags, each of which behaves like a binary semaphore. Operations are \emph{signalling} a subset of flags in a single operation, - and waiting until any are signalled. Notification capabilities + polling to check any flags, + and blocking until any are signalled. Notification capabilities can be signal-only or wait-only. \item[Virtual Address Space Objects] (see \autoref{ch:vspace}) diff --git a/manual/parts/threads.tex b/manual/parts/threads.tex index b5469293567b010838ff1fb3f15fd7d62c402702..2fc1a8ecef6259d530824bcf8c2e7e084f3e3259 100644 --- a/manual/parts/threads.tex +++ b/manual/parts/threads.tex @@ -157,9 +157,8 @@ invalid capabilities silently fail). In this case, the capability on which the fault occurred may be the capability being invoked or an extra capability passed in the \texttt{caps} field in the IPC buffer. -Secondly, a capability fault can occur when \apifunc{seL4\_Wait}{sel4_wait} is -called on a capability that -does not exist, is not an endpoint or notification capability or does not have +Secondly, a capability fault can occur when \apifunc{seL4\_Recv}{sel4_recv} or \apifunc{seL4\_NBRecv}{sel4_nbrecv} +is called on a capability that does not exist, is not an endpoint or notification capability or does not have receive permissions. Replying to the fault IPC will restart the faulting thread. The contents of the @@ -172,7 +171,7 @@ IPC message are given in \autoref{tbl:ipc_contents}.\\ \midrule Address at which to restart execution & \ipcbloc{IPCBuffer[0]} \\ Capability address & \ipcbloc{IPCBuffer[1]}\\ -In receive phase (1 if the fault happened during a wait system call, 0 +In receive phase (1 if the fault happened during a receive system call, 0 otherwise) & \ipcbloc{IPCBuffer[2]}\\ Lookup failure description. As described in \autoref{sec:lookup_fail_desc} & \ipcbloc{IPCBuffer[3..]}\\ diff --git a/src/api/syscall.c b/src/api/syscall.c index a5c0fadb2906dd2c247166c9efdda5e9012fa0e2..7b45cb4863edd3f7f37a2969dc232c0ac98c1ad6 100644 --- a/src/api/syscall.c +++ b/src/api/syscall.c @@ -309,7 +309,7 @@ handleReply(void) } static void -handleWait(bool_t isBlocking) +handleRecv(bool_t isBlocking) { word_t epCPtr; lookupCap_ret_t lu_ret; @@ -406,21 +406,21 @@ handleSyscall(syscall_t syscall) } break; - case SysWait: - handleWait(true); + case SysRecv: + handleRecv(true); break; case SysReply: handleReply(); break; - case SysReplyWait: + case SysReplyRecv: handleReply(); - handleWait(true); + handleRecv(true); break; - case SysNBWait: - handleWait(false); + case SysNBRecv: + handleRecv(false); break; case SysYield: diff --git a/src/arch/arm/traps.S b/src/arch/arm/traps.S index f07f5348560484324c82fd37f388bbd20714382d..567032fa93343a1f7e422d2cedb37c36853ae84e 100644 --- a/src/arch/arm/traps.S +++ b/src/arch/arm/traps.S @@ -91,7 +91,7 @@ BEGIN_FUNC(arm_swi_syscall) str lr, [sp, #(PT_FaultInstruction - PT_LR_svc)] #ifdef FASTPATH - cmp r7, #SYSCALL_REPLY_WAIT + cmp r7, #SYSCALL_REPLY_RECV #endif /* Stack all user registers */ @@ -108,7 +108,7 @@ BEGIN_FUNC(arm_swi_syscall) * greater than -2. */ bhi fastpath_call - beq fastpath_reply_wait + beq fastpath_reply_recv #endif /* Load system call number for handleSyscall and handleUnknownSyscall() */ diff --git a/src/arch/x86/c_traps.c b/src/arch/x86/c_traps.c index 5332ec03becf75be9720fc8aab2d0d301d4682d8..675cf9f5bef3b0eb27f4dd0cd847797d4cb3f574 100644 --- a/src/arch/x86/c_traps.c +++ b/src/arch/x86/c_traps.c @@ -163,8 +163,8 @@ void VISIBLE c_handle_syscall(syscall_t syscall, word_t cptr, word_t msgInfo) #ifdef FASTPATH if (syscall == SysCall) { fastpath_call(cptr, msgInfo); - } else if (syscall == SysReplyWait) { - fastpath_reply_wait(cptr, msgInfo); + } else if (syscall == SysReplyRecv) { + fastpath_reply_recv(cptr, msgInfo); } #endif diff --git a/src/fastpath/fastpath.c b/src/fastpath/fastpath.c index 2d3a3996a7158d7a226d4b1857e3e94b9acf379f..a2dfbb080c643f8168074cb6cbfdd03ff9828997 100644 --- a/src/fastpath/fastpath.c +++ b/src/fastpath/fastpath.c @@ -155,7 +155,7 @@ void #ifdef ARCH_IA32 FASTCALL #endif -fastpath_reply_wait(word_t cptr, word_t msgInfo) +fastpath_reply_recv(word_t cptr, word_t msgInfo) { message_info_t info; cap_t ep_cap; @@ -181,7 +181,7 @@ fastpath_reply_wait(word_t cptr, word_t msgInfo) * saved fault. */ if (unlikely(fastpath_mi_check(msgInfo) || fault_type != fault_null_fault)) { - slowpath(SysReplyWait); + slowpath(SysReplyRecv); } /* Lookup the cap */ @@ -191,13 +191,13 @@ fastpath_reply_wait(word_t cptr, word_t msgInfo) /* Check it's an endpoint */ if (unlikely(!cap_capType_equals(ep_cap, cap_endpoint_cap) || !cap_endpoint_cap_get_capCanReceive(ep_cap))) { - slowpath(SysReplyWait); + slowpath(SysReplyRecv); } /* Check there is nothing waiting on the notification */ if (ksCurThread->tcbBoundNotification && notification_ptr_get_state(ksCurThread->tcbBoundNotification) == NtfnState_Active) { - slowpath(SysReplyWait); + slowpath(SysReplyRecv); } /* Get the endpoint address */ @@ -205,14 +205,14 @@ fastpath_reply_wait(word_t cptr, word_t msgInfo) /* Check that there's not a thread waiting to send */ if (unlikely(endpoint_ptr_get_state(ep_ptr) == EPState_Send)) { - slowpath(SysReplyWait); + slowpath(SysReplyRecv); } /* Only reply if the reply cap is valid. */ callerSlot = TCB_PTR_CTE_PTR(ksCurThread, tcbCaller); callerCap = callerSlot->cap; if (unlikely(!fastpath_reply_cap_check(callerCap))) { - slowpath(SysReplyWait); + slowpath(SysReplyRecv); } /* Determine who the caller is. */ @@ -222,7 +222,7 @@ fastpath_reply_wait(word_t cptr, word_t msgInfo) reply is generated instead. */ fault_type = fault_get_faultType(caller->tcbFault); if (unlikely(fault_type != fault_null_fault)) { - slowpath(SysReplyWait); + slowpath(SysReplyRecv); } /* Get destination thread.*/ @@ -237,7 +237,7 @@ fastpath_reply_wait(word_t cptr, word_t msgInfo) /* Ensure that the destination has a valid MMU. */ if (unlikely(! isValidVTableRoot_fp (newVTable))) { - slowpath(SysReplyWait); + slowpath(SysReplyRecv); } #ifdef ARCH_ARM @@ -247,19 +247,19 @@ fastpath_reply_wait(word_t cptr, word_t msgInfo) /* Ensure the original caller can be scheduled directly. */ if (unlikely(caller->tcbPriority < ksCurThread->tcbPriority)) { - slowpath(SysReplyWait); + slowpath(SysReplyRecv); } #ifdef ARCH_ARM /* Ensure the HWASID is valid. */ if (unlikely(!pde_pde_invalid_get_stored_asid_valid(stored_hw_asid))) { - slowpath(SysReplyWait); + slowpath(SysReplyRecv); } #endif /* Ensure the original caller is in the current domain and can be scheduled directly. */ if (unlikely(caller->tcbDomain != ksCurDomain && maxDom)) { - slowpath(SysReplyWait); + slowpath(SysReplyRecv); } /* diff --git a/src/kernel/thread.c b/src/kernel/thread.c index 0d0b68bf2b923221c4217308b4071e471cd1b97d..cf18e9acfb5788afb0d452be2c4180e460271de9 100644 --- a/src/kernel/thread.c +++ b/src/kernel/thread.c @@ -261,7 +261,7 @@ transferCaps(message_info_t info, extra_caps_t caps, return message_info_set_msgExtraCaps(info, i); } -void doNBWaitFailedTransfer(tcb_t *thread) +void doNBRecvFailedTransfer(tcb_t *thread) { /* Set the badge register to 0 to indicate there was no message */ setRegister(thread, badgeRegister, 0); diff --git a/src/object/endpoint.c b/src/object/endpoint.c index edc31602a6250808738fafe4882f8f47c65d0b8c..2254b4e8dd16d511e09fe3627fe25346d8d40c98 100644 --- a/src/object/endpoint.c +++ b/src/object/endpoint.c @@ -150,7 +150,7 @@ receiveIPC(tcb_t *thread, cap_t cap, bool_t isBlocking) endpoint_ptr_set_state(epptr, EPState_Recv); ep_ptr_set_queue(epptr, queue); } else { - doNBWaitFailedTransfer(thread); + doNBRecvFailedTransfer(thread); } break; } diff --git a/src/object/notification.c b/src/object/notification.c index a8ae888b2b09be475af1f8cec029335cb8f78573..afd9f7d20fdaf05bae42f9d040689b2050ca80b0 100644 --- a/src/object/notification.c +++ b/src/object/notification.c @@ -132,7 +132,7 @@ receiveSignal(tcb_t *thread, cap_t cap, bool_t isBlocking) notification_ptr_set_state(ntfnPtr, NtfnState_Waiting); ntfn_ptr_set_queue(ntfnPtr, ntfn_queue); } else { - doNBWaitFailedTransfer(thread); + doNBRecvFailedTransfer(thread); } break; diff --git a/src/plat/allwinnerA20/linker.lds b/src/plat/allwinnerA20/linker.lds index 4f6bec2d8b0be90d22affb995b1f162a32deb24e..b885b8fb7395a4d594d7d457bc9d93ec03d3e6ff 100755 --- a/src/plat/allwinnerA20/linker.lds +++ b/src/plat/allwinnerA20/linker.lds @@ -37,7 +37,7 @@ SECTIONS /* Fastpath code */ *(.vectors.fastpath_call) - *(.vectors.fastpath_reply_wait) + *(.vectors.fastpath_reply_recv) *(.vectors.text) /* Anything else that should be in the vectors page. */ diff --git a/src/plat/am335x/linker.lds b/src/plat/am335x/linker.lds index a1e4168cbacd0f6fe9b1d51c81db97c5bcb2be90..f7ce96ad1324b5c0759a75b67e67ae3e8cfd5408 100644 --- a/src/plat/am335x/linker.lds +++ b/src/plat/am335x/linker.lds @@ -37,7 +37,7 @@ SECTIONS /* Fastpath code */ *(.vectors.fastpath_call) - *(.vectors.fastpath_reply_wait) + *(.vectors.fastpath_reply_recv) *(.vectors.text) /* Anything else that should be in the vectors page. */ diff --git a/src/plat/apq8064/linker.lds b/src/plat/apq8064/linker.lds index e972a3f7a6aa9e180b22d659805c5f6eb6e32cd8..ba046abe72ce115fba771a944718f087e1c8d10e 100644 --- a/src/plat/apq8064/linker.lds +++ b/src/plat/apq8064/linker.lds @@ -37,7 +37,7 @@ SECTIONS /* Fastpath code */ *(.vectors.fastpath_call) - *(.vectors.fastpath_reply_wait) + *(.vectors.fastpath_reply_recv) *(.vectors.text) /* Anything else that should be in the vectors page. */ diff --git a/src/plat/exynos4/linker.lds b/src/plat/exynos4/linker.lds index d7bc863093eb3ab56ddae1b6e014c0d126ccd1ac..8a7f37f7b79dd9131b2583dd267bec47de74e9cd 100644 --- a/src/plat/exynos4/linker.lds +++ b/src/plat/exynos4/linker.lds @@ -37,7 +37,7 @@ SECTIONS /* Fastpath code */ *(.vectors.fastpath_call) - *(.vectors.fastpath_reply_wait) + *(.vectors.fastpath_reply_recv) *(.vectors.text) /* Anything else that should be in the vectors page. */ diff --git a/src/plat/exynos5/linker.lds b/src/plat/exynos5/linker.lds index d7bc863093eb3ab56ddae1b6e014c0d126ccd1ac..8a7f37f7b79dd9131b2583dd267bec47de74e9cd 100644 --- a/src/plat/exynos5/linker.lds +++ b/src/plat/exynos5/linker.lds @@ -37,7 +37,7 @@ SECTIONS /* Fastpath code */ *(.vectors.fastpath_call) - *(.vectors.fastpath_reply_wait) + *(.vectors.fastpath_reply_recv) *(.vectors.text) /* Anything else that should be in the vectors page. */ diff --git a/src/plat/imx31/linker.lds b/src/plat/imx31/linker.lds index a1e4168cbacd0f6fe9b1d51c81db97c5bcb2be90..f7ce96ad1324b5c0759a75b67e67ae3e8cfd5408 100644 --- a/src/plat/imx31/linker.lds +++ b/src/plat/imx31/linker.lds @@ -37,7 +37,7 @@ SECTIONS /* Fastpath code */ *(.vectors.fastpath_call) - *(.vectors.fastpath_reply_wait) + *(.vectors.fastpath_reply_recv) *(.vectors.text) /* Anything else that should be in the vectors page. */ diff --git a/src/plat/imx6/linker.lds b/src/plat/imx6/linker.lds index a85c5ad6dd34458ddb204d8d05f328f942cb1a5d..836ca3c6a015ff82960b0f3b8bc061f31b037476 100644 --- a/src/plat/imx6/linker.lds +++ b/src/plat/imx6/linker.lds @@ -37,7 +37,7 @@ SECTIONS /* Fastpath code */ *(.vectors.fastpath_call) - *(.vectors.fastpath_reply_wait) + *(.vectors.fastpath_reply_recv) *(.vectors.text) /* Anything else that should be in the vectors page. */ diff --git a/src/plat/omap3/linker.lds b/src/plat/omap3/linker.lds index a1e4168cbacd0f6fe9b1d51c81db97c5bcb2be90..f7ce96ad1324b5c0759a75b67e67ae3e8cfd5408 100644 --- a/src/plat/omap3/linker.lds +++ b/src/plat/omap3/linker.lds @@ -37,7 +37,7 @@ SECTIONS /* Fastpath code */ *(.vectors.fastpath_call) - *(.vectors.fastpath_reply_wait) + *(.vectors.fastpath_reply_recv) *(.vectors.text) /* Anything else that should be in the vectors page. */ diff --git a/src/plat/zynq7000/linker.lds b/src/plat/zynq7000/linker.lds index 80b116d9475581a8d09054452996f0e4e7d16f91..5694967868f7e5e2cf3d3f6a5ac20211ac7053fb 100644 --- a/src/plat/zynq7000/linker.lds +++ b/src/plat/zynq7000/linker.lds @@ -37,7 +37,7 @@ SECTIONS /* Fastpath code */ *(.vectors.fastpath_call) - *(.vectors.fastpath_reply_wait) + *(.vectors.fastpath_reply_recv) *(.vectors.text) /* Anything else that should be in the vectors page. */