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.

Initialising

# For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials
#
# 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

Prerequisites

1. Set up your machine.
2. Camkes 2

CapDL Loader

This tutorial uses the capDL loader, a root task which allocates statically configured objects and capabilities.

Initialising

# For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials
#
# 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

# For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials
#
# Follow these instructions to initialise the tutorial
# initialising the build directory with a tutorial exercise
./init --solution --tut hello-camkes-timer
# building the tutorial exercise
cd hello-camkes-timer_build
ninja

Exercises - Part 1

Instantiate a Timer and Timerbase

Start in hello-camkes-timer.camkes.

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.camkes for the definitions of the components.

Once you open the file, you will notice three different components. The Timer and Timerbase components represents the timer driver and the timer hardware respectively. The TimerDTB component represents both the timer driver and the timer hardware. This component is meant to be used with the seL4DTBHardware CAmkES connector to automatically initialise hardware resources. The second part of the tutorial will go into more detail about the TimerDTB component and the seL4DTBHardware connector.

For now, instantiate the Timer and Timerbase components.

Note the lines connection seL4RPCCall hello_timer(from client.hello, to timer.hello); and timer.sem_value = 0; in the hello-camkes-timer.camkes 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.

    /* Part 1, TASK 1: component instances */
    /* hint 1: one hardware component and one driver component
        * hint 2: look at
        * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
        */

    /* Part 1, TASK 1: component instances */
    component Timerbase timerbase;
    component Timer timer;

Connect a timer driver component

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.

    /* Part 1, TASK 2: connections */
    /* hint 1: use seL4HardwareMMIO to connect device memory
        * hint 2: use seL4HardwareInterrupt to connect interrupt
        * hint 3: look at
        * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
        */

    /* Part 1, TASK 2: connections */
    connection seL4HardwareMMIO timer_mem(from timer.reg, to timerbase.reg);
    connection seL4HardwareInterrupt timer_irq(from timerbase.irq, to timer.irq);

Configure a timer hardware component instance

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.

    /* Part 1, TASK 3: hardware resources */
    /* Timer and Timerbase:
        * hint 1: find out the device memory address and IRQ number from the hardware data sheet
        * hint 2: look at
        * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#hardware-components
        */

    /* Part 1, TASK 3: hardware resources */
    timerbase.reg_paddr = 0xF8001000;   // paddr of mmio registers
    timerbase.reg_size = 0x1000;        // size of mmio registers
    timerbase.irq_irq_number = 42;      // timer irq number

Call into a supplied driver to handle the interrupt

Now open components/Timer/src/timer.c.

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>_handle, where <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 called.

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.

    /* Part 1, TASK 4: call into the supplied driver to handle the interrupt. */
    /* hint: timer_handle_irq
     */

    /* Part 1, TASK 4: call into the supplied driver to handle the interrupt. */
    timer_handle_irq(&timer_drv);

Stop a timer

Stop the timer from running. The timer_stop function will be helpful here.

    /* Part 1, TASK 5: stop the timer. */
    /* hint: timer_stop
     */

    /* Part 1, TASK 5: stop the timer. */
    timer_stop(&timer_drv);

Acknowledge an interrupt

The interrupt now needs to be acknowledged.

CAmkES generates the seL4-specific code for ack-ing an interrupt and provides a function <interface>_acknowldege for IRQ interfaces (specifically those connected with seL4HardwareInterrupt).

    /* Part 1, TASK 6: acknowledge the interrupt */
    /* hint 1: use the function <irq interface name>_acknowledge()
     */

    /* Part 1, TASK 6: acknowledge the interrupt */
    error = irq_acknowledge();
    ZF_LOGF_IF(error != 0, "failed to acknowledge interrupt");

Get a timer handler

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 timer_drv.

    /* Part 1, TASK 7: call into the supplied driver to get the timer handler */
    /* hint1: timer_init
     * hint2: The timer ID is supplied as a #define in this file
     * hint3: The register's variable name is the same name as the dataport in the Timer component
     */

    /* Part 1, TASK 7: call into the supplied driver to get the timer handler */
    int error = timer_init(&timer_drv, DEFAULT_TIMER_ID, reg);
    assert(error == 0);

Start a timer

After initialising the timer, we now need to start the timer. Do so by calling timer_start and passing the handle to the driver.

    /* Part 1, TASK 8: start the timer */
    /* hint: timer_start
     */

    /* Part 1, TASK 8: start the timer */
    error = timer_start(&timer_drv);
    assert(error == 0);

Implement a RPC interface

Note that this task is to understand the existing code. You won’t have to modify anything for this task.

