%
% Copyright 2014, General Dynamics C4 Systems
%
% This software may be distributed and modified according to the terms of
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
% See "LICENSE_GPLv2.txt" for details.
%
% @TAG(GD_GPL)
%

\chapter{\label{ch:notifications}Notifications}

Notifications are a simple, non-blocking signalling mechanism that
logically represents a set of binary semaphores.

\section{Notification Objects}

A \obj{Notification} object contains a single data word, called the
\emph{notification word}. Such an object supports two operations:
\apifunc{seL4\_Signal}{sel4_signal} and
\apifunc{seL4\_Wait}{sel4_wait}.

\obj{Notification} capabilities can be badged, using
\apifunc{seL4\_CNode\_Mutate}{cnode_mutate} or
\apifunc{seL4\_CNode\_Mint}{cnode_mint}, just like \obj{Endpoint}
capabilities (see \autoref{sec:ep-badges}). As with \obj{Endpoint}
capabilities, badged \obj{Notification} capabilities cannot be
  unbadged, rebadged or used to create child capabilities with
  different badges. \label{s:notif-badge}

\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}
of the invoked notification capability. It also unblocks the first
thread waiting on the notification (if any). As such,
\apifunc{seL4\_Signal}{sel4_signal} works like concurrently signalling
multiple semaphores (those indicated by the bits set in the badge).
If the signal sender capability was unbadged or 0-badged, the operation degrades
to just waking up the first thread waiting on the notification (also see below).

The \apifunc{seL4\_Wait}{sel4_wait} method works similarly to a
select-style wait on the set of semaphores: If the notification word is
zero at the time \apifunc{seL4\_Wait}{sel4_wait} is called, the
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
next time the notification is signalled. 

If \apifunc{seL4\_Signal}{sel4_signal} is invoked with an unbadged or 0-badged
capability, the first queued thread is unblocked with a zero return value. If
no thread is waiting, the \apifunc{\mbox{seL4\_Signal}}{sel4_signal} operation with
an unbadged capability has no effect.


\section{Binding Notifications}
\label{sec:notification-binding}

\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}, 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
notification --- distinct from endpoint badges --- the
message source can be determined.

Once a notification has been bound, the only thread that may perform
\apifunc{seL4\_Wait}{sel4_wait} on the notification is the bound thread.