M1: A timer driver

Your first milestone is to write a basic timer driver. However, you should use this as an opportunity to get to used working with your partner, and probably work out exactly how you can work together so you don't end up duplicating work, or worse still not completing essential parts of the project.

Group Work & Version Control

By now you should have got yourself in a group and you should have a group account setup for you. We expect that you are using Git to maintain your source code, and that a repository be setup in your group account with the correct permissions and sticky bits set so that you can both access it. See our git overview page for suggestions.

You should consider using a merge tool such as the meld (or equivalent) as the default merge program to avoid painful merges.

You have been provided with a git repository in gitlab for your group. This repository will be used for submitting all further milestones. You can clone the repository with the following command.

git clone https://gitlab.cse.unsw.edu.au/COMP9242/19T2/group-{group-number}.git aos-2019

You will need to provide your username and password when cloning. If you set up your ssh-keys on our gitlab server you can use the following command instead:

git clone gitlab@gitlab.cse.unsw.edu.au:COMP9242/19T2/group-{group-number}.git aos-2019


The aim of this milestone is to design and implement device driver to accurately provide timeouts and trigger activities. You should add a file for the timer implementation and modify the main system call loop to handle timer interrupts. See the framework page for how to add a file to the SOS build system.


Applications will eventually need to be able to make sleep system calls.

The Driver Interface

Your driver needs to export the interface specified in projects/aos/libclock/include/clock/clock.h. There are the following functions:

int start_timer(unsigned char *timer_vaddr)
Initialises the driver. Initialises the timer with the registers mapped at the provided virtual address. This should start the internal counter and allow timers to be registered.
timestamp_t get_time(void)
Read the current time in microseconds from the internal counter timer (timer E).
uint32_t register_timer(uint64_t delay, timer_callback_t callback, void *data)
Registers a callback function be called after the specified interval (in microseconds, though actual wakeup resolution will depend on the timer resolution). Several registrations may be pending at any time. The return value is zero on failure, otherwise a unique identifier for this timeout. This identifier can be used to remove a timeout. After a timeout has occurred, or the timeout has been removed, the identifier may be reused.
int remove_timer(uint32_t id)
Remove a previously registered timer callback, using the unique identifier returned by register_timer.
int stop_timer(void)
Stops operation of the driver. This will remove any outstanding time requests.
int timer_irq(void *data, seL4_Word irq, seL4_IRQHandler irq_handler)
Function to be called by the IRQ dispatch whenever an IRQ is triggered by the timer hardware. The IRQ dispatch will pass in the data and IRQ number that the callback was registered with and an IRQ handler capability that must be used to acknowledge the IRQ.

The above interface is just an internal function call interface. You do not need to export this interface to the users. User programs will indirectly access the clock driver through the sleep syscall that is implemented in a later milestone.

NOTE: After registering an interrupt, you must call seL4_IRQHandler_Ack to ensure the kernel in a sane initial state.

The timer device

Your main job is to learn how to program the timers provided on the OdroidC2's S905 system on chip (SOC). An overview of the parts in the OdroidC2 can be found here.

We have provided a small wrapper library for interacting with the timer device. Each of the first four timeout timers (A, B, C, and D) have identifiers in projects/aos/libclock/include/clock/device.h and a function that can be used to find the IRQ numbers associated with each timer. You must use one or more of these timers in your clock implementation.

There is also an internal interface to be used by libclock which is found in projects/aos/libclock/src/device.h which has been implemented in projects/aos/libclock/src/device.c. The functions here can be used to configure the timestamp (counter) timer (timer E) and each of the timeout timers. Use the constants provided here rather than those in the manual as these have been determined to work correctly. However, still refer to chapter 26 in the SOC manual to understand how the timer functions.

Implementing a device driver really just a matter of learning about its registers, what values to read and write to those registers, and when to do it.

The minimal subset of a timer module's functionality that you must understand and use is listed below.

NOTE: This section is deliberately kept short (e.g., we do not dictate which timer to use or in what mode to use it in). The idea is for you to develop your own design and implementation. There are only two conditions that must be satisfied:

  1. You must use interrupt(s) generated from at least one of timers A, B, C, or D.
  2. You must implement the driver interface described above.

Supplied Code

For this project you have been supplied with skeleton code to help you along the way. This code is intended as an implementation guide, not as a 'black-box' library.

It is important that you fully understand all provided code that you use. For the purposes of assessment, we treat any supplied code that you call as your code and as such you may be asked to describe how it works.

Now might be a good time to get familiar with the resources, especially the framework documentation

seL4/ARM Interrupts

The seL4/ARM kernel exports specific interrupts to a user level interrupt handler via asynchronous notification.

You will need to register the timer_irq function to handle the IRQs for any of the timers you decide to use. The sos_register_irq_handler function in projects/aos/sos/src/irq.h can be used to register the handler and the meson_timeout_irq function from projects/aos/libclock/include/device.h can be used to determine the IRQ for each of the timers.

The provided code already calls sos_handle_irq_notification whenever SOS receives a notification on its IRQ endpoint. This is then responsible for calling the timer_irq callback.

Before attempting this, you should read Chapter 6 of the sel4 documentation to gain an understanding of TCBs, and Section 8.1 to understand how interrupts are delivered.

Device Mappings

In seL4/ARM, device registers are memory mapped. That is, hardware registers can be accessed via normal load/store operations to special addresses. The provided code performs this mapping for the timer driver.


You may need to resolve some or all of these issues:



For the remainder of the term progress through the milestones is contingent on passing the demonstration requirements below, and not having any show stoppers.

In general, we don't mark down for milestones that don't meet minimal requirements. Instead, we'll point out what is required, which groups can then fix, and then submit the following week for a small late penalty. Thus less than perfect project marks usually come about via late penalties, not lower marks for poor solutions.

It's in your best interest to fix problems, rather than letting them snowball into something more problematic as the term progresses.

Better solutions outlines (only) some potential differentiators of solution quality that are expected to have more favourable marks at the end of the term, however they are not required.

In general, do not jeopardise the progression of your project by chasing better solutions at the expense of correctness of your project.


You should be able to show some test code that uses all the functions specified in the driver interface. You may use the functions from projects/aos/libclock/include/clock/timestamp.h to demonstrate the accuracy of your timeouts.

Specifically set up and demonstrate:

Show Stoppers

Note this is not a complete list. The following designs are considered unsatisfactory:

Better Solutions

The following approaches are considered better than minimum, and favourably contribute to the final project mark.