Implement the timer_inf RPC interface. This interface is defined in interfaces/timer.camkes, and contains a single method, sleep, which should return after a given number of seconds. in components/Timer/Timer.camkes, we can see that the timer_inf interface exposed by the Timer component is called hello. Thus, the function we need to implement is called hello_sleep.

    /* Part 1, TASK 9: implement the rpc function. */
    /* hint 1: the name of the function to implement is a composition of an interface name and a function name:
    * i.e.: <interface>_<function>
    * hint 2: the interfaces available are defined by the component, e.g. in components/timer/timer.camkes
    * hint 3: the function name is defined by the interface definition, e.g. in interfaces/timer.camkes
    * hint 4: so the function would be: hello_sleep()
    * hint 5: the camkes 'int' type maps to 'int' in c
    * hint 6: invoke a function in supplied driver the to set up the timer
    * hint 7: look at https://github.com/sel4/camkes-tool/blob/master/docs/index.md#creating-an-application
    */

/* Part 1, TASK 9: implement the rpc function. */
void hello_sleep(int sec) {
    int error = 0;

Set a timer interrupt

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.

    /* Part 1, TASK 10: invoke a function in the supplied driver to set a timeout */
    /* hint1: timer_set_timeout
     * hint2: periodic should be set to false
     */

    /* Part 1, TASK 10: invoke a function in the supplied driver to set a timeout */
    error = timer_set_timeout(&timer_drv, sec * NS_IN_SECOND, false);
    assert(error == 0);

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 automatically.

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 the tutorial.

Instantiate a TimerDTB component

Navigate to the hello-camkes-timer.camkes file.

Remove the Timerbase and Timer component instantiations and instantiate a TimerDTB component instead. Also change the connection seL4RPCCall hello_timer(from client.hello, to timer.hello); and timer.sem_value = 0; lines if necessary.

    /* Part 2, TASK 1: component instances */
    /* hint 1: a single TimerDTB component
    * hint 2: look at
    * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
    */

    /* Part 2, TASK 1: component instances */
    //uncomment the line below
//    component TimerDTB timer;

Connect interfaces using the seL4DTBHardware connector

Remove the seL4HardwareMMIO and seL4HardwareInterrupt connections. Connect the two interfaces inside the TimerDTB component with the seL4DTBHardware connector.

    /* Part 2, TASK 2: connections */
    /* hint 1: connect the dummy_source and timer interfaces
    * hint 2: the dummy_source should be the 'from' end
    * hint 3: look at
    * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
    */

      /* Part 2, TASK 2: connections */
      // uncomment the line below
//    connection seL4DTBHardware timer_dtb(from timer.dummy_source, to timer.tmr);

Configure the TimerDTB component

Before opening components/Timer/Timer.camkes, remove the Timerbase settings inside the configurations block.

Configure the 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.

    /* Part 2, TASK 3: hardware resources */
    /* TimerDTB:
     * hint 1: look in the DTB/DTS for the path of a timer
     * hint 2: set the 'dtb' setting for the tmr interface in the TimerDTB component,
     *         e.g. foo.dtb = dtb({"path" : "/bar"});
     * hint 3: set the 'generate_interrupts' setting to 1
     */

     /* Part 2, TASK 3: hardware resources */
     // uncomment the lines below
//    tmr.dtb = dtb({"path" : "/amba/timer@f8001000"});   // path of the timer in the DTB
//    tmr.generate_interrupts = 1;                        // tell seL4DTBHardware to init interrupts

Handle the interrupt

Move to components/TimerDTB/src/timerdtb.c.

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 seL4DTBHardware connector.

The IRQ handling functions of the connector follows the naming convention <to_interface>_irq_handle, where <to_interface> is the name of the interface of the ‘to’ end in an instance of a seL4DTBHardware connection. 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 timer_handle_irq.

    /* Part 2, TASK 4: call into the supplied driver to handle the interrupt. */
    /* hint: timer_handle_irq
     */

    /* Part 2, TASK 4: call into the supplied driver to handle the interrupt. */
    timer_handle_irq(&timer_drv);

Stop a timer

Stop the timer from running. The timer_stop function will be helpful here.

    /* Part 2, TASK 5: stop the timer. */
    /* hint: timer_stop
     */

    /* Part 2, TASK 5: stop the timer. */
    timer_stop(&timer_drv);

Acknowledge the interrupt

Again, the interrupt now has to be acknowledged.

For the seL4DTBHardware connector, CAmkES also generates and provides a function to acknowledge interrupts. This function follows a similar naming convention to the IRQ handler above, <to_interface>_irq_acknowledge also 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.

    /* Part 2, TASK 6: acknowledge the interrupt */
    /* hint 1: use the function <to_interface_name>_irq_acknowledge()
     * hint 2: pass in the 'irq' variable to the function
     */

    /* Part 2, TASK 6: acknowledge the interrupt */
    error = tmr_irq_acknowledge(irq);
    ZF_LOGF_IF(error != 0, "failed to acknowledge interrupt");

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.

Next: CAmkES VM

Tutorial included from github repo edit