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