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\_Mint}{cnode_mint}, just like \obj{Endpoint}
21capabilities (see \autoref{sec:ep-badges}). As with \obj{Endpoint}
22capabilities, badged \obj{Notification} capabilities cannot be
23unbadged, rebadged or used to create child capabilities with
24different badges. \label{s:notif-badge}
25
26\section{Signalling, Polling and Waiting}
27
28The \apifunc{seL4\_Signal}{sel4_signal} method updates the
29notification word by bit-wise \texttt{or}-ing it with the \emph{badge}
30of the invoked notification capability. It also unblocks the first
31thread waiting on the notification (if any). As such,
32\apifunc{seL4\_Signal}{sel4_signal} works like concurrently signalling
33multiple semaphores (those indicated by the bits set in the badge).
34If the signal sender capability was unbadged or 0-badged, the operation degrades
35to just waking up the first thread waiting on the notification (also see below).
36
37The \apifunc{seL4\_Wait}{sel4_wait} method works similarly to a
38select-style wait on the set of semaphores: If the notification word is
39zero at the time \apifunc{seL4\_Wait}{sel4_wait} is called, the
40invoker blocks. Else, the call returns immediately, setting the
41notification word to zero and returning to the invoker the previous
42notification-word value.
43
44The \apifunc{seL4\_Poll}{sel4_poll} is the same as \apifunc{seL4\_Wait}{sel4_wait}, except if
45no signals are pending (the notification word is 0) the call will return immediately
46without blocking.
47
48If threads are waiting on the \obj{Notification} object at the time
49\apifunc{seL4\_Signal}{sel4_signal} is invoked, the first queued thread
50receives the notification. All other threads keep waiting until the
51next time the notification is signalled.
52
53\section{Binding Notifications}
54\label{sec:notification-binding}
55
56\obj{Notification} objects and \obj{TCB}s can be bound together in a 1-to-1 relationship
57through the \apifunc{seL4\_TCB\_BindNotification}{tcb_bindnotification} invocation. When a
58\obj{Notification} is bound to a \obj{TCB}, signals to that notification object
59will be delivered even if the thread is receiving from an IPC
60endpoint. To distinguish whether the received message was a notification
61or an IPC, developers should check the badge value. By reserving a
62specific badge (or range of badges) for capabilities to the bound
63notification --- distinct from endpoint badges --- the
64message source can be determined.
65
66Once a notification has been bound, the only thread that may perform
67\apifunc{seL4\_Wait}{sel4_wait} on the notification is the bound thread.
68