1% 2% Copyright 2014, General Dynamics C4 Systems 3% 4% This software may be distributed and modified according to the terms of 5% the GNU General Public License version 2. Note that NO WARRANTY is provided. 6% See "LICENSE_GPLv2.txt" for details. 7% 8% @TAG(GD_GPL) 9% 10 11\chapter{\label{ch:notifications}Notifications} 12 13Notifications are a simple, non-blocking signalling mechanism that 14logically represents a set of binary semaphores. 15 16\section{Notification Objects} 17 18A \obj{Notification} object contains a single data word, called the 19\emph{notification word}. Such an object supports two operations: 20\apifunc{seL4\_Signal}{sel4_signal} and 21\apifunc{seL4\_Wait}{sel4_wait}. 22 23\obj{Notification} capabilities can be badged, using 24\apifunc{seL4\_CNode\_Mutate}{cnode_mutate} or 25\apifunc{seL4\_CNode\_Mint}{cnode_mint}, just like \obj{Endpoint} 26capabilities (see \autoref{sec:ep-badges}). As with \obj{Endpoint} 27capabilities, badged \obj{Notification} capabilities cannot be 28 unbadged, rebadged or used to create child capabilities with 29 different badges. \label{s:notif-badge} 30 31\section{Signalling, Polling and Waiting} 32 33The \apifunc{seL4\_Signal}{sel4_signal} method updates the 34notification word by bit-wise \texttt{or}-ing it with the \emph{badge} 35of the invoked notification capability. It also unblocks the first 36thread waiting on the notification (if any). As such, 37\apifunc{seL4\_Signal}{sel4_signal} works like concurrently signalling 38multiple semaphores (those indicated by the bits set in the badge). 39If the signal sender capability was unbadged or 0-badged, the operation degrades 40to just waking up the first thread waiting on the notification (also see below). 41 42The \apifunc{seL4\_Wait}{sel4_wait} method works similarly to a 43select-style wait on the set of semaphores: If the notification word is 44zero at the time \apifunc{seL4\_Wait}{sel4_wait} is called, the 45invoker blocks. Else, the call returns immediately, setting the 46notification word to zero and returning to the invoker the previous 47notification-word value. 48 49The \apifunc{seL4\_Poll}{sel4_poll} is the same as \apifunc{seL4\_Wait}{sel4_wait}, except if 50no signals are pending (the notification word is 0) the call will return immediately 51without blocking. 52 53If threads are waiting on the \obj{Notification} object at the time 54\apifunc{seL4\_Signal}{sel4_signal} is invoked, the first queued thread 55receives the notification. All other threads keep waiting until the 56next time the notification is signalled. 57 58If \apifunc{seL4\_Signal}{sel4_signal} is invoked with an unbadged or 0-badged 59capability, the first queued thread is unblocked with a zero return value. If 60no thread is waiting, the \apifunc{\mbox{seL4\_Signal}}{sel4_signal} operation with 61an unbadged capability has no effect. 62 63 64\section{Binding Notifications} 65\label{sec:notification-binding} 66 67\obj{Notification} objects and \obj{TCB}s can be bound together in a 1-to-1 relationship 68through the \apifunc{seL4\_TCB\_BindNotification}{tcb_bindnotification} invocation. When a 69\obj{Notification} is bound to a \obj{TCB}, signals to that notification object 70will be delivered even if the thread is receiving from an IPC 71endpoint. To distinguish whether the received message was a notification 72or an IPC, developers should check the badge value. By reserving a 73specific badge (or range of badges) for capabilities to the bound 74notification --- distinct from endpoint badges --- the 75message source can be determined. 76 77Once a notification has been bound, the only thread that may perform 78\apifunc{seL4\_Wait}{sel4_wait} on the notification is the bound thread. 79