CAmkES Timer Tutorial
This tutorial guides you through setting up a sample timer driver component in CAmkES and using it to delay for 2 seconds. For this tutorial, we will be using the ZYNQ7000 ARM-based platform. This platform can be simulated via QEMU so it is not a problem if you do not have access to the actual physical board.
The tutorial also has two parts to it. The first part will teach you how to manually define hardware details to configure the hardware component and initialise hardware resources. The second part will teach you how to use a CAmkES connector to initialise hardware resources automatically for you.
The solutions to this tutorial primarily uses the method of manually defining hardware details. The solutions to the second part are also included, albeit commented out.
# For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/#get-the-code # # Follow these instructions to initialise the tutorial # initialising the build directory with a tutorial exercise ./init --tut hello-camkes-timer # building the tutorial exercise cd hello-camkes-timer_build ninja
Exercises - Part 1
Instantiate some components. You’re already given one component instance
client. You need to instantiate additional components, a timer driver and a component instance representing the timer hardware itself. Look in
components/Timer/Timer.camkesfor the definitions of the components.
Once you open the file, you will notice three different components. The
Timerbase components represents the timer driver and the timer hardware
TimerDTB component represents both the timer driver and the
timer hardware. This component is meant to be used with the
CAmkES connector to automatically initialise hardware resources. The second
part of the tutorial will go into more detail about the
For now, instantiate the
Note the lines
connection seL4RPCCall hello_timer(from client.hello, to
timer.sem_value = 0; in the
file. They assume that the name of the timer ‘‘driver’’ will be
timer. If you
wish to call your driver something else, you’ll have to change these lines.
Connect the timer driver component (
Timer) to the timer hardware component
Timerbase). The timer hardware component exposes two interfaces which must
be connected to the timer driver. One of these represents memory-mapped
registers. The other represents an interrupt.
Configure the timer hardware component instance with device-specific info. The physical address of the timer’s memory-mapped registers, and its IRQ number must both be configured.
We’ll start by completing the
irq_handle function, which is called in
response to each timer interrupt. Note the name of this function. It follows
the naming convention
<interface> is the name of
an IRQ interface connected with
seL4HardwareInterrupt. When an interrupt is
received on the interface
<interface>, the function
The implementation of the timer driver is located inside a different folder and
can be found in the
projects/sel4-tutorials/zynq_timer_driver folder from the
root of the projects directory, i.e. where the
.repo folder can be found and
where the initial
repo init command was executed.
This task is to call the
timer_handle_irq function from the supply driver to
inform the driver that an interrupt has occurred.
Stop the timer from running. The
timer_stop function will be helpful here.
The interrupt now needs to be acknowledged.
CAmkES generates the seL4-specific code for ack-ing an interrupt and provides a
<interface>_acknowldege for IRQ interfaces (specifically those
Now we’ll complete
hello__init - a function which is called once
before the component’s interfaces start running.
We need to initialise a handle to the timer driver for this device, and store a
handle to the driver in the global variable
After initialising the timer, we now need to start the timer. Do so by calling
timer_start and passing the handle to the driver.
Note that this task is to understand the existing code. You won’t have to modify anything for this task.
timer_inf RPC interface. This interface is defined in
interfaces/timer.camkes, and contains a single method,
should return after a given number of seconds. in
components/Timer/Timer.camkes, we can see that the
exposed by the
Timer component is called
hello. Thus, the function we
need to implement is called
Tell the timer to interrupt after the given number of seconds. The
timer_set_timeout function from the included driver will help. Note that it
expects its time argument to be given in nanoseconds.
Note the existing code in
hello_sleep. It waits on a binary semaphore.
irq_handle will be called on another thread when the timer interrupt occurs,
and that function will post to the binary semaphore, unblocking us and allowing
the function to return after the delay.
Expect the following output with a 2 second delay between the last 2 lines:
Starting the client ------Sleep for 2 seconds------ After the client: wakeup
Exercises - Part 2
Now that you’ve learnt how to manually define the hardware details of a
hardware component to initialise hardware resources, this part of the tutorial
will teach you how to use the
seL4DTBHardware connector to do that
The connector requires a devicetree blob which describes an ARM platform.
Additionally, the blob’s interrupt fields also need to follow the same format
of the ARM GIC v1 and v2. There are devicetree source files bundled with the
kernel, look in the
tools/dts/ folder of the kernel sources. If a suitable
devicetree blob is not available for your platform, then do not proceed with
Navigate to the
Timer component instantiations and instantiate a
TimerDTB component instead. Also change the
hello_timer(from client.hello, to timer.hello); and
timer.sem_value = 0;
lines if necessary.
seL4HardwareInterrupt connections. Connect
the two interfaces inside the
TimerDTB component with the
components/Timer/Timer.camkes, remove the
inside the configurations block.
TimerDTB component to pass in the correct DTB path to a timer
to the connector and also initialise the interrupt resources for the timer.
This will allow the connector to read a device node from the devicetree blob
and grab the necessary data to initialise hardware resources. More
specifically, it reads the registers field and optionally the interrupts field
to allocate memory and interrupts.
Similar to part one, we’ll start with the
tmr_irq_handle function. This
function is called in response to a timer interrupt. The name of the function
has a special meaning and the meaning is unique to the
The IRQ handling functions of the connector follows the naming convention
<to_interface> is the name of the
interface of the ‘to’ end in an instance of a
Also notice that it takes a
ps_irq_t * type. This is because, for a given
device, there may be multiple interrupts associated with the device. A
ps_irq_t struct is given to the IRQ handling function and it contains
information about the interrupt, allowing the handler to differentiate between
the numerous interrupts of a device.
Likewise with part one, the implementation of the timer driver is in the
included driver in
timer_driver and the task here is to call
The timer needs to be stopped, the task here is the same as part one’s task 5.
Again, the interrupt now has to be acknowledged.
seL4DTBHardware connector, CAmkES also generates and provides a
function to acknowledge interrupts. This function follows a similar naming
convention to the IRQ handler above,
takes in a
ps_irq_t * argument. Similarly, the
ps_irq_t * argument helps
CAmkES to differentiate between the possibly many interrupts of a device that
you wish to acknowledge.
TASK 7 - 10
Task 7 to 10 are the exact same as the tasks in part one.
You should also expect the same output as the first part.
Stuck? See the resources below.
Tutorial included from github repo edit