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