seL4 Driver API Persistent Device Naming Scheme
Recommended prior reading for this page is the seL4 Driver API’s location-based device addressing scheme.
typedef void seL4drv_connection_t;
The seL4 Driver API requires the use of a persistent naming scheme which forms the basis of the IPC connection system between device instances. It is through this naming scheme that a device instance can call to its parent devices, and communicate with devices with which it has lateral dependencies.
Devices’ addressable names are generated by the parent driver that enumerates them. Child device enumeration is discussed in detail in the Child Enumeration article.
A driver connects to an external device that it depends on by calling
seL4drv_external_connect(), passing in the addressable name of the
particular device that it wishes to connect to. The environment shall
search its device tree for a device which has that name, and return a
handle of type
seL4drv_connection_t *. Notice that
seL4drv_connection_t is of type
void (see above):
this is because it is an opaque handle, and the
driver is not meant to dereference this handle after receiving it. This
handle is meant to be passed to subsequent function calls to the
particular API that was connected to in order to maintain context
between the driver and the target device.
If the environment is unable to locate a device whose addressable name
matches the one supplied in the call to
shall return NULL. The calling driver shall take this to mean that
the device is trying to connect to does not exist, or that it exists but
the environment does not have a driver that can drive it, and so is