CAmkES Timer Tutorial
This tutorial guides you through setting up a timer driver in CAmkES and using it to delay for 2 seconds.
# 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
Instantiate some components. You’re already given one component instance
client. You need to instantiate two more - a timer driver, and a component instance representing the timer hardware itself. Look in
components/Timer/Timer.camkesfor the definitions of both of these components.
Note the lines
connection seL4RPCCall hello_timer(from client.hello, to timer.hello);
timer.sem_value = 0;. 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 timer driver to timer hardware. 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
<interface>_handle will be
The implementation of the timer driver itself isn’t directly in this
file. The driver is implemented in a CAmkES-agnostic way in a library
This task is to call the
timer_handle_irq function from
libplatsupport, to inform the driver that an interrupt has occurred.
Acknowledge the interrupt. CAmkES generates the seL4-specific code for
ack-ing an interrupt and provides a function
<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 timer driver from
libplatsupport for this
device, and store a handle to the driver in the global variable
Note that this task is to understand the existing code. You won’t have to modify any files.
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_oneshot_relative function from
libplatsupport 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
Stuck? See the resources below.