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