From a99a10408d529289898edaad6cf044e62963306e Mon Sep 17 00:00:00 2001
From: Anna Lyons <Anna.Lyons@nicta.com.au>
Date: Tue, 10 Nov 2015 14:06:38 +1100
Subject: [PATCH] SELFOUR-279: rename Wait -> Recv, add wrappers for seL4_Poll
and seL4_Wait for notification objects.
This commit deprecates seL4_ReplyWait, removes seL4_NBwait completely,
and changes the return type of seL4_Wait to void (seL4_Wait should be
used for notification objects, and seL4_Recv should be used where
seL4_Wait was used previously for endpoints).
---
haskell/doc/figures/clientserver.mp | 2 +-
haskell/doc/figures/ipctransfer.mp | 4 +-
haskell/doc/overview.tex | 30 ++++++-------
haskell/doc/refman.tex | 2 +-
haskell/src/SEL4/API/Syscall.lhs | 26 +++++------
haskell/src/SEL4/Kernel/Thread.lhs | 2 +-
haskell/src/SEL4/Object/Endpoint.lhs | 4 +-
haskell/src/SEL4/Object/Notification.lhs | 10 ++---
haskell/src/SEL4/Object/ObjectType.lhs | 2 +-
haskell/src/SEL4/Object/TCB.lhs | 2 +-
include/api/syscall.xml | 6 +--
include/arch/arm/arch/fastpath/fastpath.h | 6 +--
include/arch/x86/arch/fastpath/fastpath.h | 2 +-
include/kernel/thread.h | 2 +-
.../arch_include/arm/sel4/arch/deprecated.h | 27 ++++++++++++
libsel4/arch_include/arm/sel4/arch/syscalls.h | 43 ++++++++++++-------
.../arch_include/x86/sel4/arch/deprecated.h | 26 +++++++++++
libsel4/arch_include/x86/sel4/arch/syscalls.h | 32 +++++++++-----
libsel4/include/api/syscall.xml | 6 +--
libsel4/include/sel4/deprecated.h | 9 ++++
manual/parts/api.tex | 8 ++--
manual/parts/api/sel4_nbrecv.tex | 21 +++++++++
manual/parts/api/sel4_poll.tex | 29 +++++++++++++
.../api/{sel4_nbwait.tex => sel4_recv.tex} | 10 ++---
...{sel4_replywait.tex => sel4_replyrecv.tex} | 10 ++---
manual/parts/api/sel4_wait.tex | 15 +++++--
manual/parts/cspace.tex | 2 +-
manual/parts/io.tex | 8 ++--
manual/parts/ipc.tex | 10 ++---
manual/parts/notifications.tex | 10 +++--
manual/parts/objects.tex | 29 +++++++------
manual/parts/threads.tex | 7 ++-
src/api/syscall.c | 14 +++---
src/arch/arm/traps.S | 4 +-
src/arch/x86/c_traps.c | 4 +-
src/fastpath/fastpath.c | 22 +++++-----
src/kernel/thread.c | 2 +-
src/object/endpoint.c | 2 +-
src/object/notification.c | 2 +-
src/plat/allwinnerA20/linker.lds | 2 +-
src/plat/am335x/linker.lds | 2 +-
src/plat/apq8064/linker.lds | 2 +-
src/plat/exynos4/linker.lds | 2 +-
src/plat/exynos5/linker.lds | 2 +-
src/plat/imx31/linker.lds | 2 +-
src/plat/imx6/linker.lds | 2 +-
src/plat/omap3/linker.lds | 2 +-
src/plat/zynq7000/linker.lds | 2 +-
48 files changed, 308 insertions(+), 162 deletions(-)
create mode 100644 libsel4/arch_include/arm/sel4/arch/deprecated.h
create mode 100644 libsel4/arch_include/x86/sel4/arch/deprecated.h
create mode 100644 manual/parts/api/sel4_nbrecv.tex
create mode 100644 manual/parts/api/sel4_poll.tex
rename manual/parts/api/{sel4_nbwait.tex => sel4_recv.tex} (68%)
rename manual/parts/api/{sel4_replywait.tex => sel4_replyrecv.tex} (71%)
diff --git a/haskell/doc/figures/clientserver.mp b/haskell/doc/figures/clientserver.mp
index 7ec574280..ff0a5ece6 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 770e4b5c8..3f0a455bc 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 78327647b..d75d23b8e 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 33ee6107b..1bf16338d 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 9e64b6b49..d2332bef6 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 a9f2182f6..2997ee98f 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 65af1e49e..a540953f5 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 9ad150293..3593341c5 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 0fa38503c..bf1543613 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 f2ae0d45c..7ed6cfeb0 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 1439680c3..980bdd50f 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 a6fb15cfc..e5a52c2f7 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 578ce421e..6a90cf50d 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 3b62e4817..7d92748cd 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 000000000..82be1c29b
--- /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 84ffc2c8f..d4ce45fe9 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 000000000..698b2b515
--- /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 4a45660da..d277a1164 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 7cacabea4..cbaed650c 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 17d4f3e0a..c6e85c440 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 35820c7d0..964adf514 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 000000000..85f7a9dd0
--- /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 000000000..2799dca70
--- /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 17f018834..2b18494de 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 dc5f894f7..4f283f0be 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 3a69bdcfe..cf49bbf30 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 3d0cd5f9b..78e274554 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 f8770ce97..893be38a9 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 59bd12bf0..045c236a3 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 35d8bd5dc..e5ad5e18f 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 862e70ccb..fb61b4061 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 b54692935..2fc1a8ece 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 a5c0fadb2..7b45cb486 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 f07f53485..567032fa9 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 5332ec03b..675cf9f5b 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 2d3a3996a..a2dfbb080 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 0d0b68bf2..cf18e9acf 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 edc31602a..2254b4e8d 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 a8ae888b2..afd9f7d20 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 4f6bec2d8..b885b8fb7 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 a1e4168cb..f7ce96ad1 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 e972a3f7a..ba046abe7 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 d7bc86309..8a7f37f7b 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 d7bc86309..8a7f37f7b 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 a1e4168cb..f7ce96ad1 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 a85c5ad6d..836ca3c6a 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 a1e4168cb..f7ce96ad1 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 80b116d94..569496786 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. */
--
GitLab