[CSE]  Advanced Operating Systems 
COMP9242 2012/S2 
CRICOS Provider
Number: 00098G

PRINTER Printer-Friendly Version

M1: A timer driver

Your first milestone is fairly straightfoward, and should only take you a few hours to complete. 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 recommend that you use Mercurial (or another version control system of your choice) to maintain your source code, (this isn't a requirement, just a suggestion), 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.

If you are using Mercurial, we recommend you set up the meld (or equivalent) merging tool as the default merge program to avoid painful merges.


The aim of this milestone is to design and implement device driver to read the time. You should add a file for the timer implementation and modify the main system call loop to handle timer interrupts.

  • Learn and understand the fundamentals of writing a device driver.
  • Play with real hardware.
  • Learn about interrupt handling in seL4.
  • Be exposed to the seL4 boot information structures, frame capabilities, and mapping.
  • Time system behaviour on seL4.


For many purposes, such as benchmarking, a high clock resolution is desired. The NSLU2/IXP420 platform features a timer cell which contains several high-frequency counters which are used as timers. Using the timer you implement in this milestone, you will be measuring the performance of the file system that you implement in milestone 6.

The Driver Interface

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

Initialises the driver.
Registers the calling thread to receive an IPC message after a specified time interval (in microseconds, though actual wakeup resolution will depend on the timer resolution). Several registrations may be pending at any time. Note: As we do not have a system call interface yet, instead of waking up threads you will print out a message showing who would have woken up, and the timestamp. This will also help you test your timer accuracy.

The IPC message sent by the timer contains in MR0 a return code (CLOCK_R_OK, CLOCK_R_UINT, CLOCK_R_CNCL) and in MR1 and MR2 the present value of the real-time clock.

Returns the current real-time clock value (microsecond accurate).
Stops operation of the driver. This will cancel any outstanding timer requests (by sending them a premature IPC indicating failure).

The 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 time and sleep syscalls (implemented in a later milestone).

NOTE: After registering an interrupt, you must call seL4_IRQHandler_Ack.

The NSLU2 "Slug"

Slug architecture This is a block diagram of the IXP420 network controller on which the slug is based. The IXP420 is a single chip computer which has an XScale processor and lots of dedicated hardware for I/O. The platform hardware reference manual can be found in [1].

Although the Slug is a very powerful platform with lots of functionality we will only be doing a driver for the 'timers' cell on the "Advanced Peripheral Bus"(APB). If you are interested in the full arcana of device drivers for the other cells particularly the networking stacks then explore the directories libs/sel4/libixp_osal and libs/sel4/libixp400_xscale_sw, but be warned it is really, really hard to read and understand code.

Timer cell (OSTS)

Your main job is to learn how to program the IXP420's timer cell (OSTS) to generate timer interrupts and how to write a seL4 driver to handle these interrupts.

The OSTS contains four functions, 2 general purpose 32 bit timers, a 32 bit time counter and an emergency watchdog timer. For our purposes, we are only interested in the OSTS as our source of timer interrupts. You will be using one of the general purpose timers and the timestamp register. The interrupt vectors for the timers are connected to the 5, 11 & 14 interrupt lines, see libs/libclock/include/nslu2.h.

There is an abundance of different devices and writing device drivers is usually seen as a very difficult task. This is true in a sense. However, programming a device is 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 the OSTS's functionality that you must understand and use is listed below (the numbers in parentheses are the offsets of the register addresses, in bytes, from the OSTS's base address). Refer to Chapter 14 of the developer's manual for more complete descriptions.

  • Time-Stamp Timer (OST_TS 0x00 R/W) : Use this register as the lower 32-bits of your timestamp value.
  • General-Purpose Timer[0-1] (OST_TIMx 0x04&0x0c RO): The actual timer/counters. You need to use at least one of them (take your pick).
  • General-Purpose Timer Reload[0-1] (OST_TIMx_RL 0x08&0x10 R/W): These registers control the behaviour of the general purpose timers.
  • Timer Status (OST_STATUS 0x20 R/W) : When an interrupt occurs, this register tells you which of the many sources of interrupts in the OSTS actually caused it. And lets you clear that interrupt when you have finished processing it.

Again, this is only the minimal understanding that you need. For deeper understanding, you are encouraged to learn about the other registers and can even play with those as well.

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 that you work things out for yourself and make your own design and implementation decisions. There are only two conditions that must be satisfied:

  1. You must use an interrupt generated from the OSTS.
  2. You must implement the driver interface described above.

Supplied Code

For this project you have been supplied with an extensive set of 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. You are encouraged to modify and improve the supplied code, though for your own sanity avoid libs/ixp_* as they are Intel's incredibly complex networking libaries. 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, e.g. 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 perform a series of steps to register to receive interrupts and manage interrupts for the timer device.

  • You need to create an interrupt handling cap using our cspace library irq_handler = cspace_irq_control_get_cap(cur_cspace, seL4_CapIRQControl, irq) (See libsel4cspace documentation).
  • We have already created and bound an async endpoint within the framework we have given you. Its cptr is _sos_interrupt_ep_cap. You should register your new interrupt handler with the kernel and direct it to forward the interrupt to the provided async endpoint seL4_IRQHandler_SetEndpoint(irq_handler, _sos_interrupt_ep_cap)

Before attempting this, you should read Chapter 5 of the sel4 documentation to gain an understanding of TCBs, and Section 7.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. To access device registers, you must first map the device to virtual memory with the appropriate attributes. To do this you must first obtain the frame capability to the physical frame containing the devices registers. See Chapter 8 (specifcally 8.2) in the seL4 reference manual. By searching for the basePaddr that matches NSLU2_OSTS_PHYS_BASE, the corresponding frame capability is identified, and can then be mapped with the appropriate cache attributes to enable register access. Mapping attributes are documented in Chapter 6 of the seL4 reference manual.


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

  • At what address do the OSTS registers need to be mapped and accessed through?
  • What value must be programmed to the timer to get a frequency of x milliseconds?
  • How are the interrupts acknowledged?
  • Single or multi-threaded driver?
  • Which data structures should I use?


You should be able to show some test code that uses all the functions specified in the driver interface. Specifically set up and demonstrate:

  • A 100ms timer tick. Set up your timer to fire an interrupt every 100ms. Then, print the value returned by time_stamp every time this interrupt is received. This should not use register_timer, as it will later be used to call a function from the NFS library to keep your file system working correctly.
  • Before entering the main system call loop, set up a few calls to register_timer. Make sure the delay used is long enough such that the system call loop is entered before these wake up. As register_timer does not IPC any threads yet, we should see print outs of the timestamp as each delay expires. This part is only as a demo, and can be removed after the milestone demonstration. You will later use register_timer to implement a sleep system call for your user-level processes.

Last modified: 24 Jul 2012